uniformContinuous_comap — Mathlib

English

If f: α → β and u is a uniform space on β, then f is uniformly continuous from (α, comap f u) to (β, u).

Русский

Если f: α → β и u — равномерная структура на β, то отображение f: (α, comap f u) → (β, u) равномерно непрерывно.

LaTeX

$$UniformContinuous f$$

Lean4

theorem uniformContinuous_comap {f : α → β} [u : UniformSpace β] :
    @UniformContinuous α β (UniformSpace.comap f u) u f :=
  tendsto_comap

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