prod_projLeft_projRight — Mathlib

English

For any p in Path.Homotopic.Quotient((a1,b1))((a2,b2)), the product of its left and right projections reconstructs p.

Русский

Для любого p в Path.Homotopic.Quotient((a1,b1))((a2,b2)) произведение проекций слева и справа возвращает p.

LaTeX

$$$\operatorname{prod}(\operatorname{projLeft}(p), \operatorname{projRight}(p)) = p$$$

Lean4

@[simp]
theorem prod_projLeft_projRight (p : Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)) : prod (projLeft p) (projRight p) = p :=
  by
  induction p using Quotient.inductionOn
  simp only [projLeft, projRight, ← Path.Homotopic.map_lift]
  congr

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