not_rotate

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#Sbtw.not_rotate

English

If h is a witness that x lies strictly between y and z, then Wbtw R z x y cannot hold.

Русский

Если h свидетельствует, что x строго между y и z, то Wbtw R z x y невозможно.

LaTeX

$$$$ \text{If } h: Sbtw R x y z, \quad \lnot Wbtw R z x y $$$$

Lean4

theorem not_rotate [NoZeroSMulDivisors R V] {x y z : P} (h : Sbtw R x y z) : ¬Wbtw R z x y := fun hs =>
  h.left_ne (h.wbtw.rotate_iff.1 hs)

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

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

Разделы

Аффилиация

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