source — Mathlib

English

For any F ∈ p0.Homotopy p1, F(t,0) = x0, i.e., the left boundary of a homotopy is the start path's start point.

Русский

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

LaTeX

$$$$\text{source }(F,t) = x_0.$$$$

Lean4

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

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