wbtw_rotate_iff — Mathlib

English

Let x, y, z be points as above. The pair Wbtw x y z and Wbtw z x y can hold simultaneously only when x = y.

Русский

Пусть x, y, z — точки. Условие Wbtw x y z и Wbtw z x y одновременно выполняются только тогда, когда x = y.

LaTeX

$$$$ (Wbtw R x y z) \land (Wbtw R z x y) \leftrightarrow x = y $$$$

Lean4

theorem wbtw_rotate_iff [NoZeroSMulDivisors R V] (x : P) {y z : P} : Wbtw R x y z ∧ Wbtw R z x y ↔ x = y := by
  rw [wbtw_comm, wbtw_swap_right_iff, eq_comm]

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