English
There is an induction principle for ENat: for any motive : ENat → Prop, if motive(0) holds, if for all n ∈ ℕ motive(n.cast) → motive(n.succ.cast), and if motive(n.cast) holds for all n ∈ ℕ then motive(⊤). Then motive(a) holds for every a ∈ ENat.
Русский
Существует индуктивность по ENat: если для мотива P выполнены условия на 0, на переход n.cast → n.succ.cast и если P(n.cast) верно для всех натуральных n, то P(⊤) и, следовательно, P(a) для любого a ∈ ENat.
LaTeX
$$$\forall {motive : ENat \to \mathrm{Prop}}\ (a : ENat),\ motive 0 \to (\forall n : \mathbb{N},\ motive (n.cast) \to motive (n.succ.cast)) \\to\ ((\forall n : \mathbb{N},\ motive (n.cast)) \to motive \top) \to motive a$$
Lean4
@[elab_as_elim]
theorem nat_induction {motive : ℕ∞ → Prop} (a : ℕ∞) (zero : motive 0) (succ : ∀ n : ℕ, motive n → motive n.succ)
(top : (∀ n : ℕ, motive n) → motive ⊤) : motive a :=
by
have A : ∀ n : ℕ, motive n := fun n => Nat.recOn n zero succ
cases a
· exact top A
· exact A _
