asUpper

Mathlib.Tactic.IntervalCases

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.IntervalCases.Bound.asUpper

Lean4

/-- Assuming `Bound` represents an upper bound, this returns the (inclusive)
greatest integer value which is allowed. So `e ≤ 3` means the lower bound is 3 and
`e < 3` means the upper bound is `2`. Note that in the case of `e < 0` on `Nat`
the upper bound is `-1`, which is not representable as a `Nat`;
this is why we have to treat the `.lt` and `.le` cases separately instead of normalizing
everything to `.le` bounds.
-/
def asUpper : Bound → ℤ
  | .lt n => n - 1
  | .le n => n

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru