cyclic_left

Mathlib.Order.Circular

URI: https://scilib.ai/kg/mathlib#Btw.btw.cyclic_left

English

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

Русский

Если a находится между b и c, то b находится между c и a.

LaTeX

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

Lean4

theorem cyclic_left {a b c : α} (h : btw a b c) : btw b c a :=
  btw_cyclic_left h

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

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

Разделы

Аффилиация

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