mk_univ_complex
theorem mk_univ_complex : Cardinal.mk ↑Set.univ = Cardinal.continuum
This theorem states that the cardinality of the set of complex numbers is equal to the cardinality of the continuum. In mathematical terms, this means that the size of the set of all complex numbers is the same as the size of the set of all real numbers, denoted as the "continuum", which is defined as the power of the set of natural numbers (2 raised to the power of ℵ₀). Essentially, it suggests that there exists a one-to-one correspondence between the set of complex numbers and the set of real numbers.
More concisely: The cardinality of the set of complex numbers is equivalent to the continuum.
|
mk_complex
theorem mk_complex : Cardinal.mk ℂ = Cardinal.continuum
The theorem `mk_complex` states that the cardinality of the set of complex numbers (`ℂ`) is equal to the cardinality of the continuum (`Cardinal.continuum`). The cardinality of the continuum is defined as the power set of the set of natural numbers, or in other words, `2` to the power of the cardinality of the set of natural numbers (`Cardinal.aleph0`).
More concisely: The cardinality of the set of complex numbers equals that of the power set of the natural numbers. In Lean notation, `Cardinal.continuum = Cardinal.powerset (Nat)`.
|
not_countable_complex
theorem not_countable_complex : ¬Set.univ.Countable
This theorem states that the set of all complex numbers is not countable. In mathematical terms, there is no one-to-one correspondence, also known as a bijection, between the set of all complex numbers (represented as `Set.univ`) and the set of all natural numbers. Therefore, you cannot enumerate or "count" all complex numbers in the same way you can with natural numbers, hence the term "not countable".
More concisely: The set of all complex numbers does not have a bijection with the set of natural numbers.
|