not_btw_of_sbtw

Mathlib.Order.Circular

URI: https://scilib.ai/kg/mathlib#not_btw_of_sbtw

English

From sbtw a b c, it follows that not btw c b a.

Русский

Из sbtw a b c следует, что не выполняется btw c b a.

LaTeX

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

Lean4

theorem not_btw_of_sbtw {a b c : α} (h : sbtw a b c) : ¬btw c b a :=
  (sbtw_iff_btw_not_btw.1 h).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru