data.nat.nth

# The nth Number Satisfying a Predicate #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• nat.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 nat.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 nat.nth p and nat.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) (n : ) :

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

### Lemmas about nat.nth on a finite set #

theorem nat.nth_of_card_le {p : Prop} (hf : (set_of p).finite) {n : } (hn : hf.to_finset.card n) :
n = 0
theorem nat.nth_eq_nthd_sort {p : Prop} (h : (set_of p).finite) (n : ) :
n = 0
theorem nat.nth_eq_order_emb_of_fin {p : Prop} (hf : (set_of p).finite) {n : } (hn : n < hf.to_finset.card) :
n = n, hn⟩
theorem nat.nth_strict_mono_on {p : Prop} (hf : (set_of p).finite) :
theorem nat.nth_lt_nth_of_lt_card {p : Prop} (hf : (set_of p).finite) {m n : } (h : m < n) (hn : n < hf.to_finset.card) :
m < n
theorem nat.nth_le_nth_of_lt_card {p : Prop} (hf : (set_of p).finite) {m n : } (h : m n) (hn : n < hf.to_finset.card) :
m n
theorem nat.lt_of_nth_lt_nth_of_lt_card {p : Prop} (hf : (set_of p).finite) {m n : } (h : m < n) (hm : m < hf.to_finset.card) :
m < n
theorem nat.le_of_nth_le_nth_of_lt_card {p : Prop} (hf : (set_of p).finite) {m n : } (h : m n) (hm : m < hf.to_finset.card) :
m n
theorem nat.nth_inj_on {p : Prop} (hf : (set_of p).finite) :
theorem nat.range_nth_of_finite {p : Prop} (hf : (set_of p).finite) :
@[simp]
theorem nat.image_nth_Iio_card {p : Prop} (hf : (set_of p).finite) :
=
theorem nat.nth_mem_of_lt_card {p : Prop} {n : } (hf : (set_of p).finite) (hlt : n < hf.to_finset.card) :
p (nat.nth p n)
theorem nat.exists_lt_card_finite_nth_eq {p : Prop} (hf : (set_of p).finite) {x : } (h : p x) :
(n : ), n < hf.to_finset.card n = x

### Lemmas about nat.nth on an infinite set #

theorem nat.nth_apply_eq_order_iso_of_nat {p : Prop} (hf : (set_of p).infinite) (n : ) :
n = n)

When s is an infinite set, nth agrees with nat.subtype.order_iso_of_nat.

theorem nat.nth_eq_order_iso_of_nat {p : Prop} (hf : (set_of p).infinite) :

When s is an infinite set, nth agrees with nat.subtype.order_iso_of_nat.

theorem nat.nth_strict_mono {p : Prop} (hf : (set_of p).infinite) :
theorem nat.nth_injective {p : Prop} (hf : (set_of p).infinite) :
theorem nat.nth_monotone {p : Prop} (hf : (set_of p).infinite) :
theorem nat.nth_lt_nth {p : Prop} (hf : (set_of p).infinite) {k n : } :
k < n k < n
theorem nat.nth_le_nth {p : Prop} (hf : (set_of p).infinite) {k n : } :
k n k n
theorem nat.range_nth_of_infinite {p : Prop} (hf : (set_of p).infinite) :
theorem nat.nth_mem_of_infinite {p : Prop} (hf : (set_of p).infinite) (n : ) :
p (nat.nth p n)

### Lemmas that work for finite and infinite sets #

theorem nat.exists_lt_card_nth_eq {p : Prop} {x : } (h : p x) :
(n : ), ( (hf : (set_of p).finite), n < hf.to_finset.card) n = x
theorem nat.subset_range_nth {p : Prop} :
theorem nat.range_nth_subset {p : Prop} :
theorem nat.nth_mem {p : Prop} (n : ) (h : (hf : (set_of p).finite), n < hf.to_finset.card) :
p (nat.nth p n)
theorem nat.nth_lt_nth' {p : Prop} {m n : } (hlt : m < n) (h : (hf : (set_of p).finite), n < hf.to_finset.card) :
m < n
theorem nat.nth_le_nth' {p : Prop} {m n : } (hle : m n) (h : (hf : (set_of p).finite), n < hf.to_finset.card) :
m n
theorem nat.le_nth {p : Prop} {n : } (h : (hf : (set_of p).finite), n < hf.to_finset.card) :
n n
theorem nat.is_least_nth {p : Prop} {n : } (h : (hf : (set_of p).finite), n < hf.to_finset.card) :
is_least {i : | p i (k : ), k < n k < i} (nat.nth p n)
theorem nat.is_least_nth_of_lt_card {p : Prop} {n : } (hf : (set_of p).finite) (hn : n < hf.to_finset.card) :
is_least {i : | p i (k : ), k < n k < i} (nat.nth p n)
theorem nat.is_least_nth_of_infinite {p : Prop} (hf : (set_of p).infinite) (n : ) :
is_least {i : | p i (k : ), k < n k < i} (nat.nth p n)
theorem nat.nth_eq_Inf (p : Prop) (n : ) :
n = has_Inf.Inf {x : | p x (k : ), k < n k < x}

An alternative recursive definition of nat.nth: nat.nth s n is the infimum of x ∈ s such that 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 Inf on ℕ and for nat.nth s n for n ≥ card s.

theorem nat.nth_zero {p : Prop} :
0 =
@[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_eq_zero {p : Prop} {n : } :
n = 0 p 0 n = 0 (hf : (set_of p).finite), hf.to_finset.card n
theorem nat.nth_eq_zero_mono {p : Prop} (h₀ : ¬p 0) {a b : } (hab : a b) (ha : a = 0) :
b = 0
theorem nat.le_nth_of_lt_nth_succ {p : Prop} {k a : } (h : a < (k + 1)) (ha : p a) :
a k
@[simp]
theorem nat.count_nth_zero (p : Prop)  :
(nat.nth p 0) = 0
theorem nat.filter_range_nth_eq_insert {p : Prop} {k : } (hlt : (hf : (set_of p).finite), k + 1 < hf.to_finset.card) :
theorem nat.filter_range_nth_eq_insert_of_finite {p : Prop} (hf : (set_of p).finite) {k : } (hlt : k + 1 < hf.to_finset.card) :
theorem nat.count_nth {p : Prop} {n : } (hn : (hf : (set_of p).finite), n < hf.to_finset.card) :
(nat.nth p n) = n
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
theorem nat.count_nth_succ {p : Prop} {n : } (hn : (hf : (set_of p).finite), n < hf.to_finset.card) :
(nat.nth p n + 1) = n + 1
@[simp]
theorem nat.nth_count {p : Prop} {n : } (hpn : p n) :
n) = n
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_count_eq_Inf (p : Prop) (n : ) :
n) = has_Inf.Inf {i : | p i n i}
theorem nat.le_nth_count' {p : Prop} {n : } (hpn : (k : ), p k n k) :
n n)
theorem nat.le_nth_count {p : Prop} (hp : (set_of p).infinite) (n : ) :
n n)
noncomputable def nat.gi_count_nth {p : Prop} (hp : (set_of p).infinite) :
(nat.nth p)

If a predicate p : ℕ → Prop is true for infinitely many numbers, then nat.count p and nat.nth p form a Galois insertion.

Equations
• = nat.gi_count_nth._proof_1 _ _
theorem nat.gc_count_nth {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