Mathlib.Data.Fintype.Pi

Fintype.piFinset definition

(t : ∀ a, Finset (δ a)) : Finset (∀ a, δ a)

Full source

/-- 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). -/
def piFinset (t : ∀ a, Finset (δ a)) : Finset (∀ a, δ a) :=
  (Finset.univ.pi t).map ⟨fun f a => f a (mem_univ a), fun _ _ =>
    by simp +contextual [funext_iff]⟩

Finite product of finite sets as a finset of functions

Informal description

Given a family of finite sets $(t_a)_{a \in \alpha}$ where each $t_a$ is a finite set of elements of type $\delta a$, the finset `Fintype.piFinset t` consists of all functions $f \colon \alpha \to \bigcup_{a \in \alpha} \delta a$ such that $f(a) \in t_a$ for every $a \in \alpha$. This is analogous to the Cartesian product of the sets $(t_a)_{a \in \alpha}$ but represented as a finset of functions.

Fintype.mem_piFinset theorem

{t : ∀ a, Finset (δ a)} {f : ∀ a, δ a} : f ∈ piFinset t ↔ ∀ a, f a ∈ t a

Full source

@[simp]
theorem mem_piFinset {t : ∀ a, Finset (δ a)} {f : ∀ a, δ a} : f ∈ piFinset tf ∈ piFinset t ↔ ∀ a, f a ∈ t a := by
  constructor
  · simp only [piFinset, mem_map, and_imp, forall_prop_of_true, exists_prop, mem_univ, exists_imp,
      mem_pi]
    rintro g hg hgf a
    rw [← hgf]
    exact hg a
  · simp only [piFinset, mem_map, forall_prop_of_true, exists_prop, mem_univ, mem_pi]
    exact fun hf => ⟨fun a _ => f a, hf, rfl⟩

Membership Criterion for Finite Product of Finite Sets: $f \in \text{piFinset}\, t \leftrightarrow \forall a, f(a) \in t_a$

Informal description

For a family of finite sets $(t_a)_{a \in \alpha}$ where each $t_a$ is a finite set of elements of type $\delta a$, and a function $f \colon \alpha \to \bigcup_{a \in \alpha} \delta a$, the function $f$ belongs to the finite product set $\text{piFinset}\, t$ if and only if for every $a \in \alpha$, the value $f(a)$ is an element of $t_a$.

Fintype.coe_piFinset theorem

(t : ∀ a, Finset (δ a)) : (piFinset t : Set (∀ a, δ a)) = Set.pi Set.univ fun a => t a

Full source

@[simp]
theorem coe_piFinset (t : ∀ a, Finset (δ a)) :
    (piFinset t : Set (∀ a, δ a)) = Set.pi Set.univ fun a => t a :=
  Set.ext fun x => by
    rw [Set.mem_univ_pi]
    exact Fintype.mem_piFinset

Equality of Finite Product Set and Universal Product: $\text{piFinset}\, t = \prod_{a \in \alpha} t_a$

Informal description

For any family of finite sets $(t_a)_{a \in \alpha}$, the coercion of the finite product set $\text{piFinset}\, t$ to a set of functions is equal to the indexed product $\prod_{a \in \alpha} t_a$ over the universal set $\alpha$. In other words, the set of functions represented by $\text{piFinset}\, t$ is exactly the set of all functions $f \colon \alpha \to \bigcup_{a \in \alpha} \delta a$ such that $f(a) \in t_a$ for every $a \in \alpha$.

Fintype.piFinset_subset theorem

(t₁ t₂ : ∀ a, Finset (δ a)) (h : ∀ a, t₁ a ⊆ t₂ a) : piFinset t₁ ⊆ piFinset t₂

Full source

theorem piFinset_subset (t₁ t₂ : ∀ a, Finset (δ a)) (h : ∀ a, t₁ a ⊆ t₂ a) :
    piFinsetpiFinset t₁ ⊆ piFinset t₂ := fun _ hg => mem_piFinset.2 fun a => h a <| mem_piFinset.1 hg a

