# 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} [] (a : α) (s : ) :

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.

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

### finset union #

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

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.)

Instances For
@[simp]
theorem Multiset.coe_ndunion {α : Type u_1} [] (l₁ : List α) (l₂ : List α) :
Multiset.ndunion l₁ l₂ = ↑(l₁ l₂)
theorem Multiset.zero_ndunion {α : Type u_1} [] (s : ) :
= s
@[simp]
theorem Multiset.cons_ndunion {α : Type u_1} [] (s : ) (t : ) (a : α) :
@[simp]
theorem Multiset.mem_ndunion {α : Type u_1} [] {s : } {t : } {a : α} :
a a s a t
theorem Multiset.le_ndunion_right {α : Type u_1} [] (s : ) (t : ) :
t
theorem Multiset.subset_ndunion_right {α : Type u_1} [] (s : ) (t : ) :
t
theorem Multiset.ndunion_le_add {α : Type u_1} [] (s : ) (t : ) :
s + t
theorem Multiset.ndunion_le {α : Type u_1} [] {s : } {t : } {u : } :
u s u t u
theorem Multiset.subset_ndunion_left {α : Type u_1} [] (s : ) (t : ) :
s
theorem Multiset.le_ndunion_left {α : Type u_1} [] {s : } (t : ) (d : ) :
s
theorem Multiset.ndunion_le_union {α : Type u_1} [] (s : ) (t : ) :
s t
theorem Multiset.Nodup.ndunion {α : Type u_1} [] (s : ) {t : } :
@[simp]
theorem Multiset.ndunion_eq_union {α : Type u_1} [] {s : } {t : } (d : ) :
= s t
theorem Multiset.dedup_add {α : Type u_1} [] (s : ) (t : ) :

### finset inter #

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

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.)

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