Documentation

Mathlib.Data.Multiset.ZeroCons

Definition of 0 and ::ₘ #

This file defines constructors for multisets:

It also defines the following predicates on multisets:

Notation #

Main results #

Empty multiset #

def Multiset.zero {α : Type u_1} :

0 : Multiset α is the empty set

Equations
    Instances For
      instance Multiset.instZero {α : Type u_1} :
      Equations
        Equations
          Equations
            @[simp]
            theorem Multiset.coe_nil {α : Type u_1} :
            [] = 0
            @[simp]
            theorem Multiset.empty_eq_zero {α : Type u_1} :
            = 0
            @[simp]
            theorem Multiset.coe_eq_zero {α : Type u_1} (l : List α) :
            l = 0 l = []
            theorem Multiset.coe_eq_zero_iff_isEmpty {α : Type u_1} (l : List α) :
            l = 0 l.isEmpty = true

            Multiset.cons #

            def Multiset.cons {α : Type u_1} (a : α) (s : Multiset α) :

            cons a s is the multiset which contains s plus one more instance of a.

            Equations
              Instances For

                cons a s is the multiset which contains s plus one more instance of a.

                Equations
                  Instances For
                    instance Multiset.instInsert {α : Type u_1} :
                    Equations
                      @[simp]
                      theorem Multiset.insert_eq_cons {α : Type u_1} (a : α) (s : Multiset α) :
                      insert a s = a ::ₘ s
                      @[simp]
                      theorem Multiset.cons_coe {α : Type u_1} (a : α) (l : List α) :
                      a ::ₘ l = ↑(a :: l)
                      @[simp]
                      theorem Multiset.cons_inj_left {α : Type u_1} {a b : α} (s : Multiset α) :
                      a ::ₘ s = b ::ₘ s a = b
                      @[simp]
                      theorem Multiset.cons_inj_right {α : Type u_1} (a : α) {s t : Multiset α} :
                      a ::ₘ s = a ::ₘ t s = t
                      theorem Multiset.induction {α : Type u_1} {p : Multiset αProp} (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p sp (a ::ₘ s)) (s : Multiset α) :
                      p s
                      theorem Multiset.induction_on {α : Type u_1} {p : Multiset αProp} (s : Multiset α) (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p sp (a ::ₘ s)) :
                      p s
                      theorem Multiset.cons_swap {α : Type u_1} (a b : α) (s : Multiset α) :
                      a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s
                      def Multiset.rec {α : Type u_1} {C : Multiset αSort u_3} (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) C_cons a' (a ::ₘ m) (C_cons a m b)) (m : Multiset α) :
                      C m

                      Dependent recursor on multisets. TODO: should be @[recursor 6], but then the definition of Multiset.pi fails with a stack overflow in whnf.

                      Equations
                        Instances For
                          def Multiset.recOn {α : Type u_1} {C : Multiset αSort u_3} (m : Multiset α) (C_0 : C 0) (C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)) (C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) C_cons a' (a ::ₘ m) (C_cons a m b)) :
                          C m

                          Companion to Multiset.rec with more convenient argument order.

                          Equations
                            Instances For
                              @[simp]
                              theorem Multiset.recOn_0 {α : Type u_1} {C : Multiset αSort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) C_cons a' (a ::ₘ m) (C_cons a m b)} :
                              Multiset.recOn 0 C_0 C_cons C_cons_heq = C_0
                              @[simp]
                              theorem Multiset.recOn_cons {α : Type u_1} {C : Multiset αSort u_3} {C_0 : C 0} {C_cons : (a : α) → (m : Multiset α) → C mC (a ::ₘ m)} {C_cons_heq : ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) C_cons a' (a ::ₘ m) (C_cons a m b)} (a : α) (m : Multiset α) :
                              (a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq)
                              @[simp]
                              theorem Multiset.mem_cons {α : Type u_1} {a b : α} {s : Multiset α} :
                              a b ::ₘ s a = b a s
                              theorem Multiset.mem_cons_of_mem {α : Type u_1} {a b : α} {s : Multiset α} (h : a s) :
                              a b ::ₘ s
                              theorem Multiset.mem_cons_self {α : Type u_1} (a : α) (s : Multiset α) :
                              a a ::ₘ s
                              theorem Multiset.forall_mem_cons {α : Type u_1} {p : αProp} {a : α} {s : Multiset α} :
                              (∀ (x : α), x a ::ₘ sp x) p a ∀ (x : α), x sp x
                              theorem Multiset.exists_cons_of_mem {α : Type u_1} {s : Multiset α} {a : α} :
                              a s (t : Multiset α), s = a ::ₘ t
                              @[simp]
                              theorem Multiset.notMem_zero {α : Type u_1} (a : α) :
                              ¬a 0
                              @[deprecated Multiset.notMem_zero (since := "2025-05-23")]
                              theorem Multiset.not_mem_zero {α : Type u_1} (a : α) :
                              ¬a 0

                              Alias of Multiset.notMem_zero.

                              theorem Multiset.eq_zero_of_forall_notMem {α : Type u_1} {s : Multiset α} :
                              (∀ (x : α), ¬x s)s = 0
                              @[deprecated Multiset.eq_zero_of_forall_notMem (since := "2025-05-23")]
                              theorem Multiset.eq_zero_of_forall_not_mem {α : Type u_1} {s : Multiset α} :
                              (∀ (x : α), ¬x s)s = 0

                              Alias of Multiset.eq_zero_of_forall_notMem.

                              theorem Multiset.eq_zero_iff_forall_notMem {α : Type u_1} {s : Multiset α} :
                              s = 0 ∀ (a : α), ¬a s
                              @[deprecated Multiset.eq_zero_iff_forall_notMem (since := "2025-05-23")]
                              theorem Multiset.eq_zero_iff_forall_not_mem {α : Type u_1} {s : Multiset α} :
                              s = 0 ∀ (a : α), ¬a s

                              Alias of Multiset.eq_zero_iff_forall_notMem.

                              theorem Multiset.exists_mem_of_ne_zero {α : Type u_1} {s : Multiset α} :
                              s 0 (a : α), a s
                              theorem Multiset.empty_or_exists_mem {α : Type u_1} (s : Multiset α) :
                              s = 0 (a : α), a s
                              @[simp]
                              theorem Multiset.zero_ne_cons {α : Type u_1} {a : α} {m : Multiset α} :
                              0 a ::ₘ m
                              @[simp]
                              theorem Multiset.cons_ne_zero {α : Type u_1} {a : α} {m : Multiset α} :
                              a ::ₘ m 0
                              theorem Multiset.cons_eq_cons {α : Type u_1} {a b : α} {as bs : Multiset α} :
                              a ::ₘ as = b ::ₘ bs a = b as = bs a b (cs : Multiset α), as = b ::ₘ cs bs = a ::ₘ cs

                              Singleton #

                              instance Multiset.instSingleton {α : Type u_1} :
                              Equations
                                @[simp]
                                theorem Multiset.cons_zero {α : Type u_1} (a : α) :
                                a ::ₘ 0 = {a}
                                @[simp]
                                theorem Multiset.coe_singleton {α : Type u_1} (a : α) :
                                [a] = {a}
                                @[simp]
                                theorem Multiset.mem_singleton {α : Type u_1} {a b : α} :
                                b {a} b = a
                                theorem Multiset.mem_singleton_self {α : Type u_1} (a : α) :
                                a {a}
                                @[simp]
                                theorem Multiset.singleton_inj {α : Type u_1} {a b : α} :
                                {a} = {b} a = b
                                @[simp]
                                theorem Multiset.coe_eq_singleton {α : Type u_1} {l : List α} {a : α} :
                                l = {a} l = [a]
                                @[simp]
                                theorem Multiset.singleton_eq_cons_iff {α : Type u_1} {a b : α} (m : Multiset α) :
                                {a} = b ::ₘ m a = b m = 0
                                theorem Multiset.pair_comm {α : Type u_1} (x y : α) :
                                {x, y} = {y, x}

                                Multiset.Subset #

                                @[simp]
                                theorem Multiset.zero_subset {α : Type u_1} (s : Multiset α) :
                                0 s
                                theorem Multiset.subset_cons {α : Type u_1} (s : Multiset α) (a : α) :
                                s a ::ₘ s
                                theorem Multiset.ssubset_cons {α : Type u_1} {s : Multiset α} {a : α} (ha : ¬a s) :
                                s a ::ₘ s
                                @[simp]
                                theorem Multiset.cons_subset {α : Type u_1} {a : α} {s t : Multiset α} :
                                a ::ₘ s t a t s t
                                theorem Multiset.cons_subset_cons {α : Type u_1} {a : α} {s t : Multiset α} :
                                s ta ::ₘ s a ::ₘ t
                                theorem Multiset.eq_zero_of_subset_zero {α : Type u_1} {s : Multiset α} (h : s 0) :
                                s = 0
                                @[simp]
                                theorem Multiset.subset_zero {α : Type u_1} {s : Multiset α} :
                                s 0 s = 0
                                @[simp]
                                theorem Multiset.zero_ssubset {α : Type u_1} {s : Multiset α} :
                                0 s s 0
                                @[simp]
                                theorem Multiset.singleton_subset {α : Type u_1} {s : Multiset α} {a : α} :
                                {a} s a s
                                theorem Multiset.induction_on' {α : Type u_1} {p : Multiset αProp} (S : Multiset α) (h₁ : p 0) (h₂ : ∀ {a : α} {s : Multiset α}, a Ss Sp sp (insert a s)) :
                                p S

                                Partial order on Multisets #

                                theorem Multiset.zero_le {α : Type u_1} (s : Multiset α) :
                                0 s
                                instance Multiset.instOrderBot {α : Type u_1} :
                                Equations
                                  @[simp]
                                  theorem Multiset.bot_eq_zero {α : Type u_1} :
                                  = 0

                                  This is a rfl and simp version of bot_eq_zero.

                                  theorem Multiset.le_zero {α : Type u_1} {s : Multiset α} :
                                  s 0 s = 0
                                  theorem Multiset.lt_cons_self {α : Type u_1} (s : Multiset α) (a : α) :
                                  s < a ::ₘ s
                                  theorem Multiset.le_cons_self {α : Type u_1} (s : Multiset α) (a : α) :
                                  s a ::ₘ s
                                  theorem Multiset.cons_le_cons_iff {α : Type u_1} {s t : Multiset α} (a : α) :
                                  a ::ₘ s a ::ₘ t s t
                                  theorem Multiset.cons_le_cons {α : Type u_1} {s t : Multiset α} (a : α) :
                                  s ta ::ₘ s a ::ₘ t
                                  @[simp]
                                  theorem Multiset.cons_lt_cons_iff {α : Type u_1} {s t : Multiset α} {a : α} :
                                  a ::ₘ s < a ::ₘ t s < t
                                  theorem Multiset.cons_lt_cons {α : Type u_1} {s t : Multiset α} (a : α) (h : s < t) :
                                  a ::ₘ s < a ::ₘ t
                                  theorem Multiset.le_cons_of_notMem {α : Type u_1} {s t : Multiset α} {a : α} (m : ¬a s) :
                                  s a ::ₘ t s t
                                  @[deprecated Multiset.le_cons_of_notMem (since := "2025-05-23")]
                                  theorem Multiset.le_cons_of_not_mem {α : Type u_1} {s t : Multiset α} {a : α} (m : ¬a s) :
                                  s a ::ₘ t s t

                                  Alias of Multiset.le_cons_of_notMem.

                                  theorem Multiset.cons_le_of_notMem {α : Type u_1} {s t : Multiset α} {a : α} (hs : ¬a s) :
                                  a ::ₘ s t a t s t
                                  @[deprecated Multiset.cons_le_of_notMem (since := "2025-05-23")]
                                  theorem Multiset.cons_le_of_not_mem {α : Type u_1} {s t : Multiset α} {a : α} (hs : ¬a s) :
                                  a ::ₘ s t a t s t

                                  Alias of Multiset.cons_le_of_notMem.

                                  @[simp]
                                  theorem Multiset.singleton_ne_zero {α : Type u_1} (a : α) :
                                  {a} 0
                                  @[simp]
                                  theorem Multiset.zero_ne_singleton {α : Type u_1} (a : α) :
                                  0 {a}
                                  @[simp]
                                  theorem Multiset.singleton_le {α : Type u_1} {a : α} {s : Multiset α} :
                                  {a} s a s
                                  @[simp]
                                  theorem Multiset.le_singleton {α : Type u_1} {s : Multiset α} {a : α} :
                                  s {a} s = 0 s = {a}
                                  @[simp]
                                  theorem Multiset.lt_singleton {α : Type u_1} {s : Multiset α} {a : α} :
                                  s < {a} s = 0
                                  @[simp]
                                  theorem Multiset.ssubset_singleton_iff {α : Type u_1} {s : Multiset α} {a : α} :
                                  s {a} s = 0

                                  Cardinality #

                                  @[simp]
                                  theorem Multiset.card_zero {α : Type u_1} :
                                  card 0 = 0
                                  @[simp]
                                  theorem Multiset.card_cons {α : Type u_1} (a : α) (s : Multiset α) :
                                  (a ::ₘ s).card = s.card + 1
                                  @[simp]
                                  theorem Multiset.card_singleton {α : Type u_1} (a : α) :
                                  {a}.card = 1
                                  theorem Multiset.card_pair {α : Type u_1} (a b : α) :
                                  {a, b}.card = 2
                                  theorem Multiset.card_eq_one {α : Type u_1} {s : Multiset α} :
                                  s.card = 1 (a : α), s = {a}
                                  theorem Multiset.lt_iff_cons_le {α : Type u_1} {s t : Multiset α} :
                                  s < t (a : α), a ::ₘ s t
                                  @[simp]
                                  theorem Multiset.card_eq_zero {α : Type u_1} {s : Multiset α} :
                                  s.card = 0 s = 0
                                  theorem Multiset.card_pos {α : Type u_1} {s : Multiset α} :
                                  0 < s.card s 0
                                  theorem Multiset.card_pos_iff_exists_mem {α : Type u_1} {s : Multiset α} :
                                  0 < s.card (a : α), a s
                                  theorem Multiset.card_eq_two {α : Type u_1} {s : Multiset α} :
                                  s.card = 2 (x : α), (y : α), s = {x, y}
                                  theorem Multiset.card_eq_three {α : Type u_1} {s : Multiset α} :
                                  s.card = 3 (x : α), (y : α), (z : α), s = {x, y, z}

                                  Map for partial functions #

                                  @[simp]
                                  theorem Multiset.pmap_zero {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (h : ∀ (a : α), a 0p a) :
                                  pmap f 0 h = 0
                                  @[simp]
                                  theorem Multiset.pmap_cons {α : Type u_1} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (a : α) (m : Multiset α) (h : ∀ (b : α), b a ::ₘ mp b) :
                                  pmap f (a ::ₘ m) h = f a ::ₘ pmap f m
                                  @[simp]
                                  theorem Multiset.attach_zero {α : Type u_1} :
                                  attach 0 = 0

                                  Lift a relation to Multisets #

                                  inductive Multiset.Rel {α : Type u_1} {β : Type v} (r : αβProp) :
                                  Multiset αMultiset βProp

                                  Rel r s t -- lift the relation r between two elements to a relation between s and t, s.t. there is a one-to-one mapping between elements in s and t following r.

                                  Instances For
                                    theorem Multiset.rel_iff {α : Type u_1} {β : Type v} (r : αβProp) (a✝ : Multiset α) (a✝¹ : Multiset β) :
                                    Rel r a✝ a✝¹ a✝ = 0 a✝¹ = 0 (a : α), (b : β), (as : Multiset α), (bs : Multiset β), r a b Rel r as bs a✝ = a ::ₘ as a✝¹ = b ::ₘ bs
                                    theorem Multiset.rel_flip {α : Type u_1} {β : Type v} {r : αβProp} {s : Multiset β} {t : Multiset α} :
                                    Rel (flip r) s t Rel r t s
                                    theorem Multiset.rel_refl_of_refl_on {α : Type u_1} {m : Multiset α} {r : ααProp} :
                                    (∀ (x : α), x mr x x)Rel r m m
                                    theorem Multiset.rel_eq_refl {α : Type u_1} {s : Multiset α} :
                                    Rel (fun (x1 x2 : α) => x1 = x2) s s
                                    theorem Multiset.rel_eq {α : Type u_1} {s t : Multiset α} :
                                    Rel (fun (x1 x2 : α) => x1 = x2) s t s = t
                                    theorem Multiset.Rel.mono {α : Type u_1} {β : Type v} {r p : αβProp} {s : Multiset α} {t : Multiset β} (hst : Rel r s t) (h : ∀ (a : α), a s∀ (b : β), b tr a bp a b) :
                                    Rel p s t
                                    theorem Multiset.rel_flip_eq {α : Type u_1} {s t : Multiset α} :
                                    Rel (fun (a b : α) => b = a) s t s = t
                                    @[simp]
                                    theorem Multiset.rel_zero_left {α : Type u_1} {β : Type v} {r : αβProp} {b : Multiset β} :
                                    Rel r 0 b b = 0
                                    @[simp]
                                    theorem Multiset.rel_zero_right {α : Type u_1} {β : Type v} {r : αβProp} {a : Multiset α} :
                                    Rel r a 0 a = 0
                                    theorem Multiset.rel_cons_left {α : Type u_1} {β : Type v} {r : αβProp} {a : α} {as : Multiset α} {bs : Multiset β} :
                                    Rel r (a ::ₘ as) bs (b : β), (bs' : Multiset β), r a b Rel r as bs' bs = b ::ₘ bs'
                                    theorem Multiset.rel_cons_right {α : Type u_1} {β : Type v} {r : αβProp} {as : Multiset α} {b : β} {bs : Multiset β} :
                                    Rel r as (b ::ₘ bs) (a : α), (as' : Multiset α), r a b Rel r as' bs as = a ::ₘ as'
                                    theorem Multiset.card_eq_card_of_rel {α : Type u_1} {β : Type v} {r : αβProp} {s : Multiset α} {t : Multiset β} (h : Rel r s t) :
                                    s.card = t.card
                                    theorem Multiset.exists_mem_of_rel_of_mem {α : Type u_1} {β : Type v} {r : αβProp} {s : Multiset α} {t : Multiset β} (h : Rel r s t) {a : α} :
                                    a s (b : β), b t r a b
                                    theorem Multiset.rel_of_forall {α : Type u_1} {m1 m2 : Multiset α} {r : ααProp} (h : ∀ (a b : α), a m1b m2r a b) (hc : m1.card = m2.card) :
                                    Rel r m1 m2
                                    theorem Multiset.Rel.trans {α : Type u_1} (r : ααProp) [IsTrans α r] {s t u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u) :
                                    Rel r s u
                                    @[simp]
                                    theorem Multiset.pairwise_zero {α : Type u_1} (r : ααProp) :
                                    @[simp]
                                    theorem Multiset.nodup_zero {α : Type u_1} :
                                    @[simp]
                                    theorem Multiset.nodup_cons {α : Type u_1} {a : α} {s : Multiset α} :
                                    theorem Multiset.Nodup.cons {α : Type u_1} {s : Multiset α} {a : α} (m : ¬a s) (n : s.Nodup) :
                                    (a ::ₘ s).Nodup
                                    theorem Multiset.Nodup.of_cons {α : Type u_1} {s : Multiset α} {a : α} (h : (a ::ₘ s).Nodup) :
                                    theorem Multiset.Nodup.notMem {α : Type u_1} {s : Multiset α} {a : α} (h : (a ::ₘ s).Nodup) :
                                    ¬a s
                                    @[deprecated Multiset.Nodup.notMem (since := "2025-05-23")]
                                    theorem Multiset.Nodup.not_mem {α : Type u_1} {s : Multiset α} {a : α} (h : (a ::ₘ s).Nodup) :
                                    ¬a s

                                    Alias of Multiset.Nodup.notMem.