sbtw_iff — Mathlib

English

For Fin(n) with its 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 (using the Fin order).

Русский

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

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

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