Enumerating a cofinal set

We define a typeclass IsRegularCardinalOrder for well-ordered types, whose order type equals (the initial ordinal of) their cofinality. This notion does not appear in the literature, but intends to generalize the properties of intervals Iio c.ord, wherever c is a regular cardinal. Other instances of this typeclass include ℕ, Ordinal, and Cardinal.

If s is a cofinal subset of a regular cardinal order α, there exists a unique order isomorphism α ≃o s, which we call Order.enum. When α = Ordinal, this is referred to as the enumerator function of the set. Note that if α = ℕ, then this definition matches Nat.nth.

Main results

• Order.enum_eq_iff: Order.enum s _ is the unique strictly monotonic function with range s.
• Order.isNormal_enum_iff_dirSupClosed: club sets correspond one to one with normal functions.

TODO

• Deprecate Ordinal.enumOrd in favor of Order.enum.
• Prove that Order.enum on the naturals coincides with Nat.nth.

class IsRegularCardinalOrder (α : Type u_2) [LinearOrder α] [WellFoundedLT α] : Prop

A typeclass which expresses that the order type of a well-order equals (the initial ordinal of) its cofinality.

If α is infinite, this implies that α is order isomorphic to Iio c.ord for some regular cardinal c. In the informal literature, one often says that α is a regular cardinal, by abuse of notation.

• type_lt_le_ord_cof : (Ordinal.type fun (x1 x2 : α) => x1 < x2) ≤ (Order.cof α).ord

instance instIsRegularCardinalOrderNat : IsRegularCardinalOrder ℕ

@[instance 100]

instance instIsRegularCardinalOrderOfSubsingleton {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [Subsingleton α] : IsRegularCardinalOrder α

instance instIsRegularCardinalOrderOrdinal : IsRegularCardinalOrder Ordinal.{u_2}

theorem Order.ord_cof_eq_type_lt {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] : (cof α).ord = Ordinal.type fun (x1 x2 : α) => x1 < x2

@[simp]

theorem Order.cof_eq_cardinalMk {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] : cof α = Cardinal.mk α

@[simp]

theorem Cardinal.ord_cardinalMk {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] : (mk α).ord = Ordinal.type fun (x1 x2 : α) => x1 < x2

theorem Order.cof_ordinal : cof Ordinal.{u} = Cardinal.univ.{u, u + 1}

theorem Order.type_eq_of_isCofinal {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} (hs : IsCofinal s) : (Ordinal.type fun (x1 x2 : ↑s) => x1 < x2) = Ordinal.type fun (x1 x2 : α) => x1 < x2

noncomputable def Order.enum {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] (s : Set α) (hs : IsCofinal s) : α ≃o ↑s

Enumerate the elements of a cofinal subset of α by α itself. This is a generalization of Nat.nth.

Equations

• Order.enum s hs = OrderIso.ofRelIsoLT ⋯.some

theorem Order.enum_le_of_forall_lt {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s} {a o : α} (ho : o ∈ s) (H : ∀ b < a, ↑((enum s hs) b) < o) : ↑((enum s hs) a) ≤ o

theorem Order.enum_succ_le_of_lt {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s} [SuccOrder α] {a o : α} (ha : o ∈ s) (H : ↑((enum s hs) a) < o) : ↑((enum s hs) (succ a)) ≤ o

@[simp]

theorem Order.enum_univ {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] (x : α) : (enum Set.univ ⋯) x = ⟨x, ⋯⟩

theorem Order.enum_anti {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s} {t : Set α} {x : α} (h : s ⊆ t) : ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)

theorem Order.enum_eq_iff {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s} {f : α → α} : Subtype.val ∘ ⇑(enum s hs) = f ↔ StrictMono f ∧ Set.range f = s

A characterization of Order.enum s _: it is the unique strictly monotone function with range s.

theorem Order.enum_range {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {f : α → α} (hf : StrictMono f) : enum (Set.range f) ⋯ = StrictMono.orderIso f hf

theorem Order.enum_bot {α : Type u_2} [ConditionallyCompleteLinearOrderBot α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s} : ↑((enum s hs) ⊥) = sInf s

theorem Order.isNormal_enum_iff_dirSupClosed {α : Type u_1} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s} : IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s

Club sets in regular cardinals correspond one to one with normal functions.

See also Order.isNormal_enum_iff_isClub.