Nuprl Lemma : iproper-roiint
∀x:ℝ. iproper((x, ∞))
Proof
Definitions occuring in Statement :
roiint: (l, ∞),
iproper: iproper(I),
real: ℝ,
all: ∀x:A. B[x]
Definitions unfolded in proof :
iproper: iproper(I),
i-finite: i-finite(I),
roiint: (l, ∞),
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
false: False,
member: t ∈ T,
prop: ℙ
Lemmas referenced :
true_wf,
false_wf,
real_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
voidElimination,
productEquality,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}x:\mBbbR{}. iproper((x, \minfty{}))
Date html generated:
2016_10_26-AM-09_29_14
Last ObjectModification:
2016_08_27-AM-10_19_20
Theory : reals
Home
Index