sbtw_comm — Mathlib

English

Strictly between is symmetric in the same sense: y strictly between x and z iff z strictly between y and x.

Русский

Строгое между сохраняет симметрию: y строго между x и z тогда и только тогда z строго между y и x.

LaTeX

$$Sbtw R x y z \iff Sbtw R z y x$$

Lean4

theorem sbtw_comm {x y z : P} : Sbtw R x y z ↔ Sbtw R z y x := by
  rw [Sbtw, Sbtw, wbtw_comm, ← and_assoc, ← and_assoc, and_right_comm]

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