not_sbtw_of_btw

Mathlib.Order.Circular

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

English

If a is between b and c, then not sbtw c b a.

Русский

Если a между b и c, то не строго между c и b.

LaTeX

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

Lean4

theorem not_sbtw_of_btw {a b c : α} (h : btw a b c) : ¬sbtw c b a := fun h' => h'.not_btw h

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

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

Разделы

Аффилиация

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