Arithmetic on families of ordinals

This file proves basic results about the suprema of families of ordinals.

Various other basic arithmetic results are given in Principal.lean instead.

Supremum of a family of ordinals

theorem Ordinal.bddAbove_of_small {s : Set Ordinal.{u}} [Small.{u, u + 1} ↑s] : BddAbove s

theorem Ordinal.bddAbove_iff_small {s : Set Ordinal.{u}} : BddAbove s ↔ Small.{u, u + 1} ↑s

theorem Ordinal.bddAbove_image {s : Set Ordinal.{u}} (hf : BddAbove s) (f : Ordinal.{u} → Ordinal.{max u v}) : BddAbove (f '' s)

theorem Ordinal.bddAbove_range_comp {ι : Type u} {f : ι → Ordinal.{v}} (hf : BddAbove (Set.range f)) (g : Ordinal.{v} → Ordinal.{max v w}) : BddAbove (Set.range (g ∘ f))

theorem Ordinal.le_iSup {ι : Type u_3} (f : ι → Ordinal.{u}) [Small.{u, u_3} ι] (i : ι) : f i ≤ ⨆ (i : ι), f i

le_ciSup whenever the input type is small in the output universe. This lemma sometimes fails to infer f in simple cases and needs it to be given explicitly.

@[simp]

theorem Ordinal.iSup_le_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] : ⨆ (i : ι), f i ≤ a ↔ ∀ (i : ι), f i ≤ a

ciSup_le_iff' whenever the input type is small in the output universe.

theorem Ordinal.iSup_le {ι : Sort u_3} {f : ι → Ordinal.{u_4}} {a : Ordinal.{u_4}} : (∀ (i : ι), f i ≤ a) → ⨆ (i : ι), f i ≤ a

An alias of ciSup_le' for discoverability.

@[simp]

theorem Ordinal.lt_iSup_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] : a < ⨆ (i : ι), f i ↔ ∃ (i : ι), a < f i

lt_ciSup_iff' whenever the input type is small in the output universe.

theorem Ordinal.lt_iSup_add_one {ι : Type u_3} (f : ι → Ordinal.{u}) [Small.{u, u_3} ι] (i : ι) : f i < ⨆ (i : ι), f i + 1

theorem Ordinal.iSup_add_one_le_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] : ⨆ (i : ι), f i + 1 ≤ a ↔ ∀ (i : ι), f i < a

theorem Ordinal.iSup_add_one_le {ι : Sort u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} (h : ∀ (i : ι), f i < a) : ⨆ (i : ι), f i + 1 ≤ a

theorem Ordinal.lt_iSup_add_one_iff {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι] : a < ⨆ (i : ι), f i + 1 ↔ ∃ (i : ι), a ≤ f i

theorem Ordinal.succ_lt_iSup_of_ne_iSup {ι : Type u_3} {f : ι → Ordinal.{u}} [Small.{u, u_3} ι] (hf : ∀ (i : ι), f i ≠ iSup f) {a : Ordinal.{u}} (hao : a < iSup f) : Order.succ a < iSup f

theorem Ordinal.iSup_eq_zero_iff {ι : Type u_3} {f : ι → Ordinal.{u}} [Small.{u, u_3} ι] : iSup f = 0 ↔ ∀ (i : ι), f i = 0

theorem Ordinal.iSup_sum {α : Type u_3} {β : Type u_4} (f : α ⊕ β → Ordinal.{u}) [Small.{u, u_3} α] [Small.{u, u_4} β] : iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))

theorem Ordinal.unbounded_range_of_le_iSup {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α) (h : type r ≤ ⨆ (i : β), (typein r).toRelEmbedding (f i)) : Set.Unbounded r (Set.range f)

theorem Ordinal.sSup_ord (s : Set Cardinal.{u_3}) : (sSup s).ord = sSup (Cardinal.ord '' s)

theorem Ordinal.iSup_ord {ι : Sort u_3} (f : ι → Cardinal.{u_4}) : (⨆ (i : ι), f i).ord = ⨆ (i : ι), (f i).ord

theorem Ordinal.lift_card_sInf_compl_le (s : Set Ordinal.{u}) : Cardinal.lift.{u + 1, u} (sInf sᶜ).card ≤ Cardinal.mk ↑s

theorem Ordinal.card_sInf_range_compl_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) : (sInf (Set.range f)ᶜ).card ≤ Cardinal.lift.{v, u} (Cardinal.mk ι)

theorem Ordinal.card_sInf_range_compl_le {ι : Type u} (f : ι → Ordinal.{u}) : (sInf (Set.range f)ᶜ).card ≤ Cardinal.mk ι

