mathlib documentation

data.multiset.lattice

Lattice operations on multisets

sup

def multiset.sup {α : Type u_1} [semilattice_sup_bot α] :
multiset α → α

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

Equations
@[simp]
theorem multiset.sup_zero {α : Type u_1} [semilattice_sup_bot α] :

@[simp]
theorem multiset.sup_cons {α : Type u_1} [semilattice_sup_bot α] (a : α) (s : multiset α) :
(a ::ₘ s).sup = a s.sup

@[simp]
theorem multiset.sup_singleton {α : Type u_1} [semilattice_sup_bot α] {a : α} :
(a ::ₘ 0).sup = a

@[simp]
theorem multiset.sup_add {α : Type u_1} [semilattice_sup_bot α] (s₁ s₂ : multiset α) :
(s₁ + s₂).sup = s₁.sup s₂.sup

theorem multiset.sup_le {α : Type u_1} [semilattice_sup_bot α] {s : multiset α} {a : α} :
s.sup a ∀ (b : α), b sb a

theorem multiset.le_sup {α : Type u_1} [semilattice_sup_bot α] {s : multiset α} {a : α} :
a sa s.sup

theorem multiset.sup_mono {α : Type u_1} [semilattice_sup_bot α] {s₁ s₂ : multiset α} :
s₁ s₂s₁.sup s₂.sup

@[simp]
theorem multiset.sup_erase_dup {α : Type u_1} [semilattice_sup_bot α] [decidable_eq α] (s : multiset α) :

@[simp]
theorem multiset.sup_ndunion {α : Type u_1} [semilattice_sup_bot α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁.ndunion s₂).sup = s₁.sup s₂.sup

@[simp]
theorem multiset.sup_union {α : Type u_1} [semilattice_sup_bot α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁ s₂).sup = s₁.sup s₂.sup

@[simp]
theorem multiset.sup_ndinsert {α : Type u_1} [semilattice_sup_bot α] [decidable_eq α] (a : α) (s : multiset α) :

inf

def multiset.inf {α : Type u_1} [semilattice_inf_top α] :
multiset α → α

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

Equations
@[simp]
theorem multiset.inf_zero {α : Type u_1} [semilattice_inf_top α] :

@[simp]
theorem multiset.inf_cons {α : Type u_1} [semilattice_inf_top α] (a : α) (s : multiset α) :
(a ::ₘ s).inf = a s.inf

@[simp]
theorem multiset.inf_singleton {α : Type u_1} [semilattice_inf_top α] {a : α} :
(a ::ₘ 0).inf = a

@[simp]
theorem multiset.inf_add {α : Type u_1} [semilattice_inf_top α] (s₁ s₂ : multiset α) :
(s₁ + s₂).inf = s₁.inf s₂.inf

theorem multiset.le_inf {α : Type u_1} [semilattice_inf_top α] {s : multiset α} {a : α} :
a s.inf ∀ (b : α), b sa b

theorem multiset.inf_le {α : Type u_1} [semilattice_inf_top α] {s : multiset α} {a : α} :
a ss.inf a

theorem multiset.inf_mono {α : Type u_1} [semilattice_inf_top α] {s₁ s₂ : multiset α} :
s₁ s₂s₂.inf s₁.inf

@[simp]
theorem multiset.inf_erase_dup {α : Type u_1} [semilattice_inf_top α] [decidable_eq α] (s : multiset α) :

@[simp]
theorem multiset.inf_ndunion {α : Type u_1} [semilattice_inf_top α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁.ndunion s₂).inf = s₁.inf s₂.inf

@[simp]
theorem multiset.inf_union {α : Type u_1} [semilattice_inf_top α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁ s₂).inf = s₁.inf s₂.inf

@[simp]
theorem multiset.inf_ndinsert {α : Type u_1} [semilattice_inf_top α] [decidable_eq α] (a : α) (s : multiset α) :