closure_submonoidClosure_eq_closure_subgroupClosure

English

The closure of the monoid-closure of s equals the closure of the subgroup-closure of s.

Русский

Замыкание подмножества, полученное как замыкание подмоноида, равно замыканию подгруппы, полученной из s.

LaTeX

$$$\\overline{\\mathrm{Submonoid.closure}(s)} = \\overline{\\mathrm{Subgroup.closure}(s)}$$$

Lean4

@[to_additive]
theorem closure_submonoidClosure_eq_closure_subgroupClosure (s : Set G) :
    closure (Submonoid.closure s : Set G) = closure (Subgroup.closure s) :=
  congrArg SetLike.coe (topologicalClosure_subgroupClosure_toSubmonoid s).symm

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