eq_of_between — Mathlib

English

If a,b are consecutive and a < x < c with a ⋖ b and b ⋖ c, then x = b.

Русский

Если a, b, c образуют последовательность и a < x < c при a ⋖ b и b ⋖ c, то x = b.

LaTeX

$${x : α} (hab : a \ CovBy b) (hbc : b \ CovBy c) (hax : a < x) (hxc : x < c) : x = b$$

Lean4

/-- If `a`, `b`, `c` are consecutive and `a < x < c` then `x = b`. -/
theorem eq_of_between {x : α} (hab : a ⋖ b) (hbc : b ⋖ c) (hax : a < x) (hxc : x < c) : x = b :=
  le_antisymm (le_of_not_gt fun h => hbc.2 h hxc) (le_of_not_gt <| hab.2 hax)

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