strong_induction_on

Mathlib.Data.Nat.Init

URI: https://scilib.ai/kg/mathlib#Nat.strong_induction_on

Lean4

@[elab_as_elim]
protected theorem strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ n, (∀ m, m < n → p m) → p n) : p n :=
  Nat.strongRecOn n h

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

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

Разделы

Аффилиация

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