not_swap_right

Mathlib.Analysis.Convex.Between

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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