subgroupClosure_mul — Mathlib

English

The product of the closure of a set with the set itself equals the closure of the set.

Русский

Произведение замыкания множества и самого множества равно замыканию множества.

LaTeX

$$closure s * s = closure s$$

Lean4

@[to_additive (attr := simp)]
theorem subgroupClosure_mul (hs : s.Nonempty) : closure s * s = closure s :=
  by
  rw [← Set.iUnion_op_smul_set]
  have h a (ha : a ∈ s) : (closure s : Set G) <• a = closure s := op_smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

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