English
For any predicate p, the n-th true value after counting equals the infimum of indices i with p(i) and i ≥ n; i.e., nth p (count p n) = sInf { i : ℕ | p(i) ∧ n ≤ i }.
Русский
Для любого предиката p n-й истинный элемент после подсчета равенInfimum индексов i с p(i) и i ≥ n.
LaTeX
$$$$\\mathrm{nth}(p,\\mathrm{count}(p,n)) = \\inf\\{i\\in\\mathbb{N} \\mid p(i) \\land n \\le i\\}. $$$$
Lean4
theorem nth_count_eq_sInf (n : ℕ) : nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i} :=
by
refine (nth_eq_sInf _ _).trans (congr_arg sInf ?_)
refine Set.ext fun a => and_congr_right fun hpa => ?_
refine ⟨fun h => not_lt.1 fun ha => ?_, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
rwa [nth_count hpa, lt_self_iff_false] at hn
