uniformContinuous_monoidHom_of_continuous

English

The uniformity can also be described using the swapped map and NHDS at 1, yielding an alternative comap expression.

Русский

Униформность может быть описана через переставление отображения и NHDS в точке 1, давая альтернативное выражение через comap.

LaTeX

$$$\\mathcal U(\\alpha) = \\mathrm{comap}\\bigl( (x,y)\\mapsto y^{-1}x \\bigr)(\\mathcal N(1))$$$

Lean4

@[to_additive]
theorem uniformContinuous_monoidHom_of_continuous {hom : Type*} [UniformSpace β] [Group β] [IsUniformGroup β]
    [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Continuous f) : UniformContinuous f :=
  uniformContinuous_of_tendsto_one <|
    suffices Tendsto f (𝓝 1) (𝓝 (f 1)) by rwa [map_one] at this
    h.tendsto 1

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