commutator_def' — Mathlib

English

If [ [H2,H3], H1 ] = ⊥ and [ [H3,H1], H2 ] = ⊥, then [ [H1,H2], H3 ] = ⊥.

Русский

Если [ [H2,H3], H1 ] = ⊥ и [ [H3,H1], H2 ] = ⊥, то [ [H1,H2], H3 ] = ⊥.

LaTeX

$$$$ [ [H_2, H_3], H_1 ] = \\perp \\;\\land\\; [ [H_3, H_1], H_2 ] = \\perp \\Rightarrow [ [H_1, H_2], H_3 ] = \\perp $$$$

Lean4

theorem commutator_def' [H₁.Normal] [H₂.Normal] : ⁅H₁, H₂⁆ = normalClosure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g} :=
  le_antisymm closure_le_normalClosure (normalClosure_le_normal subset_closure)

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