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
@[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 α} :
asMultiset.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 : as) :
Multiset.card (Multiset.ndinsert a s) = Multiset.card s + 1
theorem Multiset.dedup_cons {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} :
(a ::ₘ s).dedup = Multiset.ndinsert a s.dedup
theorem Multiset.Nodup.ndinsert {α : Type u_1} [DecidableEq α] {s : Multiset α} (a : α) :
s.Nodup(Multiset.ndinsert a s).Nodup
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.ndinsert a s).attach = Multiset.ndinsert a, (Multiset.map (fun (p : { x : α // x s }) => p, ) s.attach)
@[simp]
theorem Multiset.disjoint_ndinsert_left {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} :
(Multiset.ndinsert a s).Disjoint t at s.Disjoint t
@[simp]
theorem Multiset.disjoint_ndinsert_right {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} {t : Multiset α} :
s.Disjoint (Multiset.ndinsert a t) as s.Disjoint t

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
@[simp]
theorem Multiset.coe_ndunion {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
(↑l₁).ndunion 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 : α) :
(a ::ₘ s).ndunion t = Multiset.ndinsert a (s.ndunion t)
@[simp]
theorem Multiset.mem_ndunion {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
a s.ndunion t a s a t
theorem Multiset.le_ndunion_right {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
t s.ndunion t
theorem Multiset.subset_ndunion_right {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
t s.ndunion t
theorem Multiset.ndunion_le_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
s.ndunion t s + t
theorem Multiset.ndunion_le {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :
s.ndunion t u s u t u
theorem Multiset.subset_ndunion_left {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
s s.ndunion t
theorem Multiset.le_ndunion_left {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : s.Nodup) :
s s.ndunion t
theorem Multiset.ndunion_le_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
s.ndunion t s t
theorem Multiset.Nodup.ndunion {α : Type u_1} [DecidableEq α] (s : Multiset α) {t : Multiset α} :
t.Nodup(s.ndunion t).Nodup
@[simp]
theorem Multiset.ndunion_eq_union {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (d : s.Nodup) :
s.ndunion t = s t
theorem Multiset.dedup_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
(s + t).dedup = s.ndunion t.dedup
theorem Multiset.Disjoint.ndunion_eq {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (h : s.Disjoint t) :
s.ndunion t = s.dedup + t
theorem Multiset.Subset.ndunion_eq_right {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (h : s t) :
s.ndunion t = t

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
@[simp]
theorem Multiset.coe_ndinter {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
(↑l₁).ndinter 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) :
(a ::ₘ s).ndinter t = a ::ₘ s.ndinter t
@[simp]
theorem Multiset.ndinter_cons_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} (s : Multiset α) {t : Multiset α} (h : at) :
(a ::ₘ s).ndinter t = s.ndinter t
@[simp]
theorem Multiset.mem_ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {a : α} :
a s.ndinter t a s a t
@[simp]
theorem Multiset.Nodup.ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) :
s.Nodup(s.ndinter t).Nodup
theorem Multiset.le_ndinter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} {u : Multiset α} :
s t.ndinter u s t s u
theorem Multiset.ndinter_le_left {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
s.ndinter t s
theorem Multiset.ndinter_subset_left {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
s.ndinter t s
theorem Multiset.ndinter_subset_right {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
s.ndinter t t
theorem Multiset.ndinter_le_right {α : Type u_1} [DecidableEq α] {s : Multiset α} (t : Multiset α) (d : s.Nodup) :
s.ndinter t t
theorem Multiset.inter_le_ndinter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) :
s t s.ndinter t
@[simp]
theorem Multiset.ndinter_eq_inter {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} (d : s.Nodup) :
s.ndinter t = s t
theorem Multiset.ndinter_eq_zero_iff_disjoint {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
s.ndinter t = 0 s.Disjoint t
theorem Multiset.Disjoint.ndinter_eq_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} {t : Multiset α} :
s.Disjoint ts.ndinter t = 0

Alias of the reverse direction of Multiset.ndinter_eq_zero_iff_disjoint.

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