Set.OrdConnected.apply_wcovBy_apply_iff
theorem Set.OrdConnected.apply_wcovBy_apply_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
(Set.range ⇑f).OrdConnected → (f a ⩿ f b ↔ a ⩿ b)
This theorem states that, for any two types `α` and `β` with preorder structures, and for any function `f` from `α` to `β` which is an order-embedding, if the range of `f` is order-connected, then the relation of being covered by (`⩿`) between the images of two elements `a` and `b` under `f` is equivalent to the relation of being covered by between `a` and `b` themselves. In simpler terms, it means if `f(a)` is covered by `f(b)` then `a` is also covered by `b` and vice versa, assuming that the range of the function `f` is order-connected.
More concisely: If `f : α → β` is an order-embedding from preordered types `α` and `β`, and the range of `f` is order-connected, then for all `a, b ∈ α`, `a ⩿ b` if and only if `f a ⩿ f b`.
|
LT.lt.exists_disjoint_Iio_Ioi
theorem LT.lt.exists_disjoint_Iio_Ioi :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y
This theorem asserts that for any two elements `a` and `b` of a type `α` equipped with a linear order, if `a` is strictly less than `b`, then there exist elements `a'` and `b'` such that `a'` is strictly greater than `a`, `b'` is strictly less than `b`, and every element `x` less than `a'` is strictly less than every element `y` greater than `b'`. This ensures that the interval `(-∞, a')` is strictly to the left of the interval `(b', ∞)`.
More concisely: Given any linear order on type `α`, if `a` is strictly less than `b`, then there exist elements `a'` and `b'` such that `a` is strictly between `a'` and `b'`, and `(a', ∞)` is strictly to the right of `(b', b)`.
|
Mathlib.Order.Cover._auxLemma.4
theorem Mathlib.Order.Cover._auxLemma.4 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b)
This theorem in Lean's `Mathlib.Order.Cover._auxLemma.4` states that for any pair of propositions `a` and `b`, the existence of a proof for `a` implying `b` is equivalent to the conjunction of `a` and `b`. In more mathematical terms, it says that `∃ (_ : a), b` is equivalent to `a ∧ b`.
More concisely: The theorem in Lean's `Mathlib.Order.Cover._auxLemma.4` asserts that for all propositions `a` and `b`, the existence of a proof of `a` implies `b` is equivalent to `a` and `b` holding simultaneously.
|
WCovBy.eq_or_covBy
theorem WCovBy.eq_or_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → a = b ∨ a ⋖ b
This theorem, named `WCovBy.eq_or_covBy`, states that for any given type `α` that has a partial order, and any two instances `a` and `b` of this type, if `a` weakly covers `b` (denoted as `a ⩿ b`), then either `a` is equal to `b` or `a` is covered by `b` (denoted as `a ⋖ b`). This is effectively an alias for the forward direction of the theorem `wcovBy_iff_eq_or_covBy`.
More concisely: For any type with a partial order, if one element weakly covers another, then they are either equal or the first is covered by the second.
|
wcovBy_eq_reflGen_covBy
theorem wcovBy_eq_reflGen_covBy :
∀ {α : Type u_1} [inst : PartialOrder α], (fun x x_1 => x ⩿ x_1) = Relation.ReflGen fun x x_1 => x ⋖ x_1
This theorem states that, for any given type 'α' which has a partial order defined on it, the relation 'weakly covers', denoted as '⩿', is equivalent to the reflexive transitive closure of the 'covers' relation, denoted by '⋖'. In other words, an element weakly covers another if and only if it covers that element in a non-strict partial order, or it is equal to that element.
More concisely: For any type 'α' with a partial order, the relation 'weakly covers' ('⩿') is equal to the reflexive transitive closure of the 'covers' ('⋖') relation.
|
wcovBy_iff_le_and_eq_or_eq
theorem wcovBy_iff_le_and_eq_or_eq :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b ↔ a ≤ b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b := by
sorry
This theorem, `wcovBy_iff_le_and_eq_or_eq`, states that for any types `α` (which have a partial order), and any elements `a` and `b` of type `α`, the condition `a ⩿ b` is equivalent to the conjunction of `a ≤ b` and the statement that for all `c : α`, if `a ≤ c` and `c ≤ b`, then `c` must be equal to either `a` or `b`. In more familiar mathematical terms, this theorem asserts that `a` is weakly covered by `b` if and only if `a` is less than or equal to `b` and any element `c` that lies between `a` and `b` (inclusive) must be equal to either `a` or `b`.
More concisely: A element `a` is weakly covered by another element `b` in a partially ordered type if and only if `a ≤ b` and for all `c`, if `a ≤ c ≤ b`, then `c = a` or `c = b`.
|
WCovBy.toDual
theorem WCovBy.toDual :
∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → OrderDual.toDual b ⩿ OrderDual.toDual a
This theorem, referred to as `WCovBy.toDual`, is stating that for any type `α` with a pre-order, and for any two elements `a` and `b` of this type, if `a` is weakly covered by `b` (denoted by `a ⩿ b`), then the OrderDual of `b` is weakly covered by the OrderDual of `a`. Here, weakly covered is a relation that typically means `a` is less than or equal to `b` and the `OrderDual` of a type is just the type with the order reversed. The `OrderDual.toDual` function is used to convert `a` and `b` to their duals in the order-reversed type.
More concisely: For any type with a pre-order and any two elements `a` and `b`, if `a` is weakly covered by `b`, then the dual of `b` is weakly covered by the dual of `a` in the order-reversed pre-order.
|
not_covBy_iff
theorem not_covBy_iff : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a < b → (¬a ⋖ b ↔ ∃ c, a < c ∧ c < b)
This theorem states that for any type `α` endowed with a less-than relation `<`, given two elements `a` and `b` such that `a < b`, the proposition that `b` does not cover `a` is equivalent to the existence of an element `c` such that `a < c` and `c < b`. In other words, `b` fails to cover `a` if and only if there is another element sitting strictly between `a` and `b`.
More concisely: For any type `α` with a total order `<`, the proposition `a < b` and `∀c, a < c → c < b` are equivalent.
|
CovBy.toDual
theorem CovBy.toDual : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a ⋖ b → OrderDual.toDual b ⋖ OrderDual.toDual a := by
sorry
The theorem `CovBy.toDual` states that for any type `α` with a less-than (`LT`) operation and any two elements `a` and `b` of this type, if `a` is covered by `b` (denoted by `a ⋖ b`), then `b` is covered by `a` in the `OrderDual` of `α` (denoted by `OrderDual.toDual b ⋖ OrderDual.toDual a`). In other words, if `a` is covered by `b`, then reversing the ordering flips the cover relation. This theorem serves as an alias for the reverse direction of the theorem `toDual_covBy_toDual_iff`.
More concisely: For any type equipped with a reflexive and transitive relation `LT`, if `a LT b` implies `b LT a` in the dual order `OrderDual`, then `LT` and `OrderDual` are dual orders.
|
not_wcovBy_iff
theorem not_wcovBy_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → (¬a ⩿ b ↔ ∃ c, a < c ∧ c < b) := by
sorry
This theorem states that for any given type `α` with a preorder relation, and any two elements `a` and `b` of that type such that `a` is less than or equal to `b`, `b` does not cover `a` if and only if there exists an element `c` such that `c` is strictly between `a` and `b`. In other words, `b` does not cover `a` when there exists another element that is greater than `a` but less than `b`.
More concisely: For any preordered type `α` and elements `a` and `b` with `a ≤ b`, `a` is not covered by `b` if and only if there exists `c` such that `a < c < b`.
|
WCovBy.covBy_of_lt
theorem WCovBy.covBy_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → a < b → a ⋖ b
This theorem states that for any type `α` equipped with a preorder, given two elements `a` and `b` of type `α`, if `a` is covered by `b` (denoted `a ⩿ b`) and `a` is less than `b` (denoted `a < b`), then `a` is strictly covered by `b` (denoted `a ⋖ b`). In other words, in the context of a preorder, if one element is covered by and less than another, then it is also strictly covered by that other element.
More concisely: If `α` is a type with a preorder such that `a ⩿ b` and `a < b`, then `a ⋖ b`.
|
WCovBy.Icc_eq
theorem WCovBy.Icc_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → Set.Icc a b = {a, b}
This theorem states that for any given type `α` which has a partial order, and for any two elements `a` and `b` of this type, if `a` is incomparable to `b` (denoted by `a ⩿ b`), then the closed interval from `a` to `b` (represented by `Set.Icc a b`) is equal to the set containing just `a` and `b` (denoted by `{a, b}`). Here, a closed interval from `a` to `b` is defined as the set of all elements `x` such that `a ≤ x` and `x ≤ b`. An element is said to be incomparable to another if it is neither less than nor greater than the other.
More concisely: For any type `α` with a partial order and any incomparable elements `a` and `b` in `α`, the set of elements between `a` and `b` (inclusive) is equal to the set containing only `a` and `b`. In Lean notation, `Set.Icc a b = {a, b}`.
|
LE.le.wcovBy_of_le
theorem LE.le.wcovBy_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → b ≤ a → a ⩿ b
This theorem, named `LE.le.wcovBy_of_le`, is an alias of the `wcovBy_of_le_of_le` theorem. Given a type `α` that follows the rules of a preorder, and any two elements `a` and `b` of this type, if `a` is less than or equal to `b` and `b` is less than or equal to `a`, then `a` and `b` are weakly covered, denoted by `a ⩿ b`. In other words, this theorem states that if `a` and `b` are equal in the context of a preorder, then they are weakly covered by each other.
More concisely: In a preorder, if two elements are equal, then they are weakly covered by each other.
|
exists_lt_lt_of_not_covBy
theorem exists_lt_lt_of_not_covBy : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a < b → ¬a ⋖ b → ∃ c, a < c ∧ c < b := by
sorry
This theorem, `exists_lt_lt_of_not_covBy`, is an alias to the forward direction of the `not_covBy_iff` theorem. It states that for any types `α` with a less than (`<`) operation, and any two instances `a` and `b` of this type, if `a` is less than `b` and `b` does not cover `a` (denoted `¬a ⋖ b`), then there exists an element `c` such that `a` is less than `c` and `c` is less than `b`. In simpler terms, if `a` is less than `b` and `b` does not cover `a`, then there is an element `c` that lies between `a` and `b`.
More concisely: If `a < b` and `a ⋖ b`, then there exists `c` such that `a < c < b`.
|
Set.wcovBy_insert
theorem Set.wcovBy_insert : ∀ {α : Type u_1} (x : α) (s : Set α), s ⩿ insert x s
The theorem `Set.wcovBy_insert` states that for any type `α`, any element `x` of type `α`, and any set `s` of type `α`, the set `s` is a weak cover of the set obtained by inserting `x` into `s`. This implies that every element in the set obtained by inserting `x` into `s` is also an element of `s`, i.e., `s` contains all the elements of the insert operation.
More concisely: For any type `α`, any set `s` of `α`, and any `x` in `α`, the set `s` is a weak cover of the set `s.insert x`.
|
CovBy.lt
theorem CovBy.lt : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a ⋖ b → a < b
This theorem, `CovBy.lt`, states that for all types `α` that have a less-than (`<`) operation, if `a` is covered by `b` (denoted `a ⋖ b`), then `a` is less than `b`. This is a universal claim, holding for any possible values of `a` and `b` of type `α`.
More concisely: For all types `α` with a less-than operation, if `a ⋖ b` holds, then `a < b`.
|
Mathlib.Order.Cover._auxLemma.5
theorem Mathlib.Order.Cover._auxLemma.5 : ∀ {a : Prop}, (¬¬a) = a
This theorem, `Mathlib.Order.Cover._auxLemma.5`, states that for all propositions `a`, the double negation of `a` is equivalent to `a`. In the language of logic, this theorem asserts that stating "it is not the case that `a` is not true" is the same as stating "`a` is true".
More concisely: The theorem asserts that the double negation of a proposition is equivalent to the proposition itself.
|
Mathlib.Order.Cover._auxLemma.3
theorem Mathlib.Order.Cover._auxLemma.3 : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) = ∃ x, ¬p x
This theorem, from the `Mathlib.Order.Cover` namespace and named `_auxLemma.3`, states that for any type `α` and property `p` that each `α` might have, the statement "not all `x` in `α` have the property `p`" is logically equivalent to "there exists an `x` in `α` that does not have the property `p`". In mathematical notation, this is saying that "¬∀x, p(x)" is equivalent to "∃x, ¬p(x)".
More concisely: The theorem in Lean 4's `Mathlib.Order.Cover` namespace, named `_auxLemma.3`, asserts the logical equivalence of "not all elements in type `α` have property `p`" and "there exists an element in `α` that lacks property `p`". Mathematically, "∀x ≠ some x', ¬p(x)" is equivalent to "∃x, ¬p(x)".
|
CovBy.wcovBy
theorem CovBy.wcovBy : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b → a ⩿ b
This theorem, `CovBy.wcovBy`, states that for any type `α` that has a `Preorder` instance (i.e., for which a less-than-or-equal-to relation is defined), given any two elements `a` and `b` of type `α`, if `a` is strictly less than (`⋖`) `b`, then `a` is less than or equal to (`⩿`) `b`. Essentially, it's guaranteeing that the less-than-or-equal-to relation encompasses the strictly-less-than relation within any preordered set.
More concisely: In any preordered set, if `a ⋖ b` holds, then `a ⩿ b` holds.
|
toDual_covBy_toDual_iff
theorem toDual_covBy_toDual_iff :
∀ {α : Type u_1} [inst : LT α] {a b : α}, OrderDual.toDual b ⋖ OrderDual.toDual a ↔ a ⋖ b
This theorem, `toDual_covBy_toDual_iff`, states that for any type `α` that has a less than operation `LT α`, and for any two instances `a` and `b` of this type, the statement "the order dual of `b` is less than the order dual of `a`" is equivalent to the statement "`a` is less than `b`". In other words, applying the `OrderDual.toDual` function to `a` and `b` and then comparing them gives the same result as comparing `a` and `b` directly. This theorem essentially says that the `OrderDual.toDual` function preserves the order of elements.
More concisely: For any type equipped with a total order and its order dual, the order dual of a is less than the order dual of b if and only if a is less than b.
|
CovBy.eq_of_between
theorem CovBy.eq_of_between :
∀ {α : Type u_1} [inst : LinearOrder α] {a b c x : α}, a ⋖ b → b ⋖ c → a < x → x < c → x = b
This theorem, `CovBy.eq_of_between`, states that in a linear order `α`, if `a`, `b`, and `c` are consecutive elements such that `a` is less than `x` and `x` is less than `c`, then `x` must be equal to `b`. In other words, if `x` falls between `a` and `c`, and `b` is the element that comes immediately after `a` and immediately before `c`, then `x` has to be `b`.
More concisely: If `a`, `x`, and `b` are consecutive elements in a linear order `α` with `a < x < b`, then `x = b`.
|
LT.lt.exists_lt_lt
theorem LT.lt.exists_lt_lt : ∀ {α : Type u_1} [inst : LT α] {a b : α}, a < b → ¬a ⋖ b → ∃ c, a < c ∧ c < b
This theorem, `LT.lt.exists_lt_lt`, states that for any type `α` with a less-than relationship (`<`), given two elements `a` and `b` of type `α`, if `a` is less than `b` and `b` does not cover `a`, then there exists an element `c` such that `a` is less than `c` and `c` is less than `b`. In simple terms, if `a` is less than `b` and `b` doesn't completely 'cover' `a`, there is another element `c` that lies between `a` and `b`. This theorem is an alias of the forward direction of the `not_covBy_iff` theorem.
More concisely: If `α` is a type with a linear order relation `<` such that `a < b` and `b` does not cover `a`, then there exists `c` such that `a < c` and `c < b`.
|
CovBy.Ioo_eq
theorem CovBy.Ioo_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b → Set.Ioo a b = ∅
The theorem `CovBy.Ioo_eq` states that for any type `α` that has a preorder structure, and for any two elements `a` and `b` of type `α`, if `a` is strictly covered by `b` (`a ⋖ b`), then the left-open right-open interval between `a` and `b` (`Set.Ioo a b`) is equal to the empty set. In other words, if `a` is strictly covered by `b`, there are no elements of type `α` that are strictly greater than `a` and strictly less than `b`.
More concisely: For any preordered type `α` and elements `a` and `b` such that `a` is strictly covered by `b`, the interval `(a, b)` is empty.
|
Mathlib.Order.Cover._auxLemma.2
theorem Mathlib.Order.Cover._auxLemma.2 : ∀ (p : Prop), (True ∧ p) = p
This theorem, named `Mathlib.Order.Cover._auxLemma.2`, states that given any proposition `p`, the logical conjunction of `True` and `p` is equivalent to `p`. In other words, logically, `True` and something is always that something.
More concisely: The theorem `Mathlib.Order.Cover._auxLemma.2` in Lean 4 asserts that `True` and a proposition `p` are logically equivalent (i.e., `True ∧ p` is equivalent to `p`).
|
covBy_iff_lt_and_eq_or_eq
theorem covBy_iff_lt_and_eq_or_eq :
∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⋖ b ↔ a < b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b := by
sorry
This theorem, `covBy_iff_lt_and_eq_or_eq`, provides an "if and only if" version of `CovBy.eq_or_eq` and `covBy_of_eq_or_eq`. It applies to any type `α` that has a partial order structure. Given elements `a` and `b` of this type, the theorem states that `a` is covered by `b` (denoted `a ⋖ b`) if and only if `a` is less than `b` and for all `c` of type `α`, if `a` is less than or equal to `c` and `c` is less than or equal to `b`, then `c` equals `a` or `c` equals `b`.
More concisely: For any type with a partial order structure, `a ⋖ b` if and only if `a < b` and for all `c`, if `a ≤ c ≤ b` then `c = a` or `c = b`.
|
WCovBy.eq_or_eq
theorem WCovBy.eq_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, a ⩿ b → a ≤ c → c ≤ b → c = a ∨ c = b
This theorem, `WCovBy.eq_or_eq`, applies to any type `α` that has a partial order defined on it. It takes three instances of this type, `a`, `b`, and `c`. The theorem states that if `a` is covered by `b` (symbolized as `a ⩿ b`) and `a` is less than or equal to `c` (symbolized as `a ≤ c`) and `c` is less than or equal to `b` (symbolized as `c ≤ b`), then `c` must be equal to either `a` or `b`. In essence, this theorem defines a key property of the relationship between three elements in a partially ordered set.
More concisely: If `a ⩿ b`, `a ≤ c`, and `c ≤ b` in a partially ordered set, then `c = a` or `c = b`.
|
WCovBy.le
theorem WCovBy.le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → a ≤ b
This theorem states that for any type `α` (assuming `α` forms a preordered set), if `a` is weakly covered by `b` (indicated by `a ⩿ b`), then `a` is less than or equal to `b` (expressed as `a ≤ b`). In other words, in a preordered set, weak coverage implies the underlying ordering.
More concisely: In a preordered set, if `a` is weakly covered by `b` (`a ⩿ b`), then `a` is less than or equal to `b` (`a ≤ b`).
|
Mathlib.Order.Cover._auxLemma.10
theorem Mathlib.Order.Cover._auxLemma.10 :
∀ {α : Type u_1} [inst : LT α] {a b : α}, (OrderDual.toDual b ⋖ OrderDual.toDual a) = (a ⋖ b)
The theorem, named `Mathlib.Order.Cover._auxLemma.10`, states that for all types `α` equipped with a less-than operation, and for any two elements `a` and `b` of type `α`, the less-than relation between the `OrderDual` of `b` and the `OrderDual` of `a` is equivalent to the less-than relation between `a` and `b`. In other words, flipping the order of comparison through the `OrderDual` transformation does not change the outcome of the less-than relation, and hence the `OrderDual` is essentially a reflection of the original order.
More concisely: For all types equipped with a total order and any two elements, the order relation between their OrderDual is equivalent.
|
not_covBy
theorem not_covBy : ∀ {α : Type u_1} [inst : LT α] {a b : α} [inst_1 : DenselyOrdered α], ¬a ⋖ b
This theorem states that in a densely ordered set, no element 'a' strictly covers another element 'b'. In other words, there is no element 'a' such that it is less than 'b' and no element exists strictly between 'a' and 'b'. The term "DenselyOrdered" refers to an ordered set where between any two elements there is another element.
More concisely: In a densely ordered set, there exist no strictly increasing sequences of length 2.
|
Set.OrdConnected.apply_covBy_apply_iff
theorem Set.OrdConnected.apply_covBy_apply_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
(Set.range ⇑f).OrdConnected → (f a ⋖ f b ↔ a ⋖ b)
This theorem states that for any types `α` and `β`, and instances of preorders on `α` and `β`, given any two elements `a` and `b` of `α` and a strictly increasing function `f` from `α` to `β`, if the range of `f` is order-connected (that is, every element that lies between any two elements in the range is also in the range), then `f(a)` is less than `f(b)` if and only if `a` is less than `b`. Essentially, the ordering of elements in the domain `α` is preserved by the function `f` when moving to the range in `β`.
More concisely: Given preorders on types `α` and `β`, if `f` is a strictly increasing function from `α` to `β` with order-connected range, then `a < b` in `α` implies `f(a) < f(b)` in `β`.
|
CovBy.ofDual
theorem CovBy.ofDual : ∀ {α : Type u_1} [inst : LT α] {a b : αᵒᵈ}, b ⋖ a → OrderDual.ofDual a ⋖ OrderDual.ofDual b := by
sorry
The theorem `CovBy.ofDual` states that for any type `α` under the less-than (`LT`) operation, if `b` is covered by `a` in the order dual, then the undualized `a` is covered by the undualized `b`. Here, "covered by" (`⋖`) is a relation on an ordered set where `b` is said to cover `a` if `b > a` and there is no element `c` such that `b > c > a`. The order dual of a set reverses the order of the elements, and the function `OrderDual.ofDual` is the identity function that maps each element back to itself in the original order.
More concisely: If `a ⋖ b` holds in an ordered set under the order dual, then `OrderDual.ofDual a ⋖ OrderDual.ofDual b` holds in the original order.
|
WCovBy.ofDual
theorem WCovBy.ofDual :
∀ {α : Type u_1} [inst : Preorder α] {a b : αᵒᵈ}, b ⩿ a → OrderDual.ofDual a ⩿ OrderDual.ofDual b
The theorem `WCovBy.ofDual` states that for any preorder set `α` and any two elements `a` and `b` from the dual of `α`, if `b` weakly covers `a`, then the elements `a` and `b` when mapped through the identity function `OrderDual.ofDual` will also hold the weak covering relation but with the ordering reversed, i.e., `a` weakly covers `b` in the original preorder.
More concisely: For any preorder sets α and given elements a and b in α\*, if b weakly covers a in the dual preorder, then a weakly covers b in the original preorder.
|
WCovBy.covBy_or_eq
theorem WCovBy.covBy_or_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → a ⋖ b ∨ a = b
This theorem, `WCovBy.covBy_or_eq`, is essentially an alias of the forward direction of `wcovBy_iff_covBy_or_eq`. It states that for any type `α` that has a partial order, given any two elements `a` and `b` of this type, if `a` weakly covers `b` (denoted as `a ⩿ b`), then either `a` strictly covers `b` (denoted as `a ⋖ b`) or `a` is equal to `b`.
More concisely: If `α` is a type with a partial order, then for all `a` and `b` in `α`, if `a` weakly covers `b` (`a ⩿ b`), then `a` is related to `b` either by strict covering (`a ⋖ b`) or equality (`a = b`).
|