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)

Aleph cardinals #

def Cardinal.alephIdx.initialSeg :
(fun (x x_1 : Cardinal.{u_1}) => x < x_1) ≼i fun (x x_1 : Ordinal.{u_1}) => x < x_1

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

    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
      def Cardinal.alephIdx.relIso :
      (fun (x x_1 : Cardinal.{u}) => x < x_1) ≃r fun (x x_1 : Ordinal.{u}) => x < x_1

      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
        def Cardinal.Aleph'.relIso :
        (fun (x x_1 : Ordinal.{u_1}) => x < x_1) ≃r fun (x x_1 : Cardinal.{u_1}) => x < x_1

        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

          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.

          Equations
          Instances For
            @[simp]
            theorem Cardinal.aleph'_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
            Cardinal.aleph' o₁ < Cardinal.aleph' o₂ o₁ < o₂
            @[simp]
            @[simp]
            theorem Cardinal.aleph'_nat (n : ) :
            Cardinal.aleph' n = n

            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.

              Equations
              Instances For
                @[simp]
                theorem Cardinal.aleph_lt {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
                Cardinal.aleph o₁ < Cardinal.aleph o₂ o₁ < o₂
                @[simp]
                theorem Cardinal.aleph_le {o₁ : Ordinal.{u_1}} {o₂ : Ordinal.{u_1}} :
                @[simp]
                @[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) =

                Ordinals that are cardinals are unbounded.

                Infinite ordinals that are cardinals are unbounded.

                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
                  @[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 β] :
                  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
                  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

                      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 : Ordinal.card o 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.