Documentation

Mathlib.Data.Multiset.FinsetOps

Preparations for defining operations on Finset. #

The operations here ignore multiplicities, and preparatory for defining the corresponding operations on Finset.

finset insert #

def Multiset.ndinsert {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :

ndinsert a s is the lift of the list insert operation. This operation does not respect multiplicities, unlike cons, but it is suitable as an insert operation on Finset.

Equations
Instances For
    @[simp]
    theorem Multiset.coe_ndinsert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :
    Multiset.ndinsert a l = ↑(insert a l)
    @[simp]
    theorem Multiset.ndinsert_zero {α : Type u_1} [DecidableEq α] (a : α) :
    @[simp]
    theorem Multiset.ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
    a sMultiset.ndinsert a s = s
    @[simp]
    theorem Multiset.ndinsert_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
    ¬a sMultiset.ndinsert a s = a ::ₘ s
    @[simp]
    theorem Multiset.mem_ndinsert {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Multiset α} :
    @[simp]
    theorem Multiset.le_ndinsert_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
    theorem Multiset.mem_ndinsert_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
    theorem Multiset.mem_ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Multiset α} (h : a s) :
    @[simp]
    theorem Multiset.length_ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : a s) :
    Multiset.card (Multiset.ndinsert a s) = Multiset.card s
    @[simp]
    theorem Multiset.length_ndinsert_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : ¬a s) :
    Multiset.card (Multiset.ndinsert a s) = Multiset.card s + 1
    theorem Multiset.ndinsert_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} :
    theorem Multiset.attach_ndinsert {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
    Multiset.attach (Multiset.ndinsert a s) = Multiset.ndinsert { val := a, property := (_ : a Multiset.ndinsert a s) } (Multiset.map (fun p => { val := p, property := (_ : p Multiset.ndinsert a s) }) (Multiset.attach s))

    finset union #

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

    ndunion s t is the lift of the list union operation. This operation does not respect multiplicities, unlike s ∪ t, but it is suitable as a union operation on Finset. (s ∪ t would also work as a union operation on finset, but this is more efficient.)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Multiset.coe_ndunion {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
      Multiset.ndunion l₁ l₂ = ↑(l₁ l₂)
      theorem Multiset.zero_ndunion {α : Type u_1} [DecidableEq α] (s : Multiset α) :
      @[simp]
      theorem Multiset.cons_ndunion {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) (a : α) :
      @[simp]
      theorem Multiset.mem_ndunion {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
      theorem Multiset.le_ndunion_right {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
      theorem Multiset.ndunion_le_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
      theorem Multiset.ndunion_le {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :
      theorem Multiset.le_ndunion_left {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : Multiset.Nodup s) :
      theorem Multiset.ndunion_le_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
      @[simp]
      theorem Multiset.ndunion_eq_union {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup s) :

      finset inter #

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

      ndinter s t is the lift of the list operation. This operation does not respect multiplicities, unlike s ∩ t, but it is suitable as an intersection operation on Finset. (s ∩ t would also work as a union operation on finset, but this is more efficient.)

      Equations
      Instances For
        @[simp]
        theorem Multiset.coe_ndinter {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
        Multiset.ndinter l₁ l₂ = ↑(l₁ l₂)
        @[simp]
        theorem Multiset.zero_ndinter {α : Type u_1} [DecidableEq α] (s : Multiset α) :
        @[simp]
        theorem Multiset.cons_ndinter_of_mem {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : a t) :
        @[simp]
        theorem Multiset.ndinter_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : ¬a t) :
        @[simp]
        theorem Multiset.mem_ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
        @[simp]
        theorem Multiset.le_ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :
        theorem Multiset.ndinter_le_left {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
        theorem Multiset.ndinter_le_right {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : Multiset.Nodup s) :
        theorem Multiset.inter_le_ndinter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
        @[simp]
        theorem Multiset.ndinter_eq_inter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup s) :