eval_one — Mathlib

English

Let p0, p1 be paths from x0 to x1, and F a homotopy from p0 to p1. Then F(1) = p1.

Русский

Пусть p0, p1 — пути от x0 до x1, и F — гомотопия между ними. Тогда F(1) = p1.

LaTeX

$$$\forall X\, \forall Y\, [TopologicalSpace X] [TopologicalSpace Y] \; {x_0 x_1 : X} \; {p_0 p_1 : Path\, x_0 x_1}, (F : p_0.Homotopy p_1) \Rightarrow F.eval(1) = p_1$$$

Lean4

@[simp]
theorem eval_one (F : Homotopy p₀ p₁) : F.eval 1 = p₁ := by
  ext t
  simp [eval]

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