exists countable cofinal chain for directed posets

Stream: Is there code for X?

[Andrew Yang]

Do we have something like this in mathlib?

import Mathlib.SetTheory.Cardinal.Cofinality

example {α : Type*} [Preorder α] [IsDirected α (· ≤ ·)]
    (h : Order.cof (α := α) (· ≤ ·) ≤ .aleph0) :
    ∃ l : ℕ →o α, IsCofinal (Set.range l) := sorry

[Nir Paz]

I don't think we do.

[Junyan Xu]

Apparently there is no connection between the two concepts in mathlib
@loogle IsCofinal, Order.cof

[loogle]

:shrug: nothing found

[Violeta Hernández]

Junyan Xu said:

Apparently there is no connection between the two concepts in mathlib
loogle IsCofinal, Order.cof

IsCofinal was introduced by me not long ago. My goal is to redefine Order.cof as the least cardinality of an IsCofinal subset of a preorder, but I've been busy with other things and haven't quite been able to do that refactor yet.

[Violeta Hernández]

As of the original post, we don't currently have anything like that for either IsCofinal or Order.cof.

[Violeta Hernández]

Closest thing would be the API around docs#Ordinal.IsFundamentalSequence which unfortunately sucks