set_induction — Mathlib

English

A subset S of ℕ containing 0 and closed under successor contains every natural number.

Русский

Любое подмножество S натуральных чисел, содержащее 0 и замкнутое относительно successor, содержит все натуральные числа.

LaTeX

$$$\forall S\subseteq \mathbb{N},\; 0\in S \Rightarrow (\forall k\in \mathbb{N}, k\in S \Rightarrow k+1\in S) \Rightarrow \forall n\in \mathbb{N}, n\in S$$$

Lean4

/-- A subset of `ℕ` containing zero and closed under `Nat.succ` contains all of `ℕ`. -/
theorem set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S) (n : ℕ) : n ∈ S :=
  set_induction_bounded hb h_ind (zero_le n)

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