### Nuprl Lemma : near-fixpoint-on-0-1

`∀f:[r0, r1] ⟶ℝ`
`  ((∀x:ℝ. ((x ∈ [r0, r1]) `` (f[x] ∈ [r0, r1])))`
`  `` f[x] continuous for x ∈ [r0, r1]`
`  `` (∀e:ℝ. ((r0 < e) `` (∃x:ℝ. ((x ∈ [r0, r1]) ∧ (|f[x] - x| < e))))))`

Proof

Definitions occuring in Statement :  continuous: `f[x] continuous for x ∈ I` rfun: `I ⟶ℝ` rccint: `[l, u]` i-member: `r ∈ I` rless: `x < y` rabs: `|x|` rsub: `x - y` int-to-real: `r(n)` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s]` rfun: `I ⟶ℝ` and: `P ∧ Q` cand: `A c∧ B` uimplies: `b supposing a` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` prop: `ℙ` or: `P ∨ Q` so_lambda: `λ2x.t[x]` label: `...\$L... t` uiff: `uiff(P;Q)` rccint: `[l, u]` i-member: `r ∈ I` exists: `∃x:A. B[x]` req_int_terms: `t1 ≡ t2` rev_uimplies: `rev_uimplies(P;Q)` r-ap: `f(x)` guard: `{T}` sq_stable: `SqStable(P)` squash: `↓T` rge: `x ≥ y` subtype_rel: `A ⊆r B` true: `True`

Latex:
\mforall{}f:[r0,  r1]  {}\mrightarrow{}\mBbbR{}
((\mforall{}x:\mBbbR{}.  ((x  \mmember{}  [r0,  r1])  {}\mRightarrow{}  (f[x]  \mmember{}  [r0,  r1])))
{}\mRightarrow{}  f[x]  continuous  for  x  \mmember{}  [r0,  r1]
{}\mRightarrow{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  [r0,  r1])  \mwedge{}  (|f[x]  -  x|  <  e))))))

Date html generated: 2020_05_20-PM-00_28_38
Last ObjectModification: 2020_01_03-PM-03_50_03

Theory : reals

Home Index