Nuprl Lemma : cantor_ivl-converges

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


Proof




Definitions occuring in Statement :  cantor_ivl: cantor_ivl(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 :  all: x:A. B[x] member: t ∈ T uimplies: supposing a rleq: x ≤ y rnonneg: rnonneg(x) le: A ≤ B and: P ∧ Q not: ¬A implies:  Q false: False uall: [x:A]. B[x] subtype_rel: A ⊆B real: prop: converges: x[n]↓ as n→∞ exists: x:A. B[x] so_lambda: λ2x.t[x] top: Top so_apply: x[s] nat: less_than': less_than'(a;b) guard: {T}
Lemmas referenced :  cantor-interval-converges less_than'_wf rsub_wf real_wf nat_plus_wf converges-to_wf cantor_ivl_wf nat_wf pi1_wf_top equal_wf bool_wf rleq_wf cantor-interval_wf subtype_rel_dep_function int_seg_wf int_seg_subtype_nat false_wf subtype_rel_self converges-to_functionality cantor-interval-req req_weakening
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isect_memberFormation sqequalRule lambdaEquality productElimination independent_pairEquality voidElimination isectElimination applyEquality setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry independent_isectElimination dependent_pairFormation functionExtensionality productEquality isect_memberEquality voidEquality independent_functionElimination functionEquality because_Cache independent_pairFormation

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



Date html generated: 2017_10_03-AM-09_53_53
Last ObjectModification: 2017_07_28-AM-08_02_53

Theory : reals


Home Index