pi — Mathlib · SciLib

English

The product of a family of path homotopies is a single homotopy between Path.pi γ0 and Path.pi γ1, defined componentwise.

Русский

Произведение семейства путевых гомотопий образует одну гомотопию между Path.pi γ0 и Path.pi γ1, компонетно по i.

LaTeX

$$$\mathrm{piHomotopy}(\gamma_0,\gamma_1, H) : Path.Homotopic( Path.pi\gamma_0, Path.pi\gamma_1)$$$

Lean4

/-- The product of a family of path homotopy classes. -/
def pi (γ : ∀ i, Path.Homotopic.Quotient (as i) (bs i)) : Path.Homotopic.Quotient as bs :=
  (Quotient.map Path.pi fun x y hxy => Nonempty.map (piHomotopy x y) (Classical.nonempty_pi.mpr hxy))
    (Quotient.choice γ)

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