Cardinal.toENat_eq_top
theorem Cardinal.toENat_eq_top : ∀ {a : Cardinal.{u_1}}, Cardinal.toENat a = ⊤ ↔ Cardinal.aleph0 ≤ a
This theorem states that for any cardinal number `a`, the function `Cardinal.toENat a` equals the value `⊤` (which represents infinity in the context of the natural number extension `ℕ∞`) if and only if `a` is greater than or equal to `ℵ₀` (the smallest infinite cardinal, represented by the function `Cardinal.aleph0`). In other words, this function sends all infinite cardinal numbers to `⊤`, and finite cardinal numbers to their corresponding natural number.
More concisely: For any cardinal number `a`, `Cardinal.toENat a = ⊤` if and only if `a ≥ Cardinal.aleph0`.
|
Cardinal.toENat_ofENat
theorem Cardinal.toENat_ofENat : ∀ (n : ℕ∞), Cardinal.toENat ↑n = n
This theorem states that for every extended natural number `n`, when you convert `n` to a cardinal number (using the natural number embedding `↑n`) and then apply the function `Cardinal.toENat`, you get back the original extended natural number `n`. In other words, `Cardinal.toENat` is the right-inverse of the embedding from extended natural numbers to cardinal numbers. This property is crucial for maintaining consistency in the conversion of extended natural numbers to cardinal numbers and back.
More concisely: For every extended natural number `n`, the function `Cardinal.toENat (↑n)` equals `n`.
|
Cardinal.toENatAux_gc
theorem Cardinal.toENatAux_gc : GaloisConnection Cardinal.ofENat Cardinal.toENatAux
The theorem `Cardinal.toENatAux_gc` states that there is a Galois connection between the function `Cardinal.ofENat` and `Cardinal.toENatAux`. In other words, for any cardinal number `a` and extended natural number `b`, `Cardinal.ofENat a` is less than or equal to `b` if and only if `a` is less than or equal to `Cardinal.toENatAux b`. The functions `Cardinal.ofENat` and `Cardinal.toENatAux` represent a coercion from extended natural numbers to cardinal numbers and the other way around, respectively.
More concisely: The functions `Cardinal.ofENat` and `Cardinal.toENatAux` form a Galois connection, meaning `Cardinal.ofENat a <= b` if and only if `a <= Cardinal.toENatAux b` for all cardinal numbers `a` and extended natural numbers `b`.
|
Cardinal.enat_gc
theorem Cardinal.enat_gc : GaloisConnection Cardinal.ofENat ⇑Cardinal.toENat
The theorem `Cardinal.enat_gc` states that the functions `Cardinal.ofENat` and `Cardinal.toENat` form a Galois connection. In the context of this theorem, a Galois connection is a pair of functions `l` and `u` such that for all cardinals `a` and natural numbers `b`, the image of `a` under `l` is less than or equal to `b` if and only if `a` is less than or equal to the image of `b` under `u`. The function `Cardinal.ofENat` serves as the coercion function `l` which sends extended natural numbers to cardinals, and the function `Cardinal.toENat` serves as the projection function `u` which sends cardinals to extended natural numbers.
More concisely: The functions `Cardinal.ofENat` and `Cardinal.toENat` form a Galois connection between the extended natural numbers and cardinals.
|
Cardinal.ofENat_le_ofENat_of_le
theorem Cardinal.ofENat_le_ofENat_of_le : ∀ {m n : ℕ∞}, m ≤ n → ↑m ≤ ↑n
This theorem, known as "Cardinal.ofENat_le_ofENat_of_le", states that for any two extended natural numbers `m` and `n`, if `m` is less than or equal to `n`, then the cardinal number of `m` is less than or equal to the cardinal number of `n`. In other words, the order relation (less than or equal) is preserved when mapping from the extended natural numbers to their corresponding cardinal numbers.
More concisely: For all extended natural numbers m and n, if m <= n then |m| <= |n|, where |.| denotes the cardinality function.
|
Mathlib.SetTheory.Cardinal.ENat._auxLemma.9
theorem Mathlib.SetTheory.Cardinal.ENat._auxLemma.9 : ∀ {m n : ℕ∞}, (↑m ≤ ↑n) = (m ≤ n)
This theorem from the Set Theory Cardinal module in Mathlib states that for any two numbers `m` and `n` of potentially infinite natural numbers (`ℕ∞`), the condition that the cardinality of `m` (`↑m`) is less than or equal to the cardinality of `n` (`↑n`) is equivalent to `m` being less than or equal to `n`. In other words, the ordering of cardinalities of potentially infinite natural numbers corresponds to their natural order.
More concisely: For any two potentially infinite natural numbers `m` and `n`, the cardinality `↑m` is less than or equal to `↑n` if and only if `m` is less than or equal to `n`.
|
Cardinal.range_ofENat
theorem Cardinal.range_ofENat : Set.range Cardinal.ofENat = Set.Iic Cardinal.aleph0
The theorem `Cardinal.range_ofENat` states that the range of the function `Cardinal.ofENat`, which maps extended natural numbers to cardinals, is equivalent to the set of cardinals that are less than or equal to `aleph0`, where `aleph0` is the smallest infinite cardinal. In other words, the `Cardinal.ofENat` function maps all natural numbers and the extended natural number `⊤` to cardinals that are less than or equal to the smallest infinite cardinal, `ℵ₀`.
More concisely: The range of `Cardinal.ofENat` consists of cardinals less than or equal to `ℵ₀`.
|
Cardinal.toENat_eq_nat
theorem Cardinal.toENat_eq_nat : ∀ {a : Cardinal.{u_1}} {n : ℕ}, Cardinal.toENat a = ↑n ↔ a = ↑n
The theorem `Cardinal.toENat_eq_nat` states that for any Cardinal `a` and natural number `n`, the application of the function `Cardinal.toENat` to `a` is equal to the natural number `n` (denoted as `↑n`) if and only if `a` is itself equal to `n`. In other words, the function `Cardinal.toENat` precisely preserves the numerical value when mapping a Cardinal to a natural number, for all finite Cardinals.
More concisely: For any Cardinal `a` and natural number `n`, `Cardinal.toENat a = ↑n` if and only if `a = n`.
|
Cardinal.ofENat_lt_ofENat_of_lt
theorem Cardinal.ofENat_lt_ofENat_of_lt : ∀ {m n : ℕ∞}, m < n → ↑m < ↑n
This theorem, "Cardinal.ofENat_lt_ofENat_of_lt", is essentially an alias of the reverse direction of another theorem "Cardinal.ofENat_lt_ofENat". It states that for any two extended natural numbers `m` and `n`, if `m` is less than `n`, then the cardinality of `m` is less than the cardinality of `n`. Extended natural numbers are regular natural numbers extended with infinity, and the cardinality of a natural number is the number of elements in a set with that many elements.
More concisely: For any extended natural numbers `m` and `n` where `m` is less than `n`, the cardinality of `m` is less than the cardinality of `n`.
|
Cardinal.toENatAux_eq_top
theorem Cardinal.toENatAux_eq_top : ∀ {a : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → a.toENatAux = ⊤
This theorem states that for any cardinal number `a`, if `a` is greater than or equal to `ℵ₀` (the smallest infinite cardinal, i.e., the cardinality of the set of natural numbers), then the function `toENatAux` applied to `a` gives the extended natural number `⊤` (representing infinity). This means that any cardinality that is at least as large as the cardinality of the set of natural numbers is mapped to infinity by the `toENatAux` function.
More concisely: For any cardinal number `a ≥ ℵ₀`, the function `toENatAux` maps `a` to the extended natural number `⊤`.
|
Cardinal.lift_ofENat
theorem Cardinal.lift_ofENat : ∀ (m : ℕ∞), Cardinal.lift.{u, v} ↑m = ↑m
The theorem `Cardinal.lift_ofENat` states that for any extended natural number `m` (denoted as `ℕ∞`), lifting its cardinality from universe `v` to universe `max v u` doesn't change the cardinality. In other words, the cardinality remains invariant under the universe lift operation. This means that the size of the set represented by `m` is the same in both universes `v` and `max v u`.
More concisely: The cardinality of an extended natural number is invariant under universe lift operations.
|
Cardinal.ofENat_toENat
theorem Cardinal.ofENat_toENat : ∀ {a : Cardinal.{u_1}}, a ≤ Cardinal.aleph0 → ↑(Cardinal.toENat a) = a
This theorem, referred to as an alias of the reverse direction of `Cardinal.ofENat_toENat_eq_self`, states that for any cardinal `a`, if `a` is less than or equal to `ℵ₀` (the smallest infinite cardinal), then converting `a` to a natural number using `Cardinal.toENat` and then back to a cardinal yields `a` itself. In other words, the operations of converting from a cardinal to a natural number and back are lossless for cardinals that are less than or equal to `ℵ₀`.
More concisely: For any cardinal `a` less than or equal to `ℵ₀`, `Cardinal.toENat (Cardinal.ofENat a) = a`.
|
Mathlib.SetTheory.Cardinal.ENat._auxLemma.17
theorem Mathlib.SetTheory.Cardinal.ENat._auxLemma.17 : ∀ {m n : ℕ∞}, (↑m = ↑n) = (m = n)
This theorem states that for all natural numbers `m` and `n`, possibly extended to infinity (`ℕ∞`), the equality of their corresponding cardinal numbers (`↑m = ↑n`) is equivalent to the equality of the numbers themselves (`m = n`). In other words, in the realm of cardinalities in set theory, two natural numbers (including infinity) have the same cardinality if and only if they are the same number.
More concisely: For all natural numbers `m` and `n`, their cardinalities are equal, `↑m = ↑n`, if and only if `m` and `n` are equal, `m = n`.
|
Cardinal.ofENat_strictMono
theorem Cardinal.ofENat_strictMono : StrictMono Cardinal.ofENat
The theorem `Cardinal.ofENat_strictMono` states that the function `Cardinal.ofENat`, which maps elements of `ℕ∞` (extended natural numbers including `⊤`) to cardinals, is strictly monotone. In other words, if `a` and `b` are elements of `ℕ∞` and `a` is strictly less than `b`, then the cardinal number corresponding to `a` is strictly less than the cardinal number corresponding to `b`. Therefore, this function strictly preserves the order from the extended natural numbers to cardinal numbers.
More concisely: The function `Cardinal.ofENat` maps strictly smaller extended natural numbers to strictly smaller cardinal numbers.
|
Cardinal.ofENat_le_aleph0
theorem Cardinal.ofENat_le_aleph0 : ∀ (n : ℕ∞), ↑n ≤ Cardinal.aleph0
This theorem states that for any extended natural number `n` (which could be a standard natural number or positive infinity), the cardinality of `n` is less than or equal to `ℵ₀`, the smallest infinite cardinal, which corresponds to the cardinality of the set of natural numbers. In other words, no extended natural number can have a cardinality greater than the size of the set of natural numbers.
More concisely: For any extended natural number `n`, its cardinality is bounded above by that of the set of natural numbers, i.e., ℵ₀.
|
Cardinal.toENatAux_nat
theorem Cardinal.toENatAux_nat : ∀ (n : ℕ), (↑n).toENatAux = ↑n
This theorem states that for all natural numbers `n`, the function `Cardinal.toENatAux` when applied to `n` (coerced to a cardinal number) returns a value equal to `n` (coerced to a type `ℕ∞`, which represents either a natural number or an infinite value). In essence, it asserts a specific behavior of the function `Cardinal.toENatAux`, namely, that it behaves like the identity function when restricted to natural numbers.
More concisely: For all natural numbers n, Cardinal.toENatAux (coerce n to cardinal) = coerce n ℕ∞.
|
Mathlib.SetTheory.Cardinal.ENat._auxLemma.1
theorem Mathlib.SetTheory.Cardinal.ENat._auxLemma.1 : ∀ {m n : ℕ∞}, (↑m < ↑n) = (m < n)
This theorem from the Mathlib library in Set Theory's Cardinal module states that for any two extended natural numbers `m` and `n`, the inequality of their cardinalities (`m` is less than `n`) is equivalent to the inequality of the numbers themselves. In other words, the cardinality of `m` is less than the cardinality of `n` if and only if `m` is less than `n`.
More concisely: For any extended natural numbers `m` and `n`, `m` is less than `n` if and only if the cardinality of `m` is less than the cardinality of `n`.
|