commute_subtype_of_commute — Mathlib

English

If a family hcomm of pairwise commuting elements holds, then their images under subtype embeddings also commute in G.

Русский

Если множество коммутирует образов элементов в подгруппах, их изображения через вложение подпространствуют коммутируют.

LaTeX

$$$\\forall i,j, i\\neq j, \\forall x\\in H_i, \\forall y\\in H_j, \\mathrm{Commute}((H_i)\\!\\text{subtype} x, (H_j)\\!\\text{subtype} y).$$$

Lean4

@[to_additive]
theorem commute_subtype_of_commute (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y)
    (i j : ι) (hne : i ≠ j) : ∀ (x : H i) (y : H j), Commute ((H i).subtype x) ((H j).subtype y) :=
  by
  rintro ⟨x, hx⟩ ⟨y, hy⟩
  exact hcomm hne x y hx hy

Похожие утверждения