Documentation

Mathlib.Data.Multiset.FinsetOps

Preparations for defining operations on Finset. #

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

finset insert #

source
def Multiset.ndinsert {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
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
      source
      @[simp]
      theorem Multiset.coe_ndinsert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :
      ndinsert a ↑l = ↑(insert a l)
      source
      @[simp]
      theorem Multiset.ndinsert_zero {α : Type u_1} [DecidableEq α] (a : α) :
      ndinsert a 0 = {a}
      source
      @[simp]
      theorem Multiset.ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
      a ∈ s → ndinsert a s = s
      source
      @[simp]
      theorem Multiset.ndinsert_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
      ¬a ∈ s → ndinsert a s = a ::ₘ s
      source
      @[simp]
      theorem Multiset.mem_ndinsert {α : Type u_1} [DecidableEq α] {a b : α} {s : Multiset α} :
      a ∈ ndinsert b s ↔ a = b ∨ a ∈ s
      source
      @[simp]
      theorem Multiset.le_ndinsert_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
      s ≤ ndinsert a s
      source
      theorem Multiset.mem_ndinsert_self {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
      a ∈ ndinsert a s
      source
      theorem Multiset.mem_ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a b : α} {s : Multiset α} (h : a ∈ s) :
      a ∈ ndinsert b s
      source
      theorem Multiset.length_ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : a ∈ s) :
      (ndinsert a s).card = s.card
      source
      theorem Multiset.length_ndinsert_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : ¬a ∈ s) :
      (ndinsert a s).card = s.card + 1
      source
      theorem Multiset.dedup_cons {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
      (a ::ₘ s).dedup = ndinsert a s.dedup
      source
      theorem Multiset.Nodup.ndinsert {α : Type u_1} [DecidableEq α] {s : Multiset α} (a : α) :
      s.Nodup → (Multiset.ndinsert a s).Nodup
      source
      theorem Multiset.ndinsert_le {α : Type u_1} [DecidableEq α] {a : α} {s t : Multiset α} :
      ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t
      source
      theorem Multiset.attach_ndinsert {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
      (ndinsert a s).attach = ndinsert ⟨a, ⋯⟩ (map (fun (p : { x : α // x ∈ s }) => ⟨↑p, ⋯⟩) s.attach)
      source
      @[simp]
      theorem Multiset.disjoint_ndinsert_left {α : Type u_1} [DecidableEq α] {a : α} {s t : Multiset α} :
      Disjoint (ndinsert a s) t ↔ ¬a ∈ t ∧ Disjoint s t
      source
      @[simp]
      theorem Multiset.disjoint_ndinsert_right {α : Type u_1} [DecidableEq α] {a : α} {s t : Multiset α} :
      Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ Disjoint s t

      finset union #

      source
      def Multiset.ndunion {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
      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
        Instances For
          source
          @[simp]
          theorem Multiset.coe_ndunion {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
          (↑l₁).ndunion ↑l₂ = ↑(l₁ ∪ l₂)
          source
          theorem Multiset.zero_ndunion {α : Type u_1} [DecidableEq α] (s : Multiset α) :
          ndunion 0 s = s
          source
          @[simp]
          theorem Multiset.cons_ndunion {α : Type u_1} [DecidableEq α] (s t : Multiset α) (a : α) :
          (a ::ₘ s).ndunion t = ndinsert a (s.ndunion t)
          source
          @[simp]
          theorem Multiset.mem_ndunion {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} :
          a ∈ s.ndunion t ↔ a ∈ s ∨ a ∈ t
          source
          theorem Multiset.le_ndunion_right {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
          t ≤ s.ndunion t
          source
          theorem Multiset.subset_ndunion_right {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
          t ⊆ s.ndunion t
          source
          theorem Multiset.ndunion_le_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
          s.ndunion t ≤ s + t
          source
          theorem Multiset.ndunion_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
          s.ndunion t ≤ u ↔ s ⊆ u ∧ t ≤ u
          source
          theorem Multiset.subset_ndunion_left {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
          s ⊆ s.ndunion t
          source
          theorem Multiset.le_ndunion_left {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : s.Nodup) :
          s ≤ s.ndunion t
          source
          theorem Multiset.ndunion_le_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
          s.ndunion t ≤ s ∪ t
          source
          theorem Multiset.Nodup.ndunion {α : Type u_1} [DecidableEq α] (s : Multiset α) {t : Multiset α} :
          t.Nodup → (s.ndunion t).Nodup
          source
          @[simp]
          theorem Multiset.ndunion_eq_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} (d : s.Nodup) :
          s.ndunion t = s ∪ t
          source
          theorem Multiset.dedup_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
          (s + t).dedup = s.ndunion t.dedup
          source
          theorem Multiset.Disjoint.ndunion_eq {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : Disjoint s t) :
          s.ndunion t = s.dedup + t
          source
          theorem Multiset.Subset.ndunion_eq_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ⊆ t) :
          s.ndunion t = t

          finset inter #

          source
          def Multiset.ndinter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
          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 an intersection operation on finset, but this is more efficient.)

          Equations
            Instances For
              source
              @[simp]
              theorem Multiset.coe_ndinter {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
              (↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)
              source
              @[simp]
              theorem Multiset.zero_ndinter {α : Type u_1} [DecidableEq α] (s : Multiset α) :
              ndinter 0 s = 0
              source
              @[simp]
              theorem Multiset.cons_ndinter_of_mem {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : a ∈ t) :
              (a ::ₘ s).ndinter t = a ::ₘ s.ndinter t
              source
              @[simp]
              theorem Multiset.ndinter_cons_of_notMem {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : ¬a ∈ t) :
              (a ::ₘ s).ndinter t = s.ndinter t
              source
              @[simp]
              theorem Multiset.mem_ndinter {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} :
              a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t
              source
              theorem Multiset.Nodup.ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) :
              s.Nodup → (s.ndinter t).Nodup
              source
              theorem Multiset.le_ndinter {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
              s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u
              source
              theorem Multiset.ndinter_le_left {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
              s.ndinter t ≤ s
              source
              theorem Multiset.ndinter_subset_left {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
              s.ndinter t ⊆ s
              source
              theorem Multiset.ndinter_subset_right {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
              s.ndinter t ⊆ t
              source
              theorem Multiset.ndinter_le_right {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : s.Nodup) :
              s.ndinter t ≤ t
              source
              theorem Multiset.inter_le_ndinter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
              s ∩ t ≤ s.ndinter t
              source
              @[simp]
              theorem Multiset.ndinter_eq_inter {α : Type u_1} [DecidableEq α] {s t : Multiset α} (d : s.Nodup) :
              s.ndinter t = s ∩ t
              source
              @[simp]
              theorem Multiset.Nodup.inter {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : s.Nodup) :
              (s ∩ t).Nodup
              source
              theorem Multiset.ndinter_eq_zero_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
              s.ndinter t = 0 ↔ Disjoint s t
              source
              theorem Multiset.Disjoint.ndinter_eq_zero {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
              Disjoint s t → s.ndinter t = 0

              Alias of the reverse direction of Multiset.ndinter_eq_zero_iff_disjoint.

              source
              theorem Multiset.Subset.ndinter_eq_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ⊆ t) :
              s.ndinter t = s