Lattice operations on multisets #
sup #
Supremum of a multiset: sup {a, b, c} = a ⊔ b ⊔ c
Instances For
@[simp]
@[simp]
@[simp]
theorem
Multiset.sup_dedup
{α : Type u_1}
[SemilatticeSup α]
[OrderBot α]
[DecidableEq α]
(s : Multiset α)
:
@[simp]
theorem
Multiset.sup_ndunion
{α : Type u_1}
[SemilatticeSup α]
[OrderBot α]
[DecidableEq α]
(s₁ s₂ : Multiset α)
:
@[simp]
theorem
Multiset.sup_union
{α : Type u_1}
[SemilatticeSup α]
[OrderBot α]
[DecidableEq α]
(s₁ s₂ : Multiset α)
:
@[simp]
theorem
Multiset.sup_ndinsert
{α : Type u_1}
[SemilatticeSup α]
[OrderBot α]
[DecidableEq α]
(a : α)
(s : Multiset α)
:
inf #
Infimum of a multiset: inf {a, b, c} = a ⊓ b ⊓ c
Instances For
@[simp]
@[simp]
@[simp]
theorem
Multiset.inf_dedup
{α : Type u_1}
[SemilatticeInf α]
[OrderTop α]
[DecidableEq α]
(s : Multiset α)
:
@[simp]
theorem
Multiset.inf_ndunion
{α : Type u_1}
[SemilatticeInf α]
[OrderTop α]
[DecidableEq α]
(s₁ s₂ : Multiset α)
:
@[simp]
theorem
Multiset.inf_union
{α : Type u_1}
[SemilatticeInf α]
[OrderTop α]
[DecidableEq α]
(s₁ s₂ : Multiset α)
:
@[simp]
theorem
Multiset.inf_ndinsert
{α : Type u_1}
[SemilatticeInf α]
[OrderTop α]
[DecidableEq α]
(a : α)
(s : Multiset α)
: