# fintype instance for the product of two fintypes. #

source
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
source
theorem Set.toFinset_off_diag {α : Type u_1} {s : Set α} [DecidableEq α] [Fintype ↑s] [Fintype ↑s.offDiag] :
s.offDiag.toFinset = s.toFinset.offDiag
source
instance instFintypeProd (α : Type u_4) (β : Type u_5) [Fintype α] [Fintype β] :
Fintype (α × β)
Equations

- instFintypeProd α β = { elems := Finset.univ ×ˢ Finset.univ, complete := ⋯ }

source
@[simp]
theorem Finset.univ_product_univ {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] :
univ ×ˢ univ = univ
source
@[simp]
theorem Finset.product_eq_univ {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {s : Finset α} {t : Finset β} [Nonempty α] [Nonempty β] :
s ×ˢ t = univ ↔ s = univ ∧ t = univ
source
@[simp]
theorem Fintype.card_prod (α : Type u_4) (β : Type u_5) [Fintype α] [Fintype β] :
card (α × β) = card α * card β
source
@[simp]
theorem infinite_prod {α : Type u_1} {β : Type u_2} :
Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β
source
instance Pi.infinite_of_left {ι : Sort u_4} {π : ι → Type u_5} [∀ (i : ι), Nontrivial (π i)] [Infinite ι] :
Infinite ((i : ι) → π i)
source
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.

source
instance 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.

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

Non-dependent version of `Pi.infinite_of_left`.

source
instance 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`.