uniformContinuous — Mathlib

English

For any X with a UniformSpace, any path γ: Path x y is a UniformContinuous map from I to X, since I is compact.

Русский

Любой путь γ: Path x y является равномерно непрерывной отображением I в X, поскольку I компактно.

LaTeX

$$$\\text{UniformContinuous}(\\gamma: I \\to X)$$$

Lean4

theorem uniformContinuous (γ : Path x y) : UniformContinuous γ :=
  CompactSpace.uniformContinuous_of_continuous <| map_continuous _

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