mathlib documentation

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 #

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) :

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) :
nat.nth p 0 = has_Inf.Inf {i : | p i}
@[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_set_card_aux (p : → Prop) {n : } (hp : (set_of p).finite) (hp' : {i : | p i ∀ (t : ), t < nnat.nth p 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 < nnat.nth p 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 < nnat.nth p 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) :
nat.nth p n {i : | p i ∀ (k : ), k < nnat.nth p 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) :
nat.nth p m < nat.nth p n
theorem nat.nth_mem_of_infinite_aux (p : → Prop) (hp : (set_of p).infinite) (n : ) :
nat.nth p n {i : | p i ∀ (k : ), k < nnat.nth p 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_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) :
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 < nat.nth p k.succ) (ha : p a) :
a nat.nth p k
theorem nat.le_nth_of_lt_nth_succ_infinite (p : → Prop) {k a : } (hp : (set_of p).infinite) (h : a < nat.nth p k.succ) (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_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
@[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_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.nth_count_le (p : → Prop) [decidable_pred p] (hp : (set_of p).infinite) (n : ) :
theorem nat.count_nth_gc (p : → Prop) [decidable_pred p] (hp : (set_of p).infinite) :
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
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_zero_of_nth_zero (p : → Prop) (h₀ : ¬p 0) {a b : } (hab : a b) (ha : nat.nth p a = 0) :
nat.nth p b = 0

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