count_nth_zero — Mathlib

English

For any predicate p on the naturals with a decidable truth set, the count of p up to the index nth p 0 is zero: count p (nth p 0) = 0.

Русский

Для любого предиката p на множество натуральных чисел, для которого имеется решаемость истинности, количество истинных значений до первого истинного индекса равно нулю: count p (nth p 0) = 0.

LaTeX

$$$\\forall p:\\mathbb{N}\\to\\mathcal{P},\\, count(p, nth(p,0)) = 0$$$

Lean4

@[simp]
theorem count_nth_zero : count p (nth p 0) = 0 :=
  by
  rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
  exact fun n h₁ h₂ => (mem_range.1 h₁).not_ge (Nat.sInf_le h₂)

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