sbtw_of_btw_not_btw

Mathlib.Order.Circular

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

English

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

Русский

Если btw a b c и не выполняется btw c b a, то sbtw a b c.

LaTeX

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

Lean4

theorem sbtw_of_btw_not_btw {a b c : α} (habc : btw a b c) (hcba : ¬btw c b a) : sbtw a b c :=
  sbtw_iff_btw_not_btw.2 ⟨habc, hcba⟩

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

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

Разделы

Аффилиация

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