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_offDiag {α : Type u_1} {s : Set α} [Fintype ↑s] [Fintype ↑s.offDiag] : s.offDiag.toFinset = s.toFinset.offDiag

@[instance_reducible]

instance instFintypeProd (α : Type u_3) (β : Type u_4) [Fintype α] [Fintype β] : Fintype (α × β)

Equations

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

@[simp]

theorem Finset.univ_product_univ {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] : univ ×ˢ univ = univ

@[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

@[simp]

theorem Fintype.card_prod (α : Type u_3) (β : Type u_4) [Fintype α] [Fintype β] : card (α × β) = card α * card β

theorem Fintype.card_product_filter_lt {α : Type u_1} [Fintype α] [LinearOrder α] : {x : α × α | x.1 < x.2}.card = (card α).choose 2

The number of strictly ordered pairs (a, b) in α is (Fintype.card α).choose 2.

@[simp]

theorem infinite_prod {α : Type u_1} {β : Type u_2} : Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

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

theorem Pi.infinite_of_exists_right {ι : Sort u_3} {π : ι → Sort u_4} (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 {ι : Sort u_3} {π : ι → Type u_4} [∀ (i : ι), Infinite (π i)] [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_3} {π : Type u_4} [Nontrivial π] [Infinite ι] : Infinite (ι → π)

Non-dependent version of Pi.infinite_of_left.

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

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