### Nuprl Lemma : cantor-interval-rless

a,b:ℝ.  ((a < b)  (∀n:ℕ. ∀f:ℕn ⟶ 𝔹.  ((fst(cantor-interval(a;b;f;n))) < (snd(cantor-interval(a;b;f;n))))))

Proof

Definitions occuring in Statement :  cantor-interval: cantor-interval(a;b;f;n) rless: x < y real: int_seg: {i..j-} nat: bool: 𝔹 pi1: fst(t) pi2: snd(t) all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] natural_number: \$n
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] nat: rless: x < y sq_exists: x:{A| B[x]} sq_stable: SqStable(P) squash: T nat_plus: + decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top and: P ∧ Q so_apply: x[s] cantor-interval: cantor-interval(a;b;f;n) pi1: fst(t) pi2: snd(t) subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) real: bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b nequal: a ≠ b ∈  int_seg: {i..j-} lelt: i ≤ j < k int_nzero: -o true: True rneq: x ≠ y iff: ⇐⇒ Q rev_implies:  Q less_than: a < b
Lemmas referenced :  all_wf int_seg_wf subtract_wf bool_wf rless_wf cantor-interval_wf sq_stable__less_than nat_plus_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf real_wf pi1_wf_top equal_wf pi2_wf set_wf less_than_wf primrec-wf2 nat_wf primrec0_lemma subtype_rel_dep_function int_seg_subtype false_wf subtype_rel_self eq_int_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int decidable__lt lelt_wf int-rdiv_wf int_subtype_base equal-wf-base true_wf nequal_wf radd_wf int-rmul_wf rdiv_wf int-to-real_wf rless-int rmul_preserves_rless rmul_wf primrec-unroll rless_functionality int-rdiv-req req_weakening rmul_comm rmul-rdiv-cancel2 radd_comm radd-preserves-rless radd_functionality int-rmul-req req_transitivity req_inversion rmul-identity1 rmul-distrib2 rmul_functionality radd-int squash_wf radd_comm_eq iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin rename setElimination introduction extract_by_obid sqequalHypSubstitution isectElimination functionEquality natural_numberEquality hypothesisEquality hypothesis sqequalRule lambdaEquality because_Cache dependent_set_memberEquality independent_functionElimination imageMemberEquality baseClosed imageElimination dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll productEquality productElimination independent_pairEquality equalityTransitivity equalitySymmetry functionExtensionality applyEquality addEquality equalityElimination promote_hyp instantiate cumulativity addLevel inrFormation levelHypothesis universeEquality

Latex:
\mforall{}a,b:\mBbbR{}.
((a  <  b)
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    ((fst(cantor-interval(a;b;f;n)))  <  (snd(cantor-interval(a;b;f;n))))))

Date html generated: 2017_10_03-AM-09_51_06
Last ObjectModification: 2017_07_28-AM-08_01_22

Theory : reals

Home Index