sup_eq_closure_mul — Mathlib

English

For subgroups H,K of G, their join equals the closure of the product of the underlying sets: H ⊔ K = closure((H:Set G) * (K:Set G)).

Русский

Для подпгрупп H и K группы G их объединение равно замыканию произведения подмножеств: H ⊔ K = closure((H:Set G) * (K:Set G)).

LaTeX

$$$H \\lor K = \\mathrm{closure}\\big((H:\\mathrm{Set}~G)\\cdot(K:\\mathrm{Set}~G)\\big).$$$

Lean4

@[to_additive]
theorem sup_eq_closure_mul (H K : Subgroup G) : H ⊔ K = closure ((H : Set G) * (K : Set G)) :=
  le_antisymm
    (sup_le (fun h hh => subset_closure ⟨h, hh, 1, K.one_mem, mul_one h⟩) fun k hk =>
      subset_closure ⟨1, H.one_mem, k, hk, one_mul k⟩)
    ((closure_mul_le _ _).trans <| by rw [closure_eq, closure_eq])

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