prod_eq — Mathlib

English

For any f : Filter α and g : Filter β with a product filter f ×ˢ g, the product equals the sequential composition of the map of f by Prod.mk with g; i.e., f ×ˢ g = (f.map Prod.mk).seq g.

Русский

Для фильтра f на α и g на β множество их произведения равно последовательному объединению образа f под отображением Prod.mk с g: f ×ˢ g = (f.map Prod.mk).seq g.

LaTeX

$$$ f \\times\\! g = (f.map \\mathrm{Prod.mk}).seq\\ g $$$

Lean4

theorem prod_eq : f ×ˢ g = (f.map Prod.mk).seq g :=
  f.map_prod id g

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