btw_iff — Mathlib

English

For integers a,b,c with a circular order, btw a b c holds iff one of the cyclic inequalities a ≤ b ≤ c, b ≤ c ≤ a, or c ≤ a ≤ b holds.

Русский

Для целых чисел a, b, c в циклическом порядке выражение btw a b c истинно тогда и только тогда, когда выполняется одно из неравенств: a ≤ b ≤ c, b ≤ c ≤ a, или c ≤ a ≤ b.

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

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