sbtw_iff_not_btw — Mathlib

English

Let α be a circular order. For all a, b, c ∈ α, sbtw(a, b, c) is equivalent to not btw(c, b, a).

Русский

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

LaTeX

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

Lean4

theorem sbtw_iff_not_btw {a b c : α} : sbtw a b c ↔ ¬btw c b a :=
  by
  rw [sbtw_iff_btw_not_btw]
  exact and_iff_right_of_imp (btw_total _ _ _).resolve_left

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