Nat.card_eq_zero_of_infinite
theorem Nat.card_eq_zero_of_infinite : ∀ {α : Type u_1} [inst : Infinite α], Nat.card α = 0
The theorem `Nat.card_eq_zero_of_infinite` states that for any type `α` which is infinite, the cardinality of `α` as a natural number, denoted by `Nat.card α`, is equal to zero. In other words, for infinite types, the function `Nat.card` always returns zero. This is consistent with the definition of `Nat.card`, which assigns a cardinality of zero to all infinite types.
More concisely: For any infinite type `α`, the cardinality `Nat.card α` equals zero.
|
Nat.card_eq_one_iff_unique
theorem Nat.card_eq_one_iff_unique : ∀ {α : Type u_1}, Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α
The theorem `Nat.card_eq_one_iff_unique` states that for any type `α`, the cardinality of `α` (represented as a natural number) is equal to 1 if and only if `α` is both a subsingleton and nonempty. In other words, a type `α` has exactly one element if and only if it satisfies the two conditions: being a subsingleton (i.e., there is at most one element in `α`) and being nonempty (i.e., there is at least one element in `α`).
More concisely: The natural number representing the cardinality of a nonempty type equals 1 if and only if the type is a subsingleton.
|
Nat.card_pi
theorem Nat.card_pi :
∀ {α : Type u_1} {β : α → Type u_3} [inst : Fintype α],
Nat.card ((a : α) → β a) = Finset.univ.prod fun a => Nat.card (β a)
This theorem, `Nat.card_pi`, states that for any types `α` (which must be a finite type) and `β` (which is dependent on `α`), the cardinality of the function type `(a : α) → β a`, which is a function from `α` to `β a`, is equal to the product of the cardinalities of `β a` for each `a` in the universal finite set of `α`. In other words, the number of all possible functions from `α` to `β a` is the product of the numbers of possible values of `β a` for each element `a` of `α`.
More concisely: The cardinality of the type of functions from a finite type `α` to a dependent type `β a` is equal to the product of the cardinalities of `β a` for each `a` in `α`.
|
Nat.card_congr
theorem Nat.card_congr : ∀ {α : Type u_1} {β : Type u_2}, α ≃ β → Nat.card α = Nat.card β
The theorem `Nat.card_congr` states that for any two types `α` and `β`, if `α` is equivalent to `β` (denoted as `α ≃ β`), then the cardinality of `α` (expressed as `Nat.card α`) is equal to the cardinality of `β` (`Nat.card β`). In other words, if there is a one-to-one correspondence between two types, then they have the same cardinality.
More concisely: If two types are equivalent, they have the same cardinality.
|
Nat.card_eq_fintype_card
theorem Nat.card_eq_fintype_card : ∀ {α : Type u_1} [inst : Fintype α], Nat.card α = Fintype.card α
This theorem states that, for any type `α` that is a finite type (as indicated by `[inst : Fintype α]`), the cardinality of `α` as a natural number (`Nat.card α`) is equal to the number of elements in `α` (`Fintype.card α`). In other words, for a finite type, the number of distinct values it can take (its cardinality) is equal to the count of its elements.
More concisely: For any finite type `α`, the number of elements in `α` (`Fintype.card α`) equals its cardinality as a set (`Nat.card α`).
|
Nat.card_pos_iff
theorem Nat.card_pos_iff : ∀ {α : Type u_1}, 0 < Nat.card α ↔ Nonempty α ∧ Finite α
The theorem `Nat.card_pos_iff` states that for any type `α`, the cardinality of `α` as a natural number is greater than 0 if and only if `α` is nonempty and finite. In other words, this theorem establishes a bi-conditional relationship between a type `α` having positive cardinality and the type `α` being nonempty and finite.
More concisely: A type `α` has a positive natural number of elements if and only if it is nonempty and finite.
|
Nat.card_prod
theorem Nat.card_prod : ∀ (α : Type u_3) (β : Type u_4), Nat.card (α × β) = Nat.card α * Nat.card β
This theorem, `Nat.card_prod`, asserts that for any two types `α` and `β`, the cardinality of the Cartesian product of `α` and `β` (denoted as `α × β`) is equal to the product of the cardinalities of `α` and `β`. In Mathematical terms, if `Nat.card α` and `Nat.card β` denote the number of elements in `α` and `β` respectively, then the number of ordered pairs in the Cartesian product is `Nat.card α * Nat.card β`. However, if either `α` or `β` is infinite, then their cardinalities are defined as zero, and hence the cardinality of their Cartesian product is also zero.
More concisely: For any types `α` and `β`, the cardinality of their Cartesian product `α × β` is equal to the product of their individual cardinalities, unless one or both are infinite in which case the cardinality is zero.
|
Nat.card_image_of_injective
theorem Nat.card_image_of_injective :
∀ {α : Type u_1} {β : Type u_3} {f : α → β},
Function.Injective f → ∀ (s : Set α), Nat.card ↑(f '' s) = Nat.card ↑s
This theorem states that for any types `α` and `β` and any function `f` from `α` to `β`, if `f` is injective (meaning that different inputs always produce different outputs), then for any set `s` of elements from `α`, the cardinality of the image of `s` under `f` (denoted as `f '' s`) is equal to the cardinality of `s`. In other words, an injective function does not change the number of distinct elements when mapping a set to its image.
More concisely: If `f` is an injective function from type `α` to type `β`, then the cardinality of `f'' s` equals the cardinality of `s` for any set `s` in `α`.
|
PartENat.card_congr
theorem PartENat.card_congr : ∀ {α : Type u_3} {β : Type u_4}, α ≃ β → PartENat.card α = PartENat.card β
The theorem `PartENat.card_congr` states that for any two types `α` and `β`, if `α` is equivalent to `β` (denoted as `α ≃ β`), then the cardinality of `α` as an extended natural number (given by the function `PartENat.card α`) is equal to the cardinality of `β` as an extended natural number (`PartENat.card β`). In other words, if two types are equivalent, they have the same cardinality when measured as extended natural numbers, where the cardinality of an infinite set is represented by `⊤`.
More concisely: If two types `α` and `β` are equivalent, then their cardinalities as extended natural numbers `PartENat.card α` and `PartENat.card β` are equal.
|
Nat.card_zmod
theorem Nat.card_zmod : ∀ (n : ℕ), Nat.card (ZMod n) = n
This theorem states that for any natural number `n`, the cardinality of the set of integers modulo `n` is equal to `n` itself. It implies that there are exactly `n` distinct equivalence classes in the set of integers under modulo `n` operation. In other words, there are `n` different possible residues when dividing an integer by `n`.
More concisely: The number of integers modulo n is equal to n.
|
Nat.finite_of_card_ne_zero
theorem Nat.finite_of_card_ne_zero : ∀ {α : Type u_1}, Nat.card α ≠ 0 → Finite α
The theorem `Nat.finite_of_card_ne_zero` states that for any type `α`, if the cardinality of `α` as a natural number (i.e., `Nat.card α`) is not equal to zero, then `α` is a finite set. In other words, if a set has a non-zero cardinality when represented as a natural number, it must be finite. This follows the definition of `Nat.card`, where an infinite set has a cardinality of zero when represented as a natural number.
More concisely: If the natural number representation of the cardinality of a type `α` is non-zero, then `α` is a finite set.
|