count_eq_zero — Mathlib

English

If there exists some n with p(n), then for any n, count p n = 0 is equivalent to n ≤ nth p 0.

Русский

Если существует n с p(n), то для любого n верно: count p n = 0 тогда и только тогда, когда n ≤ nth p 0.

LaTeX

$$$$\\exists n:\\, p(n) \\Rightarrow (\\mathrm{count}(p,n)=0 \\iff n \\le \\mathrm{nth}(p,0)).$$$$

Lean4

protected theorem count_eq_zero (h : ∃ n, p n) {n : ℕ} : count p n = 0 ↔ n ≤ nth p 0 := by
  rw [nth_zero_of_exists h, le_find_iff h, Nat.count_iff_forall_not]

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