count_le_card — Mathlib

English

If the set of naturals satisfying p is finite, then for every n, the number count(p,n) does not exceed the size of that finite set.

Русский

Если множество чисел, удовлетворяющих p, конечное, то для всякого n произведение count(p,n) не превосходит размер этого множества.

LaTeX

$$$(\{k : \mathbb{N} \mid p(k)\}).Finite \Rightarrow \operatorname{count}(p,n) \leq \left|\left(\{k : \mathbb{N} \mid p(k)\} \right)\right|$$$

Lean4

theorem count_le_card (hp : (setOf p).Finite) (n : ℕ) : count p n ≤ #hp.toFinset :=
  by
  rw [count_eq_card_filter_range]
  exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2

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