sup_pure — Mathlib

English

For any basis of l, the filter l ⊔ pure x has a basis with same p and sets s_i ∪ {x}.

Русский

Для любого базиса l, фильтр l ⊔pure x имеет базис с тем же p и множества s_i ∪ {x}.

LaTeX

$$$\\text{HasBasis}\\left(l \\sups \\mathrm{pure}\,x\\right)\\left(\\lambda i: p i\\right)(\\lambda i: s(i) \\cup \\{x\\})$$$

Lean4

theorem sup_pure (hl : l.HasBasis p s) (x : α) : (l ⊔ pure x).HasBasis p fun i => s i ∪ { x } := by
  simp only [← principal_singleton, hl.sup_principal]

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