mathlib3 documentation

data.nat.upto

nat.upto #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

nat.upto p, with p a predicate on ℕ, is a subtype of elements n : ℕ such that no value (strictly) below n satisfies p.

This type has the property that > is well-founded when ∃ i, p i, which allows us to implement searches on ℕ, starting at 0 and with an unknown upper-bound.

It is similar to the well founded relation constructed to define nat.find with the difference that, in nat.upto p, p does not need to be decidable. In fact, nat.find could be slightly altered to factor decidability out of its well founded relation and would then fulfill the same purpose as this file.

source
@[reducible]
def nat.upto (p : ℕ → Prop) :
Type

The subtype of natural numbers i which have the property that no j less than i satisfies p. This is an initial segment of the natural numbers, up to and including the first value satisfying p.

We will be particularly interested in the case where there exists a value satisfying p, because in this case the > relation is well-founded.

Equations
source
@[protected]
def nat.upto.gt (p : ℕ → Prop) (x y : nat.upto p) :
Prop

Lift the "greater than" relation on natural numbers to nat.upto.

Equations
source
@[protected, instance]
def nat.upto.has_lt {p : ℕ → Prop} :
has_lt (nat.upto p)
Equations
source
@[protected]
theorem nat.upto.wf {p : ℕ → Prop} :
(∃ (x : ℕ), p x) → well_founded (nat.upto.gt p)

The "greater than" relation on upto p is well founded if (and only if) there exists a value satisfying p.

source
def nat.upto.zero {p : ℕ → Prop} :
nat.upto p

Zero is always a member of nat.upto p because it has no predecessors.

Equations
source
def nat.upto.succ {p : ℕ → Prop} (x : nat.upto p) (h : ¬p x.val) :
nat.upto p

The successor of n is in nat.upto p provided that n doesn't satisfy p.

Equations