prod — Mathlib

English

If la has basis pa sa and lb has basis pb sb, then la × lb has basis pa(i) ∧ pb(j) with basic sets sa(i) × sb(j).

Русский

Если у фильтра la есть базис pa(sa), а у lb — pb(sb), то произведение la × lb имеет базис pa(i) ∧ pb(j) и базисные множества sa(i) × sb(j).

LaTeX

$$$(la \times lb).HasBasis (\lambda (i,j), pa(i) \land pb(j)) (sa(i) \times sb(j)).$$

Lean4

theorem prod {ι ι' : Type*} {pa : ι → Prop} {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β}
    (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
    (la ×ˢ lb).HasBasis (fun i : ι × ι' => pa i.1 ∧ pb i.2) fun i => sa i.1 ×ˢ sb i.2 :=
  (hla.comap Prod.fst).inf (hlb.comap Prod.snd)

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