English
A group homomorphism is uniformly continuous if it is continuous at 1.
Русский
Гомоморфизм группы равномерно непрерывен, если он непрерывен в точке 1.
LaTeX
$$$\\text{ContinuousAt}(f,1) \\Rightarrow \\text{UniformContinuous}(f)$$$
Lean4
/-- A group homomorphism (a bundled morphism of a type that implements `MonoidHomClass`) between
two uniform groups is uniformly continuous provided that it is continuous at one. See also
`continuous_of_continuousAt_one`. -/
@[to_additive /-- An additive group homomorphism (a bundled morphism of a type that implements
`AddMonoidHomClass`) between two uniform additive groups is uniformly continuous provided that it
is continuous at zero. See also `continuous_of_continuousAt_zero`. -/
]
theorem uniformContinuous_of_continuousAt_one {hom : Type*} [UniformSpace β] [Group β] [IsUniformGroup β]
[FunLike hom α β] [MonoidHomClass hom α β] (f : hom) (hf : ContinuousAt f 1) : UniformContinuous f :=
uniformContinuous_of_tendsto_one (by simpa using hf.tendsto)
