coe_mk' — Mathlib

English

The underlying function of the constructed path mk is the function f itself, for f: I → X with appropriate endpoint data.

Русский

Опорная функция сконструированного пути mk совпадает с функцией f: I → X при задании концов пути.

LaTeX

$$$\big( (mk \langle f, h_1 \rangle h_2 h_3) : Path x y \big)^{\!\,I \to X} = f$$$

Lean4

/-- A path constructed from a continuous map `f` has the same underlying function. -/
@[simp]
theorem coe_mk' (f : C(I, X)) (h₁ h₂) : ⇑(mk f h₁ h₂ : Path x y) = f :=
  rfl

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