Documentation

Mathlib.SetTheory.Cardinal.Ordinal

Cardinals and ordinals #

Relationships between cardinals and ordinals, properties of cardinals that are proved using ordinals.

Main definitions #

Main statements #

Tags #

cardinal arithmetic (for infinite cardinals)

theorem Cardinal.ord_isLimit {c : Cardinal.{u_1}} (co : Cardinal.aleph0 c) :
c.ord.IsLimit

Aleph cardinals #

The aleph' function gives the cardinals listed by their ordinal index. aleph' n = n, aleph' ω = ℵ₀, aleph' (ω + 1) = succ ℵ₀, etc.

For the more common aleph function skipping over finite cardinals, see Cardinal.aleph.

Equations
Instances For
    @[deprecated Cardinal.aleph']
    def Cardinal.alephIdx.initialSeg :
    (fun (x1 x2 : Cardinal.{u_1}) => x1 < x2) ≼i fun (x1 x2 : Ordinal.{u_1}) => x1 < x2

    The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this definition, we register additionally that this function is an initial segment, i.e., it is order preserving and its range is an initial segment of the ordinals. For the basic function version, see alephIdx. For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

    Equations
    Instances For
      @[deprecated Cardinal.aleph']
      def Cardinal.alephIdx.relIso :
      (fun (x1 x2 : Cardinal.{u}) => x1 < x2) ≃r fun (x1 x2 : Ordinal.{u}) => x1 < x2

      The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ℵ₀ = ω, alephIdx ℵ₁ = ω + 1 and so on.) In this version, we register additionally that this function is an order isomorphism between cardinals and ordinals. For the basic function version, see alephIdx.

      Equations
      Instances For
        @[deprecated Cardinal.aleph']

        The aleph' index function, which gives the ordinal index of a cardinal. (The aleph' part is because unlike aleph this counts also the finite stages. So alephIdx n = n, alephIdx ω = ω, alephIdx ℵ₁ = ω + 1 and so on.) For an upgraded version stating that the range is everything, see AlephIdx.rel_iso.

        Equations
        Instances For
          @[deprecated]
          theorem Cardinal.alephIdx_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} :
          a.alephIdx < b.alephIdx a < b
          @[deprecated]
          theorem Cardinal.alephIdx_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} :
          a.alephIdx b.alephIdx a b
          @[deprecated]
          theorem Cardinal.alephIdx.init {a : Cardinal.{u_1}} {b : Ordinal.{u_1}} :
          b < a.alephIdx∃ (c : Cardinal.{u_1}), c.alephIdx = b
          @[deprecated Cardinal.aleph']

          The aleph' function gives the cardinals listed by their ordinal index, and is the inverse of aleph_idx. aleph' n = n, aleph' ω = ω, aleph' (ω + 1) = succ ℵ₀, etc. In this version, we register additionally that this function is an order isomorphism between ordinals and cardinals. For the basic function version, see aleph'.

          Equations
          Instances For
            theorem Cardinal.aleph'_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
            Cardinal.aleph' o₁ < Cardinal.aleph' o₂ o₁ < o₂
            theorem Cardinal.aleph'_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
            Cardinal.aleph' o₁ Cardinal.aleph' o₂ o₁ o₂
            theorem Cardinal.aleph'_max (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :
            Cardinal.aleph' (max o₁ o₂) = max (Cardinal.aleph' o₁) (Cardinal.aleph' o₂)
            @[deprecated]
            theorem Cardinal.aleph'_alephIdx (c : Cardinal.{u_1}) :
            Cardinal.aleph' c.alephIdx = c
            @[deprecated]
            theorem Cardinal.alephIdx_aleph' (o : Ordinal.{u_1}) :
            (Cardinal.aleph' o).alephIdx = o
            @[simp]
            theorem Cardinal.aleph'_zero :
            Cardinal.aleph' 0 = 0
            @[simp]
            theorem Cardinal.aleph'_succ (o : Ordinal.{u_1}) :
            Cardinal.aleph' (Order.succ o) = Order.succ (Cardinal.aleph' o)
            @[simp]
            theorem Cardinal.aleph'_nat (n : ) :
            Cardinal.aleph' n = n
            theorem Cardinal.aleph'_le_of_limit {o : Ordinal.{u_1}} (l : o.IsLimit) {c : Cardinal.{u_1}} :
            Cardinal.aleph' o c o' < o, Cardinal.aleph' o' c
            theorem Cardinal.aleph'_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :
            Cardinal.aleph' o = ⨆ (a : (Set.Iio o)), Cardinal.aleph' a
            @[deprecated Cardinal.aleph'_omega0]

            Alias of Cardinal.aleph'_omega0.

            @[deprecated Cardinal.aleph']

            aleph' and aleph_idx form an equivalence between Ordinal and Cardinal

            Equations
            Instances For

              The aleph function gives the infinite cardinals listed by their ordinal index. aleph 0 = ℵ₀, aleph 1 = succ ℵ₀ is the first uncountable cardinal, and so on.

              For a version including finite cardinals, see Cardinal.aleph'.

              Equations
              Instances For
                theorem Cardinal.aleph_eq_aleph' (o : Ordinal.{u_1}) :
                Cardinal.aleph o = Cardinal.aleph' (Ordinal.omega0 + o)
                theorem Cardinal.aleph_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
                Cardinal.aleph o₁ < Cardinal.aleph o₂ o₁ < o₂
                theorem Cardinal.aleph_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
                Cardinal.aleph o₁ Cardinal.aleph o₂ o₁ o₂
                theorem Cardinal.aleph_max (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :
                Cardinal.aleph (max o₁ o₂) = max (Cardinal.aleph o₁) (Cardinal.aleph o₂)
                @[deprecated Cardinal.aleph_max]
                theorem Cardinal.max_aleph_eq (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :
                max (Cardinal.aleph o₁) (Cardinal.aleph o₂) = Cardinal.aleph (max o₁ o₂)
                @[simp]
                theorem Cardinal.aleph_succ (o : Ordinal.{u_1}) :
                Cardinal.aleph (Order.succ o) = Order.succ (Cardinal.aleph o)
                @[simp]
                theorem Cardinal.aleph_zero :
                Cardinal.aleph 0 = Cardinal.aleph0
                theorem Cardinal.aleph_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :
                Cardinal.aleph o = ⨆ (a : (Set.Iio o)), Cardinal.aleph a
                theorem Cardinal.aleph'_pos {o : Ordinal.{u_1}} (ho : 0 < o) :
                0 < Cardinal.aleph' o
                theorem Cardinal.aleph_pos (o : Ordinal.{u_1}) :
                0 < Cardinal.aleph o
                @[simp]
                theorem Cardinal.aleph_toNat (o : Ordinal.{u_1}) :
                Cardinal.toNat (Cardinal.aleph o) = 0
                @[simp]
                theorem Cardinal.aleph_toPartENat (o : Ordinal.{u_1}) :
                Cardinal.toPartENat (Cardinal.aleph o) =
                instance Cardinal.nonempty_toType_aleph (o : Ordinal.{u_1}) :
                Nonempty (Cardinal.aleph o).ord.toType
                Equations
                • =
                theorem Cardinal.ord_aleph_isLimit (o : Ordinal.{u_1}) :
                (Cardinal.aleph o).ord.IsLimit
                Equations
                • =
                theorem Cardinal.exists_aleph {c : Cardinal.{u_1}} :
                Cardinal.aleph0 c ∃ (o : Ordinal.{u_1}), c = Cardinal.aleph o
                theorem Cardinal.countable_iff_lt_aleph_one {α : Type u_1} (s : Set α) :
                s.Countable Cardinal.mk s < Cardinal.aleph 1
                theorem Cardinal.ord_card_unbounded :
                Set.Unbounded (fun (x1 x2 : Ordinal.{u_1}) => x1 < x2) {b : Ordinal.{u_1} | b.card.ord = b}

                Ordinals that are cardinals are unbounded.

                theorem Cardinal.eq_aleph'_of_eq_card_ord {o : Ordinal.{u_1}} (ho : o.card.ord = o) :
                ∃ (a : Ordinal.{u_1}), (Cardinal.aleph' a).ord = o

                ord ∘ aleph' enumerates the ordinals that are cardinals.

                theorem Cardinal.ord_card_unbounded' :
                Set.Unbounded (fun (x1 x2 : Ordinal.{u_1}) => x1 < x2) {b : Ordinal.{u_1} | b.card.ord = b Ordinal.omega0 b}

                Infinite ordinals that are cardinals are unbounded.

                theorem Cardinal.eq_aleph_of_eq_card_ord {o : Ordinal.{u_1}} (ho : o.card.ord = o) (ho' : Ordinal.omega0 o) :
                ∃ (a : Ordinal.{u_1}), (Cardinal.aleph a).ord = o

                ord ∘ aleph enumerates the infinite ordinals that are cardinals.

                Beth cardinals #

                Beth numbers are defined so that beth 0 = ℵ₀, beth (succ o) = 2 ^ (beth o), and when o is a limit ordinal, beth o is the supremum of beth o' for o' < o.

                Assuming the generalized continuum hypothesis, which is undecidable in ZFC, beth o = aleph o for every o.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Cardinal.beth_limit {o : Ordinal.{u_1}} :
                  o.IsLimitCardinal.beth o = ⨆ (a : (Set.Iio o)), Cardinal.beth a
                  @[simp]
                  theorem Cardinal.beth_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
                  Cardinal.beth o₁ < Cardinal.beth o₂ o₁ < o₂
                  @[simp]
                  theorem Cardinal.beth_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
                  Cardinal.beth o₁ Cardinal.beth o₂ o₁ o₂

                  Properties of mul #

                  If α is an infinite type, then α × α and α have the same cardinality.

                  Properties of mul, not requiring ordinals

                  If α and β are infinite types, then the cardinality of α × β is the maximum of the cardinalities of α and β.

                  @[simp]
                  theorem Cardinal.mul_mk_eq_max {α : Type u} {β : Type u} [Infinite α] [Infinite β] :
                  @[simp]
                  theorem Cardinal.aleph_mul_aleph (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :
                  Cardinal.aleph o₁ * Cardinal.aleph o₂ = Cardinal.aleph (max o₁ o₂)
                  @[simp]
                  theorem Cardinal.aleph0_mul_aleph (o : Ordinal.{u_1}) :
                  Cardinal.aleph0 * Cardinal.aleph o = Cardinal.aleph o
                  @[simp]
                  theorem Cardinal.aleph_mul_aleph0 (o : Ordinal.{u_1}) :
                  Cardinal.aleph o * Cardinal.aleph0 = Cardinal.aleph o
                  theorem Cardinal.mul_lt_of_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 c) (h1 : a < c) (h2 : b < c) :
                  a * b < c
                  theorem Cardinal.mul_eq_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : Cardinal.aleph0 a) (hb : b a) (hb' : b 0) :
                  a * b = a
                  theorem Cardinal.mul_eq_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (hb : Cardinal.aleph0 b) (ha : a b) (ha' : a 0) :
                  a * b = b
                  theorem Cardinal.le_mul_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : b 0) :
                  a b * a
                  theorem Cardinal.le_mul_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (h : b 0) :
                  a a * b

                  Properties of add #

                  If α is an infinite type, then α ⊕ α and α have the same cardinality.

                  If α is an infinite type, then the cardinality of α ⊕ β is the maximum of the cardinalities of α and β.

                  @[simp]
                  theorem Cardinal.add_mk_eq_max {α : Type u} {β : Type u} [Infinite α] :
                  @[simp]
                  theorem Cardinal.add_le_of_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 c) (h1 : a c) (h2 : b c) :
                  a + b c
                  theorem Cardinal.add_lt_of_lt {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (hc : Cardinal.aleph0 c) (h1 : a < c) (h2 : b < c) :
                  a + b < c
                  theorem Cardinal.eq_of_add_eq_of_aleph0_le {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} {c : Cardinal.{u_1}} (h : a + b = c) (ha : a < c) (hc : Cardinal.aleph0 c) :
                  b = c
                  theorem Cardinal.add_eq_left {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (ha : Cardinal.aleph0 a) (hb : b a) :
                  a + b = a
                  theorem Cardinal.add_eq_right {a : Cardinal.{u_1}} {b : Cardinal.{u_1}} (hb : Cardinal.aleph0 b) (ha : a b) :
                  a + b = b
                  theorem Cardinal.add_nat_eq {a : Cardinal.{u_1}} (n : ) (ha : Cardinal.aleph0 a) :
                  a + n = a
                  theorem Cardinal.nat_add_eq {a : Cardinal.{u_1}} (n : ) (ha : Cardinal.aleph0 a) :
                  n + a = a
                  theorem Cardinal.ciSup_add {ι : Type u} (f : ιCardinal.{v}) [Nonempty ι] (hf : BddAbove (Set.range f)) (c : Cardinal.{v}) :
                  (⨆ (i : ι), f i) + c = ⨆ (i : ι), f i + c
                  theorem Cardinal.add_ciSup {ι : Type u} (f : ιCardinal.{v}) [Nonempty ι] (hf : BddAbove (Set.range f)) (c : Cardinal.{v}) :
                  c + ⨆ (i : ι), f i = ⨆ (i : ι), c + f i
                  theorem Cardinal.ciSup_add_ciSup {ι : Type u} {ι' : Type w} (f : ιCardinal.{v}) [Nonempty ι] [Nonempty ι'] (hf : BddAbove (Set.range f)) (g : ι'Cardinal.{v}) (hg : BddAbove (Set.range g)) :
                  (⨆ (i : ι), f i) + ⨆ (j : ι'), g j = ⨆ (i : ι), ⨆ (j : ι'), f i + g j
                  theorem Cardinal.ciSup_mul {ι : Type u} (f : ιCardinal.{v}) (c : Cardinal.{v}) :
                  (⨆ (i : ι), f i) * c = ⨆ (i : ι), f i * c
                  theorem Cardinal.mul_ciSup {ι : Type u} (f : ιCardinal.{v}) (c : Cardinal.{v}) :
                  c * ⨆ (i : ι), f i = ⨆ (i : ι), c * f i
                  theorem Cardinal.ciSup_mul_ciSup {ι : Type u} {ι' : Type w} (f : ιCardinal.{v}) (g : ι'Cardinal.{v}) :
                  (⨆ (i : ι), f i) * ⨆ (j : ι'), g j = ⨆ (i : ι), ⨆ (j : ι'), f i * g j
                  @[simp]
                  theorem Cardinal.aleph_add_aleph (o₁ : Ordinal.{u_1}) (o₂ : Ordinal.{u_1}) :
                  Cardinal.aleph o₁ + Cardinal.aleph o₂ = Cardinal.aleph (max o₁ o₂)
                  theorem Cardinal.principal_add_aleph (o : Ordinal.{u_1}) :
                  Ordinal.Principal (fun (x1 x2 : Ordinal.{u_1}) => x1 + x2) (Cardinal.aleph o).ord
                  theorem Cardinal.add_right_inj_of_lt_aleph0 {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} {γ : Cardinal.{u_1}} (γ₀ : γ < Cardinal.aleph0) :
                  α + γ = β + γ α = β
                  @[simp]
                  theorem Cardinal.add_nat_inj {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} (n : ) :
                  α + n = β + n α = β
                  @[simp]
                  theorem Cardinal.add_one_inj {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} :
                  α + 1 = β + 1 α = β
                  @[simp]
                  theorem Cardinal.add_nat_le_add_nat_iff {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} (n : ) :
                  α + n β + n α β
                  @[deprecated Cardinal.add_nat_le_add_nat_iff]
                  theorem Cardinal.add_nat_le_add_nat_iff_of_lt_aleph_0 {α : Cardinal.{u_1}} {β : Cardinal.{u_1}} (n : ) :
                  α + n β + n α β

                  Alias of Cardinal.add_nat_le_add_nat_iff.

                  @[simp]
                  @[deprecated Cardinal.add_one_le_add_one_iff]

                  Alias of Cardinal.add_one_le_add_one_iff.

                  Properties about power #

                  theorem Cardinal.pow_le {κ : Cardinal.{u}} {μ : Cardinal.{u}} (H1 : Cardinal.aleph0 κ) (H2 : μ < Cardinal.aleph0) :
                  κ ^ μ κ
                  theorem Cardinal.pow_eq {κ : Cardinal.{u}} {μ : Cardinal.{u}} (H1 : Cardinal.aleph0 κ) (H2 : 1 μ) (H3 : μ < Cardinal.aleph0) :
                  κ ^ μ = κ
                  theorem Cardinal.prod_eq_two_power {ι : Type u} [Infinite ι] {c : ιCardinal.{v}} (h₁ : ∀ (i : ι), 2 c i) (h₂ : ∀ (i : ι), Cardinal.lift.{u, v} (c i) Cardinal.lift.{v, u} (Cardinal.mk ι)) :
                  theorem Cardinal.power_eq_two_power {c₁ : Cardinal.{u_1}} {c₂ : Cardinal.{u_1}} (h₁ : Cardinal.aleph0 c₁) (h₂ : 2 c₂) (h₂' : c₂ c₁) :
                  c₂ ^ c₁ = 2 ^ c₁
                  theorem Cardinal.nat_power_eq {c : Cardinal.{u}} (h : Cardinal.aleph0 c) {n : } (hn : 2 n) :
                  n ^ c = 2 ^ c
                  theorem Cardinal.power_nat_eq {c : Cardinal.{u}} {n : } (h1 : Cardinal.aleph0 c) (h2 : 1 n) :
                  c ^ n = c

                  Computing cardinality of various types #

                  theorem Cardinal.mk_equiv_comm {α : Type u} {β' : Type v} :
                  Cardinal.mk (α β') = Cardinal.mk (β' α)

                  This lemma makes lemmas assuming Infinite α applicable to the situation where we have Infinite β instead.

                  theorem Cardinal.mk_arrow_eq_zero_iff {α : Type u} {β' : Type v} :
                  Cardinal.mk (αβ') = 0 Cardinal.mk α 0 Cardinal.mk β' = 0
                  theorem Cardinal.mk_equiv_le_embedding (α : Type u) (β' : Type v) :
                  Cardinal.mk (α β') Cardinal.mk (α β')
                  theorem Cardinal.mk_embedding_le_arrow (α : Type u) (β' : Type v) :
                  Cardinal.mk (α β') Cardinal.mk (αβ')
                  theorem Cardinal.mk_equiv_eq_arrow_of_eq {α : Type u} {β : Type u} [Infinite α] (eq : Cardinal.mk α = Cardinal.mk β) :
                  Cardinal.mk (α β) = Cardinal.mk (αβ)
                  theorem Cardinal.mk_equiv_of_eq {α : Type u} {β : Type u} [Infinite α] (eq : Cardinal.mk α = Cardinal.mk β) :
                  theorem Cardinal.mk_embedding_eq_arrow_of_le {α : Type u} {β : Type u} [Infinite α] (le : Cardinal.mk β Cardinal.mk α) :
                  Cardinal.mk (β α) = Cardinal.mk (βα)
                  theorem Cardinal.mk_surjective_eq_arrow_of_le {α : Type u} {β : Type u} [Infinite α] (le : Cardinal.mk β Cardinal.mk α) :
                  Cardinal.mk {f : αβ | Function.Surjective f} = Cardinal.mk (αβ)
                  @[simp]
                  theorem Cardinal.mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) :

                  Properties of compl #

                  theorem Cardinal.mk_compl_of_infinite {α : Type u_1} [Infinite α] (s : Set α) (h2 : Cardinal.mk s < Cardinal.mk α) :
                  theorem Cardinal.mk_compl_eq_mk_compl_infinite {α : Type u_1} [Infinite α] {s : Set α} {t : Set α} (hs : Cardinal.mk s < Cardinal.mk α) (ht : Cardinal.mk t < Cardinal.mk α) :
                  theorem Cardinal.mk_compl_eq_mk_compl_finite {α : Type u} {β : Type u} [Finite α] {s : Set α} {t : Set β} (h1 : Cardinal.mk α = Cardinal.mk β) (h : Cardinal.mk s = Cardinal.mk t) :
                  theorem Cardinal.mk_compl_eq_mk_compl_finite_same {α : Type u} [Finite α] {s : Set α} {t : Set α} (h : Cardinal.mk s = Cardinal.mk t) :

                  Extending an injection to an equiv #

                  theorem Cardinal.extend_function {α : Type u_1} {β : Type u_2} {s : Set α} (f : s β) (h : Nonempty (s (Set.range f))) :
                  ∃ (g : α β), ∀ (x : s), g x = f x
                  theorem Cardinal.extend_function_finite {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : s β) (h : Nonempty (α β)) :
                  ∃ (g : α β), ∀ (x : s), g x = f x
                  theorem Cardinal.extend_function_of_lt {α : Type u_1} {β : Type u_2} {s : Set α} (f : s β) (hs : Cardinal.mk s < Cardinal.mk α) (h : Nonempty (α β)) :
                  ∃ (g : α β), ∀ (x : s), g x = f x

                  ω_ o is a notation for the initial ordinal of cardinality aleph o. Thus, for example ω_ 0 = ω.

                  Equations
                  Instances For

                    ω₁ is the first uncountable ordinal.

                    Equations
                    Instances For
                      theorem Ordinal.omega0_lt_omega1 :
                      Ordinal.omega0 < (Cardinal.aleph 1).ord

                      Cardinal operations with ordinal indices #

                      Results on cardinality of ordinal-indexed families of sets.

                      theorem Ordinal.Cardinal.mk_iUnion_Ordinal_le_of_le {β : Type u_1} {o : Ordinal.{u_1}} {c : Cardinal.{u_1}} (ho : o.card c) (hc : Cardinal.aleph0 c) (A : Ordinal.{u_1}Set β) (hA : j < o, Cardinal.mk (A j) c) :
                      Cardinal.mk (⋃ (j : Ordinal.{u_1}), ⋃ (_ : j < o), A j) c

                      Bounding the cardinal of an ordinal-indexed union of sets.