Subset Preservation in Finite Product of Finite Sets: $\text{piFinset}\, t₁ \subseteq \text{piFinset}\, t₂$ when $t₁_a \subseteq t₂_a$ for all $a$

Informal description

For any family of finite sets $(t₁_a)_{a \in \alpha}$ and $(t₂_a)_{a \in \alpha}$ where each $t₁_a$ is a subset of $t₂_a$, the finite product set $\text{piFinset}\, t₁$ is a subset of $\text{piFinset}\, t₂$.

Fintype.piFinset_eq_empty theorem

: piFinset s = ∅ ↔ ∃ i, s i = ∅

Full source

@[simp]
theorem piFinset_eq_empty : piFinsetpiFinset s = ∅ ↔ ∃ i, s i = ∅ := by simp [piFinset]

Empty Finite Product Condition: $\text{piFinset}\, s = \emptyset \leftrightarrow \exists i, s i = \emptyset$

Informal description

The finite product of finite sets `piFinset s` is empty if and only if there exists an index `i` such that the finite set `s i` is empty.

Fintype.piFinset_empty theorem

[Nonempty α] : piFinset (fun _ => ∅ : ∀ i, Finset (δ i)) = ∅

Full source

@[simp]
theorem piFinset_empty [Nonempty α] : piFinset (fun _ => ∅ : ∀ i, Finset (δ i)) = ∅ := by simp

Empty Product of Empty Finsets is Empty

Informal description

For a nonempty type $\alpha$ and a family of empty finsets $(s_i)_{i \in \alpha}$ where each $s_i$ is the empty finset of type $\delta i$, the finset of all functions $f \colon \alpha \to \bigcup_{i \in \alpha} \delta i$ such that $f(i) \in s_i$ for every $i \in \alpha$ is empty. In other words, the product finset $\prod_{i \in \alpha} \emptyset$ is empty.

Fintype.piFinset_nonempty theorem

: (piFinset s).Nonempty ↔ ∀ a, (s a).Nonempty

Full source

@[simp]
lemma piFinset_nonempty : (piFinset s).Nonempty ↔ ∀ a, (s a).Nonempty := by simp [piFinset]

Nonemptiness of Finite Product of Finite Sets

Informal description

The finite product of finite sets `piFinset s` is nonempty if and only if each finite set `s a` in the family is nonempty.

Finset.Nonempty.piFinset_const theorem

{ι : Type*} [Fintype ι] [DecidableEq ι] {s : Finset β} (hs : s.Nonempty) : (piFinset fun _ : ι ↦ s).Nonempty

Full source

lemma _root_.Finset.Nonempty.piFinset_const {ι : Type*} [Fintype ι] [DecidableEq ι] {s : Finset β}
    (hs : s.Nonempty) : (piFinset fun _ : ι ↦ s).Nonempty := piFinset_nonempty.2 fun _ ↦ hs

Nonemptiness of Constant Finite Product of Nonempty Finite Sets

Informal description

For any finite type $\iota$ with decidable equality and any nonempty finite set $s$ of type $\beta$, the finite product $\prod_{i \in \iota} s$ is nonempty.

Fintype.piFinset_of_isEmpty theorem

[IsEmpty α] (s : ∀ a, Finset (γ a)) : piFinset s = univ

Full source

@[simp]
lemma piFinset_of_isEmpty [IsEmpty α] (s : ∀ a, Finset (γ a)) : piFinset s = univ :=
  eq_univ_of_forall fun _ ↦ by simp

Finite Product of Empty Family is Universal Set

Informal description

For any empty type $\alpha$ and any family of finite sets $(s_a)_{a \in \alpha}$ where each $s_a$ is a finite subset of $\gamma a$, the finite product of these sets `piFinset s` is equal to the universal finite set `univ` (the set of all functions from $\alpha$ to $\bigcup_{a \in \alpha} \gamma a$).

Fintype.piFinset_singleton theorem

(f : ∀ i, δ i) : piFinset (fun i => {f i} : ∀ i, Finset (δ i)) = { f }

Full source

