leRecOn_succ_left

Mathlib.Data.Nat.Init

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

Lean4

theorem leRecOn_succ_left {C : ℕ → Sort*} {n m} {next : ∀ {k}, C k → C (k + 1)} (x : C n) (h1 : n ≤ m)
    (h2 : n + 1 ≤ m) : (leRecOn h2 next (next x) : C m) = (leRecOn h1 next x : C m) :=
  leRec_succ_left (motive := fun n _ => C n) _ (fun _ _ => @next _) _ _

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

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

Разделы

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

Аффилиация

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