Fintype instances for pi types

def Fintype.piFinset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (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

• Fintype.piFinset t = Finset.map { toFun := fun (f : (a : α) → a ∈ Finset.univ → δ a) (a : α) => f a ⋯, inj' := ⋯ } (Finset.univ.pi t)

@[simp]

theorem Fintype.mem_piFinset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} {t : (a : α) → Finset (δ a)} {f : (a : α) → δ a} : f ∈ Fintype.piFinset t ↔ ∀ (a : α), f a ∈ t a

@[simp]

theorem Fintype.coe_piFinset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)) : ↑(Fintype.piFinset t) = Set.univ.pi fun (a : α) => ↑(t a)

theorem Fintype.piFinset_subset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) (h : ∀ (a : α), t₁ a ⊆ t₂ a) : Fintype.piFinset t₁ ⊆ Fintype.piFinset t₂

@[simp]

theorem Fintype.piFinset_eq_empty {α : Type u_1} [DecidableEq α] [Fintype α] {γ : α → Type u_3} {s : (a : α) → Finset (γ a)} : Fintype.piFinset s = ∅ ↔ ∃ (i : α), s i = ∅

@[simp]

theorem Fintype.piFinset_empty {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} [Nonempty α] : (Fintype.piFinset fun (x : α) => ∅) = ∅

@[simp]

theorem Fintype.piFinset_nonempty {α : Type u_1} [DecidableEq α] [Fintype α] {γ : α → Type u_3} {s : (a : α) → Finset (γ a)} : (Fintype.piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty

theorem Fintype.Aesop.piFinset_nonempty_of_forall_nonempty {α : Type u_1} [DecidableEq α] [Fintype α] {γ : α → Type u_3} {s : (a : α) → Finset (γ a)} : (∀ (a : α), (s a).Nonempty) → (Fintype.piFinset s).Nonempty

Alias of the reverse direction of Fintype.piFinset_nonempty.

theorem Finset.Nonempty.piFinset_const {β : Type u_2} {ι : Type u_5} [Fintype ι] [DecidableEq ι] {s : Finset β} (hs : s.Nonempty) : (Fintype.piFinset fun (x : ι) => s).Nonempty

@[simp]

theorem Fintype.piFinset_of_isEmpty {α : Type u_1} [DecidableEq α] [Fintype α] {γ : α → Type u_3} [IsEmpty α] (s : (a : α) → Finset (γ a)) : Fintype.piFinset s = Finset.univ

@[simp]

theorem Fintype.piFinset_singleton {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (f : (i : α) → δ i) : (Fintype.piFinset fun (i : α) => {f i}) = {f}

theorem Fintype.piFinset_subsingleton {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} {f : (i : α) → Finset (δ i)} (hf : ∀ (i : α), (↑(f i)).Subsingleton) : (↑(Fintype.piFinset f)).Subsingleton

theorem Fintype.piFinset_disjoint_of_disjoint {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) {a : α} (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (Fintype.piFinset t₁) (Fintype.piFinset t₂)

theorem Fintype.piFinset_image {α : Type u_1} [DecidableEq α] [Fintype α] {γ : α → Type u_3} {δ : α → Type u_4} [(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)) (Fintype.piFinset s)

theorem Fintype.eval_image_piFinset_subset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)) (a : α) [DecidableEq (δ a)] : Finset.image (fun (f : (a : α) → δ a) => f a) (Fintype.piFinset t) ⊆ t a

theorem Fintype.eval_image_piFinset {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)) (a : α) [DecidableEq (δ a)] (ht : ∀ (b : α), a ≠ b → (t b).Nonempty) : Finset.image (fun (f : (a : α) → δ a) => f a) (Fintype.piFinset t) = t a

theorem Fintype.eval_image_piFinset_const {α : Type u_1} [DecidableEq α] [Fintype α] {β : Type u_5} [DecidableEq β] (t : Finset β) (a : α) : Finset.image (fun (f : α → β) => f a) (Fintype.piFinset fun (_i : α) => t) = t

theorem Fintype.filter_piFinset_of_not_mem {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} [(a : α) → DecidableEq (δ a)] (t : (a : α) → Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) : Finset.filter (fun (f : (a : α) → δ a) => f a = x) (Fintype.piFinset t) = ∅

theorem Fintype.piFinset_update_eq_filter_piFinset_mem {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} [(a : α) → DecidableEq (δ a)] (s : (i : α) → Finset (δ i)) (i : α) {t : Finset (δ i)} (hts : t ⊆ s i) : Fintype.piFinset (Function.update s i t) = Finset.filter (fun (f : (a : α) → δ a) => f i ∈ t) (Fintype.piFinset s)

theorem Fintype.piFinset_update_singleton_eq_filter_piFinset_eq {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} [(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) (Fintype.piFinset s)

pi

instance Pi.fintype {α : Type u_3} {β : α → Type u_4} [DecidableEq α] [Fintype α] [(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_3} {β : α → Type u_4} [DecidableEq α] [Fintype α] [(a : α) → Fintype (β a)] : (Fintype.piFinset fun (a : α) => Finset.univ) = Finset.univ

noncomputable instance Function.Embedding.fintype {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] : Fintype (α ↪ β)

Equations

• Function.Embedding.fintype = Fintype.ofEquiv { f : α → β // Function.Injective f } (Equiv.subtypeInjectiveEquivEmbedding α β)

instance RelHom.instFintype {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] [DecidableEq α] {r : α → α → Prop} {s : β → β → Prop} [DecidableRel r] [DecidableRel s] : Fintype (r →r s)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance RelEmbedding.instFintype {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] {r : α → α → Prop} {s : β → β → Prop} : Fintype (r ↪r s)

Equations

• RelEmbedding.instFintype = Fintype.ofInjective RelEmbedding.toEmbedding ⋯

@[simp]

theorem Finset.univ_pi_univ {α : Type u_3} {β : α → Type u_4} [DecidableEq α] [Fintype α] [(a : α) → Fintype (β a)] : (Finset.univ.pi fun (a : α) => Finset.univ) = Finset.univ

Diagonal

theorem Finset.piFinset_filter_const {α : Type u_1} {ι : Type u_3} [DecidableEq (ι → α)] {s : Finset α} [DecidableEq ι] [Fintype ι] : Finset.filter (fun (f : ι → α) => ∃ a ∈ s, Function.const ι a = f) (Fintype.piFinset fun (x : ι) => s) = s.piDiag ι

theorem Finset.piDiag_subset_piFinset {α : Type u_1} {ι : Type u_3} [DecidableEq (ι → α)] {s : Finset α} [DecidableEq ι] [Fintype ι] : s.piDiag ι ⊆ Fintype.piFinset fun (x : ι) => s