English
If la has basis pa sa and lb has basis pb sb, then the product filter la × lb has a basis indexed by pairs (i, j) with basis sets sa(i) × sb(j) and index predicate pa(i) ∧ pb(j).
Русский
Если у фильтра la есть базис pa(sa), а у lb — pb(sb), то произведение фильтров la × lb имеет базис, индексы которого — пары (i, j), и базисные множества — sa(i) × sb(j), задаваемые pa(i) ∧ pb(j).
LaTeX
$$$(\mathcal{L} \times \mathcal{N})$ имеет базис $\{ sa(i) \times sb(j) \}_{(i,j) \in I\times J}$ с индикаторной функцией $(i,j) \mapsto pa(i) \land pb(j)$.$$
Lean4
theorem prod_pprod (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
(la ×ˢ lb).HasBasis (fun i : PProd ι ι' => pa i.1 ∧ pb i.2) fun i => sa i.1 ×ˢ sb i.2 :=
(hla.comap Prod.fst).inf' (hlb.comap Prod.snd)
