prodHomotopy — Mathlib

English

The product of two path homotopies h1: p1→p1' and h2: p2→p2' yields a homotopy from p1.prod p2 to p1'.prod p2'.

Русский

Произведение двух путевых гомотопий даёт гомотопию от p1.prod p2 к p1'.prod p2'.

LaTeX

$$$\mathrm{prodHomotopy}(h_1,h_2) : (p_1.prod p_2) \to (p_1'.prod p_2')$$$

Lean4

/-- The product of homotopies h₁ and h₂.
This is `HomotopyRel.prod` specialized for path homotopies. -/
def prodHomotopy (h₁ : Path.Homotopy p₁ p₁') (h₂ : Path.Homotopy p₂ p₂') : Path.Homotopy (p₁.prod p₂) (p₁'.prod p₂') :=
  ContinuousMap.HomotopyRel.prod h₁ h₂

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