top_prod — Mathlib

English

If lb has basis pb sb, then (⊤ ×ˢ lb) has basis pb with basic sets univ × sb(i).

Русский

Если lb имеет базис pb sb, то (⊤ × lb) имеет базис pb и базисные множества Univ × sb(i).

LaTeX

$$$(\top × sb) HasBasis pb (univ × sb ·).$$

Lean4

protected theorem top_prod (h : lb.HasBasis pb sb) : (⊤ ×ˢ lb : Filter (α × β)).HasBasis pb (univ ×ˢ sb ·) := by
  simpa only [principal_univ] using h.principal_prod univ

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