uniformContinuous_extend_left — Mathlib

English

The map Path.extend: Path x y → C(ℝ, X) is uniformly continuous in the path parameter.

Русский

Карта Path.extend: Path x y → C(ℝ, X) равномерно непрерывна по параметру пути.

LaTeX

$$$\\text{UniformContinuous}(\\text{Path.extend}: Path x y \\to C(\\mathbb{R},X))$$$

Lean4

/-- The function sending a path `γ` to its extension `γ.extend : ℝ → X`
is uniformly continuous in `γ`. -/
theorem uniformContinuous_extend_left : UniformContinuous (Path.extend : Path x y → C(ℝ, X)) :=
  ContinuousMap.projIccCM.uniformContinuous_comp_left.comp isUniformEmbedding_coe.uniformContinuous

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