exists_eq_succ_of_ne_one — Mathlib

English

For any n ∈ ℕ⁺ with n ≠ 1, there exists k ∈ ℕ⁺ such that n = k + 1.

Русский

Для любого n ∈ ℕ⁺, не равного 1, существует k ∈ ℕ⁺ such that n = k + 1.

LaTeX

$$$$ \forall n \in \mathbb{N}_{>0},\; n \neq 1 \Rightarrow \exists k \in \mathbb{N}_{>0},\; n = k + 1 $$$$

Lean4

/-- If `n : ℕ+` is different from `1`, then it is the successor of some `k : ℕ+`. -/
theorem exists_eq_succ_of_ne_one : ∀ {n : ℕ+} (_ : n ≠ 1), ∃ k : ℕ+, n = k + 1
  | ⟨1, _⟩, h₁ => False.elim <| h₁ rfl
  | ⟨n + 2, _⟩, _ => ⟨⟨n + 1, by simp⟩, rfl⟩

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