range_sdiff_zero — Mathlib

English

For natural numbers n, the set range(n+1) with 0 removed equals the image of range(n) under the successor map.

Русский

Для натурального числа n множество range(n+1) без 0 равно образу range(n) под отображением successor.

LaTeX

$$$\\operatorname{range}(n+1) \\setminus \\{0\\} = \\operatorname{image}(\\operatorname{Nat.succ}, \\operatorname{range}(n))$$$

Lean4

theorem range_sdiff_zero {n : ℕ} : range (n + 1) \ {0} = (range n).image Nat.succ := by
  induction n with
  | zero => simp
  | succ k hk =>
    conv_rhs => rw [range_add_one]
    rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]
    simp

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