fst_prod_snd — Mathlib

English

The product of fst and snd equals the identity on α × β, i.e., the pair (fst, snd) is the identity map.

Русский

Произведение fst и snd эквивалентно тождественному отображению на α × β, то есть пара (fst, snd) равна тождественному отображению.

LaTeX

$$$ fst\,\mathrm{prod}\, snd = id $$$

Lean4

@[simp]
theorem fst_prod_snd : (fst : α × β →o α).prod snd = id :=
  by
  ext ⟨x, y⟩ : 2
  rfl

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