comp — Mathlib

English

The composition of path homotopy classes descends to the quotient.

Русский

Составление классов однородности путей спускается на фактор-пространство.

LaTeX

$$$ \\text{def }\\text{Path.Homotopic.Quotient.comp} (P_0:P_0: Path.Homotopic.Quotient x_0 x_1) (P_1:P_1: Path.Homotopic.Quotient x_1 x_2) : Path.Homotopic.Quotient x_0 x_2$$$

Lean4

/-- The composition of path homotopy classes. This is `Path.trans` descended to the quotient. -/
def comp (P₀ : Path.Homotopic.Quotient x₀ x₁) (P₁ : Path.Homotopic.Quotient x₁ x₂) : Path.Homotopic.Quotient x₀ x₂ :=
  Quotient.map₂ Path.trans (fun (_ : Path x₀ x₁) _ hp (_ : Path x₁ x₂) _ hq => hcomp hp hq) P₀ P₁

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