principal_prod — Mathlib

English

If sa is a fixed set and lb has basis pb sb, then the product of the principal filter on sa with lb has basis pb with basic sets sa × sb(i).

Русский

Если sa — фиксированное множество, а lb имеет базис pb sb, то произведение простой фильтрации по sa и lb имеет базис pb с базисными множествами sa × sb(i).

LaTeX

$$$(\mathcal{P}(sa) \times sb) HasBasis pb (sa \times sb \cdot).$$

Lean4

protected theorem principal_prod (sa : Set α) (h : lb.HasBasis pb sb) : (𝓟 sa ×ˢ lb).HasBasis pb (sa ×ˢ sb ·) := by
  simpa only [prod_eq_inf, comap_principal, prod_eq] using (h.comap Prod.snd).principal_inf _

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