nth Number Satisfying a Predicate #
This file defines a function for "what is the
nth number that satisifies a given predicate
and provides lemmas that deal with this function and its connection to
Main definitions #
Nat.nth p n: The
k(zero-indexed) such that
p k. If there is no such natural (that is,
pis true for at most
Nat.nth p n = 0.
Main results #
Nat.nth_eq_orderEmbOfFin: For a fintely-often true
p, gives the cardinality of the set of numbers satisfying
pabove particular values of
Nat.gc_count_nth: Establishes a Galois connection between
Nat.nth_eq_orderIsoOfNat: For an infinitely-ofter true predicate,
nthagrees with the order-isomorphism of the subtype to the natural numbers.
There has been some discussion on the subject of whether both of
Nat.Subtype.orderIsoOfNat should exist. See discussion
Future work should address how lemmas that use these should be written.
n-th natural number satisfying
p (indexed from
nth p 0 is the first
natural number satisfying
0 if there is no such number. See also
Subtype.orderIsoOfNat for the order isomorphism with ℕ when
p is infinitely often true.
Lemmas that work for finite and infinite sets #
An alternative recursive definition of
Nat.nth s n is the infimum of
x ∈ s such
Nat.nth s k < x for all
k < n, if this set is nonempty. We do not assume that the set is
nonempty because we use the same "garbage value"
0 both for
ℕ and for
Nat.nth s n
n ≥ card s.