Nuprl Lemma : m-TB-sup-and-inf
∀[X:Type]
∀dX:metric(X)
(m-TB(X;dX)
⇒ (∀f:X ⟶ ℝ. (UC(f:X ⟶ ℝ) ⇒ ((∃a:ℝ. inf(λr.∃x:X. (r = (f x))) = a) ∧ (∃b:ℝ. sup(λr.∃x:X. (r = (f x))) = b)))))
Proof
Definitions occuring in Statement :
m-TB: m-TB(X;d),
m-unif-cont: UC(f:X ⟶ Y),
rmetric: rmetric(),
metric: metric(X),
inf: inf(A) = b,
sup: sup(A) = b,
req: x = y,
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,
lambda: λx.A[x],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
rge: x ≥ y,
less_than: a < b,
le: A ≤ B,
lelt: i ≤ j < k,
int_seg: {i..j-},
rev_implies: P ⇐ Q,
rneq: x ≠ y,
image-ap: f[x],
squash: ↓T,
sq_stable: SqStable(P),
meq: x ≡ y,
rset-member: x ∈ A,
pi1: fst(t),
image-space: f[X],
mdist: mdist(d;x;y),
image-metric: image-metric(d),
rmetric: rmetric(),
cand: A c∧ B,
top: Top,
false: False,
satisfiable_int_formula: satisfiable_int_formula(fmla),
not: ¬A,
or: P ∨ Q,
decidable: Dec(P),
sq_exists: ∃x:A [B[x]],
rless: x < y,
nat_plus: ℕ+,
nat: ℕ,
iff: P ⇐⇒ Q,
totally-bounded: totally-bounded(A),
and: P ∧ Q,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
exists: ∃x:A. B[x],
prop: ℙ,
rset: Set(ℝ),
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x]
Lemmas referenced :
rleq_weakening_equal,
rless_functionality_wrt_implies,
req_weakening,
rsub_functionality,
rabs_functionality,
rless_functionality,
decidable__lt,
int_seg_properties,
rless-int,
rdiv_wf,
image-ap_wf,
rabs-difference-is-zero,
sq_stable__req,
rsub_wf,
rabs_wf,
rset-member_wf,
int_seg_wf,
subtract-add-cancel,
istype-le,
int_formula_prop_wf,
int_formula_prop_less_lemma,
int_term_value_var_lemma,
int_term_value_subtract_lemma,
int_term_value_constant_lemma,
int_formula_prop_le_lemma,
int_formula_prop_not_lemma,
istype-void,
int_formula_prop_and_lemma,
istype-int,
intformless_wf,
itermVar_wf,
itermSubtract_wf,
itermConstant_wf,
intformle_wf,
intformnot_wf,
intformand_wf,
full-omega-unsat,
decidable__le,
nat_plus_properties,
subtract_wf,
image-metric_wf,
image-space_wf,
m-TB-iff,
int-to-real_wf,
rless_wf,
small-reciprocal-real,
istype-universe,
metric_wf,
m-TB_wf,
m-unif-cont_wf,
totally-bounded-sup,
totally-bounded-inf,
subtype_rel_self,
req_transitivity,
req_inversion,
req_wf,
rmetric_wf,
real_wf,
continuous-image-m-TB
Rules used in proof :
inrFormation_alt,
closedConclusion,
imageElimination,
baseClosed,
imageMemberEquality,
equalityIstype,
voidElimination,
isect_memberEquality_alt,
int_eqEquality,
approximateComputation,
unionElimination,
rename,
setElimination,
natural_numberEquality,
universeEquality,
equalitySymmetry,
equalityTransitivity,
independent_pairFormation,
instantiate,
functionIsType,
inhabitedIsType,
because_Cache,
productIsType,
independent_isectElimination,
dependent_pairFormation_alt,
productElimination,
universeIsType,
applyEquality,
productEquality,
sqequalRule,
lambdaEquality_alt,
dependent_set_memberEquality_alt,
independent_functionElimination,
hypothesis,
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{}dX:metric(X)
(m-TB(X;dX)
{}\mRightarrow{} (\mforall{}f:X {}\mrightarrow{} \mBbbR{}
(UC(f:X {}\mrightarrow{} \mBbbR{})
{}\mRightarrow{} ((\mexists{}a:\mBbbR{}. inf(\mlambda{}r.\mexists{}x:X. (r = (f x))) = a) \mwedge{} (\mexists{}b:\mBbbR{}. sup(\mlambda{}r.\mexists{}x:X. (r = (f x))) = b)))))
Date html generated:
2019_10_30-AM-06_52_21
Last ObjectModification:
2019_10_25-PM-02_08_02
Theory : reals
Home
Index