Small ordinal facts

Neutral helpers about countable ordinals, used by the Scott refinement count, the Borel BFEquiv analysis, and the ranked-thinness package. Nothing here is specific to infinitary logic, descriptive set theory, or any one of those consumers.

Both shapes of the countability statement are provided: Set.Countable (Set.Iio β) and the Countable instance on the coercion, since consumers need one or the other and converting at each site is noise.

theorem InfinitaryLogic.countable_Iio_of_lt_omega1 (β : Ordinal.{0}) (hβ : β < Ordinal.omega 1) : Countable ↑(Set.Iio β)

For β < ω₁, the ordinals below β form a countable type.

theorem InfinitaryLogic.setCountable_Iio_of_lt_omega1 (β : Ordinal.{0}) (hβ : β < Ordinal.omega 1) : (Set.Iio β).Countable

The same fact as a Set.Countable.

theorem InfinitaryLogic.add_omega0_lt_omega1 {α : Ordinal.{0}} (hα : α < (Cardinal.aleph 1).ord) : α + Ordinal.omega0 < (Cardinal.aleph 1).ord

ω₁ absorbs + ω: a countable ordinal stays countable after appending ω.

The standard way to exceed a bound α < ω₁ while staying countable — α + ω is at least α, infinite, and still countable — which is what order-type diagonalizations against a boundedness theorem need.

Rank is monotone in the relation

theorem InfinitaryLogic.rank_le_rank_of_imp {α : Type u_1} {r s : α → α → Prop} [IsWellFounded α r] [IsWellFounded α s] (h : ∀ (a b : α), r a b → s a b) (a : α) : IsWellFounded.rank r a ≤ IsWellFounded.rank s a

If r ⊆ s are both well-founded, ranks under r are bounded by ranks under s.