English
Let p be a decidable predicate on ℕ. Then count p (nth p n) = n, provided the bound holds for all finite sets of true values: ∀hf, count p n < card hf. In particular, if the finiteness condition holds for all finite subsets up to n, the equality holds by induction.
Русский
Пусть p — предикат на ℕ с разрешимостью. Тогда count p (nth p n) = n при условии, что для всех конечных множеств истинности выполняется соответствующее ограничение. В частности, при условии конечности для всех подмножеств до n равенство выполняется по индукции.
LaTeX
$$$$ \\forall p:\\mathbb{N}\\to\\mathcal{P}, \\; \\forall n:\\mathbb{N}, \\; (\\forall hf:(\\{x:p(x)\\}.Finite), n < |hf|) \\Rightarrow \\mathrm{count}(p, \\mathrm{nth}(p, n)) = n.$$$$
Lean4
theorem count_nth {n : ℕ} (hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset) : count p (nth p n) = n := by
induction n with
| zero => exact count_nth_zero _
| succ k
ihk =>
rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem, ← count_eq_card_filter_range,
ihk fun hf => lt_of_succ_lt (hn hf)]
simp
