commutator_le — Mathlib

English

The commutator [H1,H2] is contained in H3 if and only if every commutator [g1,g2] with g1 ∈ H1 and g2 ∈ H2 lies in H3.

Русский

Коммутатор [H1,H2] содержится в H3 тогда и только тогда, когда каждый [g1,g2] с g1∈H1 и g2∈H2 лежит в H3.

LaTeX

$$$$ [H_1, H_2] \\le H_3 \\iff \\forall g_1 \\in H_1, \\forall g_2 \\in H_2, [g_1, g_2] \\in H_3 $$$$

Lean4

theorem commutator_le : ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃ :=
  H₃.closure_le.trans ⟨fun h a b c d => h ⟨a, b, c, d, rfl⟩, fun h _g ⟨a, b, c, d, h_eq⟩ => h_eq ▸ h a b c d⟩

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