Nuprl Lemma : i-closed-finite-rep
∀I:Interval. (i-closed(I) ⇒ i-finite(I) ⇒ (∃a,b:ℝ. (I = [a, b] ∈ Interval)))
Proof
Definitions occuring in Statement :
rccint: [l, u],
i-closed: i-closed(I),
i-finite: i-finite(I),
interval: Interval,
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
interval: Interval,
i-finite: i-finite(I),
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
i-closed: i-closed(I),
outl: outl(x),
bnot: ¬bb,
bor: p ∨bq,
bfalse: ff,
and: P ∧ Q,
exists: ∃x:A. B[x],
member: t ∈ T,
rccint: [l, u],
uall: ∀[x:A]. B[x],
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
top: Top,
false: False
Lemmas referenced :
rccint_wf,
equal_wf,
interval_wf,
subtype_rel_product,
real_wf,
top_wf,
subtype_rel_union,
exists_wf,
i-finite_wf,
i-closed_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
unionElimination,
sqequalRule,
dependent_pairFormation,
hypothesisEquality,
because_Cache,
cut,
hypothesis,
lemma_by_obid,
isectElimination,
independent_pairEquality,
inlEquality,
voidEquality,
applyEquality,
unionEquality,
lambdaEquality,
independent_isectElimination,
voidElimination,
isect_memberEquality
Latex:
\mforall{}I:Interval. (i-closed(I) {}\mRightarrow{} i-finite(I) {}\mRightarrow{} (\mexists{}a,b:\mBbbR{}. (I = [a, b])))
Date html generated:
2016_05_18-AM-08_48_23
Last ObjectModification:
2015_12_27-PM-11_45_48
Theory : reals
Home
Index