English
The commutator is symmetric up to equality of brackets: [H1,H2] ≤ [H2,H1].
Русский
Коммутатор удовлетворяет симметрии порядка: [H1,H2] ≤ [H2,H1].
LaTeX
$$$$ [H_1, H_2] \\le [H_2, H_1] $$$$
Lean4
/-- **The Three Subgroups Lemma** (via the Hall-Witt identity) -/
theorem commutator_commutator_eq_bot_of_rotate (h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥) (h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥) :
⁅⁅H₁, H₂⁆, H₃⁆ = ⊥ :=
by
simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le, mem_centralizer_iff_commutator_eq_one, ←
commutatorElement_def] at h1 h2 ⊢
intro x hx y hy z hz
trans
x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ *
x⁻¹
-- We avoid `group` here to minimize imports while low in the hierarchy;
-- typically it would be better to invoke the tactic.
· simp [commutatorElement_def, mul_assoc]
· rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
simp [mul_assoc]
