sbtw_cyclic_left

Mathlib.Order.Circular

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

English

If a, b, c are strictly between, then sbtw b c a.

Русский

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

LaTeX

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

Lean4

theorem sbtw_cyclic_left {a b c : α} (h : sbtw a b c) : sbtw b c a :=
  h.btw.cyclic_left.sbtw_of_not_btw fun h' => h.not_btw h'.cyclic_left

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

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

Разделы

Аффилиация

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