sup_principal — Mathlib

English

If l has a basis p with s, then l ⊔ principal t has a basis with the same p and with basic sets s_i ∪ t.

Русский

Если у фильтра l есть базис p с s, то l ⊔ principal t имеет базис с тем же p и базисами s_i ∪ t.

LaTeX

$$$\\text{HasBasis}(l \\sups \\mathcal{P} t)\\left(\\lambda i: p i\\right)(\\lambda i: s(i) \\cup t)$$$$

Lean4

theorem sup_principal (hl : l.HasBasis p s) (t : Set α) : (l ⊔ 𝓟 t).HasBasis p fun i => s i ∪ t :=
  ⟨fun u => by simp only [(hl.sup' (hasBasis_principal t)).mem_iff, PProd.exists, and_true, Unique.exists_iff]⟩

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