fintype instance for the product of two fintypes. #
theorem
Set.toFinset_prod
{α : Type u_1}
{β : Type u_2}
(s : Set α)
(t : Set β)
[inst : Fintype ↑s]
[inst : Fintype ↑t]
[inst : Fintype ↑(s ×ˢ t)]
:
Set.toFinset (s ×ˢ t) = Set.toFinset s ×ᶠ Set.toFinset t
theorem
Set.toFinset_off_diag
{α : Type u_1}
{s : Set α}
[inst : DecidableEq α]
[inst : Fintype ↑s]
[inst : Fintype ↑(Set.offDiag s)]
:
@[simp]
theorem
Fintype.card_prod
(α : Type u_1)
(β : Type u_2)
[inst : Fintype α]
[inst : Fintype β]
:
Fintype.card (α × β) = Fintype.card α * Fintype.card β
instance
Pi.infinite_of_left
{ι : Sort u_1}
{π : ι → Type u_2}
[inst : ∀ (i : ι), Nontrivial (π i)]
[inst : Infinite ι]
:
Infinite ((i : ι) → π i)
instance
Pi.infinite_of_right
{ι : Type u_1}
{π : ι → Type u_2}
[inst : ∀ (i : ι), Infinite (π i)]
[inst : Nonempty ι]
:
Infinite ((i : ι) → π i)
See Pi.infinite_of_exists_right
for the case that only one π i
is infinite.
instance
Function.infinite_of_left
{ι : Sort u_1}
{π : Type u_2}
[inst : Nontrivial π]
[inst : Infinite ι]
:
Infinite (ι → π)
Non-dependent version of Pi.infinite_of_left
.
instance
Function.infinite_of_right
{ι : Type u_1}
{π : Type u_2}
[inst : Infinite π]
[inst : Nonempty ι]
:
Infinite (ι → π)
Non-dependent version of Pi.infinite_of_exists_right
and Pi.infinite_of_right
.