prod_top — Mathlib

English

If la has basis pa sa, then (la ×ˢ ⊤) has basis pa with basic sets sa(i) × univ.

Русский

Если у la есть базис pa sa, то (la × top) имеет базис pa и базисные множества sa(i) × Univ.

LaTeX

$$$(la \times \top).HasBasis pa (sa \cdot \times univ).$$

Lean4

protected theorem prod_top (h : la.HasBasis pa sa) : (la ×ˢ ⊤ : Filter (α × β)).HasBasis pa (sa · ×ˢ univ) := by
  simpa only [principal_univ] using h.prod_principal univ

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