@[simp]
theorem piFinset_singleton (f : ∀ i, δ i) : piFinset (fun i => {f i} : ∀ i, Finset (δ i)) = {f} :=
  ext fun _ => by simp only [funext_iff, Fintype.mem_piFinset, mem_singleton]

Singleton Product of Singletons Equals Singleton of Function

Informal description

For any function $f \colon \prod_{i} \delta i$, the finite product of singleton sets $\{f(i)\}$ for each $i$ is equal to the singleton set $\{f\}$. In other words, $\prod_{i} \{f(i)\} = \{f\}$.

Fintype.piFinset_subsingleton theorem

 {f : ∀ i, Finset (δ i)} (hf : ∀ i, (f i : Set (δ i)).Subsingleton) : (Fintype.piFinset f : Set (∀ i, δ i)).Subsingleton

Full source

theorem piFinset_subsingleton {f : ∀ i, Finset (δ i)} (hf : ∀ i, (f i : Set (δ i)).Subsingleton) :
    (Fintype.piFinset f : Set (∀ i, δ i)).Subsingleton := fun _ ha _ hb =>
  funext fun _ => hf _ (mem_piFinset.1 ha _) (mem_piFinset.1 hb _)

Finite Product of Subsingletons is Subsingleton

Informal description

For a family of finite sets $(f_i)_{i \in I}$ where each $f_i$ is a subsingleton (i.e., contains at most one element) in the type $\delta i$, the finite product set $\prod_{i \in I} f_i$ is also a subsingleton as a subset of the function space $\forall i, \delta i$.

Fintype.piFinset_disjoint_of_disjoint theorem

(t₁ t₂ : ∀ a, Finset (δ a)) {a : α} (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (piFinset t₁) (piFinset t₂)

Full source

theorem piFinset_disjoint_of_disjoint (t₁ t₂ : ∀ a, Finset (δ a)) {a : α}
    (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (piFinset t₁) (piFinset t₂) :=
  disjoint_iff_ne.2 fun f₁ hf₁ f₂ hf₂ eq₁₂ =>
    disjoint_iff_ne.1 h (f₁ a) (mem_piFinset.1 hf₁ a) (f₂ a) (mem_piFinset.1 hf₂ a)
      (congr_fun eq₁₂ a)

Disjointness of Finite Products under Componentwise Disjointness

Informal description

For any two families of finite sets $(t₁_a)_{a \in \alpha}$ and $(t₂_a)_{a \in \alpha}$ indexed by a finite type $\alpha$, if there exists an index $a \in \alpha$ such that the sets $t₁_a$ and $t₂_a$ are disjoint, then the finite product sets $\prod_{a \in \alpha} t₁_a$ and $\prod_{a \in \alpha} t₂_a$ are also disjoint.

Fintype.piFinset_image theorem

 [∀ a, DecidableEq (δ a)] (f : ∀ a, γ a → δ a) (s : ∀ a, Finset (γ a)) :
  piFinset (fun a ↦ (s a).image (f a)) = (piFinset s).image fun b a ↦ f _ (b a)

Full source

lemma piFinset_image [∀ a, DecidableEq (δ a)] (f : ∀ a, γ a → δ a) (s : ∀ a, Finset (γ a)) :
    piFinset (fun a ↦ (s a).image (f a)) = (piFinset s).image fun b a ↦ f _ (b a) := by
  ext; simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, funext_iff]

Image of Finite Product under Componentwise Maps

Informal description

For a finite type $\alpha$ and a family of types $\delta_a$ with decidable equality for each $a \in \alpha$, given a family of functions $f_a \colon \gamma_a \to \delta_a$ and a family of finite sets $s_a \subseteq \gamma_a$ for each $a \in \alpha$, the finite product set $\prod_{a \in \alpha} f_a(s_a)$ is equal to the image of the finite product set $\prod_{a \in \alpha} s_a$ under the map $(b_a)_{a \in \alpha} \mapsto (f_a(b_a))_{a \in \alpha}$.

Fintype.eval_image_piFinset_subset theorem

(t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)] : ((piFinset t).image fun f ↦ f a) ⊆ t a

