Nuprl Lemma : i-finite-approx
∀n,m:ℕ+. ∀I:Interval. (i-finite(i-approx(I;n)) ⇐⇒ i-finite(i-approx(I;m)))
Proof
Definitions occuring in Statement :
i-approx: i-approx(I;n),
i-finite: i-finite(I),
interval: Interval,
nat_plus: ℕ+,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
interval: Interval,
i-approx: i-approx(I;n),
i-finite: i-finite(I),
rccint: [l, u],
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
true: True,
member: t ∈ T,
prop: ℙ,
rev_implies: P ⇐ Q,
real: ℝ
Lemmas referenced :
true_wf,
interval_wf,
nat_plus_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
unionElimination,
sqequalRule,
independent_pairFormation,
natural_numberEquality,
productEquality,
cut,
introduction,
extract_by_obid,
hypothesis,
because_Cache,
setElimination,
rename
Latex:
\mforall{}n,m:\mBbbN{}\msupplus{}. \mforall{}I:Interval. (i-finite(i-approx(I;n)) \mLeftarrow{}{}\mRightarrow{} i-finite(i-approx(I;m)))
Date html generated:
2016_10_26-AM-09_29_36
Last ObjectModification:
2016_08_22-PM-09_27_41
Theory : reals
Home
Index