next_nat_zero — Mathlib

English

In a natural number indexing, next (i+1) equals i, i.e., the down-shape lowers indices by 1.

Русский

При индексации по натуральным числам, next (i+1) равняется i; форма вниз поNat уменьшает индекс на 1.

LaTeX

$$$\text{next}_{\mathbb{N}}(i+1) = i$$$

Lean4

@[simp]
theorem next_nat_zero : (ComplexShape.down ℕ).next 0 = 0 := by
  classical
  refine dif_neg ?_
  push_neg
  intro
  apply Nat.noConfusion

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