comp_lift — Mathlib

English

For any paths P0: x0→x1 and P1: x1→x2, the class of their concatenation in the quotient equals the product in the quotient of their classes. In symbols, the class of P0.trans P1 is equal to Quotient.comp applied to the classes of P0 and P1.

Русский

Для любых путей P0: x0→x1 и P1: x1→x2 класс их конкатенации в факторе равен произведению их классов в факторе.

LaTeX

$$$⟦P_0\,\text{trans}\,P_1⟧ = \operatorname{Quotient.comp} ⟦P_0⟧ ⟦P_1⟧$$$

Lean4

theorem comp_lift (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂) : ⟦P₀.trans P₁⟧ = Quotient.comp ⟦P₀⟧ ⟦P₁⟧ :=
  rfl

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