sbtw_trans_right

Mathlib.Order.Circular

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

← MathLib Explorer

English

If sbtw a b c and sbtw a c d, then sbtw a b d.

Русский

Если sbtw a b c и sbtw a c d, тогда sbtw a b d.

LaTeX

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

Lean4

theorem sbtw_trans_right {a b c d : α} (hbc : sbtw a b c) (hcd : sbtw a c d) : sbtw a b d :=
  (hbc.cyclic_left.trans_left hcd.cyclic_left).cyclic_right

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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