btw_iff — Mathlib

English

For Fin(n) with its circular order, btw a b c holds iff one of the cyclic inequalities a ≤ b ≤ c, b ≤ c ≤ a, or c ≤ a ≤ b holds (using the Fin order).

Русский

Для Fin(n) с циклическим порядком выполняется btw a b c тогда и только тогда, когда одно из неравенств a ≤ b ≤ c, b ≤ c ≤ a, или c ≤ a ≤ b верно (с учётом порядка Fin).

LaTeX

$$$ \\operatorname{btw}(a,b,c) \\iff (a \\le b \\land b \\le c) \\lor (b \\le c \\land c \\le a) \\lor (c \\le a \\land a \\le b) $$$

Lean4

theorem btw_iff : btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b :=
  .rfl

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