English
The join of a filter of filters is defined by the relation: s belongs to join f exactly when the set of all filters t with s ∈ t belongs to f.
Русский
Слияние фильтров определяется так: s ∈ join f тогда и только тогда, когда множество всех фильтров t с условием s ∈ t принадлежит f.
LaTeX
$$$ s \in \mathrm{join}(f) \iff \{ t : \mathrm{Filter}(\alpha) \mid s \in t\} \in f. $$$
Lean4
/-- The join of a filter of filters is defined by the relation `s ∈ join f ↔ {t | s ∈ t} ∈ f`. -/
def join (f : Filter (Filter α)) : Filter α
where
sets := {s | {t : Filter α | s ∈ t} ∈ f}
univ_sets := by simp only [mem_setOf_eq, univ_mem, setOf_true]
sets_of_superset hx xy := mem_of_superset hx fun f h => mem_of_superset h xy
inter_sets hx hy := mem_of_superset (inter_mem hx hy) fun f ⟨h₁, h₂⟩ => inter_mem h₁ h₂
