English
Let (P, ≤) be a preorder, p ∈ P, and 𝒟: ι → Cofinal P be a family of cofinal subsets of P indexed by ι. Then for every i ∈ ι there exists an element x ∈ 𝒟(i) that also lies in the idealOfCofinals p 𝒟, i.e., x ∈ 𝒟(i) and x ∈ idealOfCofinals(p, 𝒟).
Русский
Пусть (P, ≤) — частичный порядок. Пусть p ∈ P и 𝒟 : ι → Cofinal P — семейство когранальных подмножеств, индексируемое ι. Тогда для каждого i ∈ ι существует элемент x ∈ 𝒟(i), который также принадлежит idealOfCofinals(p, 𝒟), т.е. x ∈ 𝒟(i) и x ∈ idealOfCofinals(p, 𝒟).
LaTeX
$$$\\\\forall i \\\\, \\\\exists x \\\\, x \\\\in \\\\mathcal{D}(i) \\\\land \\\\ x \\\\in \\\\mathrm{idealOfCofinals}(p,\\\\mathcal{D}).$$$
Lean4
/-- `idealOfCofinals p 𝒟` is `𝒟`-generic. -/
theorem cofinal_meets_idealOfCofinals (i : ι) : ∃ x : P, x ∈ 𝒟 i ∧ x ∈ idealOfCofinals p 𝒟 :=
⟨_, sequenceOfCofinals.encode_mem p 𝒟 i, _, le_rfl⟩
