hcomp_half — Mathlib

English

Given a path p and a continuous f with f(0)=0 and f(1)=1, there exists a homotopy from p to p.reparam f.

Русский

Пусть p — путь, и f непрерывен с f(0)=0, f(1)=1; существует гомотопия от p к p.reparam f.

LaTeX

$$$\forall p:\, Path x_0 x_1,\; \forall f:\, I \to I,\; (\text{Continuous } f) \,\Rightarrow\, p.Homotopy (p.reparam f)$$$

Lean4

theorem hcomp_half (F : Homotopy p₀ q₀) (G : Homotopy p₁ q₁) (t : I) :
    F.hcomp G (t, ⟨1 / 2, by norm_num, by norm_num⟩) = x₁ :=
  show ite _ _ _ = _ by norm_num

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