uniformContinuous_extend — Mathlib

English

A path γ extends to a uniformly continuous map γ.extend: ℝ → X.

Русский

Путь γ продолжается до равномерно непрерывной карты γ.extend: ℝ → X.

LaTeX

$$$\\gamma.extend : \\mathbb{R} \\to X$ is UniformContinuous$$

Lean4

/-- Given a path `γ`, it extension to the real line `γ.extend : C(ℝ, X)`
is a uniformly continuous function. -/
theorem uniformContinuous_extend (γ : Path x y) : UniformContinuous γ.extend :=
  γ.uniformContinuous.comp <| LipschitzWith.projIcc _ |>.uniformContinuous

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