### Nuprl Lemma : i-approx-closed

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

Proof

Definitions occuring in Statement :  i-approx: `i-approx(I;n)` i-closed: `i-closed(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-closed: `i-closed(I)` rccint: `[l, u]` isl: `isl(x)` outl: `outl(x)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` btrue: `tt` bor: `p ∨bq` bfalse: `ff` assert: `↑b` and: `P ∧ Q` cand: `A 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-closed(i-approx(I;n))

Date html generated: 2016_05_18-AM-08_45_52
Last ObjectModification: 2015_12_27-PM-11_48_09

Theory : reals

Home Index