Nuprl Definition : nonzero-on
f[x]≠r0 for x ∈ I ==
∀m:{m:ℕ+| icompact(i-approx(I;m))} . (∃c:{ℝ| ((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ (c ≤ |f[x]|))))})
Definitions occuring in Statement :
icompact: icompact(I),
i-approx: i-approx(I;n),
i-member: r ∈ I,
rleq: x ≤ y,
rless: x < y,
rabs: |x|,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
nat_plus: ℕ+,
icompact: icompact(I),
sq_exists: ∃x:{A| B[x]},
and: P ∧ Q,
rless: x < y,
int-to-real: r(n),
natural_number: $n,
all: ∀x:A. B[x],
real: ℝ,
implies: P ⇒ Q,
i-member: r ∈ I,
i-approx: i-approx(I;n),
rleq: x ≤ y,
rabs: |x|
FDL editor aliases :
nonzero-on
Latex:
f[x]\mneq{}r0 for x \mmember{} I ==
\mforall{}m:\{m:\mBbbN{}\msupplus{}| icompact(i-approx(I;m))\}
(\mexists{}c:\{\mBbbR{}| ((r0 < c) \mwedge{} (\mforall{}x:\mBbbR{}. ((x \mmember{} i-approx(I;m)) {}\mRightarrow{} (c \mleq{} |f[x]|))))\})
Date html generated:
2016_05_18-AM-09_18_43
Last ObjectModification:
2015_09_23-AM-09_10_42
Theory : reals
Home
Index