# Lattice operations on multisets #

### sup #

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

Supremum of a multiset: sup {a, b, c} = a ⊔ b ⊔ c

Equations
Instances For
@[simp]
theorem Multiset.sup_coe {α : Type u_1} [] [] (l : List α) :
(l).sup = List.foldr (fun (x x_1 : α) => x x_1) l
@[simp]
theorem Multiset.sup_zero {α : Type u_1} [] [] :
@[simp]
theorem Multiset.sup_cons {α : Type u_1} [] [] (a : α) (s : ) :
(a ::ₘ s).sup = a s.sup
@[simp]
theorem Multiset.sup_singleton {α : Type u_1} [] [] {a : α} :
{a}.sup = a
@[simp]
theorem Multiset.sup_add {α : Type u_1} [] [] (s₁ : ) (s₂ : ) :
(s₁ + s₂).sup = s₁.sup s₂.sup
@[simp]
theorem Multiset.sup_le {α : Type u_1} [] [] {s : } {a : α} :
s.sup a bs, b a
theorem Multiset.le_sup {α : Type u_1} [] [] {s : } {a : α} (h : a s) :
a s.sup
theorem Multiset.sup_mono {α : Type u_1} [] [] {s₁ : } {s₂ : } (h : s₁ s₂) :
s₁.sup s₂.sup
@[simp]
theorem Multiset.sup_dedup {α : Type u_1} [] [] [] (s : ) :
s.dedup.sup = s.sup
@[simp]
theorem Multiset.sup_ndunion {α : Type u_1} [] [] [] (s₁ : ) (s₂ : ) :
(s₁.ndunion s₂).sup = s₁.sup s₂.sup
@[simp]
theorem Multiset.sup_union {α : Type u_1} [] [] [] (s₁ : ) (s₂ : ) :
(s₁ s₂).sup = s₁.sup s₂.sup
@[simp]
theorem Multiset.sup_ndinsert {α : Type u_1} [] [] [] (a : α) (s : ) :
().sup = a s.sup
theorem Multiset.nodup_sup_iff {α : Type u_2} [] {m : Multiset ()} :
m.sup.Nodup am, a.Nodup

### inf #

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

Infimum of a multiset: inf {a, b, c} = a ⊓ b ⊓ c

Equations
Instances For
@[simp]
theorem Multiset.inf_coe {α : Type u_1} [] [] (l : List α) :
(l).inf = List.foldr (fun (x x_1 : α) => x x_1) l
@[simp]
theorem Multiset.inf_zero {α : Type u_1} [] [] :
@[simp]
theorem Multiset.inf_cons {α : Type u_1} [] [] (a : α) (s : ) :
(a ::ₘ s).inf = a s.inf
@[simp]
theorem Multiset.inf_singleton {α : Type u_1} [] [] {a : α} :
{a}.inf = a
@[simp]
theorem Multiset.inf_add {α : Type u_1} [] [] (s₁ : ) (s₂ : ) :
(s₁ + s₂).inf = s₁.inf s₂.inf
@[simp]
theorem Multiset.le_inf {α : Type u_1} [] [] {s : } {a : α} :
a s.inf bs, a b
theorem Multiset.inf_le {α : Type u_1} [] [] {s : } {a : α} (h : a s) :
s.inf a
theorem Multiset.inf_mono {α : Type u_1} [] [] {s₁ : } {s₂ : } (h : s₁ s₂) :
s₂.inf s₁.inf
@[simp]
theorem Multiset.inf_dedup {α : Type u_1} [] [] [] (s : ) :
s.dedup.inf = s.inf
@[simp]
theorem Multiset.inf_ndunion {α : Type u_1} [] [] [] (s₁ : ) (s₂ : ) :
(s₁.ndunion s₂).inf = s₁.inf s₂.inf
@[simp]
theorem Multiset.inf_union {α : Type u_1} [] [] [] (s₁ : ) (s₂ : ) :
(s₁ s₂).inf = s₁.inf s₂.inf
@[simp]
theorem Multiset.inf_ndinsert {α : Type u_1} [] [] [] (a : α) (s : ) :
().inf = a s.inf