projLeft_prod — Mathlib

English

A simp lemma showing projection is inverse to product.

Русский

Простая лемма, показывающая что проекция является обратной умножению.

LaTeX

$$$\text{projLeft}(\mathrm{prod} \; q_1\; q_2) = q_1$$$

Lean4

/-- Lemmas showing projection is the inverse of product. -/
@[simp]
theorem projLeft_prod : projLeft (prod q₁ q₂) = q₁ :=
  by
  induction q₁, q₂ using Quotient.inductionOn₂
  rw [projLeft, prod_lift, ← Path.Homotopic.map_lift]
  congr

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