using uncountable cofinality to show a sequence is bounded

Stream: new members

[Connor Gordon]

Suppose I have an ordinal κ with κ.cof > cardinal.aleph_0 and a function f : ℕ → ordinal such that f n < κ for all n. This should imply that Sup (set.range f) < κ by the definition of uncountable cofinality, but how would I show this in Lean?

For information on cofinality in Lean: docs#cofinality

[Connor Gordon]

Update: unpacking the definitions in κ.cof > cardinal.aleph_0 yielded quotient.lift_on κ (λ (a : Well_order), strict_order.cof a.r) ordinal.cof._proof_1 > (cardinal.mk ℕ).lift which honestly raises more questions than it answers; could I possibly get some help on understanding what any of these mean?

[Junyan Xu]

I think you can just apply docs#ordinal.sup_lt_ord to the function f : ℕ → ordinal you constructed. The resulting ordinal.sup f is probably easier to work with than Sup (set.range f). You can use docs#ordinal.Sup_eq_sup if you do want Sup (set.range f).

[Matt Diamond]

could I possibly get some help on understanding what any of these mean?

I could be wrong, but my guess is that the advice will be to not worry about the underlying machinery and just focus on the API provided by Lean (i.e. the lemmas describing cofinality, such as docs#ordinal.cof_eq_Inf_lsub). However, you should definitely understand that ordinals in Lean are represented by the type of well orders quotiented by order isomorphism, which is part of what you're seeing.

[Matt Diamond]

You're also seeing that aleph_0 is defined as the cardinality of the natural numbers (cardinal.mk ℕ).

[Matt Diamond]

ordinal.cof ultimately relies on docs#order.cof