le_induction_down

Mathlib.Data.Int.Init

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

Lean4

/-- See `Int.inductionOn'` for an induction in both directions. -/
@[elab_as_elim]
protected theorem le_induction_down {m : ℤ} {motive : ∀ n, n ≤ m → Prop} (base : motive m m.le_refl)
    (pred : ∀ n hmn, motive n hmn → motive (n - 1) (by cutsat)) : ∀ n hmn, motive n hmn := fun n ↦
  Int.inductionOn' n m (fun _ ↦ base) (fun k hle _ hle' ↦ by cutsat) fun k hle hi _ ↦ pred k hle (hi hle)

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

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

Разделы

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

Аффилиация

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