Nuprl Definition : dense-in-interval
dense-in-interval(I;X) == ∀a,b:{r:ℝ| r ∈ I} . ((a < b) ⇒ (∃x:ℝ. (((a < x) ∧ (x < b)) ∧ (X x))))
Definitions occuring in Statement :
i-member: r ∈ I,
rless: x < y,
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
i-member: r ∈ I,
implies: P ⇒ Q,
exists: ∃x:A. B[x],
real: ℝ,
and: P ∧ Q,
rless: x < y,
apply: f a
FDL editor aliases :
dense-in-interval
Latex:
dense-in-interval(I;X) == \mforall{}a,b:\{r:\mBbbR{}| r \mmember{} I\} . ((a < b) {}\mRightarrow{} (\mexists{}x:\mBbbR{}. (((a < x) \mwedge{} (x < b)) \mwedge{} (X x))))
Date html generated:
2017_10_03-AM-09_47_11
Last ObjectModification:
2017_07_31-PM-01_53_53
Theory : reals
Home
Index