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