Documentation

Mathlib.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.orderIsoOfNat 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.orderIsoOfNat for the order isomorphism with ℕ when p is infinitely often true.

Equations
Instances For

    Lemmas about Nat.nth on a finite set #

    theorem Nat.nth_of_card_le {p : Prop} (hf : (setOf p).Finite) {n : } (hn : hf.toFinset.card n) :
    Nat.nth p n = 0
    theorem Nat.nth_eq_getD_sort {p : Prop} (h : (setOf p).Finite) (n : ) :
    Nat.nth p n = (Finset.sort (fun (x x_1 : ) => x x_1) h.toFinset).getD n 0
    theorem Nat.nth_eq_orderEmbOfFin {p : Prop} (hf : (setOf p).Finite) {n : } (hn : n < hf.toFinset.card) :
    Nat.nth p n = (hf.toFinset.orderEmbOfFin ) n, hn
    theorem Nat.nth_strictMonoOn {p : Prop} (hf : (setOf p).Finite) :
    StrictMonoOn (Nat.nth p) (Set.Iio hf.toFinset.card)
    theorem Nat.nth_lt_nth_of_lt_card {p : Prop} (hf : (setOf p).Finite) {m : } {n : } (h : m < n) (hn : n < hf.toFinset.card) :
    Nat.nth p m < Nat.nth p n
    theorem Nat.nth_le_nth_of_lt_card {p : Prop} (hf : (setOf p).Finite) {m : } {n : } (h : m n) (hn : n < hf.toFinset.card) :
    theorem Nat.lt_of_nth_lt_nth_of_lt_card {p : Prop} (hf : (setOf p).Finite) {m : } {n : } (h : Nat.nth p m < Nat.nth p n) (hm : m < hf.toFinset.card) :
    m < n
    theorem Nat.le_of_nth_le_nth_of_lt_card {p : Prop} (hf : (setOf p).Finite) {m : } {n : } (h : Nat.nth p m Nat.nth p n) (hm : m < hf.toFinset.card) :
    m n
    theorem Nat.nth_injOn {p : Prop} (hf : (setOf p).Finite) :
    Set.InjOn (Nat.nth p) (Set.Iio hf.toFinset.card)
    theorem Nat.range_nth_of_finite {p : Prop} (hf : (setOf p).Finite) :
    @[simp]
    theorem Nat.image_nth_Iio_card {p : Prop} (hf : (setOf p).Finite) :
    Nat.nth p '' Set.Iio hf.toFinset.card = setOf p
    theorem Nat.nth_mem_of_lt_card {p : Prop} {n : } (hf : (setOf p).Finite) (hlt : n < hf.toFinset.card) :
    p (Nat.nth p n)
    theorem Nat.exists_lt_card_finite_nth_eq {p : Prop} (hf : (setOf p).Finite) {x : } (h : p x) :
    n < hf.toFinset.card, Nat.nth p n = x

    Lemmas about Nat.nth on an infinite set #

    theorem Nat.nth_apply_eq_orderIsoOfNat {p : Prop} (hf : (setOf p).Infinite) (n : ) :

    When s is an infinite set, nth agrees with Nat.Subtype.orderIsoOfNat.

    theorem Nat.nth_eq_orderIsoOfNat {p : Prop} (hf : (setOf p).Infinite) :

    When s is an infinite set, nth agrees with Nat.Subtype.orderIsoOfNat.

    theorem Nat.nth_strictMono {p : Prop} (hf : (setOf p).Infinite) :
    theorem Nat.nth_injective {p : Prop} (hf : (setOf p).Infinite) :
    theorem Nat.nth_monotone {p : Prop} (hf : (setOf p).Infinite) :
    theorem Nat.nth_lt_nth {p : Prop} (hf : (setOf p).Infinite) {k : } {n : } :
    Nat.nth p k < Nat.nth p n k < n
    theorem Nat.nth_le_nth {p : Prop} (hf : (setOf p).Infinite) {k : } {n : } :
    Nat.nth p k Nat.nth p n k n
    theorem Nat.range_nth_of_infinite {p : Prop} (hf : (setOf p).Infinite) :
    theorem Nat.nth_mem_of_infinite {p : Prop} (hf : (setOf 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 : (setOf p).Finite), n < hf.toFinset.card) Nat.nth p n = x
    theorem Nat.nth_mem {p : Prop} (n : ) (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
    p (Nat.nth p n)
    theorem Nat.nth_lt_nth' {p : Prop} {m : } {n : } (hlt : m < n) (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
    Nat.nth p m < Nat.nth p n
    theorem Nat.nth_le_nth' {p : Prop} {m : } {n : } (hle : m n) (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
    theorem Nat.le_nth {p : Prop} {n : } (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
    n Nat.nth p n
    theorem Nat.isLeast_nth {p : Prop} {n : } (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
    IsLeast {i : | p i k < n, Nat.nth p k < i} (Nat.nth p n)
    theorem Nat.isLeast_nth_of_lt_card {p : Prop} {n : } (hf : (setOf p).Finite) (hn : n < hf.toFinset.card) :
    IsLeast {i : | p i k < n, Nat.nth p k < i} (Nat.nth p n)
    theorem Nat.isLeast_nth_of_infinite {p : Prop} (hf : (setOf p).Infinite) (n : ) :
    IsLeast {i : | p i k < n, Nat.nth p k < i} (Nat.nth p n)
    theorem Nat.nth_eq_sInf (p : Prop) (n : ) :
    Nat.nth p n = sInf {x : | p x 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 sInf 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} [DecidablePred p] (h : ∃ (n : ), p n) :
    theorem Nat.nth_eq_zero {p : Prop} {n : } :
    Nat.nth p n = 0 p 0 n = 0 ∃ (hf : (setOf p).Finite), hf.toFinset.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) [DecidablePred p] :
    Nat.count p (Nat.nth p 0) = 0
    theorem Nat.filter_range_nth_eq_insert {p : Prop} [DecidablePred p] {k : } (hlt : ∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card) :
    theorem Nat.filter_range_nth_eq_insert_of_finite {p : Prop} [DecidablePred p] (hf : (setOf p).Finite) {k : } (hlt : k + 1 < hf.toFinset.card) :
    theorem Nat.count_nth {p : Prop} [DecidablePred p] {n : } (hn : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
    Nat.count p (Nat.nth p n) = n
    theorem Nat.count_nth_of_lt_card_finite {p : Prop} [DecidablePred p] {n : } (hp : (setOf p).Finite) (hlt : n < hp.toFinset.card) :
    Nat.count p (Nat.nth p n) = n
    theorem Nat.count_nth_of_infinite {p : Prop} [DecidablePred p] (hp : (setOf p).Infinite) (n : ) :
    Nat.count p (Nat.nth p n) = n
    theorem Nat.count_nth_succ {p : Prop} [DecidablePred p] {n : } (hn : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
    Nat.count p (Nat.nth p n + 1) = n + 1
    @[simp]
    theorem Nat.nth_count {p : Prop} [DecidablePred p] {n : } (hpn : p n) :
    Nat.nth p (Nat.count p n) = n
    theorem Nat.nth_lt_of_lt_count {p : Prop} [DecidablePred p] {n : } {k : } (h : k < Nat.count p n) :
    Nat.nth p k < n
    theorem Nat.le_nth_of_count_le {p : Prop} [DecidablePred p] {n : } {k : } (h : n Nat.nth p k) :
    theorem Nat.nth_count_eq_sInf (p : Prop) [DecidablePred p] (n : ) :
    Nat.nth p (Nat.count p n) = sInf {i : | p i n i}
    theorem Nat.le_nth_count' {p : Prop} [DecidablePred p] {n : } (hpn : ∃ (k : ), p k n k) :
    theorem Nat.le_nth_count {p : Prop} [DecidablePred p] (hp : (setOf p).Infinite) (n : ) :
    noncomputable def Nat.giCountNth {p : Prop} [DecidablePred p] (hp : (setOf 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
    Instances For
      theorem Nat.gc_count_nth {p : Prop} [DecidablePred p] (hp : (setOf p).Infinite) :
      theorem Nat.count_le_iff_le_nth {p : Prop} [DecidablePred p] (hp : (setOf p).Infinite) {a : } {b : } :
      theorem Nat.lt_nth_iff_count_lt {p : Prop} [DecidablePred p] (hp : (setOf p).Infinite) {a : } {b : } :
      a < Nat.count p b Nat.nth p a < b
      theorem Nat.nth_of_forall {p : Prop} {n : } (hp : n'n, p n') :
      Nat.nth p n = n
      @[simp]
      theorem Nat.nth_true (n : ) :
      Nat.nth (fun (x : ) => True) n = n
      theorem Nat.nth_of_forall_not {p : Prop} {n : } (hp : n'n, ¬p n') :
      Nat.nth p n = 0
      @[simp]
      theorem Nat.nth_false (n : ) :
      Nat.nth (fun (x : ) => False) n = 0