uniformContinuous_symm — Mathlib

English

The reversal map Path.symm: Path x y → Path y x is uniformly continuous.

Русский

Переобразование Path.symm: Path x y → Path y x равномерно непрерывно.

LaTeX

$$$\text{UniformContinuous}(\mathrm{Path}.\mathrm{symm})$$$

Lean4

theorem uniformContinuous_symm : UniformContinuous (Path.symm : Path x y → Path y x) :=
  hasBasis_uniformity.uniformContinuous_iff hasBasis_uniformity |>.mpr fun U hU ↦ ⟨U, hU, fun _ _ h x ↦ h (σ x)⟩

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