Nuprl Lemma : cantor-interval-converges-ext

a,b:ℝ.  ∀f:ℕ ⟶ 𝔹fst(cantor-interval(a;b;f;n))↓ as n→∞ supposing a ≤ b


Proof




Definitions occuring in Statement :  cantor-interval: cantor-interval(a;b;f;n) converges: x[n]↓ as n→∞ rleq: x ≤ y real: nat: bool: 𝔹 uimplies: supposing a pi1: fst(t) all: x:A. B[x] function: x:A ⟶ B[x]
Definitions unfolded in proof :  member: t ∈ T pi1: fst(t) so_lambda: λ2x.t[x] so_apply: x[s] accelerate: accelerate(k;f) cantor-interval-converges converges-iff-cauchy cantor-interval-cauchy-ext uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] top: Top uimplies: supposing a so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  cantor-interval-converges lifting-strict-spread istype-void strict4-apply strict4-divide converges-iff-cauchy cantor-interval-cauchy-ext
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  fst(cantor-interval(a;b;f;n))\mdownarrow{}  as  n\mrightarrow{}\minfty{}  supposing  a  \mleq{}  b



Date html generated: 2019_10_30-AM-07_39_19
Last ObjectModification: 2019_04_02-AM-10_55_46

Theory : reals


Home Index