LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Data.Real.Cardinality

`Cardinal.cantorFunctionAux_true` theorem Cardinal.cantorFunctionAux_true : ∀ {c : ℝ} {f : ℕ → Bool} {n : ℕ}, f n = true → Cardinal.cantorFunctionAux c f n = c ^ n The theorem `Cardinal.cantorFunctionAux_true` states that for all real numbers `c`, functions `f` mapping natural numbers to Booleans, and natural numbers `n`, if the function `f` evaluated at `n` is true, then the function `Cardinal.cantorFunctionAux` evaluated at `c`, `f`, and `n` returns the value of `c` raised to the power `n`. In other words, if the Boolean function applied to a natural number returns true, the cantor function auxiliary gives the power of the real number to that natural number. More concisely: For all real numbers `c`, functions `f` mapping natural numbers to Booleans, and natural numbers `n`, if `f`( `n`) = `true`, then `Cardinal.cantorFunctionAux` `c` `f` `n` = `c` ^ `n`.
`Cardinal.mk_Ioc_real` theorem Cardinal.mk_Ioc_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Ioc a b) = Cardinal.continuum This theorem states that for any two real numbers 'a' and 'b' where 'a' is less than 'b', the cardinality (or the number of elements) of the interval (a, b] is equal to the cardinality of the continuum. The interval (a, b] is a left-open right-closed interval, which includes all the real numbers that are greater than 'a' and less than or equal to 'b'. The cardinality of the continuum refers to the size of the set of all real numbers, which is known to be \(2^{\aleph_0}\) (2 to the power of aleph null), where \(\aleph_0\) represents the cardinality of the set of all natural numbers. More concisely: The cardinality of the interval (a, b] of real numbers, where a < b, equals that of the real numbers.
`Cardinal.increasing_cantorFunction` theorem Cardinal.increasing_cantorFunction : ∀ {c : ℝ}, 0 < c → c < 1 / 2 → ∀ {n : ℕ} {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → Cardinal.cantorFunction c f < Cardinal.cantorFunction c g The theorem `Cardinal.increasing_cantorFunction` states that for any real number `c` between 0 and 1/2, the Cantor function `Cardinal.cantorFunction c` is strictly increasing with respect to a lexicographic order on sequences of Boolean values (interpreted as natural numbers). More precisely, if `f` and `g` are two such sequences and `f` coincides with `g` up to a certain index `n` where `f n` is `false` and `g n` is `true`, then `Cardinal.cantorFunction c f` is strictly less than `Cardinal.cantorFunction c g`. Note that the lexicographic order is not officially defined for infinite products like ℕ → Bool, but we can make sense of it in this context by comparing sequences element by element. More concisely: For any real number `c` between 0 and 1/2, the Cantor function `Cardinal.cantorFunction c` strictly increases with respect to the lexicographic order on sequences of Boolean values, i.e., if `f` and `g` are two such sequences with `f` having a first false value at a strictly smaller index than `g`, then `Cardinal.cantorFunction c f` is strictly less than `Cardinal.cantorFunction c g`.
`Cardinal.not_countable_real` theorem Cardinal.not_countable_real : ¬Set.univ.Countable Non-Denumerability of the Continuum Theorem: This theorem states that the set of all real numbers is uncountable. In other words, there is no one-to-one correspondence (or bijection) between the set of all real numbers and the set of all natural numbers, implying that the cardinality of the real numbers is strictly greater than the cardinality of the natural numbers. This result is a fundamental aspect of set theory and real analysis. More concisely: The real numbers cannot be put in one-to-one correspondence with the natural numbers.
`Cardinal.mk_Iio_real` theorem Cardinal.mk_Iio_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Iio a) = Cardinal.continuum This theorem states that for any real number `a`, the size or cardinality of the interval from negative infinity to `a` (not inclusive of `a`) is equal to the cardinality of the continuum. In mathematics, the cardinality of the continuum is the size of the set of real numbers, which is the same as the size of the power set of the set of natural numbers, and is denoted by \(2^{\aleph_0}\). Thus, this theorem asserts that the set of real numbers less than any given real number is as large as the set of all real numbers. More concisely: The cardinality of the set of real numbers less than any given real number is equal to the continuum.
`Cardinal.mk_Ico_real` theorem Cardinal.mk_Ico_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Ico a b) = Cardinal.continuum This theorem states that for any two real numbers `a` and `b` such that `a` is less than `b`, the cardinality (or the size) of the half-open interval [a, b) - that is, the set of all real numbers greater than or equal to `a` and less than `b` - is equal to the cardinality of the continuum. The continuum cardinality is defined as the cardinality of the set of all real numbers, which is equal to the power set of the set of natural numbers (notated as 2 to the power of 𝔸leph 0 in set theory). More concisely: The cardinality of the half-open interval [a, b) equals the continuum cardinality for any real numbers a < b.
`Cardinal.cantorFunctionAux_false` theorem Cardinal.cantorFunctionAux_false : ∀ {c : ℝ} {f : ℕ → Bool} {n : ℕ}, f n = false → Cardinal.cantorFunctionAux c f n = 0 The theorem `Cardinal.cantorFunctionAux_false` states that for all real numbers `c`, functions `f` from natural numbers to boolean values, and natural numbers `n`, if `f(n)` evaluates to `false`, then the value of the function `Cardinal.cantorFunctionAux` at `c`, `f`, and `n` is zero. In other words, if the boolean function `f` returns `false` when applied to a natural number `n`, the corresponding term in the summation of the Cantor function is zero. More concisely: If `f(n)` is false, then `Cardinal.cantorFunctionAux` at `c`, `f`, and `n` equals zero.
`Cardinal.mk_Ioo_real` theorem Cardinal.mk_Ioo_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Ioo a b) = Cardinal.continuum This theorem establishes that the cardinality of the open interval (a, b) in real numbers is equal to the cardinality of the continuum. In other words, for any pair of real numbers a and b where a is less than b, the set of real numbers strictly between a and b (denoted (a, b)) has the same size (cardinality) as the continuum. The continuum is defined as the set of all real numbers, represented by the cardinal number 2 raised to the power of the cardinality of the set of natural numbers (also known as aleph null). More concisely: The cardinality of the open real interval (a, b) is equal to that of the continuum.
`Cardinal.mk_Icc_real` theorem Cardinal.mk_Icc_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Icc a b) = Cardinal.continuum This theorem states that for any two real numbers `a` and `b` where `a` is less than `b`, the cardinality (or the number of elements) of the interval `[a, b]` (which includes all real numbers `x` such that `a ≤ x ≤ b`) is equal to the cardinality of the continuum. The cardinality of the continuum is defined as `2` to the power of the cardinality of the set of natural numbers (also known as `aleph null` or `aleph0`). More concisely: The cardinality of the real interval [`a`, `b`] is equal to that of the continuum, which is 2^ℵ₀.
`Cardinal.mk_Ici_real` theorem Cardinal.mk_Ici_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Ici a) = Cardinal.continuum This theorem states that for any real number 'a', the cardinality (or size) of the interval from 'a' to positive infinity, denoted [a, ∞), is equal to the cardinality of the continuum. The cardinality of the continuum refers to the size of the set of all real numbers, which is equal to the power set of the set of natural numbers, represented as 2 to the power of aleph-null (2^aleph0) in set theory. Therefore, this theorem is expressing that the size of the set of all real numbers greater than or equal to any given real number 'a' is equal to the size of the set of all real numbers. More concisely: The cardinality of the set of real numbers greater than or equal to a is equal to the cardinality of the set of all real numbers.
`Cardinal.mk_real` theorem Cardinal.mk_real : Cardinal.mk ℝ = Cardinal.continuum This theorem establishes that the cardinality of the set of real numbers, denoted as ℝ, is equal to the cardinality of the continuum. In set theory, the cardinality of a set refers to the "number of elements" in the set. The cardinality of the continuum is defined as the cardinality of the set of all infinite sequences of binary digits, which is the same as the power set of the set of natural numbers (often denoted as 2^(aleph_0) in mathematics). Thus, this theorem is stating that there are as many real numbers as there are infinite sequences of binary digits. More concisely: The theorem asserts that the cardinality of the set of real numbers equals that of the set of infinite binary sequences, i.e., ℝ ≈ 2^(aleph\_0).
`Cardinal.mk_Iic_real` theorem Cardinal.mk_Iic_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Iic a) = Cardinal.continuum This theorem states that for any real number 'a', the cardinality (or size) of the interval from negative infinity to 'a' (inclusive) is equal to the cardinality of the continuum. In other words, the set of all real numbers less than or equal to 'a' has the same number of elements as the set of all real numbers. This is consistent with the concept in mathematics that there are the same amount of numbers between any two different real numbers as there are real numbers in total, implying the idea of infinity in the real number line. More concisely: The cardinality of the set of real numbers less than or equal to a given real number is equal to the cardinality of the real numbers.
`Cardinal.mk_univ_real` theorem Cardinal.mk_univ_real : Cardinal.mk ↑Set.univ = Cardinal.continuum This theorem states that the cardinality (or the size) of the set of real numbers (`Set.univ`) is equal to the cardinality of the continuum (`Cardinal.continum`). In mathematical terms, this means that the number of elements in the set of real numbers is equal to the power of two raised to the cardinality of the set of natural numbers (`Cardinal.aleph0`). This is a fundamental result in set theory and relates to the size of different infinities. More concisely: The cardinality of the set of real numbers equals that of the continuum, which is the power of two over the cardinality of the natural numbers.
`Cardinal.cantorFunction_injective` theorem Cardinal.cantorFunction_injective : ∀ {c : ℝ}, 0 < c → c < 1 / 2 → Function.Injective (Cardinal.cantorFunction c) The theorem `Cardinal.cantorFunction_injective` states that the Cantor Function, denoted as `cantorFunction c`, is injective or one-to-one, provided the real number `c` satisfies the conditions `0 < c` and `c < 1/2`. In mathematical terms, this means if two sequences of booleans `f` and `g` have the same Cantor Function value for a certain `c` (i.e., `cantorFunction c f = cantorFunction c g`), then the two sequences `f` and `g` themselves must be identical. More concisely: If `0 < c < 1/2`, then the Cantor function `cantorFunction c` is an injection from the set of binary sequences to itself.
`Cardinal.mk_Ioi_real` theorem Cardinal.mk_Ioi_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Ioi a) = Cardinal.continuum This theorem states that for any real number 'a', the cardinality (or the size of the set in terms of the number of its elements) of the interval (a, ∞) is equal to the cardinality of the continuum. The interval (a, ∞) is defined as a set of all real numbers that are greater than 'a'. The cardinality of the continuum is defined as the size of the set of all real numbers, or equivalently, the power set of the set of natural numbers (i.e., 2 to the power of the size of the set of natural numbers, denoted as $2^{\aleph_0}$ in set theory). More concisely: The cardinality of the set of real numbers in the interval (a, ∞) equals the cardinality of the continuum.