English
WCovBy a b means that a ≤ b and there is no element strictly between a and b.
Русский
WCovBy a b означает, что a ≤ b и между ними нет элемента.
LaTeX
$$$a \le b ∧ ∀ c, a < c \rightarrow \neg c < b$$$
Lean4
/-- `WCovBy a b` means that `a = b` or `b` covers `a`.
This means that `a ≤ b` and there is no element in between. This is denoted `a ⩿ b`.
-/
def WCovBy (a b : α) : Prop :=
a ≤ b ∧ ∀ ⦃c⦄, a < c → ¬c < b