Documentation

Mathlib.SetTheory.Cardinal.Continuum

Cardinality of continuum #

In this file we define Cardinal.continuum (notation: 𝔠, localized in Cardinal) to be 2 ^ β„΅β‚€. We also prove some simp lemmas about cardinal arithmetic involving 𝔠.

Notation #

source
def Cardinal.continuum :
Cardinal.{u}

Cardinality of the continuum.

Equations
    Instances For
      source
      def Cardinal.term𝔠 :
      Lean.ParserDescr

      Cardinality of the continuum.

      Equations
        Instances For
          source
          @[simp]
          theorem Cardinal.two_power_aleph0 :
          2 ^ aleph0 = continuum
          source
          @[simp]
          theorem Cardinal.lift_continuum :
          lift.{v, u_1} continuum = continuum
          source
          @[simp]
          theorem Cardinal.continuum_le_lift {c : Cardinal.{u}} :
          continuum ≀ lift.{v, u} c ↔ continuum ≀ c
          source
          @[simp]
          theorem Cardinal.lift_le_continuum {c : Cardinal.{u}} :
          lift.{v, u} c ≀ continuum ↔ c ≀ continuum
          source
          @[simp]
          theorem Cardinal.continuum_lt_lift {c : Cardinal.{u}} :
          continuum < lift.{v, u} c ↔ continuum < c
          source
          @[simp]
          theorem Cardinal.lift_lt_continuum {c : Cardinal.{u}} :
          lift.{v, u} c < continuum ↔ c < continuum

          Inequalities #

          source
          theorem Cardinal.aleph0_lt_continuum :
          aleph0 < continuum
          source
          theorem Cardinal.aleph0_le_continuum :
          aleph0 ≀ continuum
          source
          @[simp]
          theorem Cardinal.beth_one :
          beth 1 = continuum
          source
          theorem Cardinal.nat_lt_continuum (n : β„•) :
          ↑n < continuum
          source
          theorem Cardinal.mk_set_nat :
          mk (Set β„•) = continuum
          source
          theorem Cardinal.continuum_pos :
          0 < continuum
          source
          theorem Cardinal.continuum_ne_zero :
          continuum β‰  0
          source
          theorem Cardinal.aleph_one_le_continuum :
          aleph 1 ≀ continuum
          source
          @[simp]
          theorem Cardinal.continuum_toNat :
          toNat continuum = 0
          source
          @[simp]
          theorem Cardinal.continuum_toENat :
          toENat continuum = ⊀

          Addition #

          source
          @[simp]
          theorem Cardinal.aleph0_add_continuum :
          aleph0 + continuum = continuum
          source
          @[simp]
          theorem Cardinal.continuum_add_aleph0 :
          continuum + aleph0 = continuum
          source
          @[simp]
          theorem Cardinal.continuum_add_self :
          continuum + continuum = continuum
          source
          @[simp]
          theorem Cardinal.nat_add_continuum (n : β„•) :
          ↑n + continuum = continuum
          source
          @[simp]
          theorem Cardinal.continuum_add_nat (n : β„•) :
          continuum + ↑n = continuum
          source
          @[simp]
          theorem Cardinal.ofNat_add_continuum {n : β„•} [n.AtLeastTwo] :
          OfNat.ofNat n + continuum = continuum
          source
          @[simp]
          theorem Cardinal.continuum_add_ofNat {n : β„•} [n.AtLeastTwo] :
          continuum + OfNat.ofNat n = continuum

          Multiplication #

          source
          @[simp]
          theorem Cardinal.continuum_mul_self :
          continuum * continuum = continuum
          source
          @[simp]
          theorem Cardinal.continuum_mul_aleph0 :
          continuum * aleph0 = continuum
          source
          @[simp]
          theorem Cardinal.aleph0_mul_continuum :
          aleph0 * continuum = continuum
          source
          @[simp]
          theorem Cardinal.nat_mul_continuum {n : β„•} (hn : n β‰  0) :
          ↑n * continuum = continuum
          source
          @[simp]
          theorem Cardinal.continuum_mul_nat {n : β„•} (hn : n β‰  0) :
          continuum * ↑n = continuum
          source
          @[simp]
          theorem Cardinal.ofNat_mul_continuum {n : β„•} [n.AtLeastTwo] :
          OfNat.ofNat n * continuum = continuum
          source
          @[simp]
          theorem Cardinal.continuum_mul_ofNat {n : β„•} [n.AtLeastTwo] :
          continuum * OfNat.ofNat n = continuum

          Power #

          source
          @[simp]
          theorem Cardinal.aleph0_power_aleph0 :
          aleph0 ^ aleph0 = continuum
          source
          @[simp]
          theorem Cardinal.nat_power_aleph0 {n : β„•} (hn : 2 ≀ n) :
          ↑n ^ aleph0 = continuum
          source
          @[simp]
          theorem Cardinal.continuum_power_aleph0 :
          continuum ^ aleph0 = continuum
          source
          theorem Cardinal.power_aleph0_of_le_continuum {x : Cardinal.{u_1}} (h₁ : 2 ≀ x) (hβ‚‚ : x ≀ continuum) :
          x ^ aleph0 = continuum