trans_left

Mathlib.Order.Circular

URI: https://scilib.ai/kg/mathlib#SBtw.sbtw.trans_left

English

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

Русский

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

LaTeX

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

Lean4

theorem trans_left {a b c d : α} (h : sbtw a b c) : sbtw b d c → sbtw a d c :=
  sbtw_trans_left h

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

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

Разделы

Аффилиация

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