range_add_one' — Mathlib

English

The range of n+1 equals the insert of 0 into the map of range n by adding 1 to every index.

Русский

Диапазон n+1 равен включению 0 в образ диапазона n под отображением i ↦ i+1.

LaTeX

$$$\\operatorname{range}(n+1) = \\operatorname{insert}(0, \\operatorname{map}(\\langle \\lambda i. i+1, _ \\rangle)(\\operatorname{range}(n)))$$$

Lean4

theorem range_add_one' (n : ℕ) : range (n + 1) = insert 0 ((range n).map ⟨fun i => i + 1, fun i j => by simp⟩) := by
  ext (⟨⟩ | ⟨n⟩) <;> simp [Nat.zero_lt_succ n]

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