Bound — Mathlib

Lean4
/-- A `Bound` represents the result of analyzing a lower or upper bound expression.
If `e` is the scrutinee expression, then a lower bound expression like `3 < e`
is normalized to `¬e ≤ 3` and represented as `.lt 3`, and an upper bound expression
like `e ≤ 5` is represented as `.le 5`.
-/
inductive Bound/-- A strictly less-than lower bound `n ≱ e` or upper bound `e ≱ n`. (`interval_cases` uses
  less-equal exclusively, so less-than bounds are actually written as not-less-equal
  with flipped arguments.) -/

  | lt (n : ℤ)/-- A less-than-or-equal lower bound `n ≤ e` or upper bound `e ≤ n`. -/

  | le (n : ℤ)
Похожие утверждения