theorem Ordinal.sInf_compl_lt_lift_ord_succ {ι : Type u} (f : ι → Ordinal.{max u v}) : sInf (Set.range f)ᶜ < lift.{v, u} (Order.succ (Cardinal.mk ι)).ord

theorem Ordinal.sInf_compl_lt_ord_succ {ι : Type u} (f : ι → Ordinal.{u}) : sInf (Set.range f)ᶜ < (Order.succ (Cardinal.mk ι)).ord

theorem Ordinal.bddAbove_add_one_image_iff {s : Set Ordinal.{u_3}} : BddAbove ((fun (x : Ordinal.{u_3}) => x + 1) '' s) ↔ BddAbove s

theorem Ordinal.bddAbove_range_add_one_iff {β : Type u_2} {f : β → Ordinal.{u}} : BddAbove (Set.range fun (i : β) => f i + 1) ↔ BddAbove (Set.range f)

theorem Ordinal.sSup_le_sSup_add_one (s : Set Ordinal.{u_3}) : sSup s ≤ sSup ((fun (x : Ordinal.{u_3}) => x + 1) '' s)

theorem Ordinal.iSup_le_iSup_add_one {β : Type u_2} (f : β → Ordinal.{u_3}) : ⨆ (i : β), f i ≤ ⨆ (i : β), f i + 1

theorem Ordinal.iSup_add_one {β : Type u_3} [LinearOrder β] [NoMaxOrder β] {f : β → Ordinal.{u}} (hf : StrictMono f) : ⨆ (i : β), f i + 1 = ⨆ (i : β), f i

theorem Ordinal.iSup_Iio_add_one {a : Ordinal.{u}} {f : ↑(Set.Iio a) → Ordinal.{u}} (hf : StrictMono f) (ha : Order.IsSuccPrelimit a) : ⨆ (i : ↑(Set.Iio a)), f i + 1 = ⨆ (i : ↑(Set.Iio a)), f i

Results about injectivity and surjectivity

theorem not_surjective_of_ordinal {α : Type u_1} [Small.{u, u_1} α] (f : α → Ordinal.{u}) : ¬Function.Surjective f

theorem not_injective_of_ordinal {α : Type u_1} [Small.{u, u_1} α] (f : Ordinal.{u} → α) : ¬Function.Injective f

theorem not_small_ordinal : ¬Small.{u, max (u + 1) (v + 1)} Ordinal.{max u v}

The type of ordinals in universe u is not Small.{u}. This is the type-theoretic analog of the Burali-Forti paradox.

instance Ordinal.uncountable : Uncountable Ordinal.{u}

theorem Ordinal.not_bddAbove_compl_of_small (s : Set Ordinal.{u}) [hs : Small.{u, u + 1} ↑s] : ¬BddAbove sᶜ

Casting naturals into ordinals, compatibility with operations

@[simp]

theorem Ordinal.iSup_natCast : iSup Nat.cast = omega0

theorem Ordinal.apply_omega0_of_isNormal {f : Ordinal.{u} → Ordinal.{v}} (hf : Order.IsNormal f) : ⨆ (n : ℕ), f ↑n = f omega0

@[simp]

theorem Ordinal.add_iSup (o : Ordinal.{u}) {ι : Type u_1} [Small.{u, u_1} ι] [Nonempty ι] (f : ι → Ordinal.{u}) : o + ⨆ (i : ι), f i = ⨆ (i : ι), o + f i

@[simp]

theorem Ordinal.add_sSup (o : Ordinal.{u}) {s : Set Ordinal.{u}} [Small.{u, u + 1} ↑s] (hs : s.Nonempty) : o + sSup s = sSup ((fun (x : Ordinal.{u}) => o + x) '' s)

@[simp]

theorem Ordinal.mul_sSup (o : Ordinal.{u_1}) (s : Set Ordinal.{u_1}) : o * sSup s = sSup ((fun (x : Ordinal.{u_1}) => o * x) '' s)

@[simp]

theorem Ordinal.mul_iSup (o : Ordinal.{u_1}) {ι : Sort u_2} (f : ι → Ordinal.{u_1}) : o * ⨆ (i : ι), f i = ⨆ (i : ι), o * f i

@[simp]

theorem Ordinal.iSup_add_natCast (o : Ordinal.{u_1}) : ⨆ (n : ℕ), o + ↑n = o + omega0

@[simp]

theorem Ordinal.iSup_mul_natCast (o : Ordinal.{u_1}) : ⨆ (n : ℕ), o * ↑n = o * omega0