swap_left_iff — Mathlib

English

If h is a witness that x lies between y and z (Wbtw R x y z), then Wbtw R y x z holds exactly when x = y.

Русский

Если имеется свидетельство того, что x лежит между y и z (Wbtw R x y z), то Wbtw R y x z верно тогда и только тогда, когда x = y.

LaTeX

$$$$ \text{If } h: Wbtw R x y z, \quad Wbtw R y x z \iff x = y $$$$

Lean4

theorem swap_left_iff [NoZeroSMulDivisors R V] {x y z : P} (h : Wbtw R x y z) : Wbtw R y x z ↔ x = y := by
  rw [← wbtw_swap_left_iff R z, and_iff_right h]

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