Nuprl Lemma : i-approx-elim
∀I:Interval. ∀n:ℕ+. (i-nonvoid(i-approx(I;n)) ⇒ (∃a:ℝ. ∃b:{b:ℝ| a ≤ b} . (i-approx(I;n) = [a, b] ∈ Interval)))
Proof
Definitions occuring in Statement :
i-nonvoid: i-nonvoid(I),
i-approx: i-approx(I;n),
rccint: [l, u],
interval: Interval,
rleq: x ≤ y,
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
cand: A c∧ B,
exists: ∃x:A. B[x],
prop: ℙ,
i-nonvoid: i-nonvoid(I),
top: Top,
guard: {T}
Latex:
\mforall{}I:Interval. \mforall{}n:\mBbbN{}\msupplus{}. (i-nonvoid(i-approx(I;n)) {}\mRightarrow{} (\mexists{}a:\mBbbR{}. \mexists{}b:\{b:\mBbbR{}| a \mleq{} b\} . (i-approx(I;n) = [a, b]))\000C)
Date html generated:
2020_05_20-AM-11_33_33
Last ObjectModification:
2019_12_06-PM-02_17_17
Theory : reals
Home
Index