sbtw_iff — Mathlib

English

For integers a,b,c with a circular order, sbtw a b c holds iff one of the cyclic strict inequalities a < b < c, b < c < a, or c < a < b holds.

Русский

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

LaTeX

$$$ \\operatorname{sbtw}(a,b,c) \\iff (a < b \\land b < c) \\lor (b < c \\land c < a) \\lor (c < a \\land a < b) $$$

Lean4

theorem sbtw_iff : sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b :=
  .rfl

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