# mathlib3documentation

data.multiset.finset_ops

# Preparations for defining operations on finset. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

### finset insert #

def multiset.ndinsert {α : Type u_1} [decidable_eq α] (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} [decidable_eq α] (a : α) (l : list α) :
= l)
@[simp]
theorem multiset.ndinsert_zero {α : Type u_1} [decidable_eq α] (a : α) :
= {a}
@[simp]
theorem multiset.ndinsert_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s = s
@[simp]
theorem multiset.ndinsert_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
a s = a ::ₘ s
@[simp]
theorem multiset.mem_ndinsert {α : Type u_1} [decidable_eq α] {a b : α} {s : multiset α} :
a a = b a s
@[simp]
theorem multiset.le_ndinsert_self {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
s
@[simp]
theorem multiset.mem_ndinsert_self {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
a
theorem multiset.mem_ndinsert_of_mem {α : Type u_1} [decidable_eq α] {a b : α} {s : multiset α} (h : a s) :
a
@[simp]
theorem multiset.length_ndinsert_of_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (h : a s) :
@[simp]
theorem multiset.length_ndinsert_of_not_mem {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} (h : a s) :
=
theorem multiset.dedup_cons {α : Type u_1} [decidable_eq α] {a : α} {s : multiset α} :
(a ::ₘ s).dedup =
theorem multiset.nodup.ndinsert {α : Type u_1} [decidable_eq α] {s : multiset α} (a : α) :
theorem multiset.ndinsert_le {α : Type u_1} [decidable_eq α] {a : α} {s t : multiset α} :
t s t a t
theorem multiset.attach_ndinsert {α : Type u_1} [decidable_eq α] (a : α) (s : multiset α) :
s).attach = multiset.ndinsert a, _⟩ (multiset.map (λ (p : {x // x s}), p.val, _⟩) s.attach)
@[simp]
theorem multiset.disjoint_ndinsert_left {α : Type u_1} [decidable_eq α] {a : α} {s t : multiset α} :
s).disjoint t a t s.disjoint t
@[simp]
theorem multiset.disjoint_ndinsert_right {α : Type u_1} [decidable_eq α] {a : α} {s t : multiset α} :
s.disjoint t) a s s.disjoint t

### finset union #

def multiset.ndunion {α : Type u_1} [decidable_eq α] (s 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} [decidable_eq α] (l₁ l₂ : list α) :
l₁.ndunion l₂ = (l₁ l₂)
@[simp]
theorem multiset.zero_ndunion {α : Type u_1} [decidable_eq α] (s : multiset α) :
0.ndunion s = s
@[simp]
theorem multiset.cons_ndunion {α : Type u_1} [decidable_eq α] (s t : multiset α) (a : α) :
(a ::ₘ s).ndunion t = (s.ndunion t)
@[simp]
theorem multiset.mem_ndunion {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :
a s.ndunion t a s a t
theorem multiset.le_ndunion_right {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t s.ndunion t
theorem multiset.subset_ndunion_right {α : Type u_1} [decidable_eq α] (s t : multiset α) :
t s.ndunion t
theorem multiset.ndunion_le_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s.ndunion t s + t
theorem multiset.ndunion_le {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s.ndunion t u s u t u
theorem multiset.subset_ndunion_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s s.ndunion t
theorem multiset.le_ndunion_left {α : Type u_1} [decidable_eq α] {s : multiset α} (t : multiset α) (d : s.nodup) :
s s.ndunion t
theorem multiset.ndunion_le_union {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s.ndunion t s t
theorem multiset.nodup.ndunion {α : Type u_1} [decidable_eq α] (s : multiset α) {t : multiset α} :
@[simp]
theorem multiset.ndunion_eq_union {α : Type u_1} [decidable_eq α] {s t : multiset α} (d : s.nodup) :
s.ndunion t = s t
theorem multiset.dedup_add {α : Type u_1} [decidable_eq α] (s t : multiset α) :
(s + t).dedup = s.ndunion t.dedup

### finset inter #

def multiset.ndinter {α : Type u_1} [decidable_eq α] (s 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} [decidable_eq α] (l₁ l₂ : list α) :
l₁.ndinter l₂ = (l₁ l₂)
@[simp]
theorem multiset.zero_ndinter {α : Type u_1} [decidable_eq α] (s : multiset α) :
0.ndinter s = 0
@[simp]
theorem multiset.cons_ndinter_of_mem {α : Type u_1} [decidable_eq α] {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} [decidable_eq α] {a : α} (s : multiset α) {t : multiset α} (h : a t) :
(a ::ₘ s).ndinter t = s.ndinter t
@[simp]
theorem multiset.mem_ndinter {α : Type u_1} [decidable_eq α] {s t : multiset α} {a : α} :
a s.ndinter t a s a t
@[simp]
theorem multiset.nodup.ndinter {α : Type u_1} [decidable_eq α] {s : multiset α} (t : multiset α) :
theorem multiset.le_ndinter {α : Type u_1} [decidable_eq α] {s t u : multiset α} :
s t.ndinter u s t s u
theorem multiset.ndinter_le_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s.ndinter t s
theorem multiset.ndinter_subset_left {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s.ndinter t s
theorem multiset.ndinter_subset_right {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s.ndinter t t
theorem multiset.ndinter_le_right {α : Type u_1} [decidable_eq α] {s : multiset α} (t : multiset α) (d : s.nodup) :
s.ndinter t t
theorem multiset.inter_le_ndinter {α : Type u_1} [decidable_eq α] (s t : multiset α) :
s t s.ndinter t
@[simp]
theorem multiset.ndinter_eq_inter {α : Type u_1} [decidable_eq α] {s t : multiset α} (d : s.nodup) :
s.ndinter t = s t
theorem multiset.ndinter_eq_zero_iff_disjoint {α : Type u_1} [decidable_eq α] {s t : multiset α} :
s.ndinter t = 0 s.disjoint t