wbtw_comm — Mathlib

English

The weak-between relation is symmetric with respect to swapping the endpoints: for any x, y, z, Wbtw R x y z holds if and only if Wbtw R z y x holds.

Русский

Отношение слабого между симметрично по отношению к концевым точкам: для любых x, y, z выполняется Wbtw R x y z тогда и только тогда, когда Wbtw R z y x.

LaTeX

$$Wbtw R x y z \iff Wbtw R z y x$$

Lean4

theorem wbtw_comm {x y z : P} : Wbtw R x y z ↔ Wbtw R z y x := by rw [Wbtw, Wbtw, affineSegment_comm]

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