homotopyTo_apply — Mathlib

English

A homotopy between p and q induces a homotopy between their toLoop images, parametric in t and the boundary coordinates.

Русский

Гомотопия между p и q индуцирует гомотопию между их образами через toLoop, параметрическая по t и границе.

LaTeX

$$homotopyTo : ∀ i, ∀ p q, H : p.HomotopyRel q, ContinuousMap(Prod unitInterval, unitInterval) (ContinuousMap ((Subtype ...) → unitInterval) X)$$

Lean4

theorem homotopyTo_apply (i : N) {p q : Ω^ N X x} (H : p.1.HomotopyRel q.1 <| Cube.boundary N) (t : I × I)
    (tₙ : I^{ j // j ≠ i }) : homotopyTo i H t tₙ = H (t.fst, Cube.insertAt i (t.snd, tₙ)) :=
  rfl

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