dense_submonoidClosure_iff_subgroupClosure

English

The set closure of the submonoid generated by s is dense if and only if the closure of the subgroup generated by s is dense.

Русский

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

LaTeX

$$$\\operatorname{Dense}(\\mathrm{Submonoid.closure}(s)) \\iff \\operatorname{Dense}(\\mathrm{Subgroup.closure}(s))$$$

Lean4

@[to_additive]
theorem dense_submonoidClosure_iff_subgroupClosure {s : Set G} :
    Dense (Submonoid.closure s : Set G) ↔ Dense (Subgroup.closure s : Set G) := by
  simp only [dense_iff_closure_eq, closure_submonoidClosure_eq_closure_subgroupClosure]

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