sbtw_iff_btw_not_btw — Mathlib

English

Strict between holds exactly when between holds and the reverse between does not hold.

Русский

Строгое междуние выполняется тогда и только тогда, когда выполняется между и не выполняется обратное между.

LaTeX

$$$\\forall a,b,c:\\alpha,\\ sbtw(a,b,c) \\iff (btw(a,b,c) \\land \\neg btw(c,b,a))$$$

Lean4

theorem sbtw_iff_btw_not_btw {a b c : α} : sbtw a b c ↔ btw a b c ∧ ¬btw c b a :=
  CircularPreorder.sbtw_iff_btw_not_btw

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