mathlib3 documentation

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.

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

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

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

Non-dependent version of pi.infinite_of_left.

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