Theorems · Definition · order theory

Order.sequenceOfCofinals

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

Given a starting point, and a countable family of cofinal sets, this is an increasing sequence that intersects each cofinal set.

Defined in

Mathlib.Order.Ideal

Cited by

5 results in Mathlib

Foundations

Depth 10 from the axioms · uses Classical.choice

Assumes

PreorderEncodable