mathlib3 documentation

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 #

Main results #

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) :
nat.nth p n = 0
theorem nat.nth_eq_nthd_sort {p : Prop} (h : (set_of p).finite) (n : ) :
theorem nat.nth_eq_order_emb_of_fin {p : Prop} (hf : (set_of p).finite) {n : } (hn : n < hf.to_finset.card) :
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) :
nat.nth p m < nat.nth p 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) :
theorem nat.lt_of_nth_lt_nth_of_lt_card {p : Prop} (hf : (set_of p).finite) {m n : } (h : nat.nth p m < nat.nth p 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 : nat.nth p m nat.nth p n) (hm : m < hf.to_finset.card) :
m n
theorem nat.nth_inj_on {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 nat.nth p n = x

Lemmas about nat.nth on an infinite set #

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

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 : } :
nat.nth p k < nat.nth p n k < n
theorem nat.nth_le_nth {p : Prop} (hf : (set_of p).infinite) {k n : } :
nat.nth p k nat.nth p 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) nat.nth p n = x
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) :
nat.nth p m < nat.nth p n
theorem nat.nth_le_nth' {p : Prop} {m n : } (hle : m n) (h : (hf : (set_of p).finite), n < hf.to_finset.card) :
theorem nat.le_nth {p : Prop} {n : } (h : (hf : (set_of p).finite), n < hf.to_finset.card) :
n nat.nth p 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 nat.nth p 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 nat.nth p 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 nat.nth p k < i} (nat.nth p n)
theorem nat.nth_eq_Inf (p : Prop) (n : ) :
nat.nth p n = has_Inf.Inf {x : | p x (k : ), k < n nat.nth p 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} :
@[simp]
theorem nat.nth_zero_of_zero {p : Prop} (h : p 0) :
nat.nth p 0 = 0
theorem nat.nth_zero_of_exists {p : Prop} [decidable_pred p] (h : (n : ), p n) :
theorem nat.nth_eq_zero {p : Prop} {n : } :
nat.nth p 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 : nat.nth p a = 0) :
nat.nth p b = 0
theorem nat.le_nth_of_lt_nth_succ {p : Prop} {k a : } (h : a < nat.nth p (k + 1)) (ha : p a) :
a nat.nth p k
@[simp]
theorem nat.count_nth_zero (p : Prop) [decidable_pred p] :
nat.count p (nat.nth p 0) = 0
theorem nat.count_nth {p : Prop} [decidable_pred p] {n : } (hn : (hf : (set_of p).finite), n < hf.to_finset.card) :
nat.count p (nat.nth p n) = n
theorem nat.count_nth_of_lt_card_finite {p : Prop} [decidable_pred p] {n : } (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) :
nat.count p (nat.nth p n) = n
theorem nat.count_nth_of_infinite {p : Prop} [decidable_pred p] (hp : (set_of p).infinite) (n : ) :
nat.count p (nat.nth p n) = n
theorem nat.count_nth_succ {p : Prop} [decidable_pred p] {n : } (hn : (hf : (set_of p).finite), n < hf.to_finset.card) :
nat.count p (nat.nth p n + 1) = n + 1
@[simp]
theorem nat.nth_count {p : Prop} [decidable_pred p] {n : } (hpn : p n) :
nat.nth p (nat.count p n) = n
theorem nat.nth_lt_of_lt_count {p : Prop} [decidable_pred p] {n k : } (h : k < nat.count p n) :
nat.nth p k < n
theorem nat.le_nth_of_count_le {p : Prop} [decidable_pred p] {n k : } (h : n nat.nth p k) :
theorem nat.nth_count_eq_Inf (p : Prop) [decidable_pred p] (n : ) :
nat.nth p (nat.count p n) = has_Inf.Inf {i : | p i n i}
theorem nat.le_nth_count' {p : Prop} [decidable_pred p] {n : } (hpn : (k : ), p k n k) :
theorem nat.le_nth_count {p : Prop} [decidable_pred p] (hp : (set_of p).infinite) (n : ) :
noncomputable def nat.gi_count_nth {p : Prop} [decidable_pred p] (hp : (set_of p).infinite) :

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

Equations
theorem nat.count_le_iff_le_nth {p : Prop} [decidable_pred p] (hp : (set_of p).infinite) {a b : } :
theorem nat.lt_nth_iff_count_lt {p : Prop} [decidable_pred p] (hp : (set_of p).infinite) {a b : } :
a < nat.count p b nat.nth p a < b