Documentation

Mathlib.Data.Finset.Pi

The cartesian product of finsets #

Main definitions #

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
    • s.pi t = { val := s.val.pi fun (a : α) => (t a).val, nodup := }
    Instances For
      @[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.

      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'
        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} {s : Finset α} {t : (a : α) → Finset (β a)} [DecidableEq α] :
        (s.pi 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) :
        (insert a s).pi t = (t a).biUnion fun (b : β a) => Finset.image (Finset.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₁ : (a : α) → Finset (β a)) (t₂ : (a : α) → Finset (β a)) (h : as, 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₁ : (a : α) → Finset (δ a)) (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.

        Equations
        Instances For
          @[simp]
          theorem Finset.mem_piDiag {α : Type u_1} {ι : Type u_2} [DecidableEq (ια)] {s : Finset α} {f : ια} :
          f s.piDiag ι as, Function.const ι a = f
          @[simp]
          theorem Finset.card_piDiag {α : Type u_1} (s : Finset α) (ι : Type u_3) [DecidableEq (ια)] [Nonempty ι] :
          (s.piDiag ι).card = s.card