count_nth_of_lt_card_finite — Mathlib

English

If p is a predicate with finite truth-set, then count p (nth p n) = n whenever n is less than the cardinality of that finite truth-set’s range.

Русский

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

LaTeX

$$$$ \\forall p:\\mathbb{N}\\to\\mathcal{P}, \\; (\\mathrm{setOf}\\,p)\\text{ is finite } \\Rightarrow \\forall n < |(\\mathrm{setOf}\\,p)|, \\; \\mathrm{count}(p, \\mathrm{nth}(p, n)) = n.$$$$

Lean4

theorem count_nth_of_lt_card_finite {n : ℕ} (hp : (setOf p).Finite) (hlt : n < #hp.toFinset) : count p (nth p n) = n :=
  count_nth fun _ => hlt

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