Full source

lemma eval_image_piFinset_subset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)] :
    ((piFinset t).image fun f ↦ f a) ⊆ t a := image_subset_iff.2 fun _x hx ↦ mem_piFinset.1 hx _

Image of Finite Product under Evaluation is Subset of Component

Informal description

For a family of finite sets $(t_a)_{a \in \alpha}$ indexed by a finite type $\alpha$, and for any fixed $a \in \alpha$, the image of the finite product set $\prod_{a \in \alpha} t_a$ under the evaluation map $f \mapsto f(a)$ is a subset of $t_a$.

Fintype.eval_image_piFinset theorem

 (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)] (ht : ∀ b, a ≠ b → (t b).Nonempty) :
  ((piFinset t).image fun f ↦ f a) = t a

Full source

lemma eval_image_piFinset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)]
    (ht : ∀ b, a ≠ b → (t b).Nonempty) : ((piFinset t).image fun f ↦ f a) = t a := by
  refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_
  choose f hf using ht
  exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩

Equality of Evaluation Image and Component in Finite Product of Finite Sets

Informal description

For a finite type $\alpha$ and a family of finite sets $(t_a)_{a \in \alpha}$ where each $t_a$ is a finite subset of $\delta a$, and for a fixed $a \in \alpha$, if for every $b \neq a$ the set $t_b$ is nonempty, then the image of the finite product set $\prod_{a \in \alpha} t_a$ under the evaluation map $f \mapsto f(a)$ is equal to $t_a$. In other words, under the given conditions, we have: $$\{f(a) \mid f \in \prod_{a \in \alpha} t_a\} = t_a$$

Fintype.eval_image_piFinset_const theorem

{β} [DecidableEq β] (t : Finset β) (a : α) : ((piFinset fun _i : α ↦ t).image fun f ↦ f a) = t

Full source

lemma eval_image_piFinset_const {β} [DecidableEq β] (t : Finset β) (a : α) :
    ((piFinset fun _i : α ↦ t).image fun f ↦ f a) = t := by
  obtain rfl | ht := t.eq_empty_or_nonempty
  · haveI : Nonempty α := ⟨a⟩
    simp
  · exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

Evaluation Image of Constant Finite Product Equals Component Set

Informal description

For any finite type $\alpha$, any finite set $t$ of elements of type $\beta$, and any fixed element $a \in \alpha$, the image of the finite product set $\prod_{i \in \alpha} t$ under the evaluation map $f \mapsto f(a)$ is equal to $t$. In other words, $\{f(a) \mid f \in \prod_{i \in \alpha} t\} = t$.

Fintype.filter_piFinset_of_not_mem theorem

(t : ∀ a, Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) : {f ∈ piFinset t | f a = x} = ∅

Full source

lemma filter_piFinset_of_not_mem (t : ∀ a, Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) :
    {f ∈ piFinset t | f a = x} = ∅ := by
  simp only [filter_eq_empty_iff, mem_piFinset]; rintro f hf rfl; exact hx (hf _)

Empty Filter Condition for Finite Product of Finite Sets

Informal description

Given a family of finite sets $(t_a)_{a \in \alpha}$ indexed by a type $\alpha$, where each $t_a$ is a finite subset of $\delta a$, and given an element $x \in \delta a$ such that $x \notin t_a$, the set of functions $f$ in the finite product $\prod_{a \in \alpha} t_a$ satisfying $f(a) = x$ is empty. In other words, $\{f \in \prod_{a \in \alpha} t_a \mid f(a) = x\} = \emptyset$ when $x \notin t_a$.

Fintype.piFinset_update_eq_filter_piFinset_mem theorem

 (s : ∀ i, Finset (δ i)) (i : α) {t : Finset (δ i)} (hts : t ⊆ s i) :
  piFinset (Function.update s i t) = {f ∈ piFinset s | f i ∈ t}

Full source

