English
For a sequence of sets s_n, there is an antitone sequence t_n approximating the infimum of principal filters.
Русский
Для последовательности множеств s_n существует антиобразовательная последовательность t_n, приближающая инфимум начальных фильтров.
LaTeX
$$$$\\exists t:\\mathbb N \\to \\mathcal P(\\alpha)\\;\\text{Antitone}(t)\\;\\land\\; \\bigwedge_i (\\bigwedge t) = \\bigwedge_i (\\mathcal P(s_i)) .$$$$
Lean4
theorem antitone_seq_of_seq (s : ℕ → Set α) : ∃ t : ℕ → Set α, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i) :=
by
use fun n => ⋂ m ≤ n, s m; constructor
· exact fun i j hij => biInter_mono (Iic_subset_Iic.2 hij) fun n _ => Subset.rfl
apply le_antisymm <;> rw [le_iInf_iff] <;> intro i
· rw [le_principal_iff]
refine (biInter_mem (finite_le_nat _)).2 fun j _ => ?_
exact mem_iInf_of_mem j (mem_principal_self _)
· refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)
rfl
