The n
th Number Satisfying a Predicate #
This file defines a function for "what is the n
th number that satisifies a given predicate p
",
and provides lemmas that deal with this function and its connection to nat.count
.
Main definitions #
nth p n
: Then
-th naturalk
(zero-indexed) such thatp k
. If there is no such natural (that is,p
is true for at mostn
naturals), thennth p n = 0
.
Main results #
nat.nth_set_card
: For a fintely-often truep
, gives the cardinality of the set of numbers satisfyingp
above particular values ofnth p
nat.count_nth_gc
: Establishes a Galois connection betweennth p
andcount p
.nat.nth_eq_order_iso_of_nat
: For an infinitely-ofter true predicate,nth
agrees with the order-isomorphism of the subtype to the natural numbers.
There has been some discussion on the subject of whether both of nth
and
nat.subtype.order_iso_of_nat
should exist. See discussion
here.
Future work should address how lemmas that use these should be written.
Find the n
-th natural number satisfying p
(indexed from 0
, so nth p 0
is the first
natural number satisfying p
), or 0
if there is no such number. See also
subtype.order_iso_of_nat
for the order isomorphism with ℕ when p
is infinitely often true.
@[simp]
theorem
nat.filter_range_nth_eq_insert_of_finite
(p : ℕ → Prop)
[decidable_pred p]
(hp : (set_of p).finite)
{k : ℕ}
(hlt : k.succ < hp.to_finset.card) :
finset.filter p (finset.range (nat.nth p k.succ)) = has_insert.insert (nat.nth p k) (finset.filter p (finset.range (nat.nth p k)))
theorem
nat.filter_range_nth_eq_insert_of_infinite
(p : ℕ → Prop)
[decidable_pred p]
(hp : (set_of p).infinite)
(k : ℕ) :
finset.filter p (finset.range (nat.nth p k.succ)) = has_insert.insert (nat.nth p k) (finset.filter p (finset.range (nat.nth p k)))
@[simp]
theorem
nat.count_nth_gc
(p : ℕ → Prop)
[decidable_pred p]
(hp : (set_of p).infinite) :
galois_connection (nat.count p) (nat.nth p)
theorem
nat.nth_lt_of_lt_count
(p : ℕ → Prop)
[decidable_pred p]
(n k : ℕ)
(h : k < nat.count p n) :
When p
is true infinitely often, nth
agrees with nat.subtype.order_iso_of_nat
.