closure_mul_le — Mathlib

English

For any subsets S,T of G, the closure of ST is contained in the join of the closures of S and T: closure(S T) ≤ closure(S) ⊔ closure(T).

Русский

Для любых подмножеств S, T подпгруппы G верно: closure(S T) ⊆ closure(S) ⊔ closure(T).

LaTeX

$$$\\mathrm{closure}(S T) \\leq \\mathrm{closure}(S) \\;\\sqcup\\; \\mathrm{closure}(T).$$$

Lean4

@[to_additive]
theorem closure_mul_le (S T : Set G) : closure (S * T) ≤ closure S ⊔ closure T :=
  sInf_le fun _x ⟨_s, hs, _t, ht, hx⟩ =>
    hx ▸
      (closure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
        (SetLike.le_def.mp le_sup_right <| subset_closure ht)

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