Multiset.Ioc_eq_zero
theorem Multiset.Ioc_eq_zero :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Multiset.Ioc a b = 0 := by
sorry
This theorem states that for any type `α` equipped with a preorder and a locally finite order, if we take any two elements `a` and `b` from `α`, and if `a` is not less than `b`, then the multiset of elements `x` such that `a < x` and `x ≤ b` (denoted by `Multiset.Ioc a b`) is the zero multiset. In other words, there are no elements in `α` that are strictly greater than `a` and less than or equal to `b` when `a` is not less than `b`.
More concisely: For any preorder and locally finite type `α`, if `a ≤ b` in `α`, then the multiset of elements `x` in `α` with `a < x` and `x ≤ b` is empty.
|
Multiset.Ico_eq_zero
theorem Multiset.Ico_eq_zero :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a < b → Multiset.Ico a b = 0 := by
sorry
This theorem states that for any type `α` that has a preorder and a locally finite order, and any two elements `a` and `b` of `α`, if it is not the case that `a` is less than `b`, then the multiset of elements `x` such that `a ≤ x` and `x < b` (denoted by `Multiset.Ico a b`) is the zero multiset. Essentially, if `a` is not less than `b`, there are no elements `x` that satisfy the inequality `a ≤ x < b`, thus the multiset of such elements is empty.
More concisely: For any preorder type `α` with a locally finite order, the multiset of elements `x` satisfying `a ≤ x < b` is empty whenever `a` is not less than `b`.
|
Multiset.Icc_eq_zero
theorem Multiset.Icc_eq_zero :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, ¬a ≤ b → Multiset.Icc a b = 0 := by
sorry
This theorem is an alias for the reverse direction of `Multiset.Icc_eq_zero_iff`. It states that for any type `α` that has a preorder and a locally finite order, and for any two elements `a` and `b` of type `α`, if `a` is not less than or equal to `b` (i.e., `a` is strictly greater than `b`), then the multiset of elements `x` such that `a ≤ x` and `x ≤ b` (denoted as `Multiset.Icc a b`) is equal to the empty multiset, represented by `0`.
More concisely: For any type `α` with a preorder and locally finite order, if `a` is strictly greater than `b`, then the multiset of elements `x` with `a ≤ x ≤ b` is empty.
|