Nuprl Lemma : i-approx-is-subinterval
∀I:Interval. ∀n:ℕ+.  i-approx(I;n) ⊆ I 
Proof
Definitions occuring in Statement : 
subinterval: I ⊆ J 
, 
i-approx: i-approx(I;n)
, 
interval: Interval
, 
nat_plus: ℕ+
, 
all: ∀x:A. B[x]
Definitions unfolded in proof : 
subinterval: I ⊆ J 
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
member: t ∈ T
, 
prop: ℙ
, 
uall: ∀[x:A]. B[x]
Lemmas referenced : 
i-member-approx, 
i-member_wf, 
i-approx_wf, 
nat_plus_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalRule, 
sqequalReflexivity, 
sqequalTransitivity, 
computationStep, 
lambdaFormation, 
cut, 
lemma_by_obid, 
sqequalHypSubstitution, 
dependent_functionElimination, 
thin, 
hypothesisEquality, 
independent_functionElimination, 
hypothesis, 
isectElimination, 
because_Cache
Latex:
\mforall{}I:Interval.  \mforall{}n:\mBbbN{}\msupplus{}.    i-approx(I;n)  \msubseteq{}  I 
Date html generated:
2016_05_18-AM-08_49_41
Last ObjectModification:
2015_12_27-PM-11_44_00
Theory : reals
Home
Index