### Nuprl Lemma : real-fun-uniformly-less

`∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ.`
`  (real-fun(f;a;b)`
`  `` (∀c:ℝ. ((∀x:{x:ℝ| x ∈ [a, b]} . ((f x) < c)) `` (∃c':{c':ℝ| c' < c} . ∀x:{x:ℝ| x ∈ [a, b]} . ((f x) ≤ c')))))`

Proof

Definitions occuring in Statement :  real-fun: `real-fun(f;a;b)` rfun: `I ⟶ℝ` rccint: `[l, u]` i-member: `r ∈ I` rleq: `x ≤ y` rless: `x < y` real: `ℝ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` apply: `f a`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` rfun: `I ⟶ℝ` uall: `∀[x:A]. B[x]` real-fun: `real-fun(f;a;b)` top: `Top` prop: `ℙ` and: `P ∧ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uimplies: `b supposing a` guard: `{T}` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` req_int_terms: `t1 ≡ t2` false: `False` not: `¬A` exists: `∃x:A. B[x]` sq_stable: `SqStable(P)` squash: `↓T` rge: `x ≥ y`

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.
(real-fun(f;a;b)
{}\mRightarrow{}  (\mforall{}c:\mBbbR{}
((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  ((f  x)  <  c))
{}\mRightarrow{}  (\mexists{}c':\{c':\mBbbR{}|  c'  <  c\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  ((f  x)  \mleq{}  c')))))

Date html generated: 2020_05_20-PM-00_23_40
Last ObjectModification: 2019_12_05-PM-04_32_08

Theory : reals

Home Index