# fintype instance for the product of two fintypes. #

theorem Set.toFinset_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype (s ×ˢ t)] :
(s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset
theorem Set.toFinset_off_diag {α : Type u_1} {s : Set α} [] [Fintype s] [Fintype s.offDiag] :
s.offDiag.toFinset = s.toFinset.offDiag
instance instFintypeProd (α : Type u_4) (β : Type u_5) [] [] :
Fintype (α × β)
Equations
• = { elems := Finset.univ ×ˢ Finset.univ, complete := }
@[simp]
theorem Finset.univ_product_univ {α : Type u_1} {β : Type u_2} [] [] :
Finset.univ ×ˢ Finset.univ = Finset.univ
@[simp]
theorem Finset.product_eq_univ {α : Type u_1} {β : Type u_2} [] [] {s : } {t : } [] [] :
s ×ˢ t = Finset.univ s = Finset.univ t = Finset.univ
@[simp]
theorem Fintype.card_prod (α : Type u_4) (β : Type u_5) [] [] :
Fintype.card (α × β) =
@[simp]
theorem infinite_prod {α : Type u_1} {β : Type u_2} :
Infinite (α × β)
instance Pi.infinite_of_left {ι : Sort u_4} {π : ιType u_5} [∀ (i : ι), Nontrivial (π i)] [] :
Infinite ((i : ι) → π i)
Equations
• =
theorem Pi.infinite_of_exists_right {ι : Type u_4} {π : ιType 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.

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

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

Equations
• =
instance Function.infinite_of_left {ι : Sort u_4} {π : Type u_5} [] [] :
Infinite (ιπ)

Non-dependent version of Pi.infinite_of_left.

Equations
• =
instance Function.infinite_of_right {ι : Type u_4} {π : Type u_5} [] [] :
Infinite (ιπ)

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

Equations
• =