Documentation

Mathlib.Data.Finset.Pi

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
Instances For
    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
    Instances For
      @[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
      Instances For
        @[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 : as) :
        @[simp]
        theorem Finset.pi_empty {α : Type u_1} {β : αType u} [DecidableEq α] {t : (a : α) → Finset (β a)} :
        @[simp]
        theorem Finset.pi_nonempty {α : Type u_1} {β : αType u} [DecidableEq α] {s : Finset α} {t : (a : α) → Finset (β a)} :
        (Finset.pi s t).Nonempty as, (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 : as) :
        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 : as, 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₂)