Lattice operations on multisets
sup
Supremum of a multiset: sup {a, b, c} = a ⊔ b ⊔ c
Equations
- s.sup = multiset.fold has_sup.sup ⊥ s
@[simp]
@[simp]
@[simp]
@[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 α) :
@[simp]
theorem
multiset.sup_union
{α : Type u_1}
[semilattice_sup_bot α]
[decidable_eq α]
(s₁ s₂ : multiset α) :
@[simp]
theorem
multiset.sup_ndinsert
{α : Type u_1}
[semilattice_sup_bot α]
[decidable_eq α]
(a : α)
(s : multiset α) :
(multiset.ndinsert a s).sup = a ⊔ s.sup
inf
Infimum of a multiset: inf {a, b, c} = a ⊓ b ⊓ c
Equations
- s.inf = multiset.fold has_inf.inf ⊤ s
@[simp]
@[simp]
@[simp]
@[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 α) :
@[simp]
theorem
multiset.inf_union
{α : Type u_1}
[semilattice_inf_top α]
[decidable_eq α]
(s₁ s₂ : multiset α) :
@[simp]
theorem
multiset.inf_ndinsert
{α : Type u_1}
[semilattice_inf_top α]
[decidable_eq α]
(a : α)
(s : multiset α) :
(multiset.ndinsert a s).inf = a ⊓ s.inf