target — Mathlib

English

For any F ∈ p0.Homotopy p1, F(t,1) = x1; the right boundary of a homotopy is the end point of the target path.

Русский

Для любой гомотопии F между p0 и p1, F(t,1) = x1 — правая граница гомотопии соответствует концу пути.

LaTeX

$$$$\text{target }(F,t) = x_1.$$$$

Lean4

@[simp]
theorem target (F : Homotopy p₀ p₁) (t : I) : F (t, 1) = x₁ :=
  calc
    F (t, 1) = p₀ 1 := ContinuousMap.HomotopyRel.eq_fst _ _ (.inr rfl)
    _ = x₁ := p₀.target

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