English
Upto(p) is the type { i ∈ ℕ // ∀ j < i, ¬p(j) } for a predicate p on natural numbers.
Русский
Upto(p) — это тип { i ∈ ℕ | ∀ j < i, ¬p(j) } для предиката p на натуральных числах.
LaTeX
$$$$ \\text{Upto}(p) = \\{ i \\in \\mathbb{N} \\mid \\forall j < i, \\neg p(j) \\}. $$$$
Lean4
/-- 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. -/
abbrev Upto (p : ℕ → Prop) : Type :=
{ i : ℕ // ∀ j < i, ¬p j }
