eval — Mathlib

English

Evaluating a path homotopy at an intermediate time t yields a path from x0 to x1, given by the curry of F at t.

Русский

Оценка гомотопии пути в момент времени t даёт путь из x0 в x1, задаваемый карри-образом F в момент t.

LaTeX

$$$$\text{eval}(F,t) = \text{Path}(x_0,x_1) \text{ with } (F\,\text{coursed at } t).$$$$

Lean4

/-- Evaluating a path homotopy at an intermediate point, giving us a `Path`.
-/
def eval (F : Homotopy p₀ p₁) (t : I) : Path x₀ x₁
    where
  toFun := F.toHomotopy.curry t
  source' := by simp
  target' := by simp

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