prod_fst_snd — Mathlib

English

The pair of projections from A × B onto A and B recovers the identity: fst R B C · prod f g = f and snd R B C · prod f g = g; thus prod(f, g) is pairwise consistent.

Русский

Пара проекций из A × B на A и B вместе с произведением дают идентичность, то есть fst ∘ prod f g = f и snd ∘ prod f g = g.

LaTeX

$$$$ fst(R, B, C) \circ (f \ prod g) = f \quad\text{and}\quad snd(R, B, C) \circ (f \ prod g) = g. $$$$

Lean4

@[simp]
theorem prod_fst_snd : prod (fst R A B) (snd R A B) = AlgHom.id R _ :=
  rfl

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