mathlib3 documentation

data.multiset.lattice

Lattice operations on multisets #

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

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 s b 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 s a 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 α) :