### Nuprl Lemma : compact-sup-property

`∀[X:Type]`
`  ∀d:metric(X). ∀c:mcompact(X;d). ∀f:FUN(X ⟶ ℝ).`
`    ((∀x:X. ((f x) ≤ compact-sup{i:l}(d;c;f))) ∧ (∀e:ℝ. ((r0 < e) `` (∃x:X. ((compact-sup{i:l}(d;c;f) - e) < (f x))))))`

Proof

Definitions occuring in Statement :  compact-sup: `compact-sup{i:l}(d;c;f)` mcompact: `mcompact(X;d)` mfun: `FUN(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` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  compact-sup: `compact-sup{i:l}(d;c;f)` mfun: `FUN(X ⟶ Y)` pi2: `snd(t)` mcompact: `mcompact(X;d)` member: `t ∈ T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]`
Lemmas referenced :  istype-universe metric_wf mcompact_wf rmetric_wf real_wf mfun_wf compact-mc_wf m-sup-property
Rules used in proof :  universeEquality instantiate universeIsType hypothesis rename setElimination sqequalRule productElimination dependent_functionElimination hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[X:Type]
\mforall{}d:metric(X).  \mforall{}c:mcompact(X;d).  \mforall{}f:FUN(X  {}\mrightarrow{}  \mBbbR{}).
((\mforall{}x:X.  ((f  x)  \mleq{}  compact-sup\{i:l\}(d;c;f)))
\mwedge{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:X.  ((compact-sup\{i:l\}(d;c;f)  -  e)  <  (f  x))))))

Date html generated: 2019_10_30-AM-07_08_27
Last ObjectModification: 2019_10_25-PM-02_35_42

Theory : reals

Home Index