sbtw_asymm

Mathlib.Order.Circular

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

English

If sbtw a b c, then not sbtw c b a.

Русский

Если sbtw a b c, то не sbtw c b a.

LaTeX

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

Lean4

theorem sbtw_asymm {a b c : α} (h : sbtw a b c) : ¬sbtw c b a :=
  h.btw.not_sbtw

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

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

Разделы

Аффилиация

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