### Nuprl Lemma : m-sup-property

`∀[X:Type]`
`  ∀d:metric(X). ∀mtb:m-TB(X;d). ∀f:X ⟶ ℝ. ∀mc:UC(f:X ⟶ ℝ).`
`    ((∀x:X. ((f x) ≤ m-sup{i:l}(d;mtb;f;mc))) ∧ (∀e:ℝ. ((r0 < e) `` (∃x:X. ((m-sup{i:l}(d;mtb;f;mc) - e) < (f x))))))`

Proof

Definitions occuring in Statement :  m-sup: `m-sup{i:l}(d;mtb;f;mc)` m-TB: `m-TB(X;d)` m-unif-cont: `UC(f:X ⟶ Y)` rmetric: `rmetric()` metric: `metric(X)` rleq: `x ≤ y` rless: `x < y` rsub: `x - y` int-to-real: `r(n)` real: `ℝ` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  guard: `{T}` uimplies: `b supposing a` exists: `∃x:A. B[x]` prop: `ℙ` implies: `P `` Q` and: `P ∧ Q` upper-bound: `A ≤ b` rset-member: `x ∈ A` sup: `sup(A) = b` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  rleq_weakening m-sup_wf rsub_wf rless_transitivity1 req_wf req_weakening istype-universe metric_wf m-TB_wf rmetric_wf m-unif-cont_wf real_wf int-to-real_wf rless_wf m-sup-property1
Rules used in proof :  rename independent_isectElimination because_Cache dependent_pairFormation_alt applyEquality universeEquality instantiate functionIsType natural_numberEquality universeIsType independent_functionElimination promote_hyp productElimination independent_pairFormation sqequalRule dependent_functionElimination lambdaFormation_alt hypothesisEquality thin isectElimination sqequalHypSubstitution hypothesis isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut

Latex:
\mforall{}[X:Type]
\mforall{}d:metric(X).  \mforall{}mtb:m-TB(X;d).  \mforall{}f:X  {}\mrightarrow{}  \mBbbR{}.  \mforall{}mc:UC(f:X  {}\mrightarrow{}  \mBbbR{}).
((\mforall{}x:X.  ((f  x)  \mleq{}  m-sup\{i:l\}(d;mtb;f;mc)))
\mwedge{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:X.  ((m-sup\{i:l\}(d;mtb;f;mc)  -  e)  <  (f  x))))))

Date html generated: 2019_10_30-AM-06_55_05
Last ObjectModification: 2019_10_25-PM-02_23_11

Theory : reals

Home Index