asBasis — Mathlib

English

View a filter as a filter basis by taking its sets as the basis elements and closing under finite intersections via the given construction.

Русский

Рассматриваем фильтр как базис фильтра, взяв его множества за базисные элементы и замыкая по конечным пересечениям.

LaTeX

$$$\text{asBasis}(F) = \langle F.\mathrm{sets}, \langle \mathrm{univ}, \mathrm{univ\_mem}\rangle, \dots \rangle$$$

Lean4

/-- View a filter as a filter basis. -/
def asBasis (f : Filter α) : FilterBasis α :=
  ⟨f.sets, ⟨univ, univ_mem⟩, fun {x y} hx hy => ⟨x ∩ y, inter_mem hx hy, subset_rfl⟩⟩
    -- TODO: consider adding `protected`?

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