data.fintype.pi

# fintype instances for pi types #

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

def fintype.pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} (t : Π (a : α), finset (δ a)) :
finset (Π (a : α), δ a)

Given for all a : α a finset t a of δ a, then one can define the finset fintype.pi_finset t of all functions taking values in t a for all a. This is the analogue of finset.pi where the base finset is univ (but formally they are not the same, as there is an additional condition i ∈ finset.univ in the finset.pi definition).

Equations
@[simp]
theorem fintype.mem_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a} :
(a : α), f a t a
@[simp]
theorem fintype.coe_pi_finset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} (t : Π (a : α), finset (δ a)) :
= set.univ.pi (λ (a : α), (t a))
theorem fintype.pi_finset_subset {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} (t₁ t₂ : Π (a : α), finset (δ a)) (h : (a : α), t₁ a t₂ a) :
@[simp]
theorem fintype.pi_finset_empty {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} [nonempty α] :
fintype.pi_finset (λ (_x : α), ) =
@[simp]
theorem fintype.pi_finset_singleton {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} (f : Π (i : α), δ i) :
fintype.pi_finset (λ (i : α), {f i}) = {f}
theorem fintype.pi_finset_subsingleton {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} {f : Π (i : α), finset (δ i)} (hf : (i : α), (f i).subsingleton) :
theorem fintype.pi_finset_disjoint_of_disjoint {α : Type u_1} [decidable_eq α] [fintype α] {δ : α Type u_2} (t₁ t₂ : Π (a : α), finset (δ a)) {a : α} (h : disjoint (t₁ a) (t₂ a)) :

### pi #

@[protected, instance]
def pi.fintype {α : Type u_1} {β : α Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
fintype (Π (a : α), β a)

A dependent product of fintypes, indexed by a fintype, is a fintype.

Equations
@[simp]
theorem fintype.pi_finset_univ {α : Type u_1} {β : α Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :
@[protected, instance]
def function.embedding.fintype {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] :
fintype β)
Equations
@[simp]
theorem finset.univ_pi_univ {α : Type u_1} {β : α Type u_2} [decidable_eq α] [fintype α] [Π (a : α), fintype (β a)] :