mathlib documentation

data.nat.nth

The `n`th 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

nat.nth p n = has_Inf.Inf {i : ℕ | p i ∧ ∀ (k : ℕ), k < n → nat.nth p k < i}

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

nat.nth p 0 = nat.find h

theorem nat.nth_set_card_aux (p : ℕ → Prop) {n : ℕ} (hp : (set_of p).finite) (hp' : {i : ℕ | p i ∧ ∀ (t : ℕ), t < n → nat.nth p t < i}.finite) (hle : n ≤ hp.to_finset.card) :

hp'.to_finset.card = hp.to_finset.card - n

theorem nat.nth_set_card (p : ℕ → Prop) {n : ℕ} (hp : (set_of p).finite) (hp' : {i : ℕ | p i ∧ ∀ (k : ℕ), k < n → nat.nth p k < i}.finite) :

hp'.to_finset.card = hp.to_finset.card - n

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 → nat.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 < n → nat.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 < n → nat.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) :

strict_mono (nat.nth p)

theorem nat.nth_injective_of_infinite (p : ℕ → Prop) (hp : (set_of p).infinite) :

function.injective (nat.nth p)

theorem nat.nth_monotone (p : ℕ → Prop) (hp : (set_of p).infinite) :

monotone (nat.nth p)

theorem nat.nth_mono_of_finite (p : ℕ → Prop) {a b : ℕ} (hp : (set_of p).finite) (hb : b < hp.to_finset.card) (hab : a ≤ b) :

nat.nth p a ≤ nat.nth p 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.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.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.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)))

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

n ≤ nat.nth p (nat.count p n)

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.count_le_iff_le_nth (p : ℕ → Prop) [decidable_pred p] (hp : (set_of p).infinite) {a b : ℕ} :

nat.count p a ≤ b ↔ a ≤ nat.nth p 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) :

nat.count p n ≤ 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

theorem nat.nth_eq_order_iso_of_nat (p : ℕ → Prop) (i : infinite ↥(set_of p)) (n : ℕ) :

nat.nth p n = ↑(⇑(nat.subtype.order_iso_of_nat (set_of p)) n)

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