not_swap_left — Mathlib

English

For a witness h that x lies strictly between w and z (Sbtw R x y z), the statement Wbtw R y x z cannot hold.

Русский

Для свидетельства h того, что x строго между w и z (Sbtw R x y z), утверждение Wbtw R y x z невозможно.

LaTeX

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

Lean4

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

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