Nuprl Lemma : i-approx-containing
∀I:Interval. ∀x:ℝ. ((x ∈ I) ⇒ (∃m:ℕ+. (icompact(i-approx(I;m)) ∧ (x ∈ i-approx(I;m)))))
Proof
Definitions occuring in Statement :
icompact: icompact(I),
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,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
cand: A c∧ B,
exists: ∃x:A. B[x],
icompact: icompact(I),
i-nonvoid: i-nonvoid(I)
Lemmas referenced :
i-member_wf,
real_wf,
interval_wf,
i-approx-closed,
i-approx-finite,
icompact_wf,
i-approx_wf,
i-approx-containing2
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
independent_pairFormation,
productElimination,
dependent_pairFormation,
dependent_functionElimination,
because_Cache,
productEquality,
independent_functionElimination
Latex:
\mforall{}I:Interval. \mforall{}x:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (\mexists{}m:\mBbbN{}\msupplus{}. (icompact(i-approx(I;m)) \mwedge{} (x \mmember{} i-approx(I;m)))))
Date html generated:
2016_10_26-AM-09_31_39
Last ObjectModification:
2016_08_27-PM-01_42_31
Theory : reals
Home
Index