# mathlib3documentation

data.fintype.prod

# fintype instance for the product of two fintypes. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem set.to_finset_prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) [fintype s] [fintype t] [fintype (s ×ˢ t)] :
theorem set.to_finset_off_diag {α : Type u_1} {s : set α} [decidable_eq α] [fintype s] [fintype (s.off_diag)] :
@[protected, instance]
def prod.fintype (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
fintype × β)
Equations
@[simp]
theorem finset.univ_product_univ {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] :
@[simp]
theorem fintype.card_prod (α : Type u_1) (β : Type u_2) [fintype α] [fintype β] :
fintype.card × β) =
@[simp]
theorem infinite_prod {α : Type u_1} {β : Type u_2} :
infinite × β)
@[protected, instance]
def pi.infinite_of_left {ι : Sort u_1} {π : ι Type u_2} [ (i : ι), nontrivial (π i)] [infinite ι] :
infinite (Π (i : ι), π i)
theorem pi.infinite_of_exists_right {ι : Type u_1} {π : ι Type u_2} (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.

@[protected, instance]
def pi.infinite_of_right {ι : Type u_1} {π : ι Type u_2} [ (i : ι), infinite (π i)] [nonempty ι] :
infinite (Π (i : ι), π i)

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

@[protected, instance]
def function.infinite_of_left {ι : Sort u_1} {π : Type u_2} [nontrivial π] [infinite ι] :
infinite π)

Non-dependent version of pi.infinite_of_left.

@[protected, instance]
def function.infinite_of_right {ι : Type u_1} {π : Type u_2} [infinite π] [nonempty ι] :
infinite π)

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