Documentation

Mathlib.SetTheory.Ordinal.Basic

Ordinals #

Ordinals are defined as equivalences of well-ordered sets under order isomorphism. They are endowed with a total order, where an ordinal is smaller than another one if it embeds into it as an initial segment (or, equivalently, in any way). This total order is well founded.

Main definitions #

A conditionally complete linear order with bot structure is registered on ordinals, where is 0, the ordinal corresponding to the empty type, and Inf is the minimum for nonempty sets and 0 for the empty set by convention.

Notations #

Well order on an arbitrary type #

An embedding of any type to the set of cardinals.

Equations
Instances For
    def WellOrderingRel {σ : Type u} :
    σσProp

    Any type can be endowed with a well order, obtained by pulling back the well order over cardinals by some embedding.

    Equations
    Instances For
      instance WellOrderingRel.isWellOrder {σ : Type u} :
      IsWellOrder σ WellOrderingRel
      Equations
      • =
      instance IsWellOrder.subtype_nonempty {σ : Type u} :
      Nonempty { r : σσProp // IsWellOrder σ r }
      Equations
      • =

      Definition of ordinals #

      structure WellOrder :
      Type (u + 1)

      Bundled structure registering a well order on a type. Ordinals will be defined as a quotient of this type.

      • α : Type u

        The underlying type of the order.

      • r : selfselfProp

        The underlying relation of the order.

      • wo : IsWellOrder self self.r

        The proposition that r is a well-ordering for α.

      Instances For
        theorem WellOrder.wo (self : WellOrder) :
        IsWellOrder self self.r

        The proposition that r is a well-ordering for α.

        Equations
        @[simp]
        theorem WellOrder.eta (o : WellOrder) :
        { α := o, r := o.r, wo := } = o

        Equivalence relation on well orders on arbitrary types in universe u, given by order isomorphism.

        Equations
        • One or more equations did not get rendered due to their size.
        def Ordinal :
        Type (u + 1)

        Ordinal.{u} is the type of well orders in Type u, up to order isomorphism.

        Equations
        Instances For
          Equations
          instance isWellOrder_out_lt (o : Ordinal.{u_3}) :
          IsWellOrder (Quotient.out o) fun (x x_1 : (Quotient.out o)) => x < x_1
          Equations
          • =

          Basic properties of the order type #

          def Ordinal.type {α : Type u} (r : ααProp) [wo : IsWellOrder α r] :

          The order type of a well order is an ordinal.

          Equations
          Instances For
            Equations
            Equations
            def Ordinal.typein {α : Type u} (r : ααProp) [IsWellOrder α r] (a : α) :

            The order type of an element inside a well order. For the embedding as a principal segment, see typein.principalSeg.

            Equations
            Instances For
              @[simp]
              theorem Ordinal.type_def' (w : WellOrder) :
              w = Ordinal.type w.r
              @[simp]
              theorem Ordinal.type_def {α : Type u} (r : ααProp) [wo : IsWellOrder α r] :
              { α := α, r := r, wo := wo } = Ordinal.type r
              theorem Ordinal.type_eq {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
              theorem RelIso.ordinal_type_eq {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (h : r ≃r s) :
              @[simp]
              theorem Ordinal.type_lt (o : Ordinal.{u_3}) :
              (Ordinal.type fun (x x_1 : (Quotient.out o)) => x < x_1) = o
              theorem Ordinal.type_eq_zero_of_empty {α : Type u} (r : ααProp) [IsWellOrder α r] [IsEmpty α] :
              @[simp]
              theorem Ordinal.type_eq_zero_iff_isEmpty {α : Type u} {r : ααProp} [IsWellOrder α r] :
              theorem Ordinal.type_ne_zero_iff_nonempty {α : Type u} {r : ααProp} [IsWellOrder α r] :
              theorem Ordinal.type_ne_zero_of_nonempty {α : Type u} (r : ααProp) [IsWellOrder α r] [h : Nonempty α] :
              theorem Ordinal.type_pEmpty :
              Ordinal.type EmptyRelation = 0
              theorem Ordinal.type_empty :
              Ordinal.type EmptyRelation = 0
              theorem Ordinal.type_eq_one_of_unique {α : Type u} (r : ααProp) [IsWellOrder α r] [Unique α] :
              @[simp]
              theorem Ordinal.type_eq_one_iff_unique {α : Type u} {r : ααProp} [IsWellOrder α r] :
              theorem Ordinal.type_pUnit :
              Ordinal.type EmptyRelation = 1
              theorem Ordinal.type_unit :
              Ordinal.type EmptyRelation = 1
              theorem Ordinal.type_preimage {α : Type u} {β : Type u} (r : ααProp) [IsWellOrder α r] (f : β α) :
              @[simp]
              theorem Ordinal.type_preimage_aux {α : Type u} {β : Type u} (r : ααProp) [IsWellOrder α r] (f : β α) :
              (Ordinal.type fun (x y : β) => r (f x) (f y)) = Ordinal.type r
              theorem Ordinal.inductionOn {C : Ordinal.{u_3}Prop} (o : Ordinal.{u_3}) (H : ∀ (α : Type u_3) (r : ααProp) [inst : IsWellOrder α r], C (Ordinal.type r)) :
              C o

              The order on ordinals #

              For Ordinal:

              • less-equal is defined such that well orders r and s satisfy type rtype s if there exists a function embedding r as an initial segment of s.

              • less-than is defined such that well orders r and s satisfy type r < type s if there exists a function embedding r as a principal segment of s.

              Equations
              theorem Ordinal.type_le_iff {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
              theorem Ordinal.type_le_iff' {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
              theorem InitialSeg.ordinal_type_le {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (h : r ≼i s) :
              theorem RelEmbedding.ordinal_type_le {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (h : r ↪r s) :
              @[simp]
              theorem Ordinal.type_lt_iff {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
              theorem PrincipalSeg.ordinal_type_lt {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (h : r ≺i s) :
              @[simp]
              theorem Ordinal.zero_le (o : Ordinal.{u_3}) :
              0 o
              @[simp]
              @[simp]
              theorem Ordinal.le_zero {o : Ordinal.{u_3}} :
              o 0 o = 0
              def Ordinal.initialSegOut {α : Ordinal.{u_3}} {β : Ordinal.{u_3}} (h : α β) :
              (fun (x x_1 : (Quotient.out α)) => x < x_1) ≼i fun (x x_1 : (Quotient.out β)) => x < x_1

              Given two ordinals α ≤ β, then initialSegOut α β is the initial segment embedding of α to β, as map from a model type for α to a model type for β.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Ordinal.principalSegOut {α : Ordinal.{u_3}} {β : Ordinal.{u_3}} (h : α < β) :
                (fun (x x_1 : (Quotient.out α)) => x < x_1) ≺i fun (x x_1 : (Quotient.out β)) => x < x_1

                Given two ordinals α < β, then principalSegOut α β is the principal segment embedding of α to β, as map from a model type for α to a model type for β.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Ordinal.typein_lt_type {α : Type u} (r : ααProp) [IsWellOrder α r] (a : α) :
                  theorem Ordinal.typein_lt_self {o : Ordinal.{u_3}} (i : (Quotient.out o)) :
                  Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) i < o
                  @[simp]
                  theorem Ordinal.typein_top {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (f : r ≺i s) :
                  @[simp]
                  theorem Ordinal.typein_apply {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (f : r ≼i s) (a : α) :
                  @[simp]
                  theorem Ordinal.typein_lt_typein {α : Type u} (r : ααProp) [IsWellOrder α r] {a : α} {b : α} :
                  theorem Ordinal.typein_surj {α : Type u} (r : ααProp) [IsWellOrder α r] {o : Ordinal.{u}} (h : o < Ordinal.type r) :
                  ∃ (a : α), Ordinal.typein r a = o
                  theorem Ordinal.typein_injective {α : Type u} (r : ααProp) [IsWellOrder α r] :
                  @[simp]
                  theorem Ordinal.typein_inj {α : Type u} (r : ααProp) [IsWellOrder α r] {a : α} {b : α} :
                  def Ordinal.typein.principalSeg {α : Type u} (r : ααProp) [IsWellOrder α r] :
                  r ≺i fun (x x_1 : Ordinal.{u}) => x < x_1

                  Principal segment version of the typein function, embedding a well order into ordinals as a principal segment.

                  Equations
                  Instances For
                    @[simp]
                    theorem Ordinal.typein.principalSeg_coe {α : Type u} (r : ααProp) [IsWellOrder α r] :

                    Enumerating elements in a well-order with ordinals. #

                    def Ordinal.enum {α : Type u} (r : ααProp) [IsWellOrder α r] (o : Ordinal.{u}) (h : o < Ordinal.type r) :
                    α

                    enum r o h is the o-th element of α ordered by r. That is, enum maps an initial segment of the ordinals, those less than the order type of r, to the elements of α.

                    Equations
                    Instances For
                      @[simp]
                      theorem Ordinal.typein_enum {α : Type u} (r : ααProp) [IsWellOrder α r] {o : Ordinal.{u}} (h : o < Ordinal.type r) :
                      theorem Ordinal.enum_type {α : Type u_3} {β : Type u_3} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (f : s ≺i r) {h : Ordinal.type s < Ordinal.type r} :
                      @[simp]
                      theorem Ordinal.enum_typein {α : Type u} (r : ααProp) [IsWellOrder α r] (a : α) :
                      theorem Ordinal.enum_lt_enum {α : Type u} {r : ααProp} [IsWellOrder α r] {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h₁ : o₁ < Ordinal.type r) (h₂ : o₂ < Ordinal.type r) :
                      r (Ordinal.enum r o₁ h₁) (Ordinal.enum r o₂ h₂) o₁ < o₂
                      theorem Ordinal.relIso_enum' {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < Ordinal.type r) (hs : o < Ordinal.type s) :
                      f (Ordinal.enum r o hr) = Ordinal.enum s o hs
                      theorem Ordinal.relIso_enum {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) (o : Ordinal.{u}) (hr : o < Ordinal.type r) :
                      f (Ordinal.enum r o hr) = Ordinal.enum s o
                      theorem Ordinal.lt_wf :
                      WellFounded fun (x x_1 : Ordinal.{u_3}) => x < x_1
                      theorem Ordinal.induction {p : Ordinal.{u}Prop} (i : Ordinal.{u}) (h : ∀ (j : Ordinal.{u}), (k < j, p k)p j) :
                      p i

                      Reformulation of well founded induction on ordinals as a lemma that works with the induction tactic, as in induction i using Ordinal.induction with | h i IH => ?_.

                      Cardinality of ordinals #

                      The cardinal of an ordinal is the cardinality of any type on which a relation with that order type is defined.

                      Equations
                      Instances For
                        @[simp]
                        theorem Ordinal.card_type {α : Type u} (r : ααProp) [IsWellOrder α r] :
                        @[simp]
                        theorem Ordinal.card_typein {α : Type u} {r : ααProp} [IsWellOrder α r] (x : α) :
                        Cardinal.mk { y : α // r y x } = (Ordinal.typein r x).card
                        theorem Ordinal.card_le_card {o₁ : Ordinal.{u_3}} {o₂ : Ordinal.{u_3}} :
                        o₁ o₂o₁.card o₂.card

                        Lifting ordinals to a higher universe #

                        The universe lift operation for ordinals, which embeds Ordinal.{u} as a proper initial segment of Ordinal.{v} for v > u. For the initial segment version, see lift.initialSeg.

                        Equations
                        Instances For
                          theorem Ordinal.type_uLift {α : Type u} (r : ααProp) [IsWellOrder α r] :
                          @[simp]
                          theorem Ordinal.type_uLift_aux {α : Type u} (r : ααProp) [IsWellOrder α r] :
                          (Ordinal.type fun (x y : ULift.{v, u} α) => r x.down y.down) = Ordinal.lift.{v, u} (Ordinal.type r)
                          theorem RelIso.ordinal_lift_type_eq {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) :
                          theorem Ordinal.type_lift_preimage {α : Type u} {β : Type v} (r : ααProp) [IsWellOrder α r] (f : β α) :
                          @[simp]
                          theorem Ordinal.type_lift_preimage_aux {α : Type u} {β : Type v} (r : ααProp) [IsWellOrder α r] (f : β α) :
                          Ordinal.lift.{u, v} (Ordinal.type fun (x y : β) => r (f x) (f y)) = Ordinal.lift.{v, u} (Ordinal.type r)

                          lift.{max u v, u} equals lift.{v, u}.

                          lift.{max v u, u} equals lift.{v, u}.

                          An ordinal lifted to a lower or equal universe equals itself.

                          @[simp]

                          An ordinal lifted to the same universe equals itself.

                          @[simp]

                          An ordinal lifted to the zero universe equals itself.

                          theorem Ordinal.lift_type_le {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
                          theorem Ordinal.lift_type_eq {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
                          theorem Ordinal.lift_type_lt {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
                          def Ordinal.lift.initialSeg :
                          (fun (x x_1 : Ordinal.{u}) => x < x_1) ≼i fun (x x_1 : Ordinal.{max u v} ) => x < x_1

                          Initial segment version of the lift operation on ordinals, embedding ordinal.{u} in ordinal.{v} as an initial segment when u ≤ v.

                          Equations
                          Instances For

                            The first infinite ordinal omega #

                            ω is the first infinite ordinal, defined as the order type of .

                            Equations
                            Instances For

                              ω is the first infinite ordinal, defined as the order type of .

                              Equations
                              Instances For
                                @[simp]
                                theorem Ordinal.type_nat_lt :
                                (Ordinal.type fun (x x_1 : ) => x < x_1) = Ordinal.omega

                                Note that the presence of this lemma makes simp [omega] form a loop.

                                Definition and first properties of addition on ordinals #

                                In this paragraph, we introduce the addition on ordinals, and prove just enough properties to deduce that the order on ordinals is total (and therefore well-founded). Further properties of the addition, together with properties of the other operations, are proved in Mathlib/SetTheory/Ordinal/Arithmetic.lean.

                                o₁ + o₂ is the order on the disjoint union of o₁ and o₂ obtained by declaring that every element of o₁ is smaller than every element of o₂.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem Ordinal.card_add (o₁ : Ordinal.{u_3}) (o₂ : Ordinal.{u_3}) :
                                (o₁ + o₂).card = o₁.card + o₂.card
                                @[simp]
                                theorem Ordinal.type_sum_lex {α : Type u} {β : Type u} (r : ααProp) (s : ββProp) [IsWellOrder α r] [IsWellOrder β s] :
                                @[simp]
                                theorem Ordinal.card_nat (n : ) :
                                (n).card = n
                                @[simp]
                                theorem Ordinal.card_ofNat (n : ) [n.AtLeastTwo] :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem Ordinal.max_eq_zero {a : Ordinal.{u_3}} {b : Ordinal.{u_3}} :
                                max a b = 0 a = 0 b = 0
                                @[simp]

                                Successor order properties #

                                @[simp]
                                @[simp]
                                theorem Ordinal.add_succ (o₁ : Ordinal.{u_3}) (o₂ : Ordinal.{u_3}) :
                                o₁ + Order.succ o₂ = Order.succ (o₁ + o₂)
                                @[simp]
                                theorem Ordinal.le_one_iff {a : Ordinal.{u_3}} :
                                a 1 a = 0 a = 1
                                @[simp]
                                theorem Ordinal.card_succ (o : Ordinal.{u_3}) :
                                (Order.succ o).card = o.card + 1
                                theorem Ordinal.natCast_succ (n : ) :
                                n.succ = Order.succ n
                                @[deprecated Ordinal.natCast_succ]
                                theorem Ordinal.nat_cast_succ (n : ) :
                                n.succ = Order.succ n

                                Alias of Ordinal.natCast_succ.

                                theorem Ordinal.one_out_eq (x : (Quotient.out 1)) :
                                x = Ordinal.enum (fun (x x_1 : (Quotient.out 1)) => x < x_1) 0

                                Extra properties of typein and enum #

                                @[simp]
                                theorem Ordinal.typein_one_out (x : (Quotient.out 1)) :
                                Ordinal.typein (fun (x x_1 : (Quotient.out 1)) => x < x_1) x = 0
                                @[simp]
                                theorem Ordinal.typein_le_typein {α : Type u} (r : ααProp) [IsWellOrder α r] {x : α} {x' : α} :
                                theorem Ordinal.typein_le_typein' (o : Ordinal.{u_3}) {x : (Quotient.out o)} {x' : (Quotient.out o)} :
                                Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x' x x'
                                @[simp]
                                theorem Ordinal.enum_le_enum {α : Type u} (r : ααProp) [IsWellOrder α r] {o : Ordinal.{u}} {o' : Ordinal.{u}} (ho : o < Ordinal.type r) (ho' : o' < Ordinal.type r) :
                                ¬r (Ordinal.enum r o' ho') (Ordinal.enum r o ho) o o'
                                @[simp]
                                theorem Ordinal.enum_le_enum' (a : Ordinal.{u_3}) {o : Ordinal.{u_3}} {o' : Ordinal.{u_3}} (ho : o < Ordinal.type fun (x x_1 : (Quotient.out a)) => x < x_1) (ho' : o' < Ordinal.type fun (x x_1 : (Quotient.out a)) => x < x_1) :
                                Ordinal.enum (fun (x x_1 : (Quotient.out a)) => x < x_1) o ho Ordinal.enum (fun (x x_1 : (Quotient.out a)) => x < x_1) o' ho' o o'
                                theorem Ordinal.enum_zero_le {α : Type u} {r : ααProp} [IsWellOrder α r] (h0 : 0 < Ordinal.type r) (a : α) :
                                ¬r a (Ordinal.enum r 0 h0)
                                theorem Ordinal.enum_zero_le' {o : Ordinal.{u_3}} (h0 : 0 < o) (a : (Quotient.out o)) :
                                Ordinal.enum (fun (x x_1 : (Quotient.out o)) => x < x_1) 0 a
                                theorem Ordinal.le_enum_succ {o : Ordinal.{u_3}} (a : (Quotient.out (Order.succ o))) :
                                a Ordinal.enum (fun (x x_1 : (Quotient.out (Order.succ o))) => x < x_1) o
                                @[simp]
                                theorem Ordinal.enum_inj {α : Type u} {r : ααProp} [IsWellOrder α r] {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h₁ : o₁ < Ordinal.type r) (h₂ : o₂ < Ordinal.type r) :
                                Ordinal.enum r o₁ h₁ = Ordinal.enum r o₂ h₂ o₁ = o₂
                                @[simp]
                                theorem Ordinal.enumIso_apply {α : Type u} (r : ααProp) [IsWellOrder α r] (x : fun (x : Ordinal.{u}) => x < Ordinal.type r) :
                                (Ordinal.enumIso r) x = Ordinal.enum r x
                                @[simp]
                                theorem Ordinal.enumIso_symm_apply_coe {α : Type u} (r : ααProp) [IsWellOrder α r] (x : α) :
                                ((Ordinal.enumIso r).symm x) = Ordinal.typein r x
                                def Ordinal.enumIso {α : Type u} (r : ααProp) [IsWellOrder α r] :
                                (Subrel (fun (x x_1 : Ordinal.{u}) => x < x_1) fun (x : Ordinal.{u}) => x < Ordinal.type r) ≃r r

                                A well order r is order isomorphic to the set of ordinals smaller than type r.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem Ordinal.enumIsoOut_symm_apply_coe (o : Ordinal.{u_3}) (x : (Quotient.out o)) :
                                  ((RelIso.symm o.enumIsoOut) x) = Ordinal.typein (fun (x x_1 : (Quotient.out o)) => x < x_1) x
                                  @[simp]
                                  theorem Ordinal.enumIsoOut_apply (o : Ordinal.{u_3}) (x : (Set.Iio o)) :
                                  o.enumIsoOut x = Ordinal.enum (fun (x x_1 : (Quotient.out o)) => x < x_1) x
                                  noncomputable def Ordinal.enumIsoOut (o : Ordinal.{u_3}) :
                                  (Set.Iio o) ≃o (Quotient.out o)

                                  The order isomorphism between ordinals less than o and o.out.α.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    o.out.α is an OrderBot whenever 0 < o.

                                    Equations
                                    Instances For
                                      theorem Ordinal.enum_zero_eq_bot {o : Ordinal.{u_3}} (ho : 0 < o) :
                                      Ordinal.enum (fun (x x_1 : (Quotient.out o)) => x < x_1) 0 =

                                      Universal ordinal #

                                      univ.{u v} is the order type of the ordinals of Type u as a member of Ordinal.{v} (when u < v). It is an inaccessible cardinal.

                                      Equations
                                      Instances For
                                        def Ordinal.lift.principalSeg :
                                        (fun (x x_1 : Ordinal.{u}) => x < x_1) ≺i fun (x x_1 : Ordinal.{max (u + 1) v} ) => x < x_1

                                        Principal segment version of the lift operation on ordinals, embedding ordinal.{u} in ordinal.{v} as a principal segment when u < v.

                                        Equations
                                        Instances For

                                          Representing a cardinal with an ordinal #

                                          The ordinal corresponding to a cardinal c is the least ordinal whose cardinal is c. For the order-embedding version, see ord.order_embedding.

                                          Equations
                                          Instances For
                                            theorem Cardinal.ord_eq_Inf (α : Type u) :
                                            (Cardinal.mk α).ord = ⨅ (r : { r : ααProp // IsWellOrder α r }), Ordinal.type r
                                            theorem Cardinal.ord_eq (α : Type u_3) :
                                            ∃ (r : ααProp) (wo : IsWellOrder α r), (Cardinal.mk α).ord = Ordinal.type r
                                            theorem Cardinal.ord_le_type {α : Type u} (r : ααProp) [h : IsWellOrder α r] :
                                            theorem Cardinal.ord_le {c : Cardinal.{u_3}} {o : Ordinal.{u_3}} :
                                            c.ord o c o.card
                                            theorem Cardinal.lt_ord {c : Cardinal.{u_3}} {o : Ordinal.{u_3}} :
                                            o < c.ord o.card < c
                                            @[simp]
                                            theorem Cardinal.card_ord (c : Cardinal.{u_3}) :
                                            c.ord.card = c
                                            theorem Cardinal.ord_card_le (o : Ordinal.{u_3}) :
                                            o.card.ord o
                                            theorem Cardinal.card_le_of_le_ord {o : Ordinal.{u_3}} {c : Cardinal.{u_3}} (ho : o c.ord) :
                                            o.card c

                                            A variation on Cardinal.lt_ord using : If o is no greater than the initial ordinal of cardinality c, then its cardinal is no greater than c.

                                            The converse, however, is false (for instance, o = ω+1 and c = ℵ₀).

                                            @[simp]
                                            theorem Cardinal.ord_le_ord {c₁ : Cardinal.{u_3}} {c₂ : Cardinal.{u_3}} :
                                            c₁.ord c₂.ord c₁ c₂
                                            @[simp]
                                            theorem Cardinal.ord_lt_ord {c₁ : Cardinal.{u_3}} {c₂ : Cardinal.{u_3}} :
                                            c₁.ord < c₂.ord c₁ < c₂
                                            @[simp]
                                            theorem Cardinal.ord_nat (n : ) :
                                            (n).ord = n
                                            @[simp]
                                            theorem Cardinal.ord_ofNat (n : ) [n.AtLeastTwo] :
                                            theorem Cardinal.card_typein_lt {α : Type u} (r : ααProp) [IsWellOrder α r] (x : α) (h : (Cardinal.mk α).ord = Ordinal.type r) :
                                            theorem Cardinal.card_typein_out_lt (c : Cardinal.{u_3}) (x : (Quotient.out c.ord)) :
                                            (Ordinal.typein (fun (x x_1 : (Quotient.out c.ord)) => x < x_1) x).card < c

                                            The ordinal corresponding to a cardinal c is the least ordinal whose cardinal is c. This is the order-embedding version. For the regular function, see ord.

                                            Equations
                                            Instances For

                                              The cardinal univ is the cardinality of ordinal univ, or equivalently the cardinal of Ordinal.{u}, or Cardinal.{u}, as an element of Cardinal.{v} (when u < v).

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem Ordinal.nat_le_card {o : Ordinal.{u_3}} {n : } :
                                                n o.card n o
                                                @[simp]
                                                theorem Ordinal.one_le_card {o : Ordinal.{u_3}} :
                                                1 o.card 1 o
                                                @[simp]
                                                theorem Ordinal.ofNat_le_card {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
                                                @[simp]
                                                theorem Ordinal.nat_lt_card {o : Ordinal.{u_3}} {n : } :
                                                n < o.card n < o
                                                @[simp]
                                                theorem Ordinal.zero_lt_card {o : Ordinal.{u_3}} :
                                                0 < o.card 0 < o
                                                @[simp]
                                                theorem Ordinal.one_lt_card {o : Ordinal.{u_3}} :
                                                1 < o.card 1 < o
                                                @[simp]
                                                theorem Ordinal.ofNat_lt_card {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
                                                @[simp]
                                                theorem Ordinal.card_lt_nat {o : Ordinal.{u_3}} {n : } :
                                                o.card < n o < n
                                                @[simp]
                                                theorem Ordinal.card_lt_ofNat {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
                                                @[simp]
                                                theorem Ordinal.card_le_nat {o : Ordinal.{u_3}} {n : } :
                                                o.card n o n
                                                @[simp]
                                                theorem Ordinal.card_le_one {o : Ordinal.{u_3}} :
                                                o.card 1 o 1
                                                @[simp]
                                                theorem Ordinal.card_le_ofNat {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
                                                @[simp]
                                                theorem Ordinal.card_eq_nat {o : Ordinal.{u_3}} {n : } :
                                                o.card = n o = n
                                                @[simp]
                                                theorem Ordinal.card_eq_zero {o : Ordinal.{u_3}} :
                                                o.card = 0 o = 0
                                                @[simp]
                                                theorem Ordinal.card_eq_one {o : Ordinal.{u_3}} :
                                                o.card = 1 o = 1
                                                @[simp]
                                                theorem Ordinal.card_eq_ofNat {o : Ordinal.{u_3}} {n : } [n.AtLeastTwo] :
                                                @[simp]
                                                theorem Ordinal.type_fintype {α : Type u} (r : ααProp) [IsWellOrder α r] [Fintype α] :
                                                theorem Ordinal.type_fin (n : ) :
                                                (Ordinal.type fun (x x_1 : Fin n) => x < x_1) = n

                                                Sorted lists #

                                                theorem List.Sorted.lt_ord_of_lt {α : Type u} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] {l : List α} {m : List α} {o : Ordinal.{u}} (hl : List.Sorted (fun (x x_1 : α) => x > x_1) l) (hm : List.Sorted (fun (x x_1 : α) => x > x_1) m) (hmltl : m < l) (hlt : il, Ordinal.typein (fun (x x_1 : α) => x < x_1) i < o) (i : α) :
                                                i mOrdinal.typein (fun (x x_1 : α) => x < x_1) i < o