English
Product of filters. This is the filter generated by Cartesian products of elements of the component filters, defined as f.comap Prod.fst ⊓ g.comap Prod.snd.
Русский
Произведение фильтров. Фильтр, порождённый декартовым произведением элементов двух фильтров, равен f.comap Prod.fst ⊓ g.comap Prod.snd.
LaTeX
$$$\\text{instSProd} : SProd (Filter \\alpha) (Filter \\beta) (Filter (\\alpha \\times \\beta))\\;:\\; sprod\\ f\\ g := f.comap Prod.fst \\inf\\ g.comap Prod.snd$$$
Lean4
/-- Product of filters. This is the filter generated by Cartesian products
of elements of the component filters. -/
instance instSProd : SProd (Filter α) (Filter β) (Filter (α × β)) where sprod f g := f.comap Prod.fst ⊓ g.comap Prod.snd
