Multiset.sup_cons
theorem Multiset.sup_cons :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (a : α) (s : Multiset α),
(a ::ₘ s).sup = a ⊔ s.sup
The theorem `Multiset.sup_cons` states that for any type `α` equipped with a semilattice structure and a least element (`OrderBot`), and for any element `a` of type `α` and multiset `s` of elements of the same type `α`, the supremum of the multiset obtained by consing `a` onto `s` (denoted `a ::ₘ s`) is equal to the supremum of `a` and the supremum of `s`. In mathematical terminology, this states that for all `a` and `s`, $\bigvee (a :: s) = a \vee \bigvee s$, where $::$ denotes consing an element to a multiset, $\bigvee$ denotes the supremum, and $\vee$ is the sup operation in the semilattice.
More concisely: For any semilattice `α` with least element and multiset `s` of `α`, the supremum of `a :: s` is equal to the supremum of `a` and the supremum of `s`, i.e., $\bigvee (a :: s) = a \vee \bigvee s$.
|
Multiset.sup_le
theorem Multiset.sup_le :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Multiset α} {a : α},
s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a
The theorem `Multiset.sup_le` states that for any type `α` which has a semilattice structure with supremum (`SemilatticeSup α`) and a bottom element (`OrderBot α`), and for any multiset `s` of type `α` and any element `a` of type `α`, the supremum of the multiset `s` is less than or equal to `a` if and only if every element `b` in the multiset `s` is less than or equal to `a`. In other words, the greatest element of a multiset (considering duplicates) is less than or equal to `a` iff every element in the multiset is less than or equal to `a`.
More concisely: For any semilattice with supremum and bottom element type `α`, the multiset supremum of `α` is less than or equal to any element `a` if and only if every element in the multiset is less than or equal to `a`.
|
Multiset.inf_cons
theorem Multiset.inf_cons :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (a : α) (s : Multiset α),
(a ::ₘ s).inf = a ⊓ s.inf
The theorem `Multiset.inf_cons` states that for any multiset `s` and any element `a` of type `α`, where `α` is a semilattice with an order top, the infimum of the multiset obtained by consing `a` onto `s` is equal to the infimum of `a` and the infimum of `s`. In mathematical terms, given a multiset `s` and `a` in a semilattice `α`, we have `inf(a ∪ s) = a ⊓ inf(s)`.
More concisely: For any multiset `s` and element `a` in a semilattice `α` with an order top, the infimum of `a` combined with `s` is equal to the infimum of `a` and the infimum of `s` (i.e., `inf(a ∪ s) = a ∧ inf(s)`).
|
Multiset.inf_dedup
theorem Multiset.inf_dedup :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (s : Multiset α),
s.dedup.inf = s.inf
The theorem `Multiset.inf_dedup` states that for any type `α` that is a semilattice with an infimum operation, has a top element, and for which equality is decidable, the infimum of a multiset `s` remains the same even after removing duplicates from `s`. In other words, for any multiset `s` of elements of such a type `α`, the infimum of `s` is equal to the infimum of `s` with duplicates removed. This is characterized by the equation `Multiset.inf (Multiset.dedup s) = Multiset.inf s`.
More concisely: For any semilattice `α` with decidable equality and a top element, the infimum of a multiset remains unchanged when duplicates are removed. That is, `Multiset.inf (Multiset.dedup s) = Multiset.inf s` for any multiset `s` of elements from `α`.
|
Multiset.sup_dedup
theorem Multiset.sup_dedup :
∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] (s : Multiset α),
s.dedup.sup = s.sup
The theorem `Multiset.sup_dedup` states that for all types `α` equipped with a SemilatticeSup structure, an OrderBot structure and a DecidableEq structure, and for all multisets `s` of type `α`, the supremum of the multiset obtained by removing duplicates from `s` (`Multiset.dedup s`) is equal to the supremum of the multiset `s`. In other words, removing duplicates from a multiset does not change its supremum. This supremum is the join (`⊔`) of all elements in the multiset.
More concisely: For any semilattice-supplied, ordered type α with decidable equality, the supremum of a multiset equals the supremum of its deduplicated version.
|