Nuprl Definition : pseudo-positive
pseudo-positive(x) == ∀y:ℝ. ((¬¬(r0 < y)) ∨ (¬¬(y < x)))
Definitions occuring in Statement :
rless: x < y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
not: ¬A,
or: P ∨ Q,
natural_number: $n
Definitions occuring in definition :
rless: x < y,
not: ¬A,
natural_number: $n,
int-to-real: r(n),
or: P ∨ Q,
real: ℝ,
all: ∀x:A. B[x]
FDL editor aliases :
pseudo-positive
Latex:
pseudo-positive(x) == \mforall{}y:\mBbbR{}. ((\mneg{}\mneg{}(r0 < y)) \mvee{} (\mneg{}\mneg{}(y < x)))
Date html generated:
2017_01_09-AM-08_56_24
Last ObjectModification:
2016_11_16-PM-06_27_18
Theory : reals
Home
Index