HepLean 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
    Equations
    Instances For
      source
      @[simp]
      theorem Cardinal.two_power_aleph0 :
      2 ^ Cardinal.aleph0 = Cardinal.continuum
      source
      @[simp]
      theorem Cardinal.lift_continuum :
      Cardinal.lift.{v, u_1} Cardinal.continuum = Cardinal.continuum
      source
      @[simp]
      theorem Cardinal.continuum_le_lift {c : Cardinal.{u}} :
      Cardinal.continuum โ‰ค Cardinal.lift.{v, u} c โ†” Cardinal.continuum โ‰ค c
      source
      @[simp]
      theorem Cardinal.lift_le_continuum {c : Cardinal.{u}} :
      Cardinal.lift.{v, u} c โ‰ค Cardinal.continuum โ†” c โ‰ค Cardinal.continuum
      source
      @[simp]
      theorem Cardinal.continuum_lt_lift {c : Cardinal.{u}} :
      Cardinal.continuum < Cardinal.lift.{v, u} c โ†” Cardinal.continuum < c
      source
      @[simp]
      theorem Cardinal.lift_lt_continuum {c : Cardinal.{u}} :
      Cardinal.lift.{v, u} c < Cardinal.continuum โ†” c < Cardinal.continuum

      Inequalities #

      source
      theorem Cardinal.aleph0_lt_continuum :
      Cardinal.aleph0 < Cardinal.continuum
      source
      theorem Cardinal.aleph0_le_continuum :
      Cardinal.aleph0 โ‰ค Cardinal.continuum
      source
      @[simp]
      theorem Cardinal.beth_one :
      Cardinal.beth 1 = Cardinal.continuum
      source
      theorem Cardinal.nat_lt_continuum (n : โ„•) :
      โ†‘n < Cardinal.continuum
      source
      theorem Cardinal.mk_set_nat :
      Cardinal.mk (Set โ„•) = Cardinal.continuum
      source
      theorem Cardinal.continuum_pos :
      0 < Cardinal.continuum
      source
      theorem Cardinal.continuum_ne_zero :
      Cardinal.continuum โ‰  0
      source
      theorem Cardinal.aleph_one_le_continuum :
      Cardinal.aleph 1 โ‰ค Cardinal.continuum
      source
      @[simp]
      theorem Cardinal.continuum_toNat :
      Cardinal.toNat Cardinal.continuum = 0
      source
      @[simp]
      theorem Cardinal.continuum_toPartENat :
      Cardinal.toPartENat Cardinal.continuum = โŠค

      Addition #

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

      Multiplication #

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

      Power #

      source
      @[simp]
      theorem Cardinal.aleph0_power_aleph0 :
      Cardinal.aleph0 ^ Cardinal.aleph0 = Cardinal.continuum
      source
      @[simp]
      theorem Cardinal.nat_power_aleph0 {n : โ„•} (hn : 2 โ‰ค n) :
      โ†‘n ^ Cardinal.aleph0 = Cardinal.continuum
      source
      @[simp]
      theorem Cardinal.continuum_power_aleph0 :
      Cardinal.continuum ^ Cardinal.aleph0 = Cardinal.continuum
      source
      theorem Cardinal.power_aleph0_of_le_continuum {x : Cardinal.{u_1}} (hโ‚ : 2 โ‰ค x) (hโ‚‚ : x โ‰ค Cardinal.continuum) :
      x ^ Cardinal.aleph0 = Cardinal.continuum