fst_prod_snd — Mathlib

English

The pair of projection maps from M1×M2 onto M1 and M2, when combined as a product map, yields the identity on M1×M2.

Русский

Пара проекций из M1×M2 на M1 и M2, объединенная в произведение, задает тождественное отображение на M1×M2.

LaTeX

$$$(\\mathrm{fst}\\,R\\,M_1\\,M_2) \\times (\\mathrm{snd}\\,R\\,M_1\\,M_2) = \\mathrm{id}_{M_1 \\times M_2}$$$

Lean4

@[simp]
theorem fst_prod_snd : (fst R M₁ M₂).prod (snd R M₁ M₂) = .id R (M₁ × M₂) :=
  ext fun ⟨_x, _y⟩ => rfl

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