mathlib documentation

data.multiset.lattice

Lattice operations on multisets #

sup #

def multiset.sup {α : Type u_1} [semilattice_sup α] [order_bot α] (s : multiset α) :
α

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

Equations
@[simp]
theorem multiset.sup_coe {α : Type u_1} [semilattice_sup α] [order_bot α] (l : list α) :
@[simp]
theorem multiset.sup_zero {α : Type u_1} [semilattice_sup α] [order_bot α] :
@[simp]
theorem multiset.sup_cons {α : Type u_1} [semilattice_sup α] [order_bot α] (a : α) (s : multiset α) :
(a ::ₘ s).sup = a s.sup
@[simp]
theorem multiset.sup_singleton {α : Type u_1} [semilattice_sup α] [order_bot α] {a : α} :
{a}.sup = a
@[simp]
theorem multiset.sup_add {α : Type u_1} [semilattice_sup α] [order_bot α] (s₁ s₂ : multiset α) :
(s₁ + s₂).sup = s₁.sup s₂.sup
theorem multiset.sup_le {α : Type u_1} [semilattice_sup α] [order_bot α] {s : multiset α} {a : α} :
s.sup a ∀ (b : α), b sb a
theorem multiset.le_sup {α : Type u_1} [semilattice_sup α] [order_bot α] {s : multiset α} {a : α} (h : a s) :
a s.sup
theorem multiset.sup_mono {α : Type u_1} [semilattice_sup α] [order_bot α] {s₁ s₂ : multiset α} (h : s₁ s₂) :
s₁.sup s₂.sup
@[simp]
theorem multiset.sup_dedup {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (s : multiset α) :
@[simp]
theorem multiset.sup_ndunion {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁.ndunion s₂).sup = s₁.sup s₂.sup
@[simp]
theorem multiset.sup_union {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁ s₂).sup = s₁.sup s₂.sup
@[simp]
theorem multiset.sup_ndinsert {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (a : α) (s : multiset α) :
theorem multiset.nodup_sup_iff {α : Type u_1} [decidable_eq α] {m : multiset (multiset α)} :
m.sup.nodup ∀ (a : multiset α), a m → a.nodup

inf #

def multiset.inf {α : Type u_1} [semilattice_inf α] [order_top α] (s : multiset α) :
α

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

Equations
@[simp]
theorem multiset.inf_coe {α : Type u_1} [semilattice_inf α] [order_top α] (l : list α) :
@[simp]
theorem multiset.inf_zero {α : Type u_1} [semilattice_inf α] [order_top α] :
@[simp]
theorem multiset.inf_cons {α : Type u_1} [semilattice_inf α] [order_top α] (a : α) (s : multiset α) :
(a ::ₘ s).inf = a s.inf
@[simp]
theorem multiset.inf_singleton {α : Type u_1} [semilattice_inf α] [order_top α] {a : α} :
{a}.inf = a
@[simp]
theorem multiset.inf_add {α : Type u_1} [semilattice_inf α] [order_top α] (s₁ s₂ : multiset α) :
(s₁ + s₂).inf = s₁.inf s₂.inf
theorem multiset.le_inf {α : Type u_1} [semilattice_inf α] [order_top α] {s : multiset α} {a : α} :
a s.inf ∀ (b : α), b sa b
theorem multiset.inf_le {α : Type u_1} [semilattice_inf α] [order_top α] {s : multiset α} {a : α} (h : a s) :
s.inf a
theorem multiset.inf_mono {α : Type u_1} [semilattice_inf α] [order_top α] {s₁ s₂ : multiset α} (h : s₁ s₂) :
s₂.inf s₁.inf
@[simp]
theorem multiset.inf_dedup {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (s : multiset α) :
@[simp]
theorem multiset.inf_ndunion {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁.ndunion s₂).inf = s₁.inf s₂.inf
@[simp]
theorem multiset.inf_union {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (s₁ s₂ : multiset α) :
(s₁ s₂).inf = s₁.inf s₂.inf
@[simp]
theorem multiset.inf_ndinsert {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (a : α) (s : multiset α) :