Nuprl Lemma : i-approx-containing2
∀I:Interval. ∀a,b:ℝ. (((a ∈ I) ∧ (b ∈ I)) ⇒ (∃n:ℕ+. ((a ∈ i-approx(I;n)) ∧ (b ∈ i-approx(I;n)))))
Proof
Definitions occuring in Statement :
i-approx: i-approx(I;n),
i-member: r ∈ I,
interval: Interval,
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
prop: ℙ,
rev_implies: P ⇐ Q,
cand: A c∧ B,
exists: ∃x:A. B[x],
subinterval: I ⊆ J ,
top: Top
Lemmas referenced :
compact-subinterval,
rccint-icompact,
rmin_wf,
rmax_wf,
rmin-rleq-rmax,
rccint_wf,
icompact_wf,
rcc-subinterval,
rmin-i-member,
rmax-i-member,
rleq_wf,
and_wf,
i-member_wf,
real_wf,
interval_wf,
member_rccint_lemma,
rmin-rleq,
rleq-rmax,
i-approx_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
cut,
lemma_by_obid,
dependent_functionElimination,
hypothesisEquality,
isectElimination,
hypothesis,
independent_functionElimination,
dependent_set_memberEquality,
because_Cache,
independent_pairFormation,
dependent_pairFormation,
setElimination,
rename,
sqequalRule,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}I:Interval. \mforall{}a,b:\mBbbR{}. (((a \mmember{} I) \mwedge{} (b \mmember{} I)) {}\mRightarrow{} (\mexists{}n:\mBbbN{}\msupplus{}. ((a \mmember{} i-approx(I;n)) \mwedge{} (b \mmember{} i-approx(I;n)))))
Date html generated:
2016_05_18-AM-08_50_19
Last ObjectModification:
2015_12_27-PM-11_43_48
Theory : reals
Home
Index