### Nuprl Lemma : cantor-to-interval-req

`∀a,b,x:ℝ. ∀f:ℕ ⟶ 𝔹.`
`  ((∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))])) `` (cantor-to-interval(a;b;f) = x))`

Proof

Definitions occuring in Statement :  cantor-to-interval: `cantor-to-interval(a;b;f)` cantor-interval: `cantor-interval(a;b;f;n)` rccint: `[l, u]` i-member: `r ∈ I` req: `x = y` real: `ℝ` nat: `ℕ` bool: `𝔹` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` uall: `∀[x:A]. B[x]` cantor-interval: `cantor-interval(a;b;f;n)` i-member: `r ∈ I` rccint: `[l, u]` top: `Top` pi1: `fst(t)` pi2: `snd(t)` guard: `{T}` uimplies: `b supposing a` squash: `↓T` sq_stable: `SqStable(P)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` int_nzero: `ℤ-o` true: `True` nequal: `a ≠ b ∈ T ` sq_type: `SQType(T)` cand: `A c∧ B` int_upper: `{i...}` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rneq: `x ≠ y` less_than: `a < b` nat_plus: `ℕ+` uiff: `uiff(P;Q)` req_int_terms: `t1 ≡ t2` rev_uimplies: `rev_uimplies(P;Q)` rdiv: `(x/y)` rbetween: `x≤y≤z` rge: `x ≥ y`
Lemmas referenced :  istype-false istype-le primrec0_lemma istype-void rleq_transitivity cantor-to-interval_wf1 sq_stable__req unique-limit req_inversion istype-nat i-member_wf rccint_wf cantor-interval_wf subtype_rel_function nat_wf bool_wf int_seg_wf int_seg_subtype_nat subtype_rel_self real_wf common-limit-squeeze-ext int-rdiv_wf exp_wf3 subtype_base_sq int_subtype_base istype-int nequal_wf int-rmul_wf exp_wf2 rsub_wf cantor-interval-inclusion nat_properties decidable__le full-omega-unsat intformnot_wf intformle_wf itermVar_wf itermAdd_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_wf intformand_wf int_formula_prop_and_lemma rleq_weakening_equal constant-limit req_weakening rnexp-converges-ext rdiv_wf int-to-real_wf rless-int rless_wf rabs_wf rleq-int-fractions2 istype-less_than rless-int-fractions3 rless_functionality rabs-of-nonneg rmul-limit rnexp_wf rmul_wf itermSubtract_wf itermMultiply_wf req-iff-rsub-is-0 real_polynomial_null real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma real_term_value_const_lemma converges-to_functionality not-equal-2 exp_wf_nat_plus nat_plus_properties intformless_wf int_formula_prop_less_lemma exp-positive-stronger rneq_functionality rnexp-int req_functionality rmul_functionality rnexp-rdiv rdiv_functionality int-rdiv-req int-rmul-req rmul_preserves_req rinv_wf2 req_transitivity rmul-rinv3 rleq_weakening rleq_functionality_wrt_implies rsub_functionality_wrt_rleq rleq_functionality cantor-interval-length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut hypothesis sqequalHypSubstitution dependent_functionElimination thin dependent_set_memberEquality_alt natural_numberEquality sqequalRule independent_pairFormation introduction extract_by_obid isectElimination because_Cache hypothesisEquality isect_memberEquality_alt voidElimination productElimination independent_isectElimination applyLambdaEquality setElimination rename imageMemberEquality baseClosed imageElimination equalityTransitivity equalitySymmetry independent_functionElimination lambdaEquality_alt inhabitedIsType equalityIsType1 functionIsType universeIsType applyEquality instantiate cumulativity intEquality equalityIsType4 closedConclusion addEquality unionElimination approximateComputation dependent_pairFormation_alt int_eqEquality inrFormation_alt

Latex:
\mforall{}a,b,x:\mBbbR{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.
((\mforall{}n:\mBbbN{}.  (x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]))
{}\mRightarrow{}  (cantor-to-interval(a;b;f)  =  x))

Date html generated: 2019_10_30-AM-07_40_07
Last ObjectModification: 2018_11_14-AM-10_07_05

Theory : reals

Home Index