rotate_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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