twoStepInduction

Mathlib.Data.Nat.Init

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

Lean4

/-- Induction principle deriving the next case from the two previous ones. -/
def twoStepInduction {P : ℕ → Sort*} (zero : P 0) (one : P 1) (more : ∀ n, P n → P (n + 1) → P (n + 2)) : ∀ a, P a
  | 0 => zero
  | 1 => one
  | _ + 2 => more _ (twoStepInduction zero one more _) (twoStepInduction zero one more _)

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

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

Разделы

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

Аффилиация

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