WCovBy — Mathlib

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

Похожие утверждения