English
The coe (as a set) of the bottom subgroup's topologicalClosure equals the closure of {1}.
Русский
Переобразование вниз по подгруппе и её топологическому замыканию эквивалентно замыканию множества {1}.
LaTeX
$$$((\perp : Subgroup G).topologicalClosure : Set G) = \overline{\{1\}}$$$
Lean4
@[to_additive continuous_of_continuousAt_zero₂]
theorem continuous_of_continuousAt_one₂ {H M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [Group H]
[TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H →* M) (hf : ContinuousAt (fun x : G × H ↦ f x.1 x.2) (1, 1))
(hl : ∀ x, ContinuousAt (f x) 1) (hr : ∀ y, ContinuousAt (f · y) 1) : Continuous (fun x : G × H ↦ f x.1 x.2) :=
continuous_iff_continuousAt.2 fun (x, y) =>
by
simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y, prod_map_map_eq,
tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *
refine
((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul (((hl x).comp tendsto_snd).mul hf)).mono_right
(le_of_eq ?_)
simp only [map_one, mul_one, MonoidHom.one_apply]
