Cardinal.toPartENat_apply_of_aleph0_le
theorem Cardinal.toPartENat_apply_of_aleph0_le :
∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Cardinal.toPartENat c = ⊤
The theorem `Cardinal.toPartENat_apply_of_aleph0_le` states that for any cardinal number `c`, if the cardinality of `c` is greater than or equal to the cardinality of the set of natural numbers (ℵ₀), then the function `Cardinal.toPartENat` applied to `c` returns the greatest possible element (⊤). In other words, the function `Cardinal.toPartENat` maps any infinite cardinal (cardinal at least as large as the set of natural numbers) to the top element, indicating that the cardinality of the set is infinite.
More concisely: For any infinite cardinal number `c`, `Cardinal.toPartENat c = ⊤`.
|
Cardinal.toPartENat_natCast
theorem Cardinal.toPartENat_natCast : ∀ (n : ℕ), Cardinal.toPartENat ↑n = ↑n
This theorem states that for any natural number `n`, the function `Cardinal.toPartENat` when applied to the cardinal number corresponding to `n` (denoted by `↑n`), yields the partial extended natural number also corresponding to `n` (also denoted by `↑n`). In essence, this theorem asserts that the `Cardinal.toPartENat` function behaves as expected when dealing with finite cardinals that originate from natural numbers, mapping them to their corresponding partial extended natural numbers.
More concisely: For any natural number `n`, the function `Cardinal.toPartENat (↑n) = ↑n` holds in Lean 4.
|