curry_one — Mathlib

English

Extend(F) is the real-line extension of the curried homotopy, obtained by extending F.curry from I to all of R via an Icc extension.

Русский

Extend(F) — это продолжение гомотопии по всей ℝ, полученное продолжением F.curry с I на всю ℝ через расширение Icc.

LaTeX

$$$\mathrm{extend}(F) = F\text{.curry}.\mathrm{IccExtend}(0\le 1)$$$

Lean4

@[simp]
theorem curry_one (F : Homotopy f₀ f₁) : F.curry 1 = f₁ := by ext; simp

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