Nuprl Lemma : sq_stable__icompact
∀I:Interval. SqStable(icompact(I))
Proof
Definitions occuring in Statement :
icompact: icompact(I),
interval: Interval,
sq_stable: SqStable(P),
all: ∀x:A. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
interval: Interval,
icompact: icompact(I),
i-finite: i-finite(I),
i-closed: i-closed(I),
i-nonvoid: i-nonvoid(I),
isl: isl(x),
outl: outl(x),
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
btrue: tt,
assert: ↑b,
bor: p ∨bq,
bfalse: ff,
i-member: r ∈ I,
sq_stable: SqStable(P),
implies: P ⇒ Q,
and: P ∧ Q,
cand: A c∧ B,
true: True,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
squash: ↓T,
false: False,
exists: ∃x:A. B[x],
uimplies: b supposing a,
guard: {T}
Lemmas referenced :
rleq_transitivity,
sq_stable__rleq,
interval_wf,
rleq_weakening_equal,
false_wf,
rless_wf,
true_wf,
rleq_wf,
real_wf,
exists_wf,
and_wf,
squash_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
unionElimination,
sqequalRule,
cut,
independent_pairFormation,
hypothesis,
natural_numberEquality,
because_Cache,
lemma_by_obid,
isectElimination,
lambdaEquality,
hypothesisEquality,
imageElimination,
voidElimination,
dependent_pairFormation,
independent_isectElimination,
independent_functionElimination,
introduction,
imageMemberEquality,
baseClosed
Latex:
\mforall{}I:Interval. SqStable(icompact(I))
Date html generated:
2016_05_18-AM-08_48_13
Last ObjectModification:
2016_01_17-AM-02_26_16
Theory : reals
Home
Index