data.nat.nth

# The nth Number Satisfying a Predicate #

This file defines a function for "what is the nth 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: The n-th natural k (zero-indexed) such that p k. If there is no such natural (that is, p is true for at most n naturals), then nth p n = 0.

## Main results #

• nat.nth_set_card: For a fintely-often true p, gives the cardinality of the set of numbers satisfying p above particular values of nth p
• nat.count_nth_gc: Establishes a Galois connection between nth p and count 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.

noncomputable def nat.nth (p : → Prop) :

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.

Equations
theorem nat.nth_zero (p : → Prop) :
0 = has_Inf.Inf {i : | p i}
@[simp]
theorem nat.nth_zero_of_zero (p : → Prop) (h : p 0) :
0 = 0
theorem nat.nth_zero_of_exists (p : → Prop) (h : ∃ (n : ), p n) :
0 =
theorem nat.nth_set_card_aux (p : → Prop) {n : } (hp : (set_of p).finite) (hp' : {i : | p i ∀ (t : ), t < n t < i}.finite) (hle : n hp.to_finset.card) :
theorem nat.nth_set_card (p : → Prop) {n : } (hp : (set_of p).finite) (hp' : {i : | p i ∀ (k : ), k < n k < i}.finite) :
theorem nat.nth_set_nonempty_of_lt_card (p : → Prop) {n : } (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) :
{i : | p i ∀ (k : ), k < n k < i}.nonempty
theorem nat.nth_mem_of_lt_card_finite_aux (p : → Prop) (n : ) (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) :
n {i : | p i ∀ (k : ), k < n k < i}
theorem nat.nth_mem_of_lt_card_finite (p : → Prop) {n : } (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) :
p (nat.nth p n)
theorem nat.nth_strict_mono_of_finite (p : → Prop) {m n : } (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) (hmn : m < n) :
m < n
theorem nat.nth_mem_of_infinite_aux (p : → Prop) (hp : (set_of p).infinite) (n : ) :
n {i : | p i ∀ (k : ), k < n k < i}
theorem nat.nth_mem_of_infinite (p : → Prop) (hp : (set_of p).infinite) (n : ) :
p (nat.nth p n)
theorem nat.nth_strict_mono (p : → Prop) (hp : (set_of p).infinite) :
theorem nat.nth_injective_of_infinite (p : → Prop) (hp : (set_of p).infinite) :
theorem nat.nth_monotone (p : → Prop) (hp : (set_of p).infinite) :
theorem nat.nth_mono_of_finite (p : → Prop) {a b : } (hp : (set_of p).finite) (hb : b < hp.to_finset.card) (hab : a b) :
a b
theorem nat.le_nth_of_lt_nth_succ_finite (p : → Prop) {k a : } (hp : (set_of p).finite) (hlt : k.succ < hp.to_finset.card) (h : a < k.succ) (ha : p a) :
a k
theorem nat.le_nth_of_lt_nth_succ_infinite (p : → Prop) {k a : } (hp : (set_of p).infinite) (h : a < k.succ) (ha : p a) :
a k
@[simp]
theorem nat.count_nth_zero (p : → Prop)  :
(nat.nth p 0) = 0
theorem nat.count_nth_of_lt_card_finite (p : → Prop) {n : } (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) :
(nat.nth p n) = n
theorem nat.count_nth_of_infinite (p : → Prop) (hp : (set_of p).infinite) (n : ) :
(nat.nth p n) = n
@[simp]
theorem nat.nth_count (p : → Prop) {n : } (hpn : p n) :
n) = n
theorem nat.nth_count_eq_Inf (p : → Prop) {n : } :
n) = has_Inf.Inf {i : | p i n i}
theorem nat.nth_count_le (p : → Prop) (hp : (set_of p).infinite) (n : ) :
n n)
theorem nat.count_nth_gc (p : → Prop) (hp : (set_of p).infinite) :
(nat.nth p)
theorem nat.count_le_iff_le_nth (p : → Prop) (hp : (set_of p).infinite) {a b : } :
a b a b
theorem nat.lt_nth_iff_count_lt (p : → Prop) (hp : (set_of p).infinite) {a b : } :
a < b a < b
theorem nat.nth_lt_of_lt_count (p : → Prop) (n k : ) (h : k < n) :
k < n
theorem nat.le_nth_of_count_le (p : → Prop) (n k : ) (h : n k) :
n k
theorem nat.nth_zero_of_nth_zero (p : → Prop) (h₀ : ¬p 0) {a b : } (hab : a b) (ha : a = 0) :
b = 0
theorem nat.nth_eq_order_iso_of_nat (p : → Prop) (i : infinite (set_of p)) (n : ) :
n = n)

When p is true infinitely often, nth agrees with nat.subtype.order_iso_of_nat.