Documentation

Mathlib.Data.Multiset.UnionInter

Distributive lattice structure on multisets #

This file defines an instance DistribLattice (Multiset α) using the union and intersection operators:

Union #

def Multiset.union {α : Type u_1} [DecidableEq α] (s t : Multiset α) :

s ∪ t is the multiset such that the multiplicity of each a in it is the maximum of the multiplicity of a in s and t. This is the supremum of multisets.

Equations
    Instances For
      instance Multiset.instUnion {α : Type u_1} [DecidableEq α] :
      Equations
        theorem Multiset.union_def {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
        s t = s - t + t
        theorem Multiset.le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
        s s t
        theorem Multiset.le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
        t s t
        theorem Multiset.eq_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
        t ss t = s
        theorem Multiset.union_le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s t) (u : Multiset α) :
        s u t u
        theorem Multiset.union_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s u) (h₂ : t u) :
        s t u
        @[simp]
        theorem Multiset.mem_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} :
        a s t a s a t
        @[simp]
        theorem Multiset.map_union {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] {f : αβ} (finj : Function.Injective f) {s t : Multiset α} :
        map f (s t) = map f s map f t
        @[simp]
        theorem Multiset.zero_union {α : Type u_1} [DecidableEq α] {s : Multiset α} :
        0 s = s
        @[simp]
        theorem Multiset.union_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} :
        s 0 = s
        @[simp]
        theorem Multiset.count_union {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
        count a (s t) = max (count a s) (count a t)
        @[simp]
        theorem Multiset.filter_union {α : Type u_1} [DecidableEq α] (p : αProp) [DecidablePred p] (s t : Multiset α) :
        filter p (s t) = filter p s filter p t

        Intersection #

        def Multiset.inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :

        s ∩ t is the multiset such that the multiplicity of each a in it is the minimum of the multiplicity of a in s and t. This is the infimum of multisets.

        Equations
          Instances For
            instance Multiset.instInter {α : Type u_1} [DecidableEq α] :
            Equations
              @[simp]
              theorem Multiset.inter_zero {α : Type u_1} [DecidableEq α] (s : Multiset α) :
              s 0 = 0
              @[simp]
              theorem Multiset.zero_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) :
              0 s = 0
              @[simp]
              theorem Multiset.cons_inter_of_pos {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) :
              a t → (a ::ₘ s) t = a ::ₘ s t.erase a
              @[simp]
              theorem Multiset.cons_inter_of_neg {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) :
              at → (a ::ₘ s) t = s t
              theorem Multiset.inter_le_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
              s t s
              theorem Multiset.inter_le_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
              s t t
              theorem Multiset.le_inter {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s t) (h₂ : s u) :
              s t u
              @[simp]
              theorem Multiset.mem_inter {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} :
              a s t a s a t
              instance Multiset.instLattice {α : Type u_1} [DecidableEq α] :
              Equations
                @[simp]
                theorem Multiset.sup_eq_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                st = s t
                @[simp]
                theorem Multiset.inf_eq_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                st = s t
                @[simp]
                theorem Multiset.le_inter_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
                s t u s t s u
                @[simp]
                theorem Multiset.union_le_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
                s t u s u t u
                theorem Multiset.union_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                s t = t s
                theorem Multiset.inter_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                s t = t s
                theorem Multiset.eq_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s t) :
                s t = t
                theorem Multiset.union_le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s t) (u : Multiset α) :
                u s u t
                theorem Multiset.union_le_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                s t s + t
                theorem Multiset.union_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
                s t + u = s + u (t + u)
                theorem Multiset.add_union_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
                s + (t u) = s + t (s + u)
                theorem Multiset.cons_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
                a ::ₘ (s t) = a ::ₘ s a ::ₘ t
                theorem Multiset.inter_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
                s t + u = (s + u) (t + u)
                theorem Multiset.add_inter_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
                s + t u = (s + t) (s + u)
                theorem Multiset.cons_inter_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
                a ::ₘ s t = (a ::ₘ s) (a ::ₘ t)
                theorem Multiset.union_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                s t + s t = s + t
                theorem Multiset.sub_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                s - t + s t = s
                theorem Multiset.sub_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
                s - s t = s - t
                @[simp]
                theorem Multiset.count_inter {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
                count a (s t) = min (count a s) (count a t)
                @[simp]
                theorem Multiset.coe_inter {α : Type u_1} [DecidableEq α] (s t : List α) :
                s t = (s.bagInter t)
                @[simp]
                theorem Multiset.filter_inter {α : Type u_1} [DecidableEq α] (p : αProp) [DecidablePred p] (s t : Multiset α) :
                filter p (s t) = filter p s filter p t
                @[simp]
                theorem Multiset.replicate_inter {α : Type u_1} [DecidableEq α] (n : ) (x : α) (s : Multiset α) :
                replicate n x s = replicate (min n (count x s)) x
                @[simp]
                theorem Multiset.inter_replicate {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ) (x : α) :
                s replicate n x = replicate (min (count x s) n) x
                theorem Multiset.inter_add_sub_of_add_eq_add {α : Type u_1} [DecidableEq α] {M N P Q : Multiset α} (h : M + N = P + Q) :
                N Q + (P - M) = N

                Disjoint multisets #

                @[deprecated Disjoint (since := "2024-11-01")]
                def Multiset.Disjoint {α : Type u_1} (s t : Multiset α) :

                Disjoint s t means that s and t have no elements in common.

                Equations
                  Instances For
                    theorem Multiset.disjoint_left {α : Type u_1} {s t : Multiset α} :
                    Disjoint s t ∀ {a : α}, a sat
                    theorem Disjoint.notMem_of_mem_left_multiset {α : Type u_1} {s t : Multiset α} :
                    Disjoint s t∀ {a : α}, a sat

                    Alias of the forward direction of Multiset.disjoint_left.

                    @[deprecated Disjoint.notMem_of_mem_left_multiset (since := "2025-05-23")]
                    theorem Disjoint.not_mem_of_mem_left_multiset {α : Type u_1} {s t : Multiset α} :
                    Disjoint s t∀ {a : α}, a sat

                    Alias of the forward direction of Multiset.disjoint_left.


                    Alias of the forward direction of Multiset.disjoint_left.

                    @[simp]
                    theorem Multiset.coe_disjoint {α : Type u_1} (l₁ l₂ : List α) :
                    Disjoint l₁ l₂ l₁.Disjoint l₂
                    @[deprecated Disjoint.symm (since := "2024-11-01")]
                    theorem Multiset.Disjoint.symm {α : Type u_1} [PartialOrder α] [OrderBot α] a b : α :
                    Disjoint a bDisjoint b a

                    Alias of Disjoint.symm.

                    @[deprecated disjoint_comm (since := "2024-11-01")]
                    theorem Multiset.disjoint_comm {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} :

                    Alias of disjoint_comm.

                    theorem Multiset.disjoint_right {α : Type u_1} {s t : Multiset α} :
                    Disjoint s t ∀ {a : α}, a tas
                    theorem Disjoint.notMem_of_mem_right_multiset {α : Type u_1} {s t : Multiset α} :
                    Disjoint s t∀ {a : α}, a tas

                    Alias of the forward direction of Multiset.disjoint_right.

                    @[deprecated Disjoint.notMem_of_mem_right_multiset (since := "2025-05-23")]
                    theorem Disjoint.not_mem_of_mem_right_multiset {α : Type u_1} {s t : Multiset α} :
                    Disjoint s t∀ {a : α}, a tas

                    Alias of the forward direction of Multiset.disjoint_right.


                    Alias of the forward direction of Multiset.disjoint_right.

                    theorem Multiset.disjoint_iff_ne {α : Type u_1} {s t : Multiset α} :
                    Disjoint s t as, bt, a b
                    theorem Multiset.disjoint_of_subset_left {α : Type u_1} {s t u : Multiset α} (h : s u) (d : Disjoint u t) :
                    theorem Multiset.disjoint_of_subset_right {α : Type u_1} {s t u : Multiset α} (h : t u) (d : Disjoint s u) :
                    @[deprecated Disjoint.mono_left (since := "2024-11-01")]
                    theorem Multiset.disjoint_of_le_left {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} (h : a b) :
                    Disjoint b cDisjoint a c

                    Alias of Disjoint.mono_left.

                    @[deprecated Disjoint.mono_right (since := "2024-11-01")]
                    theorem Multiset.disjoint_of_le_right {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} :
                    b cDisjoint a cDisjoint a b

                    Alias of Disjoint.mono_right.

                    @[simp]
                    theorem Multiset.zero_disjoint {α : Type u_1} (l : Multiset α) :
                    @[simp]
                    theorem Multiset.singleton_disjoint {α : Type u_1} {l : Multiset α} {a : α} :
                    Disjoint {a} l al
                    @[simp]
                    theorem Multiset.disjoint_singleton {α : Type u_1} {l : Multiset α} {a : α} :
                    Disjoint l {a} al
                    @[simp]
                    theorem Multiset.disjoint_add_left {α : Type u_1} {s t u : Multiset α} :
                    Disjoint (s + t) u Disjoint s u Disjoint t u
                    @[simp]
                    theorem Multiset.disjoint_add_right {α : Type u_1} {s t u : Multiset α} :
                    Disjoint s (t + u) Disjoint s t Disjoint s u
                    @[simp]
                    theorem Multiset.disjoint_cons_left {α : Type u_1} {a : α} {s t : Multiset α} :
                    Disjoint (a ::ₘ s) t at Disjoint s t
                    @[simp]
                    theorem Multiset.disjoint_cons_right {α : Type u_1} {a : α} {s t : Multiset α} :
                    Disjoint s (a ::ₘ t) as Disjoint s t
                    theorem Multiset.inter_eq_zero_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
                    s t = 0 Disjoint s t
                    @[simp]
                    theorem Multiset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
                    @[simp]
                    theorem Multiset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
                    theorem Multiset.add_eq_union_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
                    s + t = s t Disjoint s t
                    theorem Multiset.add_eq_union_left_of_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h : t s) :
                    u + s = u t Disjoint u s s = t
                    theorem Multiset.add_eq_union_right_of_le {α : Type u_1} [DecidableEq α] {x y z : Multiset α} (h : z y) :
                    x + y = x z y = z Disjoint x y
                    theorem Multiset.disjoint_map_map {α : Type u_1} {β : Type v} {γ : Type u_2} {f : αγ} {g : βγ} {s : Multiset α} {t : Multiset β} :
                    Disjoint (map f s) (map g t) as, bt, f a g b
                    theorem Multiset.map_set_pairwise {α : Type u_1} {β : Type v} {f : αβ} {r : ββProp} {m : Multiset α} (h : {a : α | a m}.Pairwise fun (a₁ a₂ : α) => r (f a₁) (f a₂)) :
                    {b : β | b map f m}.Pairwise r
                    theorem Multiset.nodup_add {α : Type u_1} {s t : Multiset α} :
                    theorem Multiset.disjoint_of_nodup_add {α : Type u_1} {s t : Multiset α} (d : (s + t).Nodup) :
                    theorem Multiset.Nodup.add_iff {α : Type u_1} {s t : Multiset α} (d₁ : s.Nodup) (d₂ : t.Nodup) :
                    (s + t).Nodup Disjoint s t
                    theorem Multiset.Nodup.inter_left {α : Type u_1} {s : Multiset α} [DecidableEq α] (t : Multiset α) :
                    s.Nodup(s t).Nodup
                    theorem Multiset.Nodup.inter_right {α : Type u_1} {t : Multiset α} [DecidableEq α] (s : Multiset α) :
                    t.Nodup(s t).Nodup
                    @[simp]
                    theorem Multiset.nodup_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} :