Theorems · Definition · order theory

Order.idealOfCofinals

{P : Type u_1} → [inst : Preorder P] → P → {ι : Type u_2} → [Encodable ι] → (ι → Order.Cofinal P) → Order.Ideal P

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.

Defined in

Mathlib.Order.Ideal

Cited by

4 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderEncodable