Cardinal.toNat_strictMonoOn
theorem Cardinal.toNat_strictMonoOn : StrictMonoOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
The theorem `Cardinal.toNat_strictMonoOn` states that the function `Cardinal.toNat`, which maps finite cardinal numbers to their corresponding natural number while assigning 0 to all infinite cardinal numbers, is strictly increasing on the left-infinite right-open interval of cardinals less than `ℵ₀` (the smallest infinite cardinal). In other words, for all cardinals `a` and `b` in this interval such that `a` is less than `b`, the natural number associated with `a` by `Cardinal.toNat` is less than the natural number associated with `b`.
More concisely: For all $a, b$ with $0 < a < \aleph\_0$ and $a < b$, we have $\text{Cardinal.toNat}\ a < \text{Cardinal.toNat}\ b$.
|
Cardinal.toNat_lift
theorem Cardinal.toNat_lift : ∀ (c : Cardinal.{v}), Cardinal.toNat (Cardinal.lift.{u, v} c) = Cardinal.toNat c := by
sorry
The theorem `Cardinal.toNat_lift` states that for any cardinal number `c` (from the universe `v`), the process of converting that cardinal to a natural number remains unchanged, whether the cardinal is first lifted to a higher universe (from `v` to `max v u`) or not. In other words, lifting the universe of the cardinal does not affect its conversion to a natural number. This theorem guarantees the compatibility of the cardinal number universe lifting operation with the function that maps cardinals to natural numbers.
More concisely: For any cardinal number `c`, the function `Cardinal.toNat` from cardinal numbers to natural numbers is invariant under universe lifting, i.e., `Cardinal.toNat c = Cardinal.toNat (lift c)`.
|
Cardinal.toNat_le_toNat
theorem Cardinal.toNat_le_toNat :
∀ {c d : Cardinal.{u}}, c ≤ d → d < Cardinal.aleph0 → Cardinal.toNat c ≤ Cardinal.toNat d
This theorem states that for any two cardinal numbers `c` and `d` in a particular type `u`, if `c` is less than or equal to `d` and `d` is less than the smallest infinite cardinal (also known as `ℵ₀` or aleph null), then the natural number corresponding to `c` is less than or equal to the natural number corresponding to `d`. Here, the function `Cardinal.toNat` is used to map the cardinal numbers `c` and `d` to natural numbers, returning 0 for infinite cardinals.
More concisely: If `c` is a finite cardinal number less than or equal to `d`, and `d` is less than the smallest infinite cardinal, then `Cardinal.toNat c` is less than or equal to `Cardinal.toNat d`.
|
Mathlib.SetTheory.Cardinal.ToNat._auxLemma.1
theorem Mathlib.SetTheory.Cardinal.ToNat._auxLemma.1 :
∀ {c : Cardinal.{u}}, (Cardinal.toNat c = 0) = (c = 0 ∨ Cardinal.aleph0 ≤ c)
This theorem states that for any cardinal number `c`, the function `Cardinal.toNat` mapping `c` to a natural number results in zero if and only if `c` is zero or `c` is greater than or equal to `ℵ₀`, the smallest infinite cardinal. In other words, `Cardinal.toNat` returns zero for finite cardinals that are zero and for all infinite cardinals.
More concisely: The theorem asserts that `Cardinal.toNat` maps every finite cardinal number, including zero, and every infinite cardinal number, specifically `ℵ₀`, to zero.
|
Cardinal.toNat_natCast
theorem Cardinal.toNat_natCast : ∀ (n : ℕ), Cardinal.toNat ↑n = n
This theorem states that for every natural number `n`, when `n` is cast to a `Cardinal` type and then the `toNat` function is applied to it, the result is equal to `n`. In other words, the process of converting a natural number to a cardinal and then converting that cardinal back to a natural number is faithful. This means it preserves the original value of the natural number.
More concisely: For every natural number `n`, the conversion from `n` to `Cardinal` and back to natural number, using the functions `toCardinal` and `toNat` respectively, results in the original value of `n`. In Lean notation: `toNat (toCardinal n) = n`.
|
Cardinal.toNat_mul
theorem Cardinal.toNat_mul : ∀ (x y : Cardinal.{u_1}), Cardinal.toNat (x * y) = Cardinal.toNat x * Cardinal.toNat y
This theorem states that for any two cardinal numbers, `x` and `y`, the cardinal-to-natural function applied to the product of `x` and `y` is equal to the product of the cardinal-to-natural function applied to `x` and the same function applied to `y`. In other words, the function `Cardinal.toNat` preserves multiplication between cardinal numbers. This matches the property of homomorphisms in algebra, where applying the operation (in this case, multiplication) after the function is the same as applying the function first and then the operation.
More concisely: For any cardinal numbers `x` and `y`, `Cardinal.toNat (x * y) = Cardinal.toNat x * Cardinal.toNat y`.
|
Cardinal.cast_toNat_of_lt_aleph0
theorem Cardinal.cast_toNat_of_lt_aleph0 : ∀ {c : Cardinal.{u_1}}, c < Cardinal.aleph0 → ↑(Cardinal.toNat c) = c := by
sorry
This theorem states that for any cardinal number `c`, if `c` is less than `ℵ₀` (the smallest infinite cardinal), the natural number obtained by converting `c` using the `Cardinal.toNat` function actually equals `c` itself. In other words, the `Cardinal.toNat` function effectively acts as an identity for finite cardinal numbers less than `ℵ₀`.
More concisely: For any finite cardinal number `c` less than `ℵ₀`, the function `Cardinal.toNat` maps `c` to itself.
|
Cardinal.toNat_eq_ofNat
theorem Cardinal.toNat_eq_ofNat :
∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.toNat c = OfNat.ofNat n ↔ c = OfNat.ofNat n
This theorem, `Cardinal.toNat_eq_ofNat`, asserts that for any cardinal number `c` of any type and a natural number `n` that is at least two, the cardinal's equivalence to the natural number when converted via `Cardinal.toNat` is equivalent to the cardinal's equality to the natural number translation via `OfNat.ofNat`. In simpler terms, the theorem is stating that the cardinality of a set is equal to a given natural number if and only if, when we convert that cardinality to a natural number, we get that natural number. This essentially allows us to compare cardinalities of sets with natural numbers in a meaningful way.
More concisely: For any cardinal number `c` and natural number `n` with `n ≥ 2`, `Cardinal.toNat c = OfNat.ofNat n` if and only if `c = nat.fromCardinal n`.
|
Cardinal.toNat_congr
theorem Cardinal.toNat_congr :
∀ {α : Type u} {β : Type v}, α ≃ β → Cardinal.toNat (Cardinal.mk α) = Cardinal.toNat (Cardinal.mk β)
This theorem states that for any two types `α` and `β`, if there exists a bijective mapping (or an equivalence) between `α` and `β`, then the cardinality (or size) of `α` and `β` when mapped to natural numbers using the `Cardinal.toNat` function are equal. Here, the cardinality is captured using `Cardinal.mk`, which gives the cardinal number of a type. If `α` and `β` are infinite, the `Cardinal.toNat` function assigns them a cardinality of 0. If `α` and `β` are finite, then their cardinalities are the corresponding natural numbers. This theorem encapsulates the principle that equivalent (bijectively mappable) types have the same cardinality.
More concisely: For any types `α` and `β` with a bijective mapping between them, their cardinalities (as natural numbers) are equal.
|
Cardinal.mk_toNat_eq_card
theorem Cardinal.mk_toNat_eq_card :
∀ {α : Type u} [inst : Fintype α], Cardinal.toNat (Cardinal.mk α) = Fintype.card α
This theorem states that for any finite type `α` (i.e., a type `α` with a `Fintype` instance), the function `Cardinal.toNat` applied to the cardinality of `α` (i.e., `Cardinal.mk α`) is equal to the cardinality of `α` as computed by the `Fintype.card` function. In other words, when dealing with finite types, the function `Cardinal.toNat` when composed with `Cardinal.mk` gives the same result as `Fintype.card`. This ensures the coherence between two different methods of computing the cardinality of a finite type.
More concisely: For any finite type `α`, the cardinalities computed by `Cardinal.mk α` and `Fintype.card α` are equal, i.e., `Cardinal.toNat (Cardinal.mk α) = Fintype.card α`.
|
Cardinal.toNat_rightInverse
theorem Cardinal.toNat_rightInverse : Function.RightInverse Nat.cast ⇑Cardinal.toNat
The theorem `Cardinal.toNat_rightInverse` states that the natural number casting function `Nat.cast` is a right inverse to the function `Cardinal.toNat`. This means that if we apply `Cardinal.toNat` to a cardinal number and then apply `Nat.cast` to the result, we get back the original cardinal number. In terms of function composition, this can be stated as `(Nat.cast ∘ Cardinal.toNat) = id`, where `id` is the identity function.
More concisely: The natural number casting function `Nat.cast` is a right inverse of the `Cardinal.toNat` function, that is, `Cardinal.toNat ∘ Nat.cast = id`.
|
Cardinal.toNat_apply_of_aleph0_le
theorem Cardinal.toNat_apply_of_aleph0_le : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Cardinal.toNat c = 0 := by
sorry
The theorem `Cardinal.toNat_apply_of_aleph0_le` asserts that for any cardinal number `c`, if `c` is greater than or equal to `ℵ₀` (the smallest infinite cardinal number), the function `Cardinal.toNat` applied to `c` equals to zero. In other words, this theorem is stating that the function `Cardinal.toNat` maps infinite cardinal numbers to zero. The function `Cardinal.toNat` is designed to send finite cardinal numbers to their corresponding natural numbers, and all infinite cardinal numbers to zero.
More concisely: For any cardinal number `c` greater than or equal to `ℵ₀`, `Cardinal.toNat c = 0`.
|
Cardinal.toNat_eq_iff_eq_of_lt_aleph0
theorem Cardinal.toNat_eq_iff_eq_of_lt_aleph0 :
∀ {c d : Cardinal.{u}}, c < Cardinal.aleph0 → d < Cardinal.aleph0 → (Cardinal.toNat c = Cardinal.toNat d ↔ c = d)
The theorem `Cardinal.toNat_eq_iff_eq_of_lt_aleph0` states that for any two finite cardinal numbers `c` and `d` (i.e., cardinal numbers that are less than `ℵ₀`, the smallest infinite cardinal), the equality of their projections to natural numbers (obtained by the function `Cardinal.toNat`) is equivalent to the equality of the cardinals themselves. In other words, two finite cardinal numbers are equal if and only if their corresponding natural numbers obtained via the `Cardinal.toNat` function are equal.
More concisely: For any finite cardinal numbers `c` and `d`, `Cardinal.toNat c = Cardinal.toNat d` if and only if `c = d`.
|