swap_right_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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