Documentation

Mathlib.Data.Multiset.Pi

The cartesian product of multisets #

Main definitions #

def Multiset.Pi.empty {α : Type u_1} (δ : αSort u_3) (a : α) :
a 0δ a

Given δ : α → Sort*, Pi.empty δ is the trivial dependent function out of the empty multiset.

Equations
    Instances For
      def Multiset.Pi.cons {α : Type u_1} [DecidableEq α] {δ : αSort u_2} (m : Multiset α) (a : α) (b : δ a) (f : (a : α) → a mδ a) (a' : α) :
      a' a ::ₘ mδ a'

      Given δ : α → Sort*, a multiset m and a term a, as well as a term b : δ a and a function f such that f a' : δ a' for all a' in m, Pi.cons m a b f is a function g such that g a'' : δ a'' for all a'' in a ::ₘ m.

      Equations
      Instances For
        theorem Multiset.Pi.cons_same {α : Type u_1} [DecidableEq α] {δ : αSort u_2} {m : Multiset α} {a : α} {b : δ a} {f : (a : α) → a mδ a} (h : a a ::ₘ m) :
        Multiset.Pi.cons m a b f a h = b
        theorem Multiset.Pi.cons_ne {α : Type u_1} [DecidableEq α] {δ : αSort u_2} {m : Multiset α} {a : α} {a' : α} {b : δ a} {f : (a : α) → a mδ a} (h' : a' a ::ₘ m) (h : a' a) :
        Multiset.Pi.cons m a b f a' h' = f a'
        theorem Multiset.Pi.cons_swap {α : Type u_1} [DecidableEq α] {δ : αSort u_2} {a : α} {a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : (a : α) → a mδ a} (h : a a') :
        HEq (Multiset.Pi.cons (a' ::ₘ m) a b (Multiset.Pi.cons m a' b' f)) (Multiset.Pi.cons (a ::ₘ m) a' b' (Multiset.Pi.cons m a b f))
        @[simp]
        theorem Multiset.Pi.cons_eta {α : Type u_1} [DecidableEq α] {δ : αSort u_2} {m : Multiset α} {a : α} (f : (a' : α) → a' a ::ₘ mδ a') :
        (Multiset.Pi.cons m a (f a ) fun (a' : α) (ha' : a' m) => f a' ) = f
        theorem Multiset.Pi.cons_map {α : Type u_1} [DecidableEq α] {δ : αSort u_2} {m : Multiset α} {a : α} (b : δ a) (f : (a' : α) → a' mδ a') {δ' : αSort u_3} (φ : a' : α⦄ → δ a'δ' a') :
        (Multiset.Pi.cons m a (φ b) fun (a' : α) (ha' : a' m) => φ (f a' ha')) = fun (a' : α) (ha' : a' a ::ₘ m) => φ (Multiset.Pi.cons m a b f a' ha')
        theorem Multiset.Pi.forall_rel_cons_ext {α : Type u_1} [DecidableEq α] {δ : αSort u_2} {m : Multiset α} {a : α} {r : a : α⦄ → δ aδ aProp} {b₁ : δ a✝} {b₂ : δ a✝} {f₁ : (a' : α) → a' mδ a'} {f₂ : (a' : α) → a' mδ a'} (hb : r b₁ b₂) (hf : ∀ (a : α) (ha : a m), r (f₁ a ha) (f₂ a ha)) (a : α) (ha : a a✝ ::ₘ m) :
        r (Multiset.Pi.cons m a✝ b₁ f₁ a ha) (Multiset.Pi.cons m a✝ b₂ f₂ a ha)
        theorem Multiset.Pi.cons_injective {α : Type u_1} [DecidableEq α] {δ : αSort u_2} {a : α} {b : δ a} {s : Multiset α} (hs : as) :
        def Multiset.pi {α : Type u_1} [DecidableEq α] {β : αType u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) :
        Multiset ((a : α) → a mβ a)

        pi m t constructs the Cartesian product over t indexed by m.

        Equations
        Instances For
          @[simp]
          theorem Multiset.pi_zero {α : Type u_1} [DecidableEq α] {β : αType u_2} (t : (a : α) → Multiset (β a)) :
          @[simp]
          theorem Multiset.pi_cons {α : Type u_1} [DecidableEq α] {β : αType u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) (a : α) :
          (a ::ₘ m).pi t = (t a).bind fun (b : β a) => Multiset.map (Multiset.Pi.cons m a b) (m.pi t)
          theorem Multiset.card_pi {α : Type u_1} [DecidableEq α] {β : αType u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) :
          Multiset.card (m.pi t) = (Multiset.map (fun (a : α) => Multiset.card (t a)) m).prod
          theorem Multiset.Nodup.pi {α : Type u_1} [DecidableEq α] {β : αType u_2} {s : Multiset α} {t : (a : α) → Multiset (β a)} :
          s.Nodup(∀ as, (t a).Nodup)(s.pi t).Nodup
          theorem Multiset.mem_pi {α : Type u_1} [DecidableEq α] {β : αType u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) (f : (a : α) → a mβ a) :
          f m.pi t ∀ (a : α) (h : a m), f a h t a