English
If a group homomorphism f is tending to 1 in the target under the identity neighborhood, then f is uniformly continuous.
Русский
Если гипоморфизм f стремится к единице в пределе при идентичной окрестности, то f равномерно непрерывен.
LaTeX
$$$\\text{UniformContinuous}(f)\\;\\Leftarrow\\; \\text{Tendsto}(f,\\mathcal N(1),\\mathcal N(1))$$$
Lean4
@[to_additive]
theorem uniformContinuous_of_tendsto_one {hom : Type*} [UniformSpace β] [Group β] [IsUniformGroup β] [FunLike hom α β]
[MonoidHomClass hom α β] {f : hom} (h : Tendsto f (𝓝 1) (𝓝 1)) : UniformContinuous f :=
by
have : ((fun x : β × β => x.2 / x.1) ∘ fun x : α × α => (f x.1, f x.2)) = fun x : α × α => f (x.2 / x.1) := by ext;
simp only [Function.comp_apply, map_div]
rw [UniformContinuous, uniformity_eq_comap_nhds_one α, uniformity_eq_comap_nhds_one β, tendsto_comap_iff, this]
exact Tendsto.comp h tendsto_comap
