prod_eq_inf — Mathlib

English

The product of filters equals the infimum of the pulled-back filters: f ×ˢ g = f.comap Prod.fst ⊓ g.comap Prod.snd.

Русский

Произведение фильтров равно их произведению-образу (наименьшее ограничение): f ×ˢ g = f.comap Prod.fst ⊓ g.comap Prod.snd.

LaTeX

$$$f \\timesˢ g = f.comap Prod.fst \\inf\\ g.comap Prod.snd$$$

Lean4

theorem prod_eq_inf (f : Filter α) (g : Filter β) : f ×ˢ g = f.comap Prod.fst ⊓ g.comap Prod.snd :=
  rfl

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