doc-next-gen

Mathlib.Data.Finset.Pi

Module docstring

{"# The cartesian product of finsets

Main definitions

  • Finset.pi: Cartesian product of finsets indexed by a finset. ","### pi ","### Diagonal ","### Restriction "}
Finset.Pi.empty definition
(β : α → Sort*) (a : α) (h : a ∈ (∅ : Finset α)) : β a
Full source 
/-- The empty dependent product function, defined on the empty set. The assumption `a ∈ ∅` is never
satisfied. -/
def Pi.empty (β : α → Sort*) (a : α) (h : a ∈ (∅ : Finset α)) : β a :=
  Multiset.Pi.empty β a h
Empty dependent function on finite sets
Informal description
The empty dependent function, defined on the empty finite set. For any type family $\beta : \alpha \to \text{Type}$ and any element $a$ in the empty finite set $\emptyset$, this function returns an element of $\beta a$. The condition $a \in \emptyset$ is never satisfied, making this function vacuously defined.
Finset.pi definition
(s : Finset α) (t : ∀ a, Finset (β a)) : Finset (∀ a ∈ s, β a)
Full source 
/-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `δ a`, then one can define the
finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
Note that the elements of `s.pi t` are only partially defined, on `s`. -/
def pi (s : Finset α) (t : ∀ a, Finset (β a)) : Finset (∀ a ∈ s, β a) :=
  ⟨s.1.pi fun a => (t a).1, s.nodup.pi fun a _ => (t a).nodup⟩
Cartesian product of finite sets
Informal description
Given a finite set $s$ of elements of type $\alpha$ and for each $a \in \alpha$ a finite set $t(a)$ of elements of type $\beta(a)$, the cartesian product $s.\text{pi}\, t$ is the finite set of all dependent functions $f$ such that for every $a \in s$, $f(a) \in t(a)$. The construction is defined by lifting the underlying multisets and ensuring the result has no duplicates.
Finset.pi_val theorem
(s : Finset α) (t : ∀ a, Finset (β a)) : (s.pi t).1 = s.1.pi fun a => (t a).1
Full source 
@[simp]
theorem pi_val (s : Finset α) (t : ∀ a, Finset (β a)) : (s.pi t).1 = s.1.pi fun a => (t a).1 :=
  rfl
Multiset Representation of Finite Cartesian Product
Informal description
For any finite set $s$ of type $\alpha$ and any family of finite sets $t(a)$ of type $\beta(a)$ indexed by $a \in \alpha$, the underlying multiset of the cartesian product $s.\text{pi}\, t$ is equal to the multiset cartesian product of the underlying multisets of $s$ and $t(a)$ for each $a \in \alpha$. In other words, the multiset underlying the finite set cartesian product is the cartesian product of the underlying multisets.
Finset.mem_pi theorem
{s : Finset α} {t : ∀ a, Finset (β a)} {f : ∀ a ∈ s, β a} : f ∈ s.pi t ↔ ∀ (a) (h : a ∈ s), f a h ∈ t a
Full source 
@[simp]
theorem mem_pi {s : Finset α} {t : ∀ a, Finset (β a)} {f : ∀ a ∈ s, β a} :
    f ∈ s.pi tf ∈ s.pi t ↔ ∀ (a) (h : a ∈ s), f a h ∈ t a :=
  Multiset.mem_pi _ _ _
Membership Criterion for Finite Cartesian Product: $f \in s.\text{pi}\, t \leftrightarrow \forall a \in s, f(a) \in t(a)$
Informal description
For any finite set $s$ of type $\alpha$ and any family of finite sets $t(a)$ of type $\beta(a)$ indexed by $a \in \alpha$, a dependent function $f$ (where $f(a) \in \beta(a)$ for each $a \in s$) belongs to the cartesian product $s.\text{pi}\, t$ if and only if for every $a \in s$ and every proof $h$ that $a \in s$, the value $f(a, h)$ is an element of $t(a)$.
Finset.Pi.cons definition
(s : Finset α) (a : α) (b : δ a) (f : ∀ a, a ∈ s → δ a) (a' : α) (h : a' ∈ insert a s) : δ a'
Full source 
/-- Given a function `f` defined on a finset `s`, define a new function on the finset `s ∪ {a}`,
equal to `f` on `s` and sending `a` to a given value `b`. This function is denoted
`s.Pi.cons a b f`. If `a` already belongs to `s`, the new function takes the value `b` at `a`
anyway. -/
def Pi.cons (s : Finset α) (a : α) (b : δ a) (f : ∀ a, a ∈ s → δ a) (a' : α) (h : a' ∈ insert a s) :
    δ a' :=
  Multiset.Pi.cons s.1 a b f _ (Multiset.mem_cons.2 <| mem_insert.symm.2 h)
Function extension for finite set cartesian product
Informal description
Given a finite set $s$ of type $\alpha$, an element $a \in \alpha$, a value $b \in \delta a$, and a function $f$ defined on $s$ such that $f(a') \in \delta a'$ for all $a' \in s$, the function $\text{Pi.cons}(s, a, b, f)$ constructs a new function defined on $s \cup \{a\}$ by: - Setting its value at $a$ to be $b$, and - Keeping its value at any $a' \in s$ to be $f(a')$. This holds even if $a$ is already in $s$, in which case the new function will still take the value $b$ at $a$.
Finset.Pi.cons_same theorem
(s : Finset α) (a : α) (b : δ a) (f : ∀ a, a ∈ s → δ a) (h : a ∈ insert a s) : Pi.cons s a b f a h = b
Full source 
@[simp]
theorem Pi.cons_same (s : Finset α) (a : α) (b : δ a) (f : ∀ a, a ∈ s → δ a) (h : a ∈ insert a s) :
    Pi.cons s a b f a h = b :=
  Multiset.Pi.cons_same _
Consistency of Function Extension in Finite Cartesian Product: $\text{Pi.cons}(s, a, b, f)(a, h) = b$
Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Type}^*$ a type family, $s$ a finite subset of $\alpha$, $a \in \alpha$, $b \in \delta a$, and $f : \forall a' \in s, \delta a'$ a function. Then the extended function $\text{Pi.cons}(s, a, b, f)$ satisfies $\text{Pi.cons}(s, a, b, f)(a, h) = b$ for any proof $h$ that $a$ is in the set $s \cup \{a\}$.
Finset.Pi.cons_ne theorem
{s : Finset α} {a a' : α} {b : δ a} {f : ∀ a, a ∈ s → δ a} {h : a' ∈ insert a s} (ha : a ≠ a') : Pi.cons s a b f a' h = f a' ((mem_insert.1 h).resolve_left ha.symm)
Full source 
theorem Pi.cons_ne {s : Finset α} {a a' : α} {b : δ a} {f : ∀ a, a ∈ s → δ a} {h : a' ∈ insert a s}
    (ha : a ≠ a') : Pi.cons s a b f a' h = f a' ((mem_insert.1 h).resolve_left ha.symm) :=
  Multiset.Pi.cons_ne _ (Ne.symm ha)
Consistency of Function Extension at Distinct Points in Finite Cartesian Product
Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Type}^*$ a type family, $s$ a finite subset of $\alpha$, $a \in \alpha$, $b \in \delta a$, and $f : \forall a' \in s, \delta a'$ a function. For any $a' \in s \cup \{a\}$ with $a' \neq a$, the extended function $\text{Pi.cons}(s, a, b, f)$ satisfies $\text{Pi.cons}(s, a, b, f)(a') = f(a')$.
Finset.Pi.cons_injective theorem
{a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) : Function.Injective (Pi.cons s a b)
Full source 
theorem Pi.cons_injective {a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) :
    Function.Injective (Pi.cons s a b) := fun e₁ e₂ eq =>
  @Multiset.Pi.cons_injective α _ δ a b s.1 hs _ _ <|
    funext fun e =>
      funext fun h =>
        have :
          Pi.cons s a b e₁ e (by simpa only [Multiset.mem_cons, mem_insert] using h) =
            Pi.cons s a b e₂ e (by simpa only [Multiset.mem_cons, mem_insert] using h) := by
          rw [eq]
        this
Injectivity of Finite Cartesian Product Extension When $a \notin s$
Informal description
Let $\alpha$ be a type, $\delta : \alpha \to \text{Type}^*$ a type family, $a \in \alpha$, $b \in \delta a$, and $s$ a finite subset of $\alpha$ such that $a \notin s$. Then the function extension operation $\text{Pi.cons}(s, a, b)$, which maps a function $f : \forall a' \in s, \delta a'$ to a new function defined on $s \cup \{a\}$ by setting its value at $a$ to $b$ and keeping other values unchanged, is injective. That is, for any two functions $f_1, f_2 : \forall a' \in s, \delta a'$, if $\text{Pi.cons}(s, a, b, f_1) = \text{Pi.cons}(s, a, b, f_2)$, then $f_1 = f_2$.
Finset.pi_empty theorem
{t : ∀ a : α, Finset (β a)} : pi (∅ : Finset α) t = singleton (Pi.empty β)
Full source 
@[simp]
theorem pi_empty {t : ∀ a : α, Finset (β a)} : pi (∅ : Finset α) t = singleton (Pi.empty β) :=
  rfl
Cartesian Product of Empty Finite Set is Singleton of Empty Function
Informal description
For any family of finite sets $\{t(a) \subseteq \beta(a)\}_{a \in \alpha}$, the cartesian product of the empty finite set $\emptyset \subseteq \alpha$ with $t$ is equal to the singleton set containing the empty dependent function $\text{Pi.empty}(\beta)$.
Finset.pi_nonempty theorem
: (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty
Full source 
@[simp]
lemma pi_nonempty : (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty := by
  simp [Finset.Nonempty, Classical.skolem]
Nonemptiness of Finite Cartesian Product $\prod_{a \in s} t(a) \neq \emptyset$ iff All $t(a) \neq \emptyset$ for $a \in s$
Informal description
The cartesian product $\prod_{a \in s} t(a)$ of finite sets is nonempty if and only if for every element $a$ in the finite set $s$, the corresponding set $t(a)$ is nonempty.
Finset.pi_eq_empty theorem
: s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅
Full source 
@[simp]
lemma pi_eq_empty : s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅ := by
  simp [← not_nonempty_iff_eq_empty]
Cartesian Product of Finite Sets is Empty iff a Component is Empty
Informal description
For a finite set $s$ of elements of type $\alpha$ and a family of finite sets $t(a)$ of elements of type $\beta(a)$ indexed by $a \in \alpha$, the cartesian product $s.\text{pi}\, t$ is empty if and only if there exists an element $a \in s$ such that $t(a)$ is empty.
Finset.pi_insert theorem
[∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, Finset (β a)} {a : α} (ha : a ∉ s) : pi (insert a s) t = (t a).biUnion fun b => (pi s t).image (Pi.cons s a b)
Full source 
@[simp]
theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, Finset (β a)} {a : α}
    (ha : a ∉ s) : pi (insert a s) t = (t a).biUnion fun b => (pi s t).image (Pi.cons s a b) := by
  apply eq_of_veq
  rw [← (pi (insert a s) t).2.dedup]
  refine
    (fun s' (h : s' = a ::ₘ s.1) =>
        (?_ :
          dedup (Multiset.pi s' fun a => (t a).1) =
            dedup
              ((t a).1.bind fun b =>
                dedup <|
                  (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' =>
                    Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
      _ (insert_val_of_not_mem ha)
  subst s'; rw [pi_cons]
  congr; funext b
  exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm
Cartesian Product Construction via Insertion: $\text{pi}(s \cup \{a\}, t) = \bigcup_{b \in t(a)} \{\text{Pi.cons}(s, a, b, f) \mid f \in \text{pi}(s, t)\}$
Informal description
Let $\alpha$ be a type with decidable equality for $\beta(a)$ for all $a \in \alpha$, $s$ be a finite subset of $\alpha$, $t : \alpha \to \text{Finset}(\beta(a))$ a family of finite sets, and $a \in \alpha$ such that $a \notin s$. Then the cartesian product $\text{pi}(\text{insert}(a, s), t)$ is equal to the union over all $b \in t(a)$ of the images of the functions $\text{Pi.cons}(s, a, b)$ applied to the cartesian product $\text{pi}(s, t)$. In other words, the cartesian product over $s \cup \{a\}$ can be constructed by: 1. For each element $b$ in $t(a)$, 2. Extending each function in $\text{pi}(s, t)$ by setting its value at $a$ to be $b$, 3. Taking the union of all such extended functions.
Finset.pi_singletons theorem
{β : Type*} (s : Finset α) (f : α → β) : (s.pi fun a => ({f a} : Finset β)) = {fun a _ => f a}
Full source 
theorem pi_singletons {β : Type*} (s : Finset α) (f : α → β) :
    (s.pi fun a => ({f a} : Finset β)) = {fun a _ => f a} := by
  rw [eq_singleton_iff_unique_mem]
  constructor
  · simp
  intro a ha
  ext i hi
  rw [mem_pi] at ha
  simpa using ha i hi
Cartesian Product of Singletons Yields Constant Function
Informal description
For any finite set $s$ of elements of type $\alpha$ and any function $f \colon \alpha \to \beta$, the cartesian product of the singleton sets $\{f(a)\}$ for each $a \in s$ is equal to the singleton set containing the constant function $\lambda a \_, f(a)$. That is, \[ \prod_{a \in s} \{f(a)\} = \{\lambda a \_, f(a)\}. \]
Finset.pi_const_singleton theorem
{β : Type*} (s : Finset α) (i : β) : (s.pi fun _ => ({ i } : Finset β)) = {fun _ _ => i}
Full source 
theorem pi_const_singleton {β : Type*} (s : Finset α) (i : β) :
    (s.pi fun _ => ({i} : Finset β)) = {fun _ _ => i} :=
  pi_singletons s fun _ => i
Cartesian Product of Constant Singletons Yields Constant Function
Informal description
For any finite set $s$ of elements of type $\alpha$ and any element $i$ of type $\beta$, the cartesian product of the singleton sets $\{i\}$ for each $a \in s$ is equal to the singleton set containing the constant function $\lambda a \_, i$. That is, \[ \prod_{a \in s} \{i\} = \{\lambda a \_, i\}. \]
Finset.pi_subset theorem
{s : Finset α} (t₁ t₂ : ∀ a, Finset (β a)) (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.pi t₁ ⊆ s.pi t₂
Full source 
theorem pi_subset {s : Finset α} (t₁ t₂ : ∀ a, Finset (β a)) (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) :
    s.pi t₁ ⊆ s.pi t₂ := fun _ hg => mem_pi.2 fun a ha => h a ha (mem_pi.mp hg a ha)
Inclusion of Finite Cartesian Products under Componentwise Subset Condition
Informal description
Let $s$ be a finite subset of a type $\alpha$, and for each $a \in \alpha$, let $t_1(a)$ and $t_2(a)$ be finite subsets of a type $\beta(a)$. If for every $a \in s$ we have $t_1(a) \subseteq t_2(a)$, then the cartesian product $\prod_{a \in s} t_1(a)$ is a subset of the cartesian product $\prod_{a \in s} t_2(a)$.
Finset.pi_disjoint_of_disjoint theorem
{δ : α → Type*} {s : Finset α} (t₁ t₂ : ∀ a, Finset (δ a)) {a : α} (ha : a ∈ s) (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (s.pi t₁) (s.pi t₂)
Full source 
theorem pi_disjoint_of_disjoint {δ : α → Type*} {s : Finset α} (t₁ t₂ : ∀ a, Finset (δ a)) {a : α}
    (ha : a ∈ s) (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (s.pi t₁) (s.pi t₂) :=
  disjoint_iff_ne.2 fun f₁ hf₁ f₂ hf₂ eq₁₂ =>
    disjoint_iff_ne.1 h (f₁ a ha) (mem_pi.mp hf₁ a ha) (f₂ a ha) (mem_pi.mp hf₂ a ha) <|
      congr_fun (congr_fun eq₁₂ a) ha
Disjointness of Cartesian Products When Components Are Disjoint
Informal description
Let $s$ be a finite set of type $\alpha$, and for each $a \in \alpha$, let $t₁(a)$ and $t₂(a)$ be finite sets of type $\delta(a)$. If for some $a \in s$, the sets $t₁(a)$ and $t₂(a)$ are disjoint (i.e., they have no common elements), then the cartesian products $\prod_{a\in s} t₁(a)$ and $\prod_{a\in s} t₂(a)$ are also disjoint.
Finset.piDiag definition
(s : Finset α) (ι : Type*) [DecidableEq (ι → α)] : Finset (ι → α)
Full source 
/-- The diagonal of a finset `s : Finset α` as a finset of functions `ι → α`, namely the set of
constant functions valued in `s`. -/
def piDiag (s : Finset α) (ι : Type*) [DecidableEq (ι → α)] : Finset (ι → α) := s.image (const ι)
Diagonal of a finite set as constant functions
Informal description
Given a finite set $s$ of type $\alpha$ and a type $\iota$, the diagonal of $s$ is the finite set of constant functions from $\iota$ to $\alpha$ where the constant value is an element of $s$. In other words, it consists of all functions $f : \iota \to \alpha$ such that there exists an element $a \in s$ with $f(i) = a$ for all $i \in \iota$.
Finset.mem_piDiag theorem
: f ∈ s.piDiag ι ↔ ∃ a ∈ s, const ι a = f
Full source 
@[simp] lemma mem_piDiag : f ∈ s.piDiag ιf ∈ s.piDiag ι ↔ ∃ a ∈ s, const ι a = f := mem_image
Characterization of Diagonal Membership via Constant Functions
Informal description
A function $f : \iota \to \alpha$ belongs to the diagonal of a finite set $s \subseteq \alpha$ if and only if there exists an element $a \in s$ such that $f$ is the constant function with value $a$ on $\iota$, i.e., $f(i) = a$ for all $i \in \iota$.
Finset.card_piDiag theorem
(s : Finset α) (ι : Type*) [DecidableEq (ι → α)] [Nonempty ι] : (s.piDiag ι).card = s.card
Full source 
@[simp] lemma card_piDiag (s : Finset α) (ι : Type*) [DecidableEq (ι → α)] [Nonempty ι] :
    (s.piDiag ι).card = s.card := by rw [piDiag, card_image_of_injective _ const_injective]
Cardinality of Diagonal Constant Functions Equals Original Set Size
Informal description
For any finite set $s$ of type $\alpha$ and any nonempty type $\iota$, the cardinality of the diagonal of $s$ (viewed as constant functions from $\iota$ to $\alpha$) equals the cardinality of $s$, i.e., $|s.\mathrm{piDiag}(\iota)| = |s|$.
Finset.restrict definition
(s : Finset ι) (f : (i : ι) → π i) : (i : s) → π i
Full source 
/-- Restrict domain of a function `f` to a finite set `s`. -/
@[simp]
def restrict (s : Finset ι) (f : (i : ι) → π i) : (i : s) → π i := fun x ↦ f x
Restriction of a function to a finite set
Informal description
Given a finite set $s$ of type $\iota$ and a function $f$ defined on $\iota$ with values in $\pi i$ for each $i \in \iota$, the restriction of $f$ to $s$ is the function that maps each element $x \in s$ to $f(x)$. In other words, for a finite subset $s \subseteq \iota$, the restriction $f|_s$ is the function from $s$ to $\prod_{i \in s} \pi i$ defined by $f|_s(x) = f(x)$ for all $x \in s$.
Finset.restrict_def theorem
(s : Finset ι) : s.restrict (π := π) = fun f x ↦ f x
Full source 
theorem restrict_def (s : Finset ι) : s.restrict (π := π) = fun f x ↦ f x := rfl
Definition of Restriction Operation on Finite Sets
Informal description
For any finite set $s$ of type $\iota$ and any family of types $\pi_i$ indexed by $\iota$, the restriction operation `s.restrict` is equal to the function that maps a function $f \colon \prod_{i \in \iota} \pi_i$ and an element $x \in s$ to $f(x)$. In other words, the restriction of $f$ to $s$ is simply the evaluation of $f$ at each point in $s$.
Set.piCongrLeft_comp_restrict theorem
: (s.equivToSet.symm.piCongrLeft (fun i : s.toSet ↦ π i)) ∘ s.toSet.restrict = s.restrict
Full source 
theorem _root_.Set.piCongrLeft_comp_restrict :
    (s.equivToSet.symm.piCongrLeft (fun i : s.toSet ↦ π i)) ∘ s.toSet.restrict = s.restrict := rfl
Compatibility of Restriction with Equivalence for Finite Sets
Informal description
Given a finite set $s$ of type $\alpha$ and a family of types $\pi_i$ indexed by $i \in \alpha$, the composition of the following two maps is equal to the restriction map from $s$ to $\prod_{i \in s} \pi_i$: 1. The restriction of a function $f \colon \prod_{i \in \alpha} \pi_i$ to the set $s$ (viewed as a subset of $\alpha$). 2. The equivalence induced by the inverse of the bijection between $s$ and its corresponding set, applied to the family $\pi_i$ for $i \in s$. In other words, the diagram commutes: the restriction operation on the finite set $s$ factors through the set-theoretic restriction via this equivalence.
Finset.piCongrLeft_comp_restrict theorem
: (s.equivToSet.piCongrLeft (fun i : s ↦ π i)) ∘ s.restrict = s.toSet.restrict
Full source 
theorem piCongrLeft_comp_restrict :
    (s.equivToSet.piCongrLeft (fun i : s ↦ π i)) ∘ s.restrict = s.toSet.restrict := rfl
Compatibility of Restriction with Equivalence between Finite Set and its Underlying Set
Informal description
For any finite set $s$ of type $\iota$ and any family of types $\pi_i$ indexed by $\iota$, the composition of the equivalence $\alpha \simeq \beta$ (where $\alpha = s$ and $\beta = s.toSet$) with the restriction operation on $s$ is equal to the restriction operation on $s.toSet$. In other words, the following diagram commutes: \[ \begin{CD} \prod_{i \in \iota} \pi_i @>{s.\text{restrict}}>> \prod_{i \in s} \pi_i \\ @V{\text{equivToSet.piCongrLeft}}VV @VV{\text{id}}V \\ \prod_{i \in s.toSet} \pi_i @>{s.toSet.\text{restrict}}>> \prod_{i \in s.toSet} \pi_i \end{CD} \] where the vertical map is the equivalence induced by the bijection between $s$ and $s.toSet$.
Finset.restrict₂ definition
(hst : s ⊆ t) (f : (i : t) → π i) (i : s) : π i
Full source 
/-- If a function `f` is restricted to a finite set `t`, and `s ⊆ t`,
this is the restriction to `s`. -/
@[simp]
def restrict₂ (hst : s ⊆ t) (f : (i : t) → π i) (i : s) : π i := f ⟨i.1, hst i.2⟩
Restriction of a function to a subset of a finite set
Informal description
Given finite sets $s$ and $t$ with $s \subseteq t$, and a function $f$ defined on $t$, the restriction of $f$ to $s$ is the function that maps each element $i \in s$ to $f(i)$, where $i$ is viewed as an element of $t$ via the inclusion $s \subseteq t$.
Finset.restrict₂_def theorem
(hst : s ⊆ t) : restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩
Full source 
theorem restrict₂_def (hst : s ⊆ t) : restrict₂ (π := π) hst = fun f x ↦ f ⟨x.1, hst x.2⟩ := rfl
Definition of Restriction Operation on Finite Subsets
Informal description
Given finite sets $s$ and $t$ with $s \subseteq t$, the restriction operation `restrict₂` (with respect to a family of types $\pi$) is defined as the function that maps any function $f$ defined on $t$ and any element $x \in s$ to $f(\langle x.1, hst x.2 \rangle)$, where $hst$ is the proof that $s \subseteq t$ and $\langle x.1, hst x.2 \rangle$ is the element $x$ viewed as an element of $t$ via the inclusion $s \subseteq t$.
Finset.restrict₂_comp_restrict theorem
(hst : s ⊆ t) : (restrict₂ (π := π) hst) ∘ t.restrict = s.restrict
Full source 
theorem restrict₂_comp_restrict (hst : s ⊆ t) :
    (restrict₂ (π := π) hst) ∘ t.restrict = s.restrict := rfl
Composition of Restriction Operators Equals Direct Restriction
Informal description
For any finite sets $s$ and $t$ with $s \subseteq t$, the composition of the restriction operator $\text{restrict}_2(h_{st})$ (which restricts functions from $t$ to $s$) with the restriction operator $t.\text{restrict}$ (which restricts functions from the full domain to $t$) equals the restriction operator $s.\text{restrict}$ (which restricts functions from the full domain directly to $s$). In other words, the following diagram commutes: $$\begin{CD} (\Pi_{i \in \iota} \pi i) @>{t.\text{restrict}}>> (\Pi_{i \in t} \pi i) \\ @V{s.\text{restrict}}VV @VV{\text{restrict}_2(h_{st})}V \\ (\Pi_{i \in s} \pi i) @= (\Pi_{i \in s} \pi i) \end{CD}$$
Finset.restrict₂_comp_restrict₂ theorem
(hst : s ⊆ t) (htu : t ⊆ u) : (restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu)
Full source 
theorem restrict₂_comp_restrict₂ (hst : s ⊆ t) (htu : t ⊆ u) :
    (restrict₂ (π := π) hst) ∘ (restrict₂ htu) = restrict₂ (hst.trans htu) := rfl
Composition of Restriction Operators Equals Transitive Restriction
Informal description
Let $s$, $t$, and $u$ be finite subsets of a type $\iota$ such that $s \subseteq t \subseteq u$. For any family of types $\pi$ indexed by $\iota$, the composition of the restriction operators $\text{restrict}_2(h_{st}) \circ \text{restrict}_2(h_{tu})$ equals the restriction operator $\text{restrict}_2(h_{su})$, where $h_{su}$ is the proof that $s \subseteq u$ obtained by transitivity from $h_{st}$ and $h_{tu}$. In other words, the following diagram commutes: $$\begin{CD} (\Pi_{i \in u} \pi i) @>{\text{restrict}_2(h_{tu})}>> (\Pi_{i \in t} \pi i) \\ @V{\text{restrict}_2(h_{su})}VV @VV{\text{restrict}_2(h_{st})}V \\ (\Pi_{i \in s} \pi i) @= (\Pi_{i \in s} \pi i) \end{CD}$$
Finset.dependsOn_restrict theorem
(s : Finset ι) : DependsOn (s.restrict (π := π)) s
Full source 
lemma dependsOn_restrict (s : Finset ι) : DependsOn (s.restrict (π := π)) s :=
  (s : Set ι).dependsOn_restrict
Restriction Function Depends Only on Finite Domain
Informal description
For any finite subset $s$ of $\iota$, the restriction function $s.\text{restrict} : (\Pi i, \pi i) \to (\Pi i \in s, \pi i)$ depends only on the variables in $s$. That is, if two functions $f$ and $g$ agree on $s$, then their restrictions $s.\text{restrict}(f)$ and $s.\text{restrict}(g)$ are equal.
Finset.restrict_preimage theorem
[DecidablePred (· ∈ s)] (t : (i : s) → Set (π i)) : s.restrict ⁻¹' (Set.univ.pi t) = Set.pi s (fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ)
Full source 
lemma restrict_preimage [DecidablePred (· ∈ s)] (t : (i : s) → Set (π i)) :
    s.restrict ⁻¹' (Set.univ.pi t) =
      Set.pi s (fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ) := by
  ext x
  simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, restrict, forall_const, Subtype.forall,
    mem_coe]
  refine ⟨fun h i hi ↦ by simpa [hi] using h i hi, fun h i hi ↦ ?_⟩
  convert h i hi
  rw [dif_pos hi]
Preimage of Product Set under Finite Restriction Equals Conditional Product Set
Informal description
Let $s$ be a finite subset of $\iota$, and for each $i \in s$, let $t_i$ be a subset of $\pi i$. Then the preimage of the product set $\prod_{i \in s} t_i$ under the restriction map $s.\text{restrict} : (\forall i, \pi i) \to \prod_{i \in s} \pi i$ is equal to the set of all functions $f : \iota \to \prod_i \pi i$ such that for each $i \in s$, $f(i) \in t_i$, and for $i \notin s$, $f(i)$ is unrestricted. In other words: $$\text{restrict}_s^{-1}\left(\prod_{i \in s} t_i\right) = \left\{f : \iota \to \prod_i \pi i \mid \forall i \in s, f(i) \in t_i\right\}$$
Finset.restrict₂_preimage theorem
[DecidablePred (· ∈ s)] (hst : s ⊆ t) (u : (i : s) → Set (π i)) : (restrict₂ hst) ⁻¹' (Set.univ.pi u) = (@Set.univ t).pi (fun j ↦ if h : j.1 ∈ s then u ⟨j.1, h⟩ else Set.univ)
Full source 
lemma restrict₂_preimage [DecidablePred (· ∈ s)] (hst : s ⊆ t) (u : (i : s) → Set (π i)) :
    (restrict₂ hst) ⁻¹' (Set.univ.pi u) =
      (@Set.univ t).pi (fun j ↦ if h : j.1 ∈ s then u ⟨j.1, h⟩ else Set.univ) := by
  ext x
  simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, restrict₂, forall_const, Subtype.forall]
  refine ⟨fun h i hi ↦ ?_, fun h i i_mem ↦ by simpa [i_mem] using h i (hst i_mem)⟩
  split_ifs with i_mem
  · exact h i i_mem
  · exact Set.mem_univ _
Preimage of Product Set under Finite Restriction Equals Conditional Product Set
Informal description
Let $s$ and $t$ be finite sets with $s \subseteq t$, and for each $i \in s$, let $u_i$ be a subset of $\pi i$. Then the preimage of the product set $\prod_{i \in s} u_i$ under the restriction map $\text{restrict}_2 : (\forall j \in t, \pi j) \to \prod_{i \in s} \pi i$ is equal to the set of all functions $f : t \to \prod_{j \in t} \pi j$ such that for each $j \in t$, if $j \in s$ then $f(j) \in u_j$, and otherwise $f(j)$ is unrestricted. In other words: $$\text{restrict}_2^{-1}\left(\prod_{i \in s} u_i\right) = \left\{f : t \to \prod_{j \in t} \pi j \mid \forall j \in s, f(j) \in u_j\right\}$$