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 ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Fintype.piFinset_nonempty {α : Type u_1} [DecidableEq α] [Fintype α] {γ : α → Type u_3} {s : (a : α) → Finset (γ a)} : (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) → (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)) : piFinset s = Finset.univ

@[simp]

theorem Fintype.piFinset_singleton {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (f : (i : α) → δ i) : (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) : (↑(piFinset f)).Subsingleton

theorem Fintype.piFinset_disjoint_of_disjoint {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} (t₁ t₂ : (a : α) → Finset (δ a)) {a : α} (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (piFinset t₁) (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)) : (piFinset fun (a : α) => Finset.image (f a) (s a)) = Finset.image (fun (b : (a : α) → γ a) (a : α) => f a (b a)) (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) (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) (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) (piFinset fun (_i : α) => t) = t

theorem Fintype.filter_piFinset_of_notMem {α : Type u_1} [DecidableEq α] [Fintype α] {δ : α → Type u_4} [(a : α) → DecidableEq (δ a)] (t : (a : α) → Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) : {f ∈ piFinset t | f a = x} = ∅

@[deprecated Fintype.filter_piFinset_of_notMem (since := "2025-05-23")]

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) : {f ∈ piFinset t | f a = x} = ∅

Alias of Fintype.filter_piFinset_of_notMem.

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) : piFinset (Function.update s i t) = {f ∈ piFinset s | f i ∈ t}

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) : piFinset (Function.update s i {a}) = {f ∈ piFinset s | f i = a}

pi

instance Pi.instFintype {α : 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.instFintype = { elems := Fintype.piFinset fun (x : α) => Finset.univ, complete := ⋯ }

@[simp]

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

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

There are finitely many embeddings between finite types.

This instance used to be computable (using DecidableEq arguments), but it makes things a lot harder to work with here.

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)] : (univ.pi fun (a : α) => univ) = univ

Diagonal

theorem Finset.piFinset_filter_const {α : Type u_1} {ι : Type u_3} [DecidableEq (ι → α)] {s : Finset α} [DecidableEq ι] [Fintype ι] : {f ∈ Fintype.piFinset fun (x : ι) => s | ∃ a ∈ s, Function.const ι a = f} = 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

Constructors for Set.Finite

Every constructor here should have a corresponding Fintype instance in the previous section (or in the Fintype module).

The implementation of these constructors ideally should be no more than Set.toFinite, after possibly setting up some Fintype and classical Decidable instances.

theorem Set.Finite.pi {ι : Type u_3} [Finite ι] {κ : ι → Type u_4} {t : (i : ι) → Set (κ i)} (ht : ∀ (i : ι), (t i).Finite) : (univ.pi t).Finite

Finite product of finite sets is finite

theorem Set.Finite.pi' {ι : Type u_3} [Finite ι] {κ : ι → Type u_4} {t : (i : ι) → Set (κ i)} (ht : ∀ (i : ι), (t i).Finite) : {f : (i : ι) → κ i | ∀ (i : ι), f i ∈ t i}.Finite

Finite product of finite sets is finite. Note this is a variant of Set.Finite.pi without the extra i ∈ univ binder.

theorem Set.forall_finite_image_eval_iff {δ : Type u_3} [Finite δ] {κ : δ → Type u_4} {s : Set ((d : δ) → κ d)} : (∀ (d : δ), (Function.eval d '' s).Finite) ↔ s.Finite