Nuprl Definition : increasing-sequence
increasing-sequence(a) == ∀n:ℕ. (((a (n + 1)) = (a n) ∈ ℕ) ∨ ((a (n + 1)) = ((a n) + 1) ∈ ℕ))
Definitions occuring in Statement :
nat: ℕ,
all: ∀x:A. B[x],
or: P ∨ Q,
apply: f a,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
natural_number: $n,
apply: f a,
add: n + m,
nat: ℕ,
equal: s = t ∈ T,
or: P ∨ Q,
all: ∀x:A. B[x]
FDL editor aliases :
increasing-sequence
Latex:
increasing-sequence(a) == \mforall{}n:\mBbbN{}. (((a (n + 1)) = (a n)) \mvee{} ((a (n + 1)) = ((a n) + 1)))
Date html generated:
2017_04_20-AM-07_36_24
Last ObjectModification:
2017_04_15-PM-05_03_04
Theory : continuity
Home
Index