piHomotopy — Mathlib

English

The relative product of homotopies is induced componentwise by taking the product of the HomotopyRel's.

Русский

Относительное произведение гомотопий задано компонентной конструкцией через произведение соответствующих гомотопий.

LaTeX

$$$\mathrm{prod}(F,G) : \mathrm{HomotopyRel}(f_0,f_1,S) \to \mathrm{HomotopyRel}(g_0,g_1,S)$$$

Lean4

/-- The product of a family of path homotopies. This is just a specialization of `HomotopyRel`. -/
def piHomotopy (γ₀ γ₁ : ∀ i, Path (as i) (bs i)) (H : ∀ i, Path.Homotopy (γ₀ i) (γ₁ i)) :
    Path.Homotopy (Path.pi γ₀) (Path.pi γ₁) :=
  ContinuousMap.HomotopyRel.pi H

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