fintype instance for the product of two fintypes.

theorem Set.toFinset_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [Fintype s.Elem] [Fintype t.Elem] [Fintype (SProd.sprod s t).Elem] : Eq (SProd.sprod s t).toFinset (SProd.sprod s.toFinset t.toFinset)

theorem Set.toFinset_off_diag {α : Type u_1} {s : Set α} [DecidableEq α] [Fintype s.Elem] [Fintype s.offDiag.Elem] : Eq s.offDiag.toFinset s.toFinset.offDiag

def instFintypeProd (α : Type u_4) (β : Type u_5) [Fintype α] [Fintype β] : Fintype (Prod α β)

Equations

• Eq (instFintypeProd α β) { elems := SProd.sprod Finset.univ Finset.univ, complete := ⋯ }

theorem Finset.univ_product_univ {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] : Eq (SProd.sprod univ univ) univ

theorem Finset.product_eq_univ {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {s : Finset α} {t : Finset β} [Nonempty α] [Nonempty β] : Iff (Eq (SProd.sprod s t) univ) (And (Eq s univ) (Eq t univ))

theorem Fintype.card_prod (α : Type u_4) (β : Type u_5) [Fintype α] [Fintype β] : Eq (card (Prod α β)) (HMul.hMul (card α) (card β))

theorem infinite_prod {α : Type u_1} {β : Type u_2} : Iff (Infinite (Prod α β)) (Or (And (Infinite α) (Nonempty β)) (And (Nonempty α) (Infinite β)))

theorem Pi.infinite_of_left {ι : Sort u_4} {π : ι → Type u_5} [∀ (i : ι), Nontrivial (π i)] [Infinite ι] : Infinite ((i : ι) → π i)

theorem Pi.infinite_of_exists_right {ι : Sort u_4} {π : ι → Sort u_5} (i : ι) [Infinite (π i)] [∀ (i : ι), Nonempty (π i)] : Infinite ((i : ι) → π i)

If at least one π i is infinite and the rest nonempty, the pi type of all π is infinite.

theorem Pi.infinite_of_right {ι : Sort u_4} {π : ι → Type u_5} [∀ (i : ι), Infinite (π i)] [Nonempty ι] : Infinite ((i : ι) → π i)

See Pi.infinite_of_exists_right for the case that only one π i is infinite.

theorem Function.infinite_of_left {ι : Sort u_4} {π : Type u_5} [Nontrivial π] [Infinite ι] : Infinite (ι → π)

Non-dependent version of Pi.infinite_of_left.

theorem Function.infinite_of_right {ι : Sort u_4} {π : Type u_5} [Infinite π] [Nonempty ι] : Infinite (ι → π)

Non-dependent version of Pi.infinite_of_exists_right and Pi.infinite_of_right.