Nuprl Lemma : iproper-nonvoid
∀I:Interval. (iproper(I) ⇒ i-nonvoid(I))
Proof
Definitions occuring in Statement :
i-nonvoid: i-nonvoid(I),
iproper: iproper(I),
interval: Interval,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
interval: Interval,
iproper: iproper(I),
right-endpoint: right-endpoint(I),
left-endpoint: left-endpoint(I),
i-finite: i-finite(I),
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
i-nonvoid: i-nonvoid(I),
endpoints: endpoints(I),
outl: outl(x),
pi1: fst(t),
pi2: snd(t),
i-member: r ∈ I,
bfalse: ff,
exists: ∃x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
true: True,
prop: ℙ,
and: P ∧ Q,
cand: A c∧ B,
guard: {T},
uimplies: b supposing a,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
rsub: x - y,
subtype_rel: A ⊆r B
Lemmas referenced :
int-to-real_wf,
true_wf,
iproper_wf,
interval_wf,
ravg-between,
rless_transitivity2,
ravg_wf,
rleq_weakening_rless,
rleq_weakening_equal,
rleq_wf,
rless_wf,
rsub_wf,
radd-preserves-rless,
rminus_wf,
rless-int,
radd_wf,
rmul_wf,
iff_transitivity,
rless_functionality,
req_weakening,
rmul-zero-both,
req_transitivity,
radd-ac,
radd_functionality,
radd_comm,
radd-rminus-both,
radd-zero-both,
squash_wf,
real_wf,
rminus-int,
iff_weakening_equal,
rmul_functionality,
radd-int,
req_inversion,
rminus-as-rmul,
rmul-identity1,
rmul-distrib2,
radd-assoc
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
unionElimination,
sqequalRule,
dependent_pairFormation,
cut,
introduction,
extract_by_obid,
isectElimination,
natural_numberEquality,
hypothesis,
hypothesisEquality,
dependent_functionElimination,
independent_functionElimination,
independent_pairFormation,
because_Cache,
independent_isectElimination,
productEquality,
minusEquality,
imageMemberEquality,
baseClosed,
addEquality,
addLevel,
levelHypothesis,
applyEquality,
lambdaEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
universeEquality
Latex:
\mforall{}I:Interval. (iproper(I) {}\mRightarrow{} i-nonvoid(I))
Date html generated:
2016_10_26-AM-09_30_21
Last ObjectModification:
2016_08_24-PM-11_15_42
Theory : reals
Home
Index