English
The filter represented by a CFilter is the collection of supersets of elements of the filter base. Concretely, a ⊆ α lies in F.toFilter iff ∃ b with F b ⊆ a.
Русский
Фильтр, порожденный CFilter, состоит из множеств-наверх. Точка зрения: a ∈ F.toFilter тогда и только тогда, когда существует b such that F b ⊆ a.
LaTeX
$$$F.toFilter = \\{ a\\subseteq α : ∃ b, F b \\subseteq a \\}$.$$
Lean4
/-- The filter represented by a `CFilter` is the collection of supersets of
elements of the filter base. -/
def toFilter (F : CFilter (Set α) σ) : Filter α
where
sets := {a | ∃ b, F b ⊆ a}
univ_sets := ⟨F.pt, subset_univ _⟩
sets_of_superset := fun ⟨b, h⟩ s ↦ ⟨b, Subset.trans h s⟩
inter_sets := fun ⟨a, h₁⟩ ⟨b, h₂⟩ ↦
⟨F.inf a b, subset_inter (Subset.trans (F.inf_le_left _ _) h₁) (Subset.trans (F.inf_le_right _ _) h₂)⟩