lemma piFinset_update_eq_filter_piFinset_mem (s : ∀ i, Finset (δ i)) (i : α) {t : Finset (δ i)}
    (hts : t ⊆ s i) : piFinset (Function.update s i t) = {f ∈ piFinset s | f i ∈ t} := by
  ext f
  simp only [mem_piFinset, mem_filter]
  refine ⟨fun h ↦ ?_, fun h j ↦ ?_⟩
  · have := by simpa using h i
    refine ⟨fun j ↦ ?_, this⟩
    obtain rfl | hji := eq_or_ne j i
    · exact hts this
    · simpa [hji] using h j
  · obtain rfl | hji := eq_or_ne j i
    · simpa using h.2
    · simpa [hji] using h.1 j

Equality between Updated Finite Product and Filtered Finite Product of Functions

Informal description

Let $\alpha$ be a finite type and $\delta \colon \alpha \to Type$ be a family of types. For each $i \in \alpha$, let $s(i)$ be a finite set of elements of type $\delta(i)$. Given an index $i \in \alpha$ and a subset $t \subseteq s(i)$, the finite product of updated sets $\prod_{j \in \alpha} s'(j)$, where $s'(j) = t$ if $j = i$ and $s'(j) = s(j)$ otherwise, is equal to the set of functions $\{f \in \prod_{j \in \alpha} s(j) \mid f(i) \in t\}$.

Fintype.piFinset_update_singleton_eq_filter_piFinset_eq theorem

 (s : ∀ i, Finset (δ i)) (i : α) {a : δ i} (ha : a ∈ s i) :
  piFinset (Function.update s i { a }) = {f ∈ piFinset s | f i = a}

Full source

lemma piFinset_update_singleton_eq_filter_piFinset_eq (s : ∀ i, Finset (δ i)) (i : α) {a : δ i}
    (ha : a ∈ s i) :
    piFinset (Function.update s i {a}) = {f ∈ piFinset s | f i = a} := by
  simp [piFinset_update_eq_filter_piFinset_mem, ha]

Equality between Updated Singleton Product and Filtered Finite Product of Functions

Informal description

Let $\alpha$ be a finite type and $\delta \colon \alpha \to Type$ be a family of types. For each $i \in \alpha$, let $s(i)$ be a finite set of elements of type $\delta(i)$. Given an index $i \in \alpha$ and an element $a \in s(i)$, the finite product of updated sets $\prod_{j \in \alpha} s'(j)$, where $s'(j) = \{a\}$ if $j = i$ and $s'(j) = s(j)$ otherwise, is equal to the set of functions $\{f \in \prod_{j \in \alpha} s(j) \mid f(i) = a\}$.

Pi.instFintype instance

{α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] : Fintype (∀ a, β a)

Full source

/-- A dependent product of fintypes, indexed by a fintype, is a fintype. -/
instance Pi.instFintype {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α]
    [∀ a, Fintype (β a)] : Fintype (∀ a, β a) :=
  ⟨Fintype.piFinset fun _ => univ, by simp⟩

Finite Product of Finite Types is Finite

Informal description

For any finite type $\alpha$ and a family of finite types $(\beta_a)_{a \in \alpha}$, the dependent function type $\forall a, \beta a$ is also finite.

Fintype.piFinset_univ theorem

 {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] :
  (Fintype.piFinset fun a : α => (Finset.univ : Finset (β a))) = (Finset.univ : Finset (∀ a, β a))

Full source

@[simp]
theorem Fintype.piFinset_univ {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α]
    [∀ a, Fintype (β a)] :
    (Fintype.piFinset fun a : α => (Finset.univ : Finset (β a))) =
      (Finset.univ : Finset (∀ a, β a)) :=
  rfl

Universal Finset of Function Space Equals Product of Universal Finsets

Informal description

For a finite type $\alpha$ and a family of finite types $(\beta_a)_{a \in \alpha}$, the finset of all functions $f \colon \alpha \to \bigcup_{a \in \alpha} \beta a$ such that $f(a) \in \text{univ}_{\beta a}$ for every $a \in \alpha$ is equal to the universal finset of the function type $\forall a, \beta a$. Here, $\text{univ}_{\beta a}$ denotes the universal finset containing all elements of $\beta a$.

