btw_iff_not_sbtw — Mathlib

English

Let α be a circular order. For all a, b, c ∈ α, btw(a, b, c) if and only if not sbtw(c, b, a).

Русский

Пусть α — циклический порядок. Для любых a, b, c ∈ α верно: btw(a, b, c) тогда и только тогда, когда не sbtw(c, b, a).

LaTeX

$$$\\forall a,b,c \\in \\alpha, \\mathrm{btw}(a,b,c) \\iff \\neg \\mathrm{sbtw}(c,b,a).$$$

Lean4

theorem btw_iff_not_sbtw {a b c : α} : btw a b c ↔ ¬sbtw c b a :=
  iff_not_comm.1 sbtw_iff_not_btw

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