nth_count — Mathlib

English

For infinite p, count p (nth p n + 1) = n + 1 holds for all n; a direct corollary of the infinite case.

Русский

Для бесконечного p выполняется count p (nth p n + 1) = n + 1 для всех n.

LaTeX

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

Lean4

@[simp]
theorem nth_count {n : ℕ} (hpn : p n) : nth p (count p n) = n :=
  have : ∀ hf : (setOf p).Finite, count p n < #hf.toFinset := fun hf => count_lt_card hf hpn
  count_injective (nth_mem _ this) hpn (count_nth this)

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