prod — Mathlib

English

If hl : l.Subsingleton and hl' : l'.Subsingleton, then the product filter l ×ˢ l' is subsingleton.

Русский

Если l и l' являются подсинглетными фильтрами, то их произведение l ×ˢ l' тоже подсинглетно.

LaTeX

$$$hl.Subsingleton \to \forall {l' : Filter \beta}, l'.Subsingleton \Rightarrow (l \timesˢ l').Subsingleton$$$

Lean4

theorem prod (hl : l.Subsingleton) {l' : Filter β} (hl' : l'.Subsingleton) : (l ×ˢ l').Subsingleton :=
  let ⟨s, hsl, hs⟩ := hl;
  let ⟨t, htl', ht⟩ := hl';
  ⟨s ×ˢ t, prod_mem_prod hsl htl', hs.prod ht⟩

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