btw_of_sbtw

Mathlib.Order.Circular

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

English

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

Русский

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

LaTeX

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

Lean4

theorem btw_of_sbtw {a b c : α} (h : sbtw a b c) : btw a b c :=
  (sbtw_iff_btw_not_btw.1 h).1

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

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

Разделы

Аффилиация

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