The cartesian product of finsets

Main definitions

• Finset.pi: Cartesian product of finsets indexed by a finset.

pi

def Finset.Pi.empty {α : Type u_1} (β : α → Sort u_2) (a : α) (h : a ∈ ∅) : β a

The empty dependent product function, defined on the empty set. The assumption a ∈ ∅ is never satisfied.

def Finset.pi {α : Type u_1} {β : α → Type u} [DecidableEq α] (s : Finset α) (t : (a : α) → Finset (β a)) : Finset ((a : α) → a ∈ s → β a)

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.

@[simp]

theorem Finset.pi_val {α : Type u_1} {β : α → Type u} [DecidableEq α] (s : Finset α) (t : (a : α) → Finset (β a)) : (s.pi t).val = s.val.pi fun (a : α) => (t a).val

@[simp]

theorem Finset.mem_pi {α : Type u_1} {β : α → Type u} [DecidableEq α] {s : Finset α} {t : (a : α) → Finset (β a)} {f : (a : α) → a ∈ s → β a} : f ∈ s.pi t ↔ ∀ (a : α) (h : a ∈ s), f a h ∈ t a

def Finset.Pi.cons {α : Type u_1} {δ : α → Sort v} [DecidableEq α] (s : Finset α) (a : α) (b : δ a) (f : (a : α) → a ∈ s → δ a) (a' : α) (h : a' ∈ insert a s) : δ a'

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.

@[simp]

theorem Finset.Pi.cons_same {α : Type u_1} {δ : α → Sort v} [DecidableEq α] (s : Finset α) (a : α) (b : δ a) (f : (a : α) → a ∈ s → δ a) (h : a ∈ insert a s) : cons s a b f a h = b

