English
For a set s of filters, l is in the closure of s iff every t ∈ l is approximated by some s ∈ s, i.e., ∃ l' ∈ s with t ∈ l'.
Русский
Для множества s фильтров: l принадлежит замыканию s тогда и только тогда, когда каждый t ∈ l приближается к некоторому l' ∈ s, где t ∈ l'.
LaTeX
$$$l \in \overline{s} \iff \forall t \in l, \ exists\ l' \in s,\ t \in l'.$$$
Lean4
protected theorem mem_closure {s : Set (Filter α)} {l : Filter α} : l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l' := by
simp only [closure_eq_compl_interior_compl, Filter.mem_interior, mem_compl_iff, not_exists, not_forall,
Classical.not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic, le_principal_iff]
