The cartesian product of finsets

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.

Equations

• Finset.Pi.empty β a h = Multiset.Pi.empty β a h

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.

Equations

• Finset.pi s t = { val := Multiset.pi s.val fun (a : α) => (t a).val, nodup := (_ : Multiset.Nodup (Multiset.pi s.val fun (a : α) => (t a).val)) }

@[simp]

theorem Finset.pi_val {α : Type u_1} {β : α → Type u} [DecidableEq α] (s : Finset α) (t : (a : α) → Finset (β a)) : (Finset.pi s t).val = Multiset.pi s.val 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 ∈ Finset.pi s 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.

Equations

• Finset.Pi.cons s a b f a' h = Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val)

@[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) : Finset.Pi.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') : Finset.Pi.cons s a b f a' h = f a' (_ : a' ∈ s)

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Finset.pi_singletons {α : Type u_1} [DecidableEq α] {β : Type u_2} (s : Finset α) (f : α → β) : (Finset.pi s 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 : β) : (Finset.pi s fun (x : α) => {i}) = {fun (x : α) (x : x ∈ s) => i}

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

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