range_coe — Mathlib

English

The range of the map that sends a path to its continuous realization consists exactly of those functions f: I → X with f(0) = x and f(1) = y.

Русский

Область значений отображения пути в непрерывную карту состоит ровно из тех функций f: I → X, для которых f(0) = x и f(1) = y.

LaTeX

$$$ \\operatorname{range}(\\operatorname{toContinuousMap}) = \\{ f: I \\to X : f(0)=x \\land f(1)=y \\} $$$

Lean4

@[simp]
theorem range_coe : range ((↑) : Path x y → C(I, X)) = {f | f 0 = x ∧ f 1 = y} :=
  Subset.antisymm (range_subset_iff.mpr fun γ ↦ ⟨γ.source, γ.target⟩) fun f ⟨hf₀, hf₁⟩ ↦ ⟨⟨f, hf₀, hf₁⟩, rfl⟩

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