prod_def — Mathlib

English

The product of filters f on α and g on β is equal to f.lift (s ↦ g.lift' (t ↦ s × t)).

Русский

Произведение фильтров f на α и g на β равно f.lift (s ↦ g.lift' (t ↦ s × t)).

LaTeX

$$$f \\times^{\\mathrm{S}} g = f.lift (\\lambda s. g.lift' (\\lambda t. s \\times^{\\mathrm{S}} t))$$$

Lean4

theorem prod_def {f : Filter α} {g : Filter β} : f ×ˢ g = f.lift fun s => g.lift' fun t => s ×ˢ t := by
  simpa only [Filter.lift', Filter.lift, (f.basis_sets.prod g.basis_sets).eq_biInf, iInf_prod, iInf_and] using
    iInf_congr fun i => iInf_comm

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