prod_fst_snd — Mathlib

English

The product of the two projection maps fst and snd is the identity; i.e., fst R A B and snd R A B form a pair that is equivalent to the identity morphism on A.

Русский

Произведение двух проекций fst и snd равно единичному отображению; то есть пара fst R A B, snd R A B эквивальна тождественному отображению на A.

LaTeX

$$$ prod (fst R A B) (snd R A B) = 1 $$$

Lean4

@[simp]
theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
  DFunLike.coe_injective Pi.prod_fst_snd

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