count_iff_forall — Mathlib

English

For any p, the equality count(p,n) = n is equivalent to p(k) holding for every k < n.

Русский

Для любого p равенство count(p,n) = n эквивалентно тому, что p(k) выполняется для каждого k < n.

LaTeX

$$$\operatorname{count}(p,n) = n \;\Leftrightarrow\; \forall k < n,\ p(k)$$$

Lean4

theorem count_iff_forall {n : ℕ} : count p n = n ↔ ∀ n' < n, p n' := by
  simpa [count_eq_card_filter_range, card_range, mem_range] using card_filter_eq_iff (p := p) (s := range n)

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