mathlib3 documentation

data.nat.nth

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

nat.nth p n = dite (set_of p).finite (λ (h : (set_of p).finite), (finset.sort has_le.le h.to_finset).nthd n 0) (λ (h : ¬(set_of p).finite), ↑(⇑(nat.subtype.order_iso_of_nat (set_of p)) n))

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

nat.nth p n = (finset.sort has_le.le h.to_finset).nthd n 0

theorem nat.nth_eq_order_emb_of_fin {p : ℕ → Prop} (hf : (set_of p).finite) {n : ℕ} (hn : n < hf.to_finset.card) :

nat.nth p n = ⇑(hf.to_finset.order_emb_of_fin rfl) ⟨n, hn⟩

theorem nat.nth_strict_mono_on {p : ℕ → Prop} (hf : (set_of p).finite) :

strict_mono_on (nat.nth p) (set.Iio 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) :

nat.nth p m ≤ nat.nth p n

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

set.inj_on (nat.nth p) (set.Iio hf.to_finset.card)

theorem nat.range_nth_of_finite {p : ℕ → Prop} (hf : (set_of p).finite) :

set.range (nat.nth p) = has_insert.insert 0 (set_of p)

@[simp]

theorem nat.image_nth_Iio_card {p : ℕ → Prop} (hf : (set_of p).finite) :

nat.nth p '' set.Iio hf.to_finset.card = set_of p

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 #

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

nat.nth p n = ↑(⇑(nat.subtype.order_iso_of_nat (set_of p)) 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) :

nat.nth p = coe ∘ ⇑(nat.subtype.order_iso_of_nat (set_of p))

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

strict_mono (nat.nth p)

theorem nat.nth_injective {p : ℕ → Prop} (hf : (set_of p).infinite) :

function.injective (nat.nth p)

theorem nat.nth_monotone {p : ℕ → Prop} (hf : (set_of p).infinite) :

monotone (nat.nth p)

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

set.range (nat.nth p) = set_of p

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.subset_range_nth {p : ℕ → Prop} :

set_of p ⊆ set.range (nat.nth p)

theorem nat.range_nth_subset {p : ℕ → Prop} :

set.range (nat.nth p) ⊆ has_insert.insert 0 (set_of p)

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

nat.nth p m ≤ nat.nth p n

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

nat.nth p 0 = has_Inf.Inf (set_of p)

@[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_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.filter_range_nth_subset_insert (p : ℕ → Prop) [decidable_pred p] (k : ℕ) :

finset.filter p (finset.range (nat.nth p (k + 1))) ⊆ has_insert.insert (nat.nth p k) (finset.filter p (finset.range (nat.nth p k)))

theorem nat.filter_range_nth_eq_insert {p : ℕ → Prop} [decidable_pred p] {k : ℕ} (hlt : ∀ (hf : (set_of p).finite), k + 1 < hf.to_finset.card) :

finset.filter p (finset.range (nat.nth p (k + 1))) = has_insert.insert (nat.nth p k) (finset.filter p (finset.range (nat.nth p k)))

theorem nat.filter_range_nth_eq_insert_of_finite {p : ℕ → Prop} [decidable_pred p] (hf : (set_of p).finite) {k : ℕ} (hlt : k + 1 < hf.to_finset.card) :

finset.filter p (finset.range (nat.nth p (k + 1))) = has_insert.insert (nat.nth p k) (finset.filter p (finset.range (nat.nth p k)))

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 + 1))) = has_insert.insert (nat.nth p k) (finset.filter p (finset.range (nat.nth p k)))

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

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

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

theorem nat.le_nth_count {p : ℕ → Prop} [decidable_pred p] (hp : (set_of p).infinite) (n : ℕ) :

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

noncomputable def nat.gi_count_nth {p : ℕ → Prop} [decidable_pred p] (hp : (set_of p).infinite) :

galois_insertion (nat.count p) (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 hp = galois_insertion.monotone_intro _ nat.gi_count_nth._proof_1 _ _

theorem nat.gc_count_nth {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