count_lt_card — Mathlib

English

If the set of p is finite and p(n) holds, then count(p,n) is strictly less than the finite bound.

Русский

Если множество p конечно и выполняется p(n), то count(p,n) строго меньше данного конечного предела.

LaTeX

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

Lean4

theorem count_lt_card {n : ℕ} (hp : (setOf p).Finite) (hpn : p n) : count p n < #hp.toFinset :=
  (count_lt_count_succ_iff.2 hpn).trans_le (count_le_card hp _)

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