Nuprl Lemma : i-approx-finite

I:Interval. ∀n:ℕ+.  i-finite(i-approx(I;n))


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]
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 then else fi  btrue: tt and: P ∧ Q cand: c∧ B true: True member: t ∈ T
Lemmas referenced :  nat_plus_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin unionElimination sqequalRule cut natural_numberEquality independent_pairFormation hypothesis because_Cache lemma_by_obid

Latex:
\mforall{}I:Interval.  \mforall{}n:\mBbbN{}\msupplus{}.    i-finite(i-approx(I;n))



Date html generated: 2016_05_18-AM-08_46_04
Last ObjectModification: 2015_12_27-PM-11_47_58

Theory : reals


Home Index