Theorem I.5.2 (帰納法原理 / Induction Principle)

• Theorem I.5.2 (帰納法原理 / Induction Principle) #Card
  • $A \subset \mathbb{N}$ が $\mathbb{N}$ 全体になる条件。

Back

If $A \subset \mathbb{N}$ has the property that $0 \in A$, and $n \in A$ implies $n + 1 \in A$, then $A = \mathbb{N}$.

• Peano の公理系（1889）の「$\mathbb{N}$ はこの 2 条件を満たす最小の集合」という公理と同値。より一般の Theorem XXVII.4.5（超限帰納法）の特別な場合。
• 記法: $\mathbb{N}_m := {n \in \mathbb{N} : n \geq m}$；$n < \omega \iff n \in \mathbb{N}$（$\omega$ は最初の無限順序数）。

Lean

Nat.rec / Nat.le_induction

本ノート RoyalRoad.ChapterI.thm_I_5_2_induction（Notes/ChapterI.lean、lake build 済み）