Nuprl Lemma : cantor-to-interval-onto-lemma

a,b:ℝ.
  ∀x:ℝ. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
    ∃g:{g:ℕ1 ⟶ 𝔹x ∈ [fst(cantor-interval(a;b;g;n 1)), snd(cantor-interval(a;b;g;n 1))]} (g f ∈ (ℕn ⟶ 𝔹))\000C 
  supposing a < b


Proof




Definitions occuring in Statement :  cantor-interval: cantor-interval(a;b;f;n) rccint: [l, u] i-member: r ∈ I rless: x < y real: int_seg: {i..j-} nat: bool: 𝔹 uimplies: supposing a pi1: fst(t) pi2: snd(t) all: x:A. B[x] exists: x:A. B[x] set: {x:A| B[x]}  function: x:A ⟶ B[x] add: m natural_number: $n equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] prop: int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] guard: {T} sq_type: SQType(T) nat: rless: x < y sq_exists: x:A [B[x]] nat_plus: + pi1: fst(t) pi2: snd(t) le: A ≤ B less_than': less_than'(a;b) iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) subtract: m true: True real: sq_stable: SqStable(P) squash: T ge: i ≥  cantor-interval: cantor-interval(a;b;f;n) bool: 𝔹 unit: Unit it: btrue: tt bfalse: ff bnot: ¬bb ifthenelse: if then else fi  assert: b nequal: a ≠ b ∈  int_nzero: -o i-member: r ∈ I rccint: [l, u]
Lemmas referenced :  cantor-middle-third-lemma rless_wf real_wf int_seg_properties full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_wf decidable__equal_int subtract_wf subtype_base_sq set_subtype_base lelt_wf int_subtype_base intformnot_wf intformeq_wf itermSubtract_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_subtract_lemma decidable__le decidable__lt istype-le istype-less_than subtype_rel_self nat_plus_properties guard_wf all_wf bool_wf isect_wf i-member_wf rccint_wf cantor-interval_wf sq_exists_wf equal_wf subtype_rel_function int_seg_subtype istype-false not-le-2 condition-implies-le minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-associates add-commutes le-add-cancel sq_stable__less_than itermAdd_wf int_term_value_add_lemma primrec-wf2 nat_properties istype-nat sq_stable__i-member pi1_wf_top pi2_wf eq_int_wf eqtt_to_assert assert_of_eq_int member_rccint_lemma eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_int primrec-unroll add-subtract-cancel subtype_rel_product top_wf cantor-interval-rless btrue_wf not-equal-2 rleq_wf ifthenelse_wf lt_int_wf int-rdiv_wf nequal_wf radd_wf int-rmul_wf assert_of_lt_int iff_weakening_uiff assert_wf less_than_wf bfalse_wf sq_stable__rleq subtype_rel_set
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality because_Cache universeIsType isectElimination hypothesis inhabitedIsType natural_numberEquality setElimination rename productElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation unionElimination applyEquality instantiate cumulativity intEquality equalityTransitivity equalitySymmetry applyLambdaEquality dependent_set_memberEquality_alt productIsType hypothesis_subsumption functionIsType functionEquality closedConclusion equalityIstype addEquality productEquality minusEquality multiplyEquality imageMemberEquality baseClosed imageElimination setIsType equalityElimination promote_hyp dependent_set_memberFormation_alt independent_pairEquality spreadEquality sqequalBase dependent_pairEquality_alt functionExtensionality hyp_replacement

Latex:
\mforall{}a,b:\mBbbR{}.
    \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  .
        \mexists{}g:\{g:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;g;n  +  1)),  snd(cantor-interval(a;b;g;n  +  1))]\} 
          (g  =  f) 
    supposing  a  <  b



Date html generated: 2019_10_30-AM-07_40_35
Last ObjectModification: 2018_12_11-AM-11_12_08

Theory : reals


Home Index