Nuprl Lemma : range_sup-property

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


Proof




Definitions occuring in Statement :  range_sup: sup{f[x] x ∈ I} rrange: f[x](x∈I) icompact: icompact(I) i-member: r ∈ I interval: Interval sup: sup(A) b req: y real: uimplies: supposing a 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] uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T sq_stable: SqStable(P) implies:  Q squash: T subinterval: I ⊆  prop: ifun: ifun(f;I) real-fun: real-fun(f;a;b) subtype_rel: A ⊆B so_lambda: λ2x.t[x] and: P ∧ Q so_apply: x[s] cand: c∧ B range_sup: sup{f[x] x ∈ I} label: ...$L... t rfun: I ⟶ℝ exists: x:A. B[x] r-ap: f(x) pi1: fst(t) icompact: icompact(I)

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



Date html generated: 2020_05_20-PM-00_15_40
Last ObjectModification: 2020_01_03-PM-02_35_05

Theory : reals


Home Index