Function.Embedding.fintype instance

{α β} [Fintype α] [Fintype β] : Fintype (α ↪ β)

Full source

/-- 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.
-/
noncomputable instance _root_.Function.Embedding.fintype {α β} [Fintype α] [Fintype β] :
    Fintype (α ↪ β) := by
  classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)

Finiteness of Embeddings between Finite Types

Informal description

For any finite types $\alpha$ and $\beta$, the type of embeddings $\alpha \hookrightarrow \beta$ is finite. That is, there are only finitely many injective functions from $\alpha$ to $\beta$ up to equivalence.

RelHom.instFintype instance

 {α β} [Fintype α] [Fintype β] [DecidableEq α] {r : α → α → Prop} {s : β → β → Prop} [DecidableRel r] [DecidableRel s] :
  Fintype (r →r s)

Full source

instance RelHom.instFintype {α β} [Fintype α] [Fintype β] [DecidableEq α] {r : α → α → Prop}
    {s : β → β → Prop} [DecidableRel r] [DecidableRel s] : Fintype (r →r s) :=
  Fintype.ofEquiv {f : α → β // ∀ {x y}, r x y → s (f x) (f y)} <| Equiv.mk
    (fun f ↦ ⟨f.1, f.2⟩) (fun f ↦ ⟨f.1, f.2⟩) (fun _ ↦ rfl) (fun _ ↦ rfl)

Finiteness of Relation Homomorphisms between Finite Types

Informal description

For any finite types $\alpha$ and $\beta$ with decidable equality on $\alpha$, and decidable relations $r : \alpha \to \alpha \to \text{Prop}$ and $s : \beta \to \beta \to \text{Prop}$, the type of relation homomorphisms from $r$ to $s$ is finite.

RelEmbedding.instFintype instance

{α β} [Fintype α] [Fintype β] {r : α → α → Prop} {s : β → β → Prop} : Fintype (r ↪r s)

Full source

noncomputable instance RelEmbedding.instFintype {α β} [Fintype α] [Fintype β]
    {r : α → α → Prop} {s : β → β → Prop} : Fintype (r ↪r s) :=
  Fintype.ofInjective _ RelEmbedding.toEmbedding_injective

Finiteness of Relation Embeddings between Finite Types

Informal description

For any finite types $\alpha$ and $\beta$ equipped with relations $r : \alpha \to \alpha \to \text{Prop}$ and $s : \beta \to \beta \to \text{Prop}$ respectively, the type of relation embeddings from $r$ to $s$ is finite.

Finset.univ_pi_univ theorem

 {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α] [∀ a, Fintype (β a)] :
  (Finset.univ.pi fun a : α => (Finset.univ : Finset (β a))) = Finset.univ

Full source

@[simp]
theorem Finset.univ_pi_univ {α : Type*} {β : α → Type*} [DecidableEq α] [Fintype α]
    [∀ a, Fintype (β a)] :
    (Finset.univ.pi fun a : α => (Finset.univ : Finset (β a))) = Finset.univ := by
  ext; simp

Universal Product of Finite Sets Equals Universal Finite Set for Dependent Functions

Informal description

For any finite type $\alpha$ with decidable equality and any family of finite types $(\beta_a)_{a \in \alpha}$, the Cartesian product of the universal finite sets $\prod_{a \in \alpha} \text{univ}_{\beta_a}$ is equal to the universal finite set $\text{univ}_{\forall a, \beta a}$ of the dependent function type $\forall a, \beta a$.

Finset.piFinset_filter_const theorem

[DecidableEq ι] [Fintype ι] : {f ∈ Fintype.piFinset fun _ : ι ↦ s | ∃ a ∈ s, const ι a = f} = s.piDiag ι

Full source

lemma piFinset_filter_const [DecidableEq ι] [Fintype ι] :
    {f ∈ Fintype.piFinset fun _ : ι ↦ s | ∃ a ∈ s, const ι a = f} = s.piDiag ι := by aesop

Characterization of Constant Functions in Finite Product as Diagonal Subset

Informal description

For a finite type $\iota$ with decidable equality and a finite set $s$, the subset of functions in the finite product $\prod_{i \in \iota} s$ that are constant (i.e., functions of the form $\lambda i, a$ for some $a \in s$) is equal to the diagonal subset $s^{\iota}$ (the set of all constant functions from $\iota$ to $s$).

Finset.piDiag_subset_piFinset theorem

[DecidableEq ι] [Fintype ι] : s.piDiag ι ⊆ Fintype.piFinset fun _ ↦ s

Full source

lemma piDiag_subset_piFinset [DecidableEq ι] [Fintype ι] :
    s.piDiag ι ⊆ Fintype.piFinset fun _ ↦ s := by simp [← piFinset_filter_const]

Diagonal Functions are Subset of All Functions in Finite Type

Informal description

For any finite type $\iota$ with decidable equality and any finite set $s$, the diagonal subset $s^{\text{diag}(\iota)}$ (consisting of constant functions from $\iota$ to $s$) is contained in the finset of all functions from $\iota$ to $s$, i.e., $s^{\text{diag}(\iota)} \subseteq \prod_{i \in \iota} s$.

Set.Finite.pi theorem

(ht : ∀ i, (t i).Finite) : (pi univ t).Finite

Full source

/-- Finite product of finite sets is finite -/
theorem Finite.pi (ht : ∀ i, (t i).Finite) : (pi univ t).Finite := by
  cases nonempty_fintype ι
  lift t to ∀ d, Finset (κ d) using ht
  classical
    rw [← Fintype.coe_piFinset]
    apply Finset.finite_toSet

Finiteness of Product of Finite Sets

Informal description

For any family of sets $(t_i)_{i \in \iota}$ indexed by a type $\iota$, if each set $t_i$ is finite, then the product set $\prod_{i \in \iota} t_i$ (consisting of all functions $f \colon \iota \to \bigcup_{i \in \iota} t_i$ such that $f(i) \in t_i$ for all $i \in \iota$) is finite.

Set.Finite.pi' theorem

(ht : ∀ i, (t i).Finite) : {f : ∀ i, κ i | ∀ i, f i ∈ t i}.Finite

Full source

/-- Finite product of finite sets is finite. Note this is a variant of `Set.Finite.pi` without the
extra `i ∈ univ` binder. -/
lemma Finite.pi' (ht : ∀ i, (t i).Finite) : {f : ∀ i, κ i | ∀ i, f i ∈ t i}.Finite := by
  simpa [Set.pi] using Finite.pi ht

Finiteness of Dependent Product of Finite Sets

Informal description

For any family of sets $(t_i)_{i \in \iota}$ indexed by a type $\iota$, if each set $t_i$ is finite, then the set of all functions $f \colon \iota \to \bigcup_{i \in \iota} \kappa_i$ such that $f(i) \in t_i$ for every $i \in \iota$ is finite.

Set.forall_finite_image_eval_iff theorem

{δ : Type*} [Finite δ] {κ : δ → Type*} {s : Set (∀ d, κ d)} : (∀ d, (eval d '' s).Finite) ↔ s.Finite

Full source

theorem forall_finite_image_eval_iff {δ : Type*} [Finite δ] {κ : δ → Type*} {s : Set (∀ d, κ d)} :
    (∀ d, (eval d '' s).Finite) ↔ s.Finite :=
  ⟨fun h => (Finite.pi h).subset <| subset_pi_eval_image _ _, fun h _ => h.image _⟩

Finite Evaluation Images Imply Finite Function Set

Informal description

Let $\delta$ be a finite type and $\kappa : \delta \to \text{Type}$ be a family of types. For any set $s$ of dependent functions in $\prod_{d \in \delta} \kappa(d)$, the following are equivalent: 1. For every $d \in \delta$, the image of $s$ under evaluation at $d$ (i.e., $\{f(d) \mid f \in s\}$) is finite. 2. The set $s$ itself is finite.