induction

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.induction

← MathLib Explorer

English

`Ordinal.induction` but for NatOrdinal.

Русский

`Ordinal.induction` для NatOrdinal.

LaTeX

$$$\\forall {p: NatOrdinal \\to Prop}\\, (i: NatOrdinal),\\ (\\forall j:\\ NatOrdinal,\\ (\\forall k:\\ NatOrdinal,\\ k < j \\Rightarrow p k) \\Rightarrow p j) \\Rightarrow p i$$$

Lean4

/-- `Ordinal.induction` but for `NatOrdinal`. -/
theorem induction {p : NatOrdinal → Prop} : ∀ (i) (_ : ∀ j, (∀ k, k < j → p k) → p j), p i :=
  Ordinal.induction

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

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

Разделы

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

Аффилиация

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