# Fintype instances for pi types #

def Fintype.piFinset {α : Type u_1} [] [] {δ : αType u_3} (t : (a : α) → Finset (δ a)) :
Finset ((a : α) → δ a)

Given for all a : α a finset t a of δ a, then one can define the finset Fintype.piFinset 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
• = Finset.map { toFun := fun (f : (a : α) → a Finset.univδ a) (a : α) => f a , inj' := } (Finset.univ.pi t)
Instances For
@[simp]
theorem Fintype.mem_piFinset {α : Type u_1} [] [] {δ : αType u_3} {t : (a : α) → Finset (δ a)} {f : (a : α) → δ a} :
∀ (a : α), f a t a
@[simp]
theorem Fintype.coe_piFinset {α : Type u_1} [] [] {δ : αType u_3} (t : (a : α) → Finset (δ a)) :
() = Set.univ.pi fun (a : α) => (t a)
theorem Fintype.piFinset_subset {α : Type u_1} [] [] {δ : αType u_3} (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) (h : ∀ (a : α), t₁ a t₂ a) :
@[simp]
theorem Fintype.piFinset_empty {α : Type u_1} [] [] {δ : αType u_3} [] :
(Fintype.piFinset fun (x : α) => ) =
@[simp]
theorem Fintype.piFinset_nonempty {α : Type u_1} [] [] {γ : αType u_2} {s : (a : α) → Finset (γ a)} :
().Nonempty ∀ (a : α), (s a).Nonempty
@[simp]
theorem Fintype.piFinset_of_isEmpty {α : Type u_1} [] [] {γ : αType u_2} [] (s : (a : α) → Finset (γ a)) :
= Finset.univ
@[simp]
theorem Fintype.piFinset_singleton {α : Type u_1} [] [] {δ : αType u_3} (f : (i : α) → δ i) :
(Fintype.piFinset fun (i : α) => {f i}) = {f}
theorem Fintype.piFinset_subsingleton {α : Type u_1} [] [] {δ : αType u_3} {f : (i : α) → Finset (δ i)} (hf : ∀ (i : α), ((f i)).Subsingleton) :
(()).Subsingleton
theorem Fintype.piFinset_disjoint_of_disjoint {α : Type u_1} [] [] {δ : αType u_3} (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) {a : α} (h : Disjoint (t₁ a) (t₂ a)) :
Disjoint () ()
theorem Fintype.piFinset_image {α : Type u_1} [] [] {γ : αType u_2} {δ : αType u_3} [(a : α) → DecidableEq (δ a)] (f : (a : α) → γ aδ a) (s : (a : α) → Finset (γ a)) :
(Fintype.piFinset fun (a : α) => Finset.image (f a) (s a)) = Finset.image (fun (b : (a : α) → γ a) (a : α) => f a (b a)) ()
theorem Fintype.eval_image_piFinset_subset {α : Type u_1} [] [] {δ : αType u_3} (t : (a : α) → Finset (δ a)) (a : α) [DecidableEq (δ a)] :
Finset.image (fun (f : (a : α) → δ a) => f a) () t a
theorem Fintype.eval_image_piFinset {α : Type u_1} [] [] {δ : αType u_3} (t : (a : α) → Finset (δ a)) (a : α) [DecidableEq (δ a)] (ht : ∀ (b : α), a b(t b).Nonempty) :
Finset.image (fun (f : (a : α) → δ a) => f a) () = t a
theorem Fintype.eval_image_piFinset_const {α : Type u_1} [] [] {β : Type u_4} [] (t : ) (a : α) :
Finset.image (fun (f : αβ) => f a) (Fintype.piFinset fun (_i : α) => t) = t
theorem Fintype.filter_piFinset_of_not_mem {α : Type u_1} [] [] {δ : αType u_3} [(a : α) → DecidableEq (δ a)] (t : (a : α) → Finset (δ a)) (a : α) (x : δ a) (hx : xt a) :
Finset.filter (fun (x_1 : (a : α) → δ a) => x_1 a = x) () =
theorem Fintype.piFinset_update_eq_filter_piFinset_mem {α : Type u_1} [] [] {δ : αType u_3} [(a : α) → DecidableEq (δ a)] (s : (i : α) → Finset (δ i)) (i : α) {t : Finset (δ i)} (hts : t s i) :
Fintype.piFinset () = Finset.filter (fun (f : (a : α) → δ a) => f i t) ()
theorem Fintype.piFinset_update_singleton_eq_filter_piFinset_eq {α : Type u_1} [] [] {δ : αType u_3} [(a : α) → DecidableEq (δ a)] (s : (i : α) → Finset (δ i)) (i : α) {a : δ i} (ha : a s i) :
Fintype.piFinset (Function.update s i {a}) = Finset.filter (fun (f : (a : α) → δ a) => f i = a) ()

### pi #

instance Pi.fintype {α : Type u_2} {β : αType u_3} [] [] [(a : α) → Fintype (β a)] :
Fintype ((a : α) → β a)

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

Equations
• Pi.fintype = { elems := Fintype.piFinset fun (x : α) => Finset.univ, complete := }
@[simp]
theorem Fintype.piFinset_univ {α : Type u_2} {β : αType u_3} [] [] [(a : α) → Fintype (β a)] :
(Fintype.piFinset fun (a : α) => Finset.univ) = Finset.univ
noncomputable instance Function.Embedding.fintype {α : Type u_2} {β : Type u_3} [] [] :
Fintype (α β)
Equations
@[simp]
theorem Finset.univ_pi_univ {α : Type u_2} {β : αType u_3} [] [] [(a : α) → Fintype (β a)] :
(Finset.univ.pi fun (a : α) => Finset.univ) = Finset.univ