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
This type has the property that
> is well-founded when
∃ i, p i, which allows us to implement
ℕ, starting at
0 and with an unknown upper-bound.
It is similar to the well founded relation constructed to define
the difference that, in
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.
The subtype of natural numbers
i which have the property that
j less than
p. This is an initial segment of the
natural numbers, up to and including the first value satisfying
We will be particularly interested in the case where there exists a value
p, because in this case the
> relation is well-founded.
The "greater than" relation on
upto p is well founded if (and only if) there exists a value
Zero is always a member of
nat.upto p because it has no predecessors.
- nat.upto.zero = ⟨0, _⟩