theorem Finset.Pi.cons_ne {α : Type u_1} {δ : α → Sort v} [DecidableEq α] {s : Finset α} {a a' : α} {b : δ a} {f : (a : α) → a ∈ s → δ a} {h : a' ∈ insert a s} (ha : a ≠ a') : cons s a b f a' h = f a' ⋯

theorem Finset.Pi.cons_injective {α : Type u_1} {δ : α → Sort v} [DecidableEq α] {a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) : Function.Injective (cons s a b)

@[simp]

theorem Finset.pi_empty {α : Type u_1} {β : α → Type u} [DecidableEq α] {t : (a : α) → Finset (β a)} : ∅.pi t = {Pi.empty β}

@[simp]

theorem Finset.pi_nonempty {α : Type u_1} {β : α → Type u} {s : Finset α} {t : (a : α) → Finset (β a)} [DecidableEq α] : (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

theorem Finset.pi_nonempty_of_forall_nonempty {α : Type u_1} {β : α → Type u} {s : Finset α} {t : (a : α) → Finset (β a)} [DecidableEq α] : (∀ a ∈ s, (t a).Nonempty) → (s.pi t).Nonempty

Alias of the reverse direction of Finset.pi_nonempty.

@[simp]

theorem Finset.pi_eq_empty {α : Type u_1} {β : α → Type u} {s : Finset α} {t : (a : α) → Finset (β a)} [DecidableEq α] : s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅

@[simp]

theorem Finset.pi_insert {α : Type u_1} {β : α → Type u} [DecidableEq α] [(a : α) → DecidableEq (β a)] {s : Finset α} {t : (a : α) → Finset (β a)} {a : α} (ha : a ∉ s) : (insert a s).pi t = (t a).biUnion fun (b : β a) => image (Pi.cons s a b) (s.pi t)

theorem Finset.pi_singletons {α : Type u_1} [DecidableEq α] {β : Type u_2} (s : Finset α) (f : α → β) : (s.pi fun (a : α) => {f a}) = {fun (a : α) (x : a ∈ s) => f a}

theorem Finset.pi_const_singleton {α : Type u_1} [DecidableEq α] {β : Type u_2} (s : Finset α) (i : β) : (s.pi fun (x : α) => {i}) = {fun (x : α) (x : x ∈ s) => i}

theorem Finset.pi_subset {α : Type u_1} {β : α → Type u} [DecidableEq α] {s : Finset α} (t₁ t₂ : (a : α) → Finset (β a)) (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.pi t₁ ⊆ s.pi t₂

theorem Finset.pi_disjoint_of_disjoint {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} {s : Finset α} (t₁ t₂ : (a : α) → Finset (δ a)) {a : α} (ha : a ∈ s) (h : Disjoint (t₁ a) (t₂ a)) : Disjoint (s.pi t₁) (s.pi t₂)

Diagonal

def Finset.piDiag {α : Type u_1} (s : Finset α) (ι : Type u_3) [DecidableEq (ι → α)] : Finset (ι → α)

The diagonal of a finset s : Finset α as a finset of functions ι → α, namely the set of constant functions valued in s.

@[simp]

theorem Finset.mem_piDiag {α : Type u_1} {ι : Type u_2} [DecidableEq (ι → α)] {s : Finset α} {f : ι → α} : f ∈ s.piDiag ι ↔ ∃ a ∈ s, Function.const ι a = f

@[simp]

theorem Finset.card_piDiag {α : Type u_1} (s : Finset α) (ι : Type u_3) [DecidableEq (ι → α)] [Nonempty ι] : (s.piDiag ι).card = s.card

Restriction

def Finset.restrict {ι : Type u_2} {π : ι → Type u_3} (s : Finset ι) (f : (i : ι) → π i) (i : { x : ι // x ∈ s }) : π ↑i

Restrict domain of a function f to a finite set s.

theorem Finset.restrict_def {ι : Type u_2} {π : ι → Type u_3} (s : Finset ι) : s.restrict = fun (f : (i : ι) → π i) (x : { x : ι // x ∈ s }) => f ↑x

theorem Set.piCongrLeft_comp_restrict {ι : Type u_2} {π : ι → Type u_3} {s : Finset ι} : ⇑(Equiv.piCongrLeft (fun (i : ↑↑s) => π ↑i) s.equivToSet.symm) ∘ (↑s).restrict = s.restrict

theorem Finset.piCongrLeft_comp_restrict {ι : Type u_2} {π : ι → Type u_3} {s : Finset ι} : ⇑(Equiv.piCongrLeft (fun (i : { x : ι // x ∈ s }) => π ↑i) s.equivToSet) ∘ s.restrict = (↑s).restrict

def Finset.restrict₂ {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} (hst : s ⊆ t) (f : (i : { x : ι // x ∈ t }) → π ↑i) (i : { x : ι // x ∈ s }) : π ↑i

If a function f is restricted to a finite set t, and s ⊆ t, this is the restriction to s.

theorem Finset.restrict₂_def {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} (hst : s ⊆ t) : restrict₂ hst = fun (f : (i : { x : ι // x ∈ t }) → π ↑i) (x : { x : ι // x ∈ s }) => f ⟨↑x, ⋯⟩

theorem Finset.restrict₂_comp_restrict {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} (hst : s ⊆ t) : restrict₂ hst ∘ t.restrict = s.restrict

theorem Finset.restrict₂_comp_restrict₂ {ι : Type u_2} {π : ι → Type u_3} {s t u : Finset ι} (hst : s ⊆ t) (htu : t ⊆ u) : restrict₂ hst ∘ restrict₂ htu = restrict₂ ⋯

theorem Finset.dependsOn_restrict {ι : Type u_2} {π : ι → Type u_3} (s : Finset ι) : DependsOn s.restrict ↑s

theorem Finset.restrict_preimage {ι : Type u_2} {π : ι → Type u_3} {s : Finset ι} [DecidablePred fun (x : ι) => x ∈ s] (t : (i : { x : ι // x ∈ s }) → Set (π ↑i)) : s.restrict ⁻¹' Set.univ.pi t = (↑s).pi fun (i : ι) => if h : i ∈ s then t ⟨i, h⟩ else Set.univ

theorem Finset.restrict₂_preimage {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} [DecidablePred fun (x : ι) => x ∈ s] (hst : s ⊆ t) (u : (i : { x : ι // x ∈ s }) → Set (π ↑i)) : restrict₂ hst ⁻¹' Set.univ.pi u = Set.univ.pi fun (j : { x : ι // x ∈ t }) => if h : ↑j ∈ s then u ⟨↑j, h⟩ else Set.univ