fintype instance for the product of two fintypes. #

theorem Set.toFinset_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) [inst : Fintype ↑s] [inst : Fintype ↑t] [inst : Fintype ↑(s ×ˢ t)] :

Set.toFinset (s ×ˢ t) = Set.toFinset s ×ᶠ Set.toFinset t

source

ink

theorem Set.toFinset_off_diag {α : Type u_1} {s : Set α} [inst : DecidableEq α] [inst : Fintype ↑s] [inst : Fintype ↑(Set.offDiag s)] :

Set.toFinset (Set.offDiag s) = Finset.offDiag (Set.toFinset s)

source

ink

instance instFintypeProd (α : Type u_1) (β : Type u_2) [inst : Fintype α] [inst : Fintype β] :

Fintype (α × β)

Equations

instFintypeProd α β = { elems := Finset.univ ×ᶠ Finset.univ, complete := (_ : ∀ (x : α × β), x ∈ Finset.univ ×ᶠ Finset.univ) }

source

ink

@[simp]

theorem Finset.univ_product_univ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] :

Finset.univ ×ᶠ Finset.univ = Finset.univ

source

ink

@[simp]

theorem Fintype.card_prod (α : Type u_1) (β : Type u_2) [inst : Fintype α] [inst : Fintype β] :

Fintype.card (α × β) = Fintype.card α * Fintype.card β

source

ink

@[simp]

theorem infinite_prod {α : Type u_2} {β : Type u_1} :

Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

source

ink

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

Infinite ((i : ι) → π i)

Equations

@Pi.infinite_of_left = @Pi.infinite_of_left.proof_1

source

ink

theorem Pi.infinite_of_exists_right {ι : Type u_1} {π : ι → Type u_2} (i : ι) [inst : Infinite (π i)] [inst : ∀ (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

ink

instance Pi.infinite_of_right {ι : Type u_1} {π : ι → Type u_2} [inst : ∀ (i : ι), Infinite (π i)] [inst : Nonempty ι] :

Infinite ((i : ι) → π i)

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

Equations

@Pi.infinite_of_right = @Pi.infinite_of_right.proof_1

source

ink

instance Function.infinite_of_left {ι : Sort u_1} {π : Type u_2} [inst : Nontrivial π] [inst : Infinite ι] :

Infinite (ι → π)

Non-dependent version of Pi.infinite_of_left.

Equations

@Function.infinite_of_left = @Function.infinite_of_left.proof_1

source

ink

instance Function.infinite_of_right {ι : Type u_1} {π : Type u_2} [inst : Infinite π] [inst : Nonempty ι] :

Infinite (ι → π)

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

Equations

@Function.infinite_of_right = @Function.infinite_of_right.proof_1