le_induction

Mathlib.Data.Int.Init

URI: https://scilib.ai/kg/mathlib#Int.le_induction

Lean4

/-- See `Int.inductionOn'` for an induction in both directions. -/
@[elab_as_elim]
protected theorem le_induction {m : ℤ} {motive : ∀ n, m ≤ n → Prop} (base : motive m m.le_refl)
    (succ : ∀ n hmn, motive n hmn → motive (n + 1) (le_add_one hmn)) : ∀ n hmn, motive n hmn := by
  refine fun n ↦ Int.inductionOn' n m ?_ ?_ ?_ <;> grind

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

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

Разделы

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

Аффилиация

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