English
Let f: G → H be a continuous dense-range monoid homomorphism. If the topological closure of a subgroup s is ⊤, then the topological closure of its image s.map f is ⊤ as well.
Русский
Пусть f: G → H непрерывно отображает плотный диапазон; если замыкание подгруппы s по топологии равно ⊤, то и замыкание образа s под действием f равно ⊤.
LaTeX
$$$\text{Continuous } f \wedge DenseRange f \Rightarrow s.topologicalClosure = \top \Rightarrow (s.map f).topologicalClosure = \top$$$
Lean4
@[to_additive]
theorem topologicalClosure_map_subgroup [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {f : G →* H}
(hf : Continuous f) (hf' : DenseRange f) {s : Subgroup G} (hs : s.topologicalClosure = ⊤) :
(s.map f).topologicalClosure = ⊤ := by
rw [SetLike.ext'_iff] at hs ⊢
simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢
exact hf'.dense_image hf hs
