count_nth_succ — Mathlib

English

For a predicate p with suitable finite bounds, count p (nth p n + 1) = n + 1; i.e., advancing by one in the argument of nth increases the count by one.

Русский

При допустимых конечных ограничениях счётчик даёт: count p (nth p n + 1) = n + 1, то есть переход к следующему индексу увеличивает счетчик на единицу.

LaTeX

$$$$ \\forall n, \\; \\mathrm{count}(p, \\mathrm{nth}(p, n) + 1) = n + 1.$$$$

Lean4

theorem count_nth_succ {n : ℕ} (hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset) : count p (nth p n + 1) = n + 1 := by
  rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]

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