Documentation

Mathlib.SetTheory.Cardinal.Aleph

Omega, aleph, and beth functions #

This file defines the ω, , and functions which enumerate certain kinds of ordinals and cardinals. Each is provided in two variants: the standard versions which only take infinite values, and "preliminary" versions which include finite values and are sometimes more convenient.

Notation #

The following notations are scoped to the Ordinal namespace.

The following notations are scoped to the Cardinal namespace.

Omega ordinals #

An ordinal is initial when it is the first ordinal with a given cardinality.

This is written as o.card.ord = o, i.e. o is the smallest ordinal with cardinality o.card.

Equations
Instances For

    Initial ordinals are order-isomorphic to the cardinals.

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

      The "pre-omega" function gives the initial ordinals listed by their ordinal index. preOmega n = n, preOmega ω = ω, preOmega (ω + 1) = ω₁, etc.

      For the more common omega function skipping over finite ordinals, see Ordinal.omega.

      Equations
      Instances For
        theorem Ordinal.preOmega_lt_preOmega {o₁ o₂ : Ordinal.{u_1}} :
        preOmega o₁ < preOmega o₂ o₁ < o₂
        theorem Ordinal.preOmega_le_preOmega {o₁ o₂ : Ordinal.{u_1}} :
        preOmega o₁ preOmega o₂ o₁ o₂
        theorem Ordinal.preOmega_max (o₁ o₂ : Ordinal.{u_1}) :
        preOmega (max o₁ o₂) = max (preOmega o₁) (preOmega o₂)
        @[simp]
        theorem Ordinal.preOmega_natCast (n : ) :
        preOmega n = n
        @[simp]
        theorem Ordinal.preOmega_le_of_forall_lt {o a : Ordinal.{u_1}} (ha : a.IsInitial) (H : b < o, preOmega b < a) :

        The omega function gives the infinite initial ordinals listed by their ordinal index. omega 0 = ω, omega 1 = ω₁ is the first uncountable ordinal, and so on.

        This is not to be confused with the first infinite ordinal Ordinal.omega0.

        For a version including finite ordinals, see Ordinal.preOmega.

        Equations
        Instances For

          The omega function gives the infinite initial ordinals listed by their ordinal index. omega 0 = ω, omega 1 = ω₁ is the first uncountable ordinal, and so on.

          This is not to be confused with the first infinite ordinal Ordinal.omega0.

          For a version including finite ordinals, see Ordinal.preOmega.

          Equations
          Instances For

            ω₁ is the first uncountable ordinal.

            Equations
            Instances For
              theorem Ordinal.omega_lt_omega {o₁ o₂ : Ordinal.{u_1}} :
              omega o₁ < omega o₂ o₁ < o₂
              theorem Ordinal.omega_le_omega {o₁ o₂ : Ordinal.{u_1}} :
              omega o₁ omega o₂ o₁ o₂
              theorem Ordinal.omega_max (o₁ o₂ : Ordinal.{u_1}) :
              omega (max o₁ o₂) = max (omega o₁) (omega o₂)

              For the theorem 0 < ω, see omega0_pos.

              Aleph cardinals #

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

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

              Equations
              Instances For
                theorem Cardinal.preAleph_lt_preAleph {o₁ o₂ : Ordinal.{u_1}} :
                preAleph o₁ < preAleph o₂ o₁ < o₂
                theorem Cardinal.preAleph_le_preAleph {o₁ o₂ : Ordinal.{u_1}} :
                preAleph o₁ preAleph o₂ o₁ o₂
                theorem Cardinal.preAleph_max (o₁ o₂ : Ordinal.{u_1}) :
                preAleph (max o₁ o₂) = max (preAleph o₁) (preAleph o₂)
                @[simp]
                theorem Cardinal.preAleph_nat (n : ) :
                preAleph n = n
                @[simp]
                theorem Cardinal.preAleph_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :
                preAleph o = ⨆ (a : (Set.Iio o)), preAleph a

                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.preAleph.

                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.preAleph.

                  Equations
                  Instances For

                    ℵ₁ is the first uncountable cardinal.

                    Equations
                    Instances For
                      theorem Cardinal.aleph_lt_aleph {o₁ o₂ : Ordinal.{u_1}} :
                      aleph o₁ < aleph o₂ o₁ < o₂
                      theorem Cardinal.aleph_le_aleph {o₁ o₂ : Ordinal.{u_1}} :
                      aleph o₁ aleph o₂ o₁ o₂
                      theorem Cardinal.aleph_max (o₁ o₂ : Ordinal.{u_1}) :
                      aleph (max o₁ o₂) = max (aleph o₁) (aleph o₂)
                      @[simp]

                      For the theorem lift ω = ω, see lift_omega0.

                      theorem Cardinal.aleph_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :
                      aleph o = ⨆ (a : (Set.Iio o)), aleph a

                      Beth cardinals #

                      @[irreducible]

                      The "pre-beth" function is defined so that preBeth o is the supremum of 2 ^ preBeth a for a < o. This implies beth 0 = 0, beth (succ o) = 2 ^ beth o, and that for a limit ordinal o, beth o is the supremum of beth a for a < o.

                      For the usual function starting at ℵ₀, see Cardinal.beth.

                      Equations
                      Instances For
                        @[simp]
                        theorem Cardinal.preBeth_lt_preBeth {o₁ o₂ : Ordinal.{u_1}} :
                        preBeth o₁ < preBeth o₂ o₁ < o₂
                        @[simp]
                        theorem Cardinal.preBeth_le_preBeth {o₁ o₂ : Ordinal.{u_1}} :
                        preBeth o₁ preBeth o₂ o₁ o₂
                        theorem Cardinal.preBeth_nat (n : ) :
                        preBeth n = ((fun (x : ) => 2 ^ x)^[n] 0)
                        @[simp]
                        @[simp]

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

                        Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have ℶ_ o = ℵ_ o for all ordinals.

                        For a version which starts at zero, see Cardinal.preBeth.

                        Equations
                        Instances For

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

                          Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have ℶ_ o = ℵ_ o for all ordinals.

                          For a version which starts at zero, see Cardinal.preBeth.

                          Equations
                          Instances For
                            @[simp]
                            theorem Cardinal.beth_lt_beth {o₁ o₂ : Ordinal.{u_1}} :
                            beth o₁ < beth o₂ o₁ < o₂
                            @[deprecated Cardinal.beth_lt_beth (since := "2025-01-14")]
                            theorem Cardinal.beth_lt {o₁ o₂ : Ordinal.{u_1}} :
                            beth o₁ < beth o₂ o₁ < o₂

                            Alias of Cardinal.beth_lt_beth.

                            @[simp]
                            theorem Cardinal.beth_le_beth {o₁ o₂ : Ordinal.{u_1}} :
                            beth o₁ beth o₂ o₁ o₂
                            @[deprecated Cardinal.beth_le_beth (since := "2025-01-14")]
                            theorem Cardinal.beth_le {o₁ o₂ : Ordinal.{u_1}} :
                            beth o₁ beth o₂ o₁ o₂

                            Alias of Cardinal.beth_le_beth.

                            theorem Cardinal.beth_limit {o : Ordinal.{u_1}} (ho : o.IsLimit) :
                            beth o = ⨆ (a : (Set.Iio o)), beth a