eval_zero — Mathlib

English

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

Русский

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

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(0) = p_0$$$

Lean4

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

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