uniformContinuous_map — Mathlib

English

If f: α → β is uniformly continuous, then the induced map on SeparationQuotient α → SeparationQuotient β is uniformly continuous.

Русский

Если f: α → β равномерно непрерывен, то соответствующее отображение на SeparationQuotient является равномерно непрерывным.

LaTeX

$$Theorem: UniformContinuous f → UniformContinuous (SeparationQuotient.map f)$$

Lean4

theorem uniformContinuous_map (f : α → β) : UniformContinuous (map f) :=
  uniformContinuous_lift' _

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