Fintype.card_prod
theorem Fintype.card_prod :
∀ (α : Type u_4) (β : Type u_5) [inst : Fintype α] [inst_1 : Fintype β],
Fintype.card (α × β) = Fintype.card α * Fintype.card β
The theorem `Fintype.card_prod` states that for any two given finite types `α` and `β`, the number of elements in the Cartesian product of the two types (represented as `(α × β)`) is equal to the product of the number of elements in `α` and the number of elements in `β`. In other words, if `α` and `β` are finite sets, then the cardinality (or size) of the Cartesian product of `α` and `β` is the product of the cardinalities of `α` and `β`.
More concisely: Given finite types `α` and `β`, the cardinality of their Cartesian product `α × β` is equal to the product of the cardinalities of `α` and `β`.
|
Pi.infinite_of_exists_right
theorem Pi.infinite_of_exists_right :
∀ {ι : Type u_4} {π : ι → Type u_5} (i : ι) [inst : Infinite (π i)] [inst : ∀ (i : ι), Nonempty (π i)],
Infinite ((i : ι) → π i)
This theorem states that if we have a type function `π` mapping from a type `ι` to another type, and at least one type `π i` is infinite, with all other types `π i` being nonempty, then the Pi type that takes an `ι` and gives back a `π i` is also infinite. Here, a Pi type is a type of functions from `ι` to `π i`, and is infinite if there is no surjection from the type to the finite type `Fin n` for any natural number `n`.
More concisely: If `π : ι → Type` has an infinite type `π i`, then the Pi type `(x : ι) → π x` is infinite.
|