prod_fst_snd — Mathlib

English

Pi.prod of the projection maps fst and snd yields the identity function on the product: Pi.prod Prod.fst Prod.snd = id.

Русский

Производная Pi.prod по проекциям fst и snd даёт тождественную функцию на произведение: Pi.prod Prod.fst Prod.snd = id.

LaTeX

$$$\Pi.prod (Prod.fst) (Prod.snd) = id$$$

Lean4

theorem prod_fst_snd : Pi.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id :=
  rfl

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