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]
theorem
multiset.sup_coe
{α : Type u_1}
[semilattice_sup α]
[order_bot α]
(l : list α) :
↑l.sup = list.foldr has_sup.sup ⊥ l
@[simp]
@[simp]
theorem
multiset.sup_cons
{α : Type u_1}
[semilattice_sup α]
[order_bot α]
(a : α)
(s : multiset α) :
@[simp]
theorem
multiset.le_sup
{α : Type u_1}
[semilattice_sup α]
[order_bot α]
{s : multiset α}
{a : α}
(h : a ∈ s) :
theorem
multiset.sup_mono
{α : Type u_1}
[semilattice_sup α]
[order_bot α]
{s₁ s₂ : multiset α}
(h : s₁ ⊆ s₂) :
@[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 α) :
@[simp]
theorem
multiset.sup_union
{α : Type u_1}
[semilattice_sup α]
[order_bot α]
[decidable_eq α]
(s₁ s₂ : multiset α) :
@[simp]
theorem
multiset.sup_ndinsert
{α : Type u_1}
[semilattice_sup α]
[order_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]
theorem
multiset.inf_coe
{α : Type u_1}
[semilattice_inf α]
[order_top α]
(l : list α) :
↑l.inf = list.foldr has_inf.inf ⊤ l
@[simp]
@[simp]
theorem
multiset.inf_cons
{α : Type u_1}
[semilattice_inf α]
[order_top α]
(a : α)
(s : multiset α) :
@[simp]
theorem
multiset.inf_le
{α : Type u_1}
[semilattice_inf α]
[order_top α]
{s : multiset α}
{a : α}
(h : a ∈ s) :
theorem
multiset.inf_mono
{α : Type u_1}
[semilattice_inf α]
[order_top α]
{s₁ s₂ : multiset α}
(h : s₁ ⊆ s₂) :
@[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 α) :
@[simp]
theorem
multiset.inf_union
{α : Type u_1}
[semilattice_inf α]
[order_top α]
[decidable_eq α]
(s₁ s₂ : multiset α) :
@[simp]
theorem
multiset.inf_ndinsert
{α : Type u_1}
[semilattice_inf α]
[order_top α]
[decidable_eq α]
(a : α)
(s : multiset α) :
(multiset.ndinsert a s).inf = a ⊓ s.inf