btw_cyclic — Mathlib

English

The between relation is cyclic: btw a b c holds iff btw c a b holds.

Русский

Отношение между циклично: btw a b c выполняется тогда и только тогда, когда выполняется btw c a b.

LaTeX

$$$\\forall a,b,c:\\alpha,\\ btw(a,b,c) \\iff btw(c,a,b)$$$

Lean4

/-- The order of the `↔` has been chosen so that `rw [btw_cyclic]` cycles to the right while
`rw [← btw_cyclic]` cycles to the left (thus following the prepended arrow). -/
theorem btw_cyclic {a b c : α} : btw a b c ↔ btw c a b :=
  ⟨btw_cyclic_right, btw_cyclic_left⟩

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