### 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