theorem other other

`classes_disjoint`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  35theorem classes_disjoint (x : ℝ)
  36    (hlong : 2 ≤ x) (hshort : x ≤ 2) : x = 2 := le_antisymm hshort hlong

Lean names referenced from this declaration's body.