English
If the set {n | p(n)} is infinite, then the pair (count p, nth p) forms a Galois insertion; i.e., count p and nth p are adjoint monotone mappings satisfying the Galois insertion conditions.
Русский
Если множество истинности бесконечно и существует взаимно согласованная вставка между count p и nth p, образующая Галуа-инсерцию.
LaTeX
$$$$ \\text{If } (\\{n: p(n)\\}.Infinite) \\text{ then } (count\\,p,\\; nth\\,p) \\text{ form a Galois insertion.} $$$$
Lean4
/-- If a predicate `p : ℕ → Prop` is true for infinitely many numbers, then `Nat.count p` and
`Nat.nth p` form a Galois insertion. -/
noncomputable def giCountNth (hp : (setOf p).Infinite) : GaloisInsertion (count p) (nth p) :=
GaloisInsertion.monotoneIntro (nth_monotone hp) (count_monotone p) (le_nth_count hp) (count_nth_of_infinite hp)
