English
Given p ∈ P and a family 𝒟 of cofinal subsets of a preorder P, the set I = { x ∈ P | ∃ n, x ≤ sequenceOfCofinals p 𝒟 n } is an ideal of P, and this ideal contains p and meets every 𝒟 i (Rasiowa–Sikorski lemma).
Русский
Пусть p ∈ P и есть семейство кофинальных подмножеств 𝒟. Множество I = { x ∈ P | существует n, x ≤ sequenceOfCofinals p 𝒟 n } образует идеал в P, содержит p и пересекает каждое 𝒟 i (лемма Раcиowa–Сикорски).
LaTeX
$$$I = \\{ x \\in P \\mid \\exists n, x \\le sequenceOfCofinals\\, p\\, 𝒟\\, n \\}$ является идеалом P, p ∈ I, \\forall i, 𝒟 i \\cap I \\neq \\emptyset.$$$
Lean4
/-- Given an element `p : P` and a family `𝒟` of cofinal subsets of a preorder `P`,
indexed by a countable type, `idealOfCofinals p 𝒟` is an ideal in `P` which
- contains `p`, according to `mem_idealOfCofinals p 𝒟`, and
- intersects every set in `𝒟`, according to `cofinal_meets_idealOfCofinals p 𝒟`.
This proves the Rasiowa–Sikorski lemma. -/
def idealOfCofinals : Ideal P
where
carrier := {x : P | ∃ n, x ≤ sequenceOfCofinals p 𝒟 n}
lower' := fun _ _ hxy ⟨n, hn⟩ ↦ ⟨n, le_trans hxy hn⟩
nonempty' := ⟨p, 0, le_rfl⟩
directed' := fun _ ⟨n, hn⟩ _ ⟨m, hm⟩ ↦
⟨_, ⟨max n m, le_rfl⟩, le_trans hn <| sequenceOfCofinals.monotone p 𝒟 (le_max_left _ _),
le_trans hm <| sequenceOfCofinals.monotone p 𝒟 (le_max_right _ _)⟩
