uniformContinuous_of_continuousAt_one

English

A monoid homomorphism that is continuous at 1 is uniformly continuous.

Русский

Гомоморфизм моноида, непрерывный в точке 1, равномерно непрерывен.

LaTeX

$$$\\text{UniformContinuous}_{\\text{MonoidHom}}(f) \\Leftarrow \\text{ContinuousAt}(f,1)$$$

Lean4

@[to_additive]
theorem uniformContinuous_of_continuousAt_one [UniformSpace β] [Group β] [IsUniformGroup β] (f : α →* β)
    (hf : ContinuousAt f 1) : UniformContinuous f :=
  _root_.uniformContinuous_of_continuousAt_one f hf

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