Cardinal.aleph0_le_continuum
theorem Cardinal.aleph0_le_continuum : Cardinal.aleph0 ≤ Cardinal.continuum
The theorem `Cardinal.aleph0_le_continuum` states that the cardinality of the set of natural numbers, denoted as `ℵ₀` (or 'aleph null'), is less than or equal to the cardinality of the continuum. The cardinality of the continuum, denoted as 'Cardinal.continuum' in Lean 4, is defined as the power set of the set of natural numbers, or 2 raised to the power of `ℵ₀`. This theorem reflects the mathematical concept that there are at least as many real numbers (which form the continuum) as there are natural numbers.
More concisely: The cardinality of the set of natural numbers is less than or equal to the cardinality of the continuum.
|
Cardinal.aleph0_lt_continuum
theorem Cardinal.aleph0_lt_continuum : Cardinal.aleph0 < Cardinal.continuum
The theorem `Cardinal.aleph0_lt_continuum` states that the cardinality of the set of natural numbers, denoted as `ℵ₀` or aleph-null, is less than the cardinality of the continuum, denoted as `2^ℵ₀`. In other words, the size of the set of all real numbers is strictly larger than the size of the set of all natural numbers.
More concisely: The cardinality of the set of natural numbers is strictly less than that of the set of real numbers.
|
Cardinal.two_power_aleph0
theorem Cardinal.two_power_aleph0 : 2 ^ Cardinal.aleph0 = Cardinal.continuum
This theorem states that the cardinality of the set of all real numbers, often referred to as the "continuum", is equal to the power set of the set of all natural numbers. In particular, it asserts that the cardinality of the continuum (`Cardinal.continuum`) is equal to two raised to the power of `Cardinal.aleph0`, where `Cardinal.aleph0` represents the cardinality of the set of all natural numbers. In mathematical terms, it expresses that |ℝ| = 2^ℵ₀.
More concisely: The cardinality of the set of real numbers is equal to the power set of the natural numbers, that is, |ℝ| = 2^ℵ₀.
|
Cardinal.lift_continuum
theorem Cardinal.lift_continuum : Cardinal.lift.{v, u_1} Cardinal.continuum = Cardinal.continuum
This theorem, `Cardinal.lift_continuum`, asserts that the cardinality of the continuum (often denoted as $2^{\aleph_0}$ in set theory, and represented in Lean 4 as `Cardinal.continuum`) does not change when lifted from the universe `v` to the universe `u_1` using the universe lift operation (`Cardinal.lift`). In other words, the cardinality of the real numbers remains the same even when viewed in a larger universe of sets.
More concisely: The cardinality of the continuum is invariant under universe lifting, i.e., `Cardinal.continuum = Cardinal.lift Cardinal.continuum`.
|
Cardinal.nat_lt_continuum
theorem Cardinal.nat_lt_continuum : ∀ (n : ℕ), ↑n < Cardinal.continuum
The theorem `Cardinal.nat_lt_continuum` states that for every natural number `n`, the cardinality of `n` (when considered as a cardinal number) is strictly less than the cardinality of the continuum. In other words, no matter how large the natural number `n` is, the size of the set of all natural numbers is always smaller than the size of the real numbers (the continuum). This is expressed in the language of cardinal numbers, which are used to measure the size of sets.
More concisely: For every natural number $n$, the cardinality of $n$ is strictly less than the cardinality of the continuum.
|