Documentation

Mathlib.SetTheory.Ordinal.Arithmetic

Ordinal arithmetic #

Ordinals have an addition (corresponding to disjoint union) that turns them into an additive monoid, and a multiplication (corresponding to the lexicographic order on the product) that turns them into a monoid. One can also define correspondingly a subtraction, a division, a successor function, a power function and a logarithm function.

We also define limit ordinals and prove the basic induction principle on ordinals separating successor ordinals and limit ordinals, in limitRecOn.

Main definitions and results #

We discuss the properties of casts of natural numbers of and of ω with respect to these operations.

Some properties of the operations are also used to discuss general tools on ordinals:

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

Further properties of addition on ordinals #

theorem Ordinal.add_le_add_iff_right {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (n : ) :
a + n b + n a b
theorem Ordinal.add_right_cancel {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (n : ) :
a + n = b + n a = b

The predecessor of an ordinal #

The ordinal predecessor of o is o' if o = succ o', and o otherwise.

Equations
Instances For
    @[simp]
    theorem Ordinal.pred_succ (o : Ordinal.{u_4}) :
    (Order.succ o).pred = o

    Limit ordinals #

    A limit ordinal is an ordinal which is not zero and not a successor.

    TODO: deprecate this in favor of Order.IsSuccLimit.

    Equations
    Instances For
      @[deprecated Ordinal.IsLimit.isSuccPrelimit]

      Alias of Ordinal.IsLimit.isSuccPrelimit.

      theorem Ordinal.IsLimit.succ_lt {o : Ordinal.{u_4}} {a : Ordinal.{u_4}} (h : o.IsLimit) :
      a < oOrder.succ a < o
      @[deprecated Ordinal.isSuccPrelimit_zero]

      Alias of Ordinal.isSuccPrelimit_zero.

      theorem Ordinal.not_succ_of_isLimit {o : Ordinal.{u_4}} (h : o.IsLimit) :
      theorem Ordinal.succ_lt_of_isLimit {o : Ordinal.{u_4}} {a : Ordinal.{u_4}} (h : o.IsLimit) :
      Order.succ a < o a < o
      theorem Ordinal.limit_le {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} :
      o a x < o, x a
      theorem Ordinal.lt_limit {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_4}} :
      a < o x < o, a < x
      @[simp]
      theorem Ordinal.lift_isLimit (o : Ordinal.{v}) :
      (Ordinal.lift.{u, v} o).IsLimit o.IsLimit
      theorem Ordinal.IsLimit.pos {o : Ordinal.{u_4}} (h : o.IsLimit) :
      0 < o
      theorem Ordinal.IsLimit.one_lt {o : Ordinal.{u_4}} (h : o.IsLimit) :
      1 < o
      theorem Ordinal.IsLimit.nat_lt {o : Ordinal.{u_4}} (h : o.IsLimit) (n : ) :
      n < o
      theorem Ordinal.zero_or_succ_or_limit (o : Ordinal.{u_4}) :
      o = 0 (∃ (a : Ordinal.{u_4}), o = Order.succ a) o.IsLimit
      def Ordinal.limitRecOn {C : Ordinal.{u_5}Sort u_4} (o : Ordinal.{u_5}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_5}) → C oC (Order.succ o)) (H₃ : (o : Ordinal.{u_5}) → o.IsLimit((o' : Ordinal.{u_5}) → o' < oC o')C o) :
      C o

      Main induction principle of ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Ordinal.limitRecOn_zero {C : Ordinal.{u_4}Sort u_5} (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C oC (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit((o' : Ordinal.{u_4}) → o' < oC o')C o) :
        Ordinal.limitRecOn 0 H₁ H₂ H₃ = H₁
        @[simp]
        theorem Ordinal.limitRecOn_succ {C : Ordinal.{u_4}Sort u_5} (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C oC (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit((o' : Ordinal.{u_4}) → o' < oC o')C o) :
        (Order.succ o).limitRecOn H₁ H₂ H₃ = H₂ o (o.limitRecOn H₁ H₂ H₃)
        @[simp]
        theorem Ordinal.limitRecOn_limit {C : Ordinal.{u_4}Sort u_5} (o : Ordinal.{u_4}) (H₁ : C 0) (H₂ : (o : Ordinal.{u_4}) → C oC (Order.succ o)) (H₃ : (o : Ordinal.{u_4}) → o.IsLimit((o' : Ordinal.{u_4}) → o' < oC o')C o) (h : o.IsLimit) :
        o.limitRecOn H₁ H₂ H₃ = H₃ o h fun (x : Ordinal.{u_4}) (_h : x < o) => x.limitRecOn H₁ H₂ H₃
        def Ordinal.boundedLimitRecOn {l : Ordinal.{u_5}} (lLim : l.IsLimit) {C : (Set.Iio l)Sort u_4} (o : (Set.Iio l)) (H₁ : C 0, ) (H₂ : (o : (Set.Iio l)) → C oC Order.succ o, ) (H₃ : (o : (Set.Iio l)) → (↑o).IsLimit((o' : (Set.Iio l)) → o' < oC o')C o) :
        C o

        Bounded recursion on ordinals. Similar to limitRecOn, with the assumption o < l added to all cases. The final term's domain is the ordinals below l.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Ordinal.boundedLimitRec_zero {l : Ordinal.{u_4}} (lLim : l.IsLimit) {C : (Set.Iio l)Sort u_5} (H₁ : C 0, ) (H₂ : (o : (Set.Iio l)) → C oC Order.succ o, ) (H₃ : (o : (Set.Iio l)) → (↑o).IsLimit((o' : (Set.Iio l)) → o' < oC o')C o) :
          Ordinal.boundedLimitRecOn lLim 0, H₁ H₂ H₃ = H₁
          @[simp]
          theorem Ordinal.boundedLimitRec_succ {l : Ordinal.{u_4}} (lLim : l.IsLimit) {C : (Set.Iio l)Sort u_5} (o : (Set.Iio l)) (H₁ : C 0, ) (H₂ : (o : (Set.Iio l)) → C oC Order.succ o, ) (H₃ : (o : (Set.Iio l)) → (↑o).IsLimit((o' : (Set.Iio l)) → o' < oC o')C o) :
          Ordinal.boundedLimitRecOn lLim Order.succ o, H₁ H₂ H₃ = H₂ o (Ordinal.boundedLimitRecOn lLim o H₁ H₂ H₃)
          theorem Ordinal.boundedLimitRec_limit {l : Ordinal.{u_4}} (lLim : l.IsLimit) {C : (Set.Iio l)Sort u_5} (o : (Set.Iio l)) (H₁ : C 0, ) (H₂ : (o : (Set.Iio l)) → C oC Order.succ o, ) (H₃ : (o : (Set.Iio l)) → (↑o).IsLimit((o' : (Set.Iio l)) → o' < oC o')C o) (oLim : (↑o).IsLimit) :
          Ordinal.boundedLimitRecOn lLim o H₁ H₂ H₃ = H₃ o oLim fun (x : (Set.Iio l)) (x_1 : x < o) => Ordinal.boundedLimitRecOn lLim x H₁ H₂ H₃
          Equations
          theorem Ordinal.enum_succ_eq_top {o : Ordinal.{u_4}} :
          (Ordinal.enum fun (x1 x2 : (Order.succ o).toType) => x1 < x2) o, =
          theorem Ordinal.has_succ_of_type_succ_lt {α : Type u_4} {r : ααProp} [wo : IsWellOrder α r] (h : a < Ordinal.type r, Order.succ a < Ordinal.type r) (x : α) :
          ∃ (y : α), r x y
          theorem Ordinal.toType_noMax_of_succ_lt {o : Ordinal.{u_4}} (ho : a < o, Order.succ a < o) :
          NoMaxOrder o.toType
          @[deprecated Ordinal.toType_noMax_of_succ_lt]
          theorem Ordinal.out_no_max_of_succ_lt {o : Ordinal.{u_4}} (ho : a < o, Order.succ a < o) :
          NoMaxOrder o.toType

          Alias of Ordinal.toType_noMax_of_succ_lt.

          theorem Ordinal.bounded_singleton {α : Type u_1} {r : ααProp} [IsWellOrder α r] (hr : (Ordinal.type r).IsLimit) (x : α) :

          Normal ordinal functions #

          A normal ordinal function is a strictly increasing function which is order-continuous, i.e., the image f o of a limit ordinal o is the sup of f a for a < o.

          Equations
          Instances For
            theorem Ordinal.IsNormal.limit_le {f : Ordinal.{u_4}Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} :
            o.IsLimit∀ {a : Ordinal.{u_5}}, f o a b < o, f b a
            theorem Ordinal.IsNormal.limit_lt {f : Ordinal.{u_4}Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} (h : o.IsLimit) {a : Ordinal.{u_5}} :
            a < f o b < o, a < f b
            theorem Ordinal.isNormal_iff_strictMono_limit (f : Ordinal.{u_4}Ordinal.{u_5}) :
            Ordinal.IsNormal f StrictMono f ∀ (o : Ordinal.{u_4}), o.IsLimit∀ (a : Ordinal.{u_5}), (∀ b < o, f b a)f o a
            @[deprecated Ordinal.IsNormal.le_apply]
            theorem Ordinal.IsNormal.le_set {f : Ordinal.{u_4}Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.IsNormal f) (p : Set Ordinal.{u_4}) (p0 : p.Nonempty) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b o ap, a o) :
            f b o ap, f a o
            theorem Ordinal.IsNormal.le_set' {α : Type u_1} {f : Ordinal.{u_4}Ordinal.{u_5}} {o : Ordinal.{u_5}} (H : Ordinal.IsNormal f) (p : Set α) (p0 : p.Nonempty) (g : αOrdinal.{u_4}) (b : Ordinal.{u_4}) (H₂ : ∀ (o : Ordinal.{u_4}), b o ap, g a o) :
            f b o ap, f (g a) o
            theorem Ordinal.IsNormal.isLimit {f : Ordinal.{u_4}Ordinal.{u_5}} (H : Ordinal.IsNormal f) {o : Ordinal.{u_4}} (l : o.IsLimit) :
            (f o).IsLimit
            theorem Ordinal.add_le_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b.IsLimit) :
            a + b c b' < b, a + b' c
            theorem Ordinal.add_isLimit (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} :
            b.IsLimit(a + b).IsLimit
            theorem Ordinal.IsLimit.add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} :
            b.IsLimit(a + b).IsLimit

            Alias of Ordinal.add_isLimit.

            Subtraction on ordinals #

            a - b is the unique ordinal satisfying b + (a - b) = a when b ≤ a.

            Equations
            theorem Ordinal.sub_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
            a - b c a b + c
            theorem Ordinal.lt_sub {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
            a < b - c c + a < b
            theorem Ordinal.sub_eq_of_add_eq {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a + b = c) :
            c - a = b
            theorem Ordinal.add_sub_cancel_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : b a) :
            b + (a - b) = a
            theorem Ordinal.le_sub_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b a) :
            c a - b b + c a
            theorem Ordinal.sub_lt_of_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b a) :
            a - b < c a < b + c
            @[simp]
            theorem Ordinal.sub_zero (a : Ordinal.{u_4}) :
            a - 0 = a
            @[simp]
            theorem Ordinal.zero_sub (a : Ordinal.{u_4}) :
            0 - a = 0
            @[simp]
            theorem Ordinal.sub_self (a : Ordinal.{u_4}) :
            a - a = 0
            theorem Ordinal.sub_sub (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) :
            a - b - c = a - (b + c)
            @[simp]
            theorem Ordinal.add_sub_add_cancel (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) :
            a + b - (a + c) = b - c
            theorem Ordinal.sub_isLimit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (h : b < a) :
            (a - b).IsLimit
            @[deprecated Ordinal.one_add_omega0]

            Alias of Ordinal.one_add_omega0.

            @[deprecated Ordinal.one_add_of_omega0_le]

            Alias of Ordinal.one_add_of_omega0_le.

            Multiplication of ordinals #

            The multiplication of ordinals o₁ and o₂ is the (well founded) lexicographic order on o₂ × o₁.

            Equations
            @[simp]
            theorem Ordinal.type_prod_lex {α : Type u} {β : Type u} (r : ααProp) (s : ββProp) [IsWellOrder α r] [IsWellOrder β s] :
            @[simp]
            theorem Ordinal.card_mul (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
            (a * b).card = a.card * b.card
            theorem Ordinal.le_mul_left (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) :
            a a * b
            theorem Ordinal.le_mul_right (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (hb : 0 < b) :
            a b * a
            theorem Ordinal.mul_le_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : b.IsLimit) :
            a * b c b' < b, a * b' c
            theorem Ordinal.mul_isNormal {a : Ordinal.{u_4}} (h : 0 < a) :
            theorem Ordinal.lt_mul_of_limit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c.IsLimit) :
            a < b * c c' < c, a < b * c'
            theorem Ordinal.mul_lt_mul_iff_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) :
            a * b < a * c b < c
            theorem Ordinal.mul_le_mul_iff_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) :
            a * b a * c b c
            theorem Ordinal.mul_lt_mul_of_pos_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a < b) (c0 : 0 < c) :
            c * a < c * b
            theorem Ordinal.mul_pos {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h₁ : 0 < a) (h₂ : 0 < b) :
            0 < a * b
            theorem Ordinal.mul_ne_zero {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
            a 0b 0a * b 0
            theorem Ordinal.le_of_mul_le_mul_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c * a c * b) (h0 : 0 < c) :
            a b
            theorem Ordinal.mul_right_inj {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (a0 : 0 < a) :
            a * b = a * c b = c
            theorem Ordinal.mul_isLimit {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (a0 : 0 < a) :
            b.IsLimit(a * b).IsLimit
            theorem Ordinal.mul_isLimit_left {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (l : a.IsLimit) (b0 : 0 < b) :
            (a * b).IsLimit
            theorem Ordinal.smul_eq_mul (n : ) (a : Ordinal.{u_4}) :
            n a = a * n

            Division on ordinals #

            a / b is the unique ordinal o satisfying a = b * o + o' with o' < b.

            Equations
            @[simp]
            theorem Ordinal.div_zero (a : Ordinal.{u_4}) :
            a / 0 = 0
            theorem Ordinal.lt_mul_succ_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b 0) :
            a < b * Order.succ (a / b)
            theorem Ordinal.lt_mul_div_add (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b 0) :
            a < b * (a / b) + b
            theorem Ordinal.div_le {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (b0 : b 0) :
            a / b c a < b * Order.succ c
            theorem Ordinal.lt_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c 0) :
            a < b / c c * Order.succ a b
            theorem Ordinal.div_pos {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c 0) :
            0 < b / c c b
            theorem Ordinal.le_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (c0 : c 0) :
            a b / c c * a b
            theorem Ordinal.div_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (b0 : b 0) :
            a / b < c a < b * c
            theorem Ordinal.div_le_of_le_mul {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : a b * c) :
            a / b c
            theorem Ordinal.mul_lt_of_lt_div {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
            a < b / cc * a < b
            @[simp]
            theorem Ordinal.zero_div (a : Ordinal.{u_4}) :
            0 / a = 0
            theorem Ordinal.mul_add_div (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b 0) (c : Ordinal.{u_4}) :
            (b * a + c) / b = a + c / b
            theorem Ordinal.div_eq_zero_of_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : a < b) :
            a / b = 0
            @[simp]
            theorem Ordinal.mul_div_cancel (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (b0 : b 0) :
            b * a / b = a
            theorem Ordinal.mul_add_div_mul {a : Ordinal.{u_4}} {c : Ordinal.{u_4}} (hc : c < a) (b : Ordinal.{u_4}) (d : Ordinal.{u_4}) :
            (a * b + c) / (a * d) = b / d
            theorem Ordinal.mul_div_mul_cancel {a : Ordinal.{u_4}} (ha : a 0) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) :
            a * b / (a * c) = b / c
            @[simp]
            theorem Ordinal.div_one (a : Ordinal.{u_4}) :
            a / 1 = a
            @[simp]
            theorem Ordinal.div_self {a : Ordinal.{u_4}} (h : a 0) :
            a / a = 1
            theorem Ordinal.mul_sub (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) (c : Ordinal.{u_4}) :
            a * (b - c) = a * b - a * c
            theorem Ordinal.isLimit_add_iff {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
            (a + b).IsLimit b.IsLimit b = 0 a.IsLimit
            theorem Ordinal.dvd_add_iff {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} :
            a b(a b + c a c)
            theorem Ordinal.div_mul_cancel {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
            a 0a ba * (b / a) = b
            theorem Ordinal.le_of_dvd {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} :
            b 0a ba b
            theorem Ordinal.dvd_antisymm {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h₁ : a b) (h₂ : b a) :
            a = b

            a % b is the unique ordinal o' satisfying a = b * o + o' with o' < b.

            Equations
            theorem Ordinal.mod_def (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
            a % b = a - b * (a / b)
            @[simp]
            theorem Ordinal.mod_zero (a : Ordinal.{u_4}) :
            a % 0 = a
            theorem Ordinal.mod_eq_of_lt {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (h : a < b) :
            a % b = a
            @[simp]
            theorem Ordinal.zero_mod (b : Ordinal.{u_4}) :
            0 % b = 0
            theorem Ordinal.div_add_mod (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
            b * (a / b) + a % b = a
            theorem Ordinal.mod_lt (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} (h : b 0) :
            a % b < b
            @[simp]
            theorem Ordinal.mod_self (a : Ordinal.{u_4}) :
            a % a = 0
            @[simp]
            theorem Ordinal.mod_one (a : Ordinal.{u_4}) :
            a % 1 = 0
            theorem Ordinal.dvd_of_mod_eq_zero {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (H : a % b = 0) :
            b a
            theorem Ordinal.mod_eq_zero_of_dvd {a : Ordinal.{u_4}} {b : Ordinal.{u_4}} (H : b a) :
            a % b = 0
            @[simp]
            theorem Ordinal.mul_add_mod_self (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) (z : Ordinal.{u_4}) :
            (x * y + z) % x = z % x
            @[simp]
            theorem Ordinal.mul_mod (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) :
            x * y % x = 0
            theorem Ordinal.mul_add_mod_mul {w : Ordinal.{u_4}} {x : Ordinal.{u_4}} (hw : w < x) (y : Ordinal.{u_4}) (z : Ordinal.{u_4}) :
            (x * y + w) % (x * z) = x * (y % z) + w
            theorem Ordinal.mul_mod_mul (x : Ordinal.{u_4}) (y : Ordinal.{u_4}) (z : Ordinal.{u_4}) :
            x * y % (x * z) = x * (y % z)
            theorem Ordinal.mod_mod_of_dvd (a : Ordinal.{u_4}) {b : Ordinal.{u_4}} {c : Ordinal.{u_4}} (h : c b) :
            a % b % c = a % c
            @[simp]
            theorem Ordinal.mod_mod (a : Ordinal.{u_4}) (b : Ordinal.{u_4}) :
            a % b % b = a % b

            Families of ordinals #

            There are two kinds of indexed families that naturally arise when dealing with ordinals: those indexed by some type in the appropriate universe, and those indexed by ordinals less than another. The following API allows one to convert from one kind of family to the other.

            In many cases, this makes it easy to prove claims about one kind of family via the corresponding claim on the other.

            def Ordinal.bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] (f : ια) (a : Ordinal.{u}) :
            a < Ordinal.type rα

            Converts a family indexed by a Type u to one indexed by an Ordinal.{u} using a specified well-ordering.

            Equations
            Instances For
              def Ordinal.bfamilyOfFamily {α : Type u_1} {ι : Type u} :
              (ια)(a : Ordinal.{u}) → a < Ordinal.type WellOrderingRelα

              Converts a family indexed by a Type u to one indexed by an Ordinal.{u} using a well-ordering given by the axiom of choice.

              Equations
              Instances For
                def Ordinal.familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < oα) :
                ια

                Converts a family indexed by an Ordinal.{u} to one indexed by a Type u using a specified well-ordering.

                Equations
                Instances For
                  def Ordinal.familyOfBFamily {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < oα) :
                  o.toTypeα

                  Converts a family indexed by an Ordinal.{u} to one indexed by a Type u using a well-ordering given by the axiom of choice.

                  Equations
                  Instances For
                    @[simp]
                    theorem Ordinal.bfamilyOfFamily'_typein {α : Type u_1} {ι : Type u_4} (r : ιιProp) [IsWellOrder ι r] (f : ια) (i : ι) :
                    @[simp]
                    theorem Ordinal.bfamilyOfFamily_typein {α : Type u_1} {ι : Type u_4} (f : ια) (i : ι) :
                    Ordinal.bfamilyOfFamily f (Ordinal.typein WellOrderingRel i) = f i
                    @[simp]
                    theorem Ordinal.familyOfBFamily'_enum {α : Type u_1} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < oα) (i : Ordinal.{u}) (hi : i < o) :
                    Ordinal.familyOfBFamily' r ho f ((Ordinal.enum r) i, ) = f i hi
                    @[simp]
                    theorem Ordinal.familyOfBFamily_enum {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < oα) (i : Ordinal.{u_4}) (hi : i < o) :
                    o.familyOfBFamily f ((Ordinal.enum fun (x1 x2 : o.toType) => x1 < x2) i, ) = f i hi
                    def Ordinal.brange {α : Type u_1} (o : Ordinal.{u_4}) (f : (a : Ordinal.{u_4}) → a < oα) :
                    Set α

                    The range of a family indexed by ordinals.

                    Equations
                    Instances For
                      theorem Ordinal.mem_brange {α : Type u_1} {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < oα} {a : α} :
                      a o.brange f ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = a
                      theorem Ordinal.mem_brange_self {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oα) (i : Ordinal.{u_4}) (hi : i < o) :
                      f i hi o.brange f
                      @[simp]
                      theorem Ordinal.range_familyOfBFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < oα) :
                      @[simp]
                      theorem Ordinal.range_familyOfBFamily {α : Type u_1} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oα) :
                      Set.range (o.familyOfBFamily f) = o.brange f
                      @[simp]
                      theorem Ordinal.brange_bfamilyOfFamily' {α : Type u_1} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] (f : ια) :
                      @[simp]
                      theorem Ordinal.brange_bfamilyOfFamily {α : Type u_1} {ι : Type u} (f : ια) :
                      (Ordinal.type WellOrderingRel).brange (Ordinal.bfamilyOfFamily f) = Set.range f
                      @[simp]
                      theorem Ordinal.brange_const {α : Type u_1} {o : Ordinal.{u_4}} (ho : o 0) {c : α} :
                      (o.brange fun (x : Ordinal.{u_4}) (x : x < o) => c) = {c}
                      theorem Ordinal.comp_bfamilyOfFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] (f : ια) (g : αβ) :
                      (fun (i : Ordinal.{u}) (hi : i < Ordinal.type r) => g (Ordinal.bfamilyOfFamily' r f i hi)) = Ordinal.bfamilyOfFamily' r (g f)
                      theorem Ordinal.comp_bfamilyOfFamily {α : Type u_1} {β : Type u_2} {ι : Type u} (f : ια) (g : αβ) :
                      (fun (i : Ordinal.{u}) (hi : i < Ordinal.type WellOrderingRel) => g (Ordinal.bfamilyOfFamily f i hi)) = Ordinal.bfamilyOfFamily (g f)
                      theorem Ordinal.comp_familyOfBFamily' {α : Type u_1} {β : Type u_2} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < oα) (g : αβ) :
                      g Ordinal.familyOfBFamily' r ho f = Ordinal.familyOfBFamily' r ho fun (i : Ordinal.{u}) (hi : i < o) => g (f i hi)
                      theorem Ordinal.comp_familyOfBFamily {α : Type u_1} {β : Type u_2} {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oα) (g : αβ) :
                      g o.familyOfBFamily f = o.familyOfBFamily fun (i : Ordinal.{u_4}) (hi : i < o) => g (f i hi)

                      Supremum of a family of ordinals #

                      @[deprecated iSup]

                      The supremum of a family of ordinals

                      Equations
                      Instances For
                        @[deprecated]
                        theorem Ordinal.sSup_eq_sup {ι : Type u} (f : ιOrdinal.{max u v} ) :
                        theorem Ordinal.bddAbove_range {ι : Type u} (f : ιOrdinal.{max u v} ) :

                        The range of an indexed ordinal function, whose outputs live in a higher universe than the inputs, is always bounded above. See Ordinal.lsub for an explicit bound.

                        theorem Ordinal.le_iSup {ι : Type u} (f : ιOrdinal.{max u v} ) (i : ι) :
                        f i iSup f

                        le_ciSup whenever the outputs live in a higher universe than the inputs.

                        @[deprecated Ordinal.le_iSup]
                        theorem Ordinal.le_sup {ι : Type u} (f : ιOrdinal.{max u v} ) (i : ι) :
                        theorem Ordinal.iSup_le_iff {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                        iSup f a ∀ (i : ι), f i a

                        ciSup_le_iff' whenever the outputs live in a higher universe than the inputs.

                        @[deprecated Ordinal.iSup_le_iff]
                        theorem Ordinal.sup_le_iff {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                        Ordinal.sup f a ∀ (i : ι), f i a
                        theorem Ordinal.iSup_le {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                        (∀ (i : ι), f i a)iSup f a

                        ciSup_le' whenever the outputs live in a higher universe than the inputs.

                        @[deprecated Ordinal.iSup_le]
                        theorem Ordinal.sup_le {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                        (∀ (i : ι), f i a)Ordinal.sup f a
                        theorem Ordinal.lt_iSup {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                        a < iSup f ∃ (i : ι), a < f i
                        @[deprecated Ordinal.lt_iSup]
                        theorem Ordinal.lt_sup {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                        a < Ordinal.sup f ∃ (i : ι), a < f i
                        @[deprecated]
                        theorem Ordinal.ne_iSup_iff_lt_iSup {ι : Type u} {f : ιOrdinal.{max u v} } :
                        (∀ (i : ι), f i iSup f) ∀ (i : ι), f i < iSup f
                        @[deprecated Ordinal.ne_iSup_iff_lt_iSup]
                        theorem Ordinal.ne_sup_iff_lt_sup {ι : Type u} {f : ιOrdinal.{max u v} } :
                        (∀ (i : ι), f i Ordinal.sup f) ∀ (i : ι), f i < Ordinal.sup f
                        theorem Ordinal.succ_lt_iSup_of_ne_iSup {ι : Type u} {f : ιOrdinal.{max u v} } (hf : ∀ (i : ι), f i iSup f) {a : Ordinal.{max u v} } (hao : a < iSup f) :
                        @[deprecated Ordinal.succ_lt_iSup_of_ne_iSup]
                        theorem Ordinal.sup_not_succ_of_ne_sup {ι : Type u} {f : ιOrdinal.{max u v} } (hf : ∀ (i : ι), f i Ordinal.sup f) {a : Ordinal.{max u v} } (hao : a < Ordinal.sup f) :
                        theorem Ordinal.iSup_eq_zero_iff {ι : Type u} {f : ιOrdinal.{max u v} } :
                        iSup f = 0 ∀ (i : ι), f i = 0
                        @[deprecated Ordinal.iSup_eq_zero_iff]
                        theorem Ordinal.sup_eq_zero_iff {ι : Type u} {f : ιOrdinal.{max u v} } :
                        Ordinal.sup f = 0 ∀ (i : ι), f i = 0
                        theorem Ordinal.IsNormal.map_iSup {f : Ordinal.{max u v}Ordinal.{max u w} } (H : Ordinal.IsNormal f) {ι : Type u} (g : ιOrdinal.{max u v} ) [Nonempty ι] :
                        f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
                        @[deprecated Ordinal.IsNormal.map_iSup]
                        @[deprecated ciSup_of_empty]
                        theorem Ordinal.sup_empty {ι : Type u_4} [IsEmpty ι] (f : ιOrdinal.{max u_5 u_4} ) :
                        @[deprecated ciSup_const]
                        theorem Ordinal.sup_const {ι : Type u_4} [_hι : Nonempty ι] (o : Ordinal.{max u_5 u_4} ) :
                        (Ordinal.sup fun (x : ι) => o) = o
                        @[deprecated ciSup_unique]
                        theorem Ordinal.sup_unique {ι : Type u_4} [Unique ι] (f : ιOrdinal.{max u_5 u_4} ) :
                        Ordinal.sup f = f default
                        @[deprecated csSup_le_csSup']
                        theorem Ordinal.iSup_eq_of_range_eq {ι : Sort u_4} {ι' : Sort u_5} {f : ιOrdinal.{u_6}} {g : ι'Ordinal.{u_6}} (h : Set.range f = Set.range g) :
                        iSup f = iSup g
                        @[deprecated Ordinal.iSup_eq_of_range_eq]
                        theorem Ordinal.sup_eq_of_range_eq {ι : Type u} {ι' : Type v} {f : ιOrdinal.{max u v w} } {g : ι'Ordinal.{max u v w} } (h : Set.range f = Set.range g) :
                        theorem Ordinal.iSup_sum {α : Type u} {β : Type v} (f : α βOrdinal.{max u v w} ) :
                        iSup f = max (⨆ (a : α), f (Sum.inl a)) (⨆ (b : β), f (Sum.inr b))
                        @[deprecated Ordinal.iSup_sum]
                        theorem Ordinal.sup_sum {α : Type u} {β : Type v} (f : α βOrdinal.{max (max u v) w} ) :
                        Ordinal.sup f = max (Ordinal.sup fun (a : α) => f (Sum.inl a)) (Ordinal.sup fun (b : β) => f (Sum.inr b))
                        theorem Ordinal.unbounded_range_of_le_iSup {α : Type u} {β : Type u} (r : ααProp) [IsWellOrder α r] (f : βα) (h : Ordinal.type r ⨆ (i : β), Ordinal.typein r (f i)) :
                        @[deprecated Ordinal.unbounded_range_of_le_iSup]
                        theorem Ordinal.unbounded_range_of_sup_ge {α : Type u} {β : Type u} (r : ααProp) [IsWellOrder α r] (f : βα) (h : Ordinal.type r Ordinal.sup (Ordinal.typein r f)) :
                        @[deprecated]
                        theorem Ordinal.le_sup_shrink_equiv {s : Set Ordinal.{u}} (hs : Small.{u, u + 1} s) (a : Ordinal.{u}) (ha : a s) :
                        a Ordinal.sup fun (x : Shrink.{u, u + 1} s) => ((equivShrink s).symm x)
                        @[deprecated]
                        theorem Ordinal.sup_eq_sSup {s : Set Ordinal.{u}} (hs : Small.{u, u + 1} s) :
                        (Ordinal.sup fun (x : Shrink.{u, u + 1} s) => ((equivShrink s).symm x)) = sSup s
                        theorem Ordinal.iSup_ord {ι : Sort u_4} {f : ιCardinal.{u_5}} (hf : BddAbove (Set.range f)) :
                        (iSup f).ord = ⨆ (i : ι), (f i).ord
                        theorem Ordinal.sup_eq_sup {ι : Type u} {ι' : Type u} (r : ιιProp) (r' : ι'ι'Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :

                        The supremum of a family of ordinals indexed by the set of ordinals less than some o : Ordinal.{u}. This is a special case of sup over the family provided by familyOfBFamily.

                        Equations
                        Instances For
                          @[simp]
                          theorem Ordinal.sup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                          Ordinal.sup (o.familyOfBFamily f) = o.bsup f
                          @[simp]
                          theorem Ordinal.sup_eq_bsup' {o : Ordinal.{u}} {ι : Type u} (r : ιιProp) [IsWellOrder ι r] (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                          @[simp]
                          theorem Ordinal.sSup_eq_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                          sSup (o.brange f) = o.bsup f
                          @[simp]
                          theorem Ordinal.bsup_eq_sup' {ι : Type u} (r : ιιProp) [IsWellOrder ι r] (f : ιOrdinal.{max u v} ) :
                          theorem Ordinal.bsup_eq_bsup {ι : Type u} (r : ιιProp) (r' : ιιProp) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ιOrdinal.{max u v} ) :
                          @[simp]
                          theorem Ordinal.bsup_eq_sup {ι : Type u} (f : ιOrdinal.{max u v} ) :
                          (Ordinal.type WellOrderingRel).bsup (Ordinal.bfamilyOfFamily f) = Ordinal.sup f
                          theorem Ordinal.bsup_congr {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁Ordinal.{max u v} ) (ho : o₁ = o₂) :
                          o₁.bsup f = o₂.bsup fun (a : Ordinal.{u}) (h : a < o₂) => f a
                          theorem Ordinal.bsup_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                          o.bsup f a ∀ (i : Ordinal.{u}) (h : i < o), f i h a
                          theorem Ordinal.bsup_le {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                          (∀ (i : Ordinal.{u}) (h : i < o), f i h a)o.bsup f a
                          theorem Ordinal.le_bsup {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_5 u_4} ) (i : Ordinal.{u_4}) (h : i < o) :
                          f i h o.bsup f
                          theorem Ordinal.lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) {a : Ordinal.{max u v} } :
                          a < o.bsup f ∃ (i : Ordinal.{u}) (hi : i < o), a < f i hi
                          theorem Ordinal.IsNormal.bsup {f : Ordinal.{max u v}Ordinal.{max u w} } (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (g : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                          o 0f (o.bsup g) = o.bsup fun (a : Ordinal.{u}) (h : a < o) => f (g a h)
                          theorem Ordinal.lt_bsup_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } :
                          (∀ (i : Ordinal.{u}) (h : i < o), f i h o.bsup f) ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
                          theorem Ordinal.bsup_not_succ_of_ne_bsup {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } (hf : ∀ {i : Ordinal.{u}} (h : i < o), f i h o.bsup f) (a : Ordinal.{max u v} ) :
                          a < o.bsup fOrder.succ a < o.bsup f
                          @[simp]
                          theorem Ordinal.bsup_eq_zero_iff {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_5 u_4} } :
                          o.bsup f = 0 ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi = 0
                          theorem Ordinal.lt_bsup_of_limit {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_4 u_5} } (hf : ∀ {a a' : Ordinal.{u_4}} (ha : a < o) (ha' : a' < o), a < a'f a ha < f a' ha') (ho : a < o, Order.succ a < o) (i : Ordinal.{u_4}) (h : i < o) :
                          f i h < o.bsup f
                          theorem Ordinal.bsup_succ_of_mono {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < Order.succ oOrdinal.{max u_4 u_5} } (hf : ∀ {i j : Ordinal.{u_4}} (hi : i < Order.succ o) (hj : j < Order.succ o), i jf i hi f j hj) :
                          (Order.succ o).bsup f = f o
                          @[simp]
                          theorem Ordinal.bsup_zero (f : (a : Ordinal.{u_4}) → a < 0Ordinal.{max u_4 u_5} ) :
                          theorem Ordinal.bsup_const {o : Ordinal.{u}} (ho : o 0) (a : Ordinal.{max u v} ) :
                          (o.bsup fun (x : Ordinal.{u}) (x : x < o) => a) = a
                          @[simp]
                          theorem Ordinal.bsup_one (f : (a : Ordinal.{u_4}) → a < 1Ordinal.{max u_4 u_5} ) :
                          Ordinal.bsup 1 f = f 0
                          theorem Ordinal.bsup_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o'Ordinal.{max (max u v) w} } (h : o.brange f o'.brange g) :
                          o.bsup f o'.bsup g
                          theorem Ordinal.bsup_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o'Ordinal.{max (max u v) w} } (h : o.brange f = o'.brange g) :
                          o.bsup f = o'.bsup g

                          The least strict upper bound of a family of ordinals.

                          Equations
                          Instances For
                            @[simp]
                            theorem Ordinal.sup_eq_lsub {ι : Type u} (f : ιOrdinal.{max u v} ) :
                            Ordinal.sup (Order.succ f) = Ordinal.lsub f
                            theorem Ordinal.lsub_le_iff {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max v u} } :
                            Ordinal.lsub f a ∀ (i : ι), f i < a
                            theorem Ordinal.lsub_le {ι : Type u_4} {f : ιOrdinal.{max u_5 u_4} } {a : Ordinal.{max u_5 u_4} } :
                            (∀ (i : ι), f i < a)Ordinal.lsub f a
                            theorem Ordinal.lt_lsub {ι : Type u_4} (f : ιOrdinal.{max u_5 u_4} ) (i : ι) :
                            theorem Ordinal.lt_lsub_iff {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max v u} } :
                            a < Ordinal.lsub f ∃ (i : ι), a f i
                            theorem Ordinal.sup_succ_eq_lsub {ι : Type u} (f : ιOrdinal.{max u v} ) :
                            theorem Ordinal.sup_eq_lsub_iff_lt_sup {ι : Type u} (f : ιOrdinal.{max u v} ) :
                            Ordinal.sup f = Ordinal.lsub f ∀ (i : ι), f i < Ordinal.sup f
                            @[simp]
                            theorem Ordinal.lsub_empty {ι : Type u_4} [h : IsEmpty ι] (f : ιOrdinal.{max u_5 u_4} ) :
                            theorem Ordinal.lsub_pos {ι : Type u} [h : Nonempty ι] (f : ιOrdinal.{max u v} ) :
                            @[simp]
                            @[simp]
                            theorem Ordinal.lsub_const {ι : Type u_4} [Nonempty ι] (o : Ordinal.{max u_5 u_4} ) :
                            (Ordinal.lsub fun (x : ι) => o) = Order.succ o
                            @[simp]
                            theorem Ordinal.lsub_unique {ι : Type u_4} [Unique ι] (f : ιOrdinal.{max u_5 u_4} ) :
                            Ordinal.lsub f = Order.succ (f default)
                            @[simp]
                            theorem Ordinal.lsub_sum {α : Type u} {β : Type v} (f : α βOrdinal.{max (max u v) w} ) :
                            Ordinal.lsub f = max (Ordinal.lsub fun (a : α) => f (Sum.inl a)) (Ordinal.lsub fun (b : β) => f (Sum.inr b))
                            theorem Ordinal.nonempty_compl_range {ι : Type u} (f : ιOrdinal.{max u v} ) :
                            (Set.range f).Nonempty
                            @[simp]
                            theorem Ordinal.lsub_typein (o : Ordinal.{u}) :
                            Ordinal.lsub (Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2) = o
                            theorem Ordinal.sup_typein_limit {o : Ordinal.{u}} (ho : a < o, Order.succ a < o) :
                            Ordinal.sup (Ordinal.typein fun (x1 x2 : o.toType) => x1 < x2) = o
                            @[simp]
                            theorem Ordinal.sup_typein_succ {o : Ordinal.{u}} :
                            Ordinal.sup (Ordinal.typein fun (x1 x2 : (Order.succ o).toType) => x1 < x2) = o

                            The least strict upper bound of a family of ordinals indexed by the set of ordinals less than some o : Ordinal.{u}.

                            This is to lsub as bsup is to sup.

                            Equations
                            Instances For
                              @[simp]
                              theorem Ordinal.bsup_eq_blsub (o : Ordinal.{u}) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              (o.bsup fun (a : Ordinal.{u}) (ha : a < o) => Order.succ (f a ha)) = o.blsub f
                              theorem Ordinal.lsub_eq_blsub' {ι : Type u} (r : ιιProp) [IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              theorem Ordinal.lsub_eq_lsub {ι : Type u} {ι' : Type u} (r : ιιProp) (r' : ι'ι'Prop) [IsWellOrder ι r] [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : Ordinal.type r = o) (ho' : Ordinal.type r' = o) (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              @[simp]
                              theorem Ordinal.lsub_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              Ordinal.lsub (o.familyOfBFamily f) = o.blsub f
                              @[simp]
                              theorem Ordinal.blsub_eq_lsub' {ι : Type u} (r : ιιProp) [IsWellOrder ι r] (f : ιOrdinal.{max u v} ) :
                              theorem Ordinal.blsub_eq_blsub {ι : Type u} (r : ιιProp) (r' : ιιProp) [IsWellOrder ι r] [IsWellOrder ι r'] (f : ιOrdinal.{max u v} ) :
                              @[simp]
                              theorem Ordinal.blsub_eq_lsub {ι : Type u} (f : ιOrdinal.{max u v} ) :
                              (Ordinal.type WellOrderingRel).blsub (Ordinal.bfamilyOfFamily f) = Ordinal.lsub f
                              theorem Ordinal.blsub_congr {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁Ordinal.{max u v} ) (ho : o₁ = o₂) :
                              o₁.blsub f = o₂.blsub fun (a : Ordinal.{u}) (h : a < o₂) => f a
                              theorem Ordinal.blsub_le_iff {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                              o.blsub f a ∀ (i : Ordinal.{u}) (h : i < o), f i h < a
                              theorem Ordinal.blsub_le {o : Ordinal.{u_4}} {f : (b : Ordinal.{u_4}) → b < oOrdinal.{max u_4 u_5} } {a : Ordinal.{max u_4 u_5} } :
                              (∀ (i : Ordinal.{u_4}) (h : i < o), f i h < a)o.blsub f a
                              theorem Ordinal.lt_blsub {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_5 u_4} ) (i : Ordinal.{u_4}) (h : i < o) :
                              f i h < o.blsub f
                              theorem Ordinal.lt_blsub_iff {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{max u v} } {a : Ordinal.{max u v} } :
                              a < o.blsub f ∃ (i : Ordinal.{u}) (hi : i < o), a f i hi
                              theorem Ordinal.bsup_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              o.bsup f o.blsub f
                              theorem Ordinal.blsub_le_bsup_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              o.blsub f Order.succ (o.bsup f)
                              theorem Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              o.bsup f = o.blsub f Order.succ (o.bsup f) = o.blsub f
                              theorem Ordinal.bsup_succ_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              Order.succ (o.bsup f) o.blsub f ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f
                              theorem Ordinal.bsup_succ_eq_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              Order.succ (o.bsup f) = o.blsub f ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o.bsup f
                              theorem Ordinal.bsup_eq_blsub_iff_succ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              o.bsup f = o.blsub f a < o.blsub f, Order.succ a < o.blsub f
                              theorem Ordinal.bsup_eq_blsub_iff_lt_bsup {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                              o.bsup f = o.blsub f ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < o.bsup f
                              theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit {o : Ordinal.{u}} (ho : o.IsLimit) {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } (hf : ∀ (a : Ordinal.{u}) (ha : a < o), f a ha < f (Order.succ a) ) :
                              o.bsup f = o.blsub f
                              theorem Ordinal.blsub_succ_of_mono {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < Order.succ oOrdinal.{max u v} } (hf : ∀ {i j : Ordinal.{u}} (hi : i < Order.succ o) (hj : j < Order.succ o), i jf i hi f j hj) :
                              (Order.succ o).blsub f = Order.succ (f o )
                              @[simp]
                              theorem Ordinal.blsub_eq_zero_iff {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_5 u_4} } :
                              o.blsub f = 0 o = 0
                              @[simp]
                              theorem Ordinal.blsub_zero (f : (a : Ordinal.{u_4}) → a < 0Ordinal.{max u_4 u_5} ) :
                              theorem Ordinal.blsub_pos {o : Ordinal.{u_4}} (ho : 0 < o) (f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_4 u_5} ) :
                              0 < o.blsub f
                              theorem Ordinal.blsub_type {α : Type u} (r : ααProp) [IsWellOrder α r] (f : (a : Ordinal.{u}) → a < Ordinal.type rOrdinal.{max u v} ) :
                              (Ordinal.type r).blsub f = Ordinal.lsub fun (a : α) => f (Ordinal.typein r a)
                              theorem Ordinal.blsub_const {o : Ordinal.{u}} (ho : o 0) (a : Ordinal.{max u v} ) :
                              (o.blsub fun (x : Ordinal.{u}) (x : x < o) => a) = Order.succ a
                              @[simp]
                              theorem Ordinal.blsub_one (f : (a : Ordinal.{u_4}) → a < 1Ordinal.{max u_4 u_5} ) :
                              Ordinal.blsub 1 f = Order.succ (f 0 )
                              @[simp]
                              theorem Ordinal.blsub_id (o : Ordinal.{u}) :
                              (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o
                              theorem Ordinal.bsup_id_limit {o : Ordinal.{u}} :
                              (∀ a < o, Order.succ a < o)(o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => x) = o
                              @[simp]
                              theorem Ordinal.bsup_id_succ (o : Ordinal.{u}) :
                              ((Order.succ o).bsup fun (x : Ordinal.{u}) (x_1 : x < Order.succ o) => x) = o
                              theorem Ordinal.blsub_le_of_brange_subset {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o'Ordinal.{max (max u v) w} } (h : o.brange f o'.brange g) :
                              o.blsub f o'.blsub g
                              theorem Ordinal.blsub_eq_of_brange_eq {o : Ordinal.{u}} {o' : Ordinal.{v}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max (max u v) w} } {g : (a : Ordinal.{v}) → a < o'Ordinal.{max (max u v) w} } (h : {o_1 : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{u}) (hi : i < o), f i hi = o_1} = {o : Ordinal.{max (max u v) w} | ∃ (i : Ordinal.{v}) (hi : i < o'), g i hi = o}) :
                              o.blsub f = o'.blsub g
                              theorem Ordinal.bsup_comp {o : Ordinal.{max u v} } {o' : Ordinal.{max u v} } {f : (a : Ordinal.{max u v} ) → a < oOrdinal.{max u v w} } (hf : ∀ {i j : Ordinal.{max u v} } (hi : i < o) (hj : j < o), i jf i hi f j hj) {g : (a : Ordinal.{max u v} ) → a < o'Ordinal.{max u v} } (hg : o'.blsub g = o) :
                              (o'.bsup fun (a : Ordinal.{max u v} ) (ha : a < o') => f (g a ha) ) = o.bsup f
                              theorem Ordinal.blsub_comp {o : Ordinal.{max u v} } {o' : Ordinal.{max u v} } {f : (a : Ordinal.{max u v} ) → a < oOrdinal.{max u v w} } (hf : ∀ {i j : Ordinal.{max u v} } (hi : i < o) (hj : j < o), i jf i hi f j hj) {g : (a : Ordinal.{max u v} ) → a < o'Ordinal.{max u v} } (hg : o'.blsub g = o) :
                              (o'.blsub fun (a : Ordinal.{max u v} ) (ha : a < o') => f (g a ha) ) = o.blsub f
                              theorem Ordinal.IsNormal.bsup_eq {f : Ordinal.{u}Ordinal.{max u v} } (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (h : o.IsLimit) :
                              (o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
                              theorem Ordinal.IsNormal.blsub_eq {f : Ordinal.{u}Ordinal.{max u v} } (H : Ordinal.IsNormal f) {o : Ordinal.{u}} (h : o.IsLimit) :
                              (o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
                              theorem Ordinal.isNormal_iff_lt_succ_and_bsup_eq {f : Ordinal.{u}Ordinal.{max u v} } :
                              Ordinal.IsNormal f (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∀ (o : Ordinal.{u}), o.IsLimit(o.bsup fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
                              theorem Ordinal.isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u}Ordinal.{max u v} } :
                              Ordinal.IsNormal f (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∀ (o : Ordinal.{u}), o.IsLimit(o.blsub fun (x : Ordinal.{u}) (x_1 : x < o) => f x) = f o
                              theorem Ordinal.IsNormal.eq_iff_zero_and_succ {f : Ordinal.{u}Ordinal.{u}} {g : Ordinal.{u}Ordinal.{u}} (hf : Ordinal.IsNormal f) (hg : Ordinal.IsNormal g) :
                              f = g f 0 = g 0 ∀ (a : Ordinal.{u}), f a = g af (Order.succ a) = g (Order.succ a)

                              A two-argument version of Ordinal.blsub. We don't develop a full API for this, since it's only used in a handful of existence results.

                              Equations
                              • o₁.blsub₂ o₂ op = Ordinal.lsub fun (x : o₁.toType × o₂.toType) => op
                              Instances For
                                theorem Ordinal.lt_blsub₂ {o₁ : Ordinal.{u_4}} {o₂ : Ordinal.{u_5}} (op : {a : Ordinal.{u_4}} → a < o₁{b : Ordinal.{u_5}} → b < o₂Ordinal.{max (max u_4 u_5) u_6} ) {a : Ordinal.{u_4}} {b : Ordinal.{u_5}} (ha : a < o₁) (hb : b < o₂) :
                                op ha hb < o₁.blsub₂ o₂ fun {a : Ordinal.{u_4}} => op

                                Minimum excluded ordinals #

                                The minimum excluded ordinal in a family of ordinals.

                                Equations
                                Instances For
                                  theorem Ordinal.le_mex_of_forall {ι : Type u} {f : ιOrdinal.{max u v} } {a : Ordinal.{max u v} } (H : b < a, ∃ (i : ι), f i = b) :
                                  theorem Ordinal.ne_mex {ι : Type u} (f : ιOrdinal.{max u v} ) (i : ι) :
                                  theorem Ordinal.mex_le_of_ne {ι : Type u_4} {f : ιOrdinal.{max u_5 u_4} } {a : Ordinal.{max u_5 u_4} } (ha : ∀ (i : ι), f i a) :
                                  theorem Ordinal.exists_of_lt_mex {ι : Type u_4} {f : ιOrdinal.{max u_5 u_4} } {a : Ordinal.{max u_4 u_5} } (ha : a < Ordinal.mex f) :
                                  ∃ (i : ι), f i = a
                                  theorem Ordinal.mex_monotone {α : Type u} {β : Type u} {f : αOrdinal.{max u v} } {g : βOrdinal.{max u v} } (h : Set.range f Set.range g) :

                                  The minimum excluded ordinal of a family of ordinals indexed by the set of ordinals less than some o : Ordinal.{u}. This is a special case of mex over the family provided by familyOfBFamily.

                                  This is to mex as bsup is to sup.

                                  Equations
                                  Instances For
                                    theorem Ordinal.bmex_not_mem_brange {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_4 u_5} ) :
                                    o.bmex fo.brange f
                                    theorem Ordinal.le_bmex_of_forall {o : Ordinal.{u_4}} (f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_4 u_5} ) {a : Ordinal.{max u_4 u_5} } (H : b < a, ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = b) :
                                    a o.bmex f
                                    theorem Ordinal.ne_bmex {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) {i : Ordinal.{u}} (hi : i < o) :
                                    f i hi o.bmex f
                                    theorem Ordinal.bmex_le_of_ne {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_4 u_5} } {a : Ordinal.{max u_4 u_5} } (ha : ∀ (i : Ordinal.{u_4}) (hi : i < o), f i hi a) :
                                    o.bmex f a
                                    theorem Ordinal.exists_of_lt_bmex {o : Ordinal.{u_4}} {f : (a : Ordinal.{u_4}) → a < oOrdinal.{max u_4 u_5} } {a : Ordinal.{max u_5 u_4} } (ha : a < o.bmex f) :
                                    ∃ (i : Ordinal.{u_4}) (hi : i < o), f i hi = a
                                    theorem Ordinal.bmex_le_blsub {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} ) :
                                    o.bmex f o.blsub f
                                    theorem Ordinal.bmex_monotone {o : Ordinal.{u}} {o' : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {g : (a : Ordinal.{u}) → a < o'Ordinal.{max u v} } (h : o.brange f o'.brange g) :
                                    o.bmex f o'.bmex g
                                    theorem Ordinal.bmex_lt_ord_succ_card {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < oOrdinal.{u}) :
                                    o.bmex f < (Order.succ o.card).ord

                                    Results about injectivity and surjectivity #

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

                                    Enumerating unbounded sets of ordinals with ordinals #

                                    Enumerator function for an unbounded set of ordinals.

                                    Equations
                                    Instances For
                                      theorem Ordinal.enumOrd_def' {S : Set Ordinal.{u}} (o : Ordinal.{u}) :
                                      Ordinal.enumOrd S o = sInf (S Set.Ici (o.blsub fun (a : Ordinal.{u}) (x : a < o) => Ordinal.enumOrd S a))

                                      The equation that characterizes enumOrd definitionally. This isn't the nicest expression to work with, so consider using enumOrd_def instead.

                                      theorem Ordinal.enumOrd_def'_nonempty {S : Set Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) (a : Ordinal.{u}) :
                                      (S Set.Ici a).Nonempty

                                      The set in enumOrd_def' is nonempty.

                                      theorem Ordinal.enumOrd_mem {S : Set Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) (o : Ordinal.{u}) :
                                      theorem Ordinal.blsub_le_enumOrd {S : Set Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) (o : Ordinal.{u}) :
                                      (o.blsub fun (c : Ordinal.{u}) (x : c < o) => Ordinal.enumOrd S c) Ordinal.enumOrd S o
                                      theorem Ordinal.enumOrd_def {S : Set Ordinal.{u}} (o : Ordinal.{u}) :
                                      Ordinal.enumOrd S o = sInf (S {b : Ordinal.{u} | c < o, Ordinal.enumOrd S c < b})

                                      A more workable definition for enumOrd.

                                      theorem Ordinal.enumOrd_def_nonempty {S : Set Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) {o : Ordinal.{u}} :
                                      {x : Ordinal.{u} | x S c < o, Ordinal.enumOrd S c < x}.Nonempty

                                      The set in enumOrd_def is nonempty.

                                      @[simp]
                                      theorem Ordinal.enumOrd_succ_le {S : Set Ordinal.{u}} {a : Ordinal.{u}} {b : Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) (ha : a S) (hb : Ordinal.enumOrd S b < a) :
                                      theorem Ordinal.enumOrd_surjective {S : Set Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) (s : Ordinal.{u}) :
                                      s S∃ (a : Ordinal.{u}), Ordinal.enumOrd S a = s
                                      def Ordinal.enumOrdOrderIso {S : Set Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) :

                                      An order isomorphism between an unbounded set of ordinals and the ordinals.

                                      Equations
                                      Instances For
                                        theorem Ordinal.range_enumOrd {S : Set Ordinal.{u}} (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) :
                                        theorem Ordinal.eq_enumOrd {S : Set Ordinal.{u}} (f : Ordinal.{u}Ordinal.{u}) (hS : Set.Unbounded (fun (x1 x2 : Ordinal.{u}) => x1 < x2) S) :

                                        A characterization of enumOrd: it is the unique strict monotonic function with range S.

                                        Casting naturals into ordinals, compatibility with operations #

                                        @[simp]
                                        theorem Ordinal.one_add_natCast (m : ) :
                                        1 + m = (Order.succ m)
                                        @[deprecated Ordinal.one_add_natCast]
                                        theorem Ordinal.one_add_nat_cast (m : ) :
                                        1 + m = (Order.succ m)

                                        Alias of Ordinal.one_add_natCast.

                                        @[simp]
                                        theorem Ordinal.one_add_ofNat (m : ) [m.AtLeastTwo] :
                                        @[simp]
                                        theorem Ordinal.natCast_mul (m : ) (n : ) :
                                        (m * n) = m * n
                                        @[deprecated Ordinal.natCast_mul]
                                        theorem Ordinal.nat_cast_mul (m : ) (n : ) :
                                        (m * n) = m * n

                                        Alias of Ordinal.natCast_mul.

                                        theorem Ordinal.natCast_le {m : } {n : } :
                                        m n m n

                                        Alias of Nat.cast_le, specialized to Ordinal -

                                        @[deprecated Ordinal.natCast_le]
                                        theorem Ordinal.nat_cast_le {m : } {n : } :
                                        m n m n

                                        Alias of Ordinal.natCast_le.


                                        Alias of Nat.cast_le, specialized to Ordinal -

                                        theorem Ordinal.natCast_inj {m : } {n : } :
                                        m = n m = n

                                        Alias of Nat.cast_inj, specialized to Ordinal -

                                        @[deprecated Ordinal.natCast_inj]
                                        theorem Ordinal.nat_cast_inj {m : } {n : } :
                                        m = n m = n

                                        Alias of Ordinal.natCast_inj.


                                        Alias of Nat.cast_inj, specialized to Ordinal -

                                        theorem Ordinal.natCast_lt {m : } {n : } :
                                        m < n m < n

                                        Alias of Nat.cast_lt, specialized to Ordinal -

                                        @[deprecated Ordinal.natCast_lt]
                                        theorem Ordinal.nat_cast_lt {m : } {n : } :
                                        m < n m < n

                                        Alias of Ordinal.natCast_lt.


                                        Alias of Nat.cast_lt, specialized to Ordinal -

                                        theorem Ordinal.natCast_eq_zero {n : } :
                                        n = 0 n = 0

                                        Alias of Nat.cast_eq_zero, specialized to Ordinal -

                                        @[deprecated Ordinal.natCast_eq_zero]
                                        theorem Ordinal.nat_cast_eq_zero {n : } :
                                        n = 0 n = 0

                                        Alias of Ordinal.natCast_eq_zero.


                                        Alias of Nat.cast_eq_zero, specialized to Ordinal -

                                        theorem Ordinal.natCast_ne_zero {n : } :
                                        n 0 n 0

                                        Alias of Nat.cast_eq_zero, specialized to Ordinal -

                                        @[deprecated Ordinal.natCast_ne_zero]
                                        theorem Ordinal.nat_cast_ne_zero {n : } :
                                        n 0 n 0

                                        Alias of Ordinal.natCast_ne_zero.


                                        Alias of Nat.cast_eq_zero, specialized to Ordinal -

                                        theorem Ordinal.natCast_pos {n : } :
                                        0 < n 0 < n

                                        Alias of Nat.cast_pos', specialized to Ordinal -

                                        @[deprecated Ordinal.natCast_pos]
                                        theorem Ordinal.nat_cast_pos {n : } :
                                        0 < n 0 < n

                                        Alias of Ordinal.natCast_pos.


                                        Alias of Nat.cast_pos', specialized to Ordinal -

                                        @[simp]
                                        theorem Ordinal.natCast_sub (m : ) (n : ) :
                                        (m - n) = m - n
                                        @[deprecated Ordinal.natCast_sub]
                                        theorem Ordinal.nat_cast_sub (m : ) (n : ) :
                                        (m - n) = m - n

                                        Alias of Ordinal.natCast_sub.

                                        @[simp]
                                        theorem Ordinal.natCast_div (m : ) (n : ) :
                                        (m / n) = m / n
                                        @[deprecated Ordinal.natCast_div]
                                        theorem Ordinal.nat_cast_div (m : ) (n : ) :
                                        (m / n) = m / n

                                        Alias of Ordinal.natCast_div.

                                        @[simp]
                                        theorem Ordinal.natCast_mod (m : ) (n : ) :
                                        (m % n) = m % n
                                        @[deprecated Ordinal.natCast_mod]
                                        theorem Ordinal.nat_cast_mod (m : ) (n : ) :
                                        (m % n) = m % n

                                        Alias of Ordinal.natCast_mod.

                                        @[simp]
                                        @[deprecated Ordinal.lift_natCast]

                                        Alias of Ordinal.lift_natCast.

                                        @[simp]

                                        Properties of ω #

                                        theorem Ordinal.lt_add_of_limit {a : Ordinal.{u}} {b : Ordinal.{u}} {c : Ordinal.{u}} (h : c.IsLimit) :
                                        a < b + c c' < c, a < b + c'
                                        theorem Ordinal.lt_omega0 {o : Ordinal.{u_1}} :
                                        o < Ordinal.omega0 ∃ (n : ), o = n
                                        @[deprecated Ordinal.lt_omega0]
                                        theorem Ordinal.lt_omega {o : Ordinal.{u_1}} :
                                        o < Ordinal.omega0 ∃ (n : ), o = n

                                        Alias of Ordinal.lt_omega0.

                                        @[deprecated Ordinal.nat_lt_omega0]

                                        Alias of Ordinal.nat_lt_omega0.

                                        @[deprecated]
                                        @[deprecated Ordinal.omega0_ne_zero]

                                        Alias of Ordinal.omega0_ne_zero.

                                        @[deprecated Ordinal.one_lt_omega0]

                                        Alias of Ordinal.one_lt_omega0.

                                        @[deprecated Ordinal.omega0_isLimit]

                                        Alias of Ordinal.omega0_isLimit.

                                        @[deprecated Ordinal.omega0_le]
                                        theorem Ordinal.omega_le {o : Ordinal.{u_1}} :
                                        Ordinal.omega0 o ∀ (n : ), n o

                                        Alias of Ordinal.omega0_le.

                                        @[deprecated Ordinal.iSup_natCast]
                                        @[deprecated Ordinal.sup_natCast]

                                        Alias of Ordinal.sup_natCast.

                                        theorem Ordinal.nat_lt_limit {o : Ordinal.{u_1}} (h : o.IsLimit) (n : ) :
                                        n < o
                                        @[deprecated Ordinal.omega0_le_of_isLimit]

                                        Alias of Ordinal.omega0_le_of_isLimit.

                                        @[deprecated Ordinal.isLimit_iff_omega0_dvd]

                                        Alias of Ordinal.isLimit_iff_omega0_dvd.

                                        theorem Ordinal.add_mul_limit_aux {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (ba : b + a = a) (l : c.IsLimit) (IH : c' < c, (a + b) * Order.succ c' = a * Order.succ c' + b) :
                                        (a + b) * c = a * c
                                        theorem Ordinal.add_mul_succ {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} (c : Ordinal.{u_1}) (ba : b + a = a) :
                                        (a + b) * Order.succ c = a * Order.succ c + b
                                        theorem Ordinal.add_mul_limit {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (ba : b + a = a) (l : c.IsLimit) :
                                        (a + b) * c = a * c
                                        theorem Ordinal.add_le_of_forall_add_lt {a : Ordinal.{u_1}} {b : Ordinal.{u_1}} {c : Ordinal.{u_1}} (hb : 0 < b) (h : d < b, a + d < c) :
                                        a + b c
                                        @[deprecated Ordinal.IsNormal.apply_omega0]

                                        Alias of Ordinal.IsNormal.apply_omega0.

                                        @[simp]
                                        theorem Ordinal.iSup_add_nat (o : Ordinal.{u_1}) :
                                        ⨆ (n : ), o + n = o + Ordinal.omega0
                                        @[deprecated Ordinal.iSup_add_nat]
                                        theorem Ordinal.sup_add_nat (o : Ordinal.{u_1}) :
                                        (Ordinal.sup fun (n : ) => o + n) = o + Ordinal.omega0
                                        @[simp]
                                        theorem Ordinal.iSup_mul_nat (o : Ordinal.{u_1}) :
                                        ⨆ (n : ), o * n = o * Ordinal.omega0
                                        @[deprecated Ordinal.iSup_add_nat]
                                        theorem Ordinal.sup_mul_nat (o : Ordinal.{u_1}) :
                                        (Ordinal.sup fun (n : ) => o * n) = o * Ordinal.omega0
                                        noncomputable def Acc.rank {α : Type u} {r : ααProp} {a : α} (h : Acc r a) :

                                        The rank of an element a accessible under a relation r is defined inductively as the smallest ordinal greater than the ranks of all elements below it (i.e. elements b such that r b a).

                                        Equations
                                        Instances For
                                          theorem Acc.rank_eq {α : Type u} {r : ααProp} {a : α} (h : Acc r a) :
                                          h.rank = ⨆ (b : { b : α // r b a }), Order.succ .rank
                                          theorem Acc.rank_lt_of_rel {α : Type u} {r : ααProp} {a : α} {b : α} (hb : Acc r b) (h : r a b) :
                                          .rank < hb.rank

                                          if r a b then the rank of a is less than the rank of b.

                                          noncomputable def WellFounded.rank {α : Type u} {r : ααProp} (hwf : WellFounded r) (a : α) :

                                          The rank of an element a under a well-founded relation r is defined inductively as the smallest ordinal greater than the ranks of all elements below it (i.e. elements b such that r b a).

                                          Equations
                                          • hwf.rank a = .rank
                                          Instances For
                                            theorem WellFounded.rank_eq {α : Type u} {r : ααProp} {a : α} (hwf : WellFounded r) :
                                            hwf.rank a = ⨆ (b : { b : α // r b a }), Order.succ (hwf.rank b)
                                            theorem WellFounded.rank_lt_of_rel {α : Type u} {r : ααProp} {a : α} {b : α} (hwf : WellFounded r) (h : r a b) :
                                            hwf.rank a < hwf.rank b