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 α) : 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

• Multiset.ndinsert a s = Quot.liftOn s (fun (l : List α) => ↑(List.insert a l)) ⋯

@[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 : α) : Multiset.ndinsert a 0 = {a}

@[simp]

theorem Multiset.ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∈ s → Multiset.ndinsert a s = s

@[simp]

theorem Multiset.ndinsert_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : a ∉ s → Multiset.ndinsert a s = a ::ₘ s

@[simp]

theorem Multiset.mem_ndinsert {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Multiset α} : a ∈ Multiset.ndinsert b s ↔ a = b ∨ a ∈ s

@[simp]

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

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

theorem Multiset.mem_ndinsert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {b : α} {s : Multiset α} (h : a ∈ s) : a ∈ Multiset.ndinsert b 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.dedup_cons {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} : Multiset.dedup (a ::ₘ s) = Multiset.ndinsert a (Multiset.dedup s)

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

theorem Multiset.ndinsert_le {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} : Multiset.ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t

theorem Multiset.attach_ndinsert {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) : Multiset.attach (Multiset.ndinsert a s) = Multiset.ndinsert { val := a, property := ⋯ } (Multiset.map (fun (p : { x : α // x ∈ s }) => { val := ↑p, property := ⋯ }) (Multiset.attach s))

@[simp]

theorem Multiset.disjoint_ndinsert_left {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} : Multiset.Disjoint (Multiset.ndinsert a s) t ↔ a ∉ t ∧ Multiset.Disjoint s t

@[simp]

theorem Multiset.disjoint_ndinsert_right {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} : Multiset.Disjoint s (Multiset.ndinsert a t) ↔ a ∉ s ∧ Multiset.Disjoint s t

finset union

def Multiset.ndunion {α : Type u_1} [DecidableEq α] (s : Multiset α) (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

• Multiset.ndunion s t = Quotient.liftOn₂ s t (fun (l₁ l₂ : List α) => ↑(List.union l₁ l₂)) ⋯

@[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 α) : Multiset.ndunion 0 s = s

@[simp]

theorem Multiset.cons_ndunion {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) (a : α) : Multiset.ndunion (a ::ₘ s) t = Multiset.ndinsert a (Multiset.ndunion s t)

@[simp]

theorem Multiset.mem_ndunion {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} : a ∈ Multiset.ndunion s t ↔ a ∈ s ∨ a ∈ t

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

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

theorem Multiset.ndunion_le_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : Multiset.ndunion s t ≤ s + t

theorem Multiset.ndunion_le {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} : Multiset.ndunion s t ≤ u ↔ s ⊆ u ∧ t ≤ u

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

theorem Multiset.le_ndunion_left {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : Multiset.Nodup s) : s ≤ Multiset.ndunion s t

theorem Multiset.ndunion_le_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : Multiset.ndunion s t ≤ s ∪ t

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

@[simp]

theorem Multiset.ndunion_eq_union {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup s) : Multiset.ndunion s t = s ∪ t

theorem Multiset.dedup_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : Multiset.dedup (s + t) = Multiset.ndunion s (Multiset.dedup t)

finset inter

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

Equations

• Multiset.ndinter s t = Multiset.filter (fun (x : α) => x ∈ t) s

@[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 α) : Multiset.ndinter 0 s = 0

@[simp]

theorem Multiset.cons_ndinter_of_mem {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : a ∈ t) : Multiset.ndinter (a ::ₘ s) t = a ::ₘ Multiset.ndinter s t

@[simp]

theorem Multiset.ndinter_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : a ∉ t) : Multiset.ndinter (a ::ₘ s) t = Multiset.ndinter s t

@[simp]

theorem Multiset.mem_ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} : a ∈ Multiset.ndinter s t ↔ a ∈ s ∧ a ∈ t

@[simp]

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

theorem Multiset.le_ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} : s ≤ Multiset.ndinter t u ↔ s ≤ t ∧ s ⊆ u

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

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

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

theorem Multiset.ndinter_le_right {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : Multiset.Nodup s) : Multiset.ndinter s t ≤ t

theorem Multiset.inter_le_ndinter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : s ∩ t ≤ Multiset.ndinter s t

@[simp]

theorem Multiset.ndinter_eq_inter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (d : Multiset.Nodup s) : Multiset.ndinter s t = s ∩ t

theorem Multiset.ndinter_eq_zero_iff_disjoint {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} : Multiset.ndinter s t = 0 ↔ Multiset.Disjoint s t