set_induction_bounded — Mathlib

English

If a subset S of ℕ contains k and is closed under successor, and k ≤ n, then n ∈ S.

Русский

Пусть S ⊆ ℕ содержит k и замкнуто относительно successor, и k ≤ n; тогда n ∈ S.

LaTeX

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

Lean4

/-- A subset of `ℕ` containing `k : ℕ` and closed under `Nat.succ` contains every `n ≥ k`. -/
theorem set_induction_bounded {S : Set ℕ} (hk : k ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S) (hnk : k ≤ n) : n ∈ S :=
  @leRecOn (fun n => n ∈ S) k n hnk (@h_ind) hk

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