Nuprl Lemma : range_sup-bound

I:{I:Interval| icompact(I)} . ∀f:{x:ℝx ∈ I}  ⟶ ℝ.
  ∀[c:ℝ]. sup{f[x] x ∈ I} ≤ supposing ∀x:ℝ((x ∈ I)  (f[x] ≤ c)) 
  supposing ∀x,y:{x:ℝx ∈ I} .  ((x y)  (f[x] f[y]))


Proof




Definitions occuring in Statement :  range_sup: sup{f[x] x ∈ I} icompact: icompact(I) i-member: r ∈ I interval: Interval rleq: x ≤ y req: y real: uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uimplies: supposing a uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] prop: implies:  Q rleq: x ≤ y rnonneg: rnonneg(x) le: A ≤ B and: P ∧ Q label: ...$L... t rfun: I ⟶ℝ uiff: uiff(P;Q) sup: sup(A) b sq_stable: SqStable(P) squash: T exists: x:A. B[x] rrange: f[x](x∈I) rset-member: x ∈ A rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y guard: {T} req_int_terms: t1 ≡ t2 false: False not: ¬A iff: ⇐⇒ Q

Latex:
\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}f:\{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}.
    \mforall{}[c:\mBbbR{}].  sup\{f[x]  |  x  \mmember{}  I\}  \mleq{}  c  supposing  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  (f[x]  \mleq{}  c)) 
    supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))



Date html generated: 2020_05_20-PM-00_16_03
Last ObjectModification: 2020_01_03-PM-02_33_33

Theory : reals


Home Index