strengthenStrictInt

Mathlib.Tactic.Linarith.Preprocessing

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.strengthenStrictInt

Lean4

/-- `strengthenStrictInt h` turns a proof `h` of a strict integer inequality `t1 < t2`
into a proof of `t1 ≤ t2 + 1`. -/
def strengthenStrictInt : Preprocessor
    where
  description := "strengthen strict inequalities over int"
  transform h := return [(← mkNonstrictIntProof h).getD h]

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

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

Разделы

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

Аффилиация

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