English
The filter associated to a filter basis is the collection of sets containing a basis member; closed under supersets and finite intersections as specified.
Русский
Фильтр, связанный с базисом фильтра, состоит из множеств, содержащих некоторый базисный элемент; закрыт по надмножинам и конечным пересечениям.
LaTeX
$$$\text{FilterBasis.filter}(B) = \{ s : Set\,\alpha \;|\; \exists t \in B, t \subseteq s\}$$$
Lean4
/-- The filter associated to a filter basis. -/
protected def filter (B : FilterBasis α) : Filter α
where
sets := {s | ∃ t ∈ B, t ⊆ s}
univ_sets := B.nonempty.imp fun s s_in => ⟨s_in, s.subset_univ⟩
sets_of_superset := fun ⟨s, s_in, h⟩ hxy => ⟨s, s_in, Set.Subset.trans h hxy⟩
inter_sets := fun ⟨_s, s_in, hs⟩ ⟨_t, t_in, ht⟩ =>
let ⟨u, u_in, u_sub⟩ := B.inter_sets s_in t_in
⟨u, u_in, u_sub.trans (inter_subset_inter hs ht)⟩
