projRight_prod — Mathlib

English

Let q1 and q2 be homotopy quotient classes of paths in α and β. The right projection of their product recovers the second component: the right projection of the product equals q2.

Русский

Пусть q1 и q2 — классы гомотопий путей в α и β. Правая проекция произведения восстанавливает второй компонент: projRight(prod q1 q2) = q2.

LaTeX

$$$\operatorname{projRight}(\operatorname{prod}(q_{1}, q_{2})) = q_{2}$$$

Lean4

@[simp]
theorem projRight_prod : projRight (prod q₁ q₂) = q₂ :=
  by
  induction q₁, q₂ using Quotient.inductionOn₂
  rw [projRight, prod_lift, ← Path.Homotopic.map_lift]
  congr

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