prodMap_def — Mathlib

English

The map prodMap f g is exactly the map obtained by composing with the projections and pairing the results.

Русский

Отображение prodMap f g точно есть отображение, получаемое путём композиции с проекциями и образования пары.

LaTeX

$$$ prodMap f g = (f \\circ \\mathrm{fst} R S) \\mathrm{.prod} (g \\circ \\mathrm{snd} R S). $$$

Lean4

theorem prodMap_def : prodMap f g = (f.comp (fst R S)).prod (g.comp (snd R S)) :=
  rfl

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