antisymm

Mathlib.Order.Circular

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

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 antisymm {a b c : α} (h : btw a b c) : btw c b a → a = b ∨ b = c ∨ c = a :=
  btw_antisymm h

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

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

Разделы

Аффилиация

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