Nuprl Lemma : unit-balls-homeomorphic+

n:ℕ+homeomorphic+({q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ;rn-metric(n);{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} \000C;max-metric(n))


Proof




Definitions occuring in Statement :  max-metric: max-metric(n) rn-metric: rn-metric(n) real-vec: ^n homeomorphic+: homeomorphic+(X;dX;Y;dY) mdist: mdist(d;x;y) rleq: x ≤ y int-to-real: r(n) nat_plus: + all: x:A. B[x] set: {x:A| B[x]}  lambda: λx.A[x] natural_number: $n
Definitions unfolded in proof :  rge: x ≥ y less_than': less_than'(a;b) meq: x ≡ y metric: metric(X) rtermConstant: "const" req-vec: req-vec(n;x;y) real-vec-mul: a*X so_lambda: λ2x.t[x] so_apply: x[s] rat_term_to_real: rat_term_to_real(f;t) rtermDivide: num "/" denom rat_term_ind: rat_term_ind rtermVar: rtermVar(var) pi1: fst(t) rtermMultiply: left "*" right pi2: snd(t) true: True label: ...$L... t sq_stable: SqStable(P) squash: T rdiv: (x/y) rneq: x ≠ y stable: Stable{P} req_int_terms: t1 ≡ t2 rev_uimplies: rev_uimplies(P;Q) uiff: uiff(P;Q) sq_exists: x:A [B[x]] rless: x < y scale-metric: c*d rev_implies:  Q iff: ⇐⇒ Q is-mfun: f:FUN(X;Y) mfun: FUN(X ⟶ Y) homeomorphic+: homeomorphic+(X;dX;Y;dY) mdist: mdist(d;x;y) rn-metric: rn-metric(n) metric-leq: d1 ≤ d2 prop: top: Top false: False exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) implies:  Q not: ¬A uimplies: supposing a or: P ∨ Q decidable: Dec(P) nat: guard: {T} subtype_rel: A ⊆B ext-eq: A ≡ B nat_plus: + le: A ≤ B and: P ∧ Q lelt: i ≤ j < k int_seg: {i..j-} uall: [x:A]. B[x] member: t ∈ T real-vec: ^n all: x:A. B[x]
Lemmas referenced :  itermAdd_wf int_term_value_add_lemma int_term_value_mul_lemma istype-less_than rleq_functionality_wrt_implies rleq_weakening_equal real-vec-norm-0 rmul-rinv rn-metric-meq req-vec_inversion mdist-same not-rless rleq_antisymmetry real-vec-norm-nonneg real-vec-norm-is-0 istype-false meq_inversion meq-max-metric-iff-meq-rn-metric meq_weakening meq_functionality iff_weakening_uiff req_witness meq-max-metric real-vec-mul-mul req-vec_weakening real-vec-mul_functionality req-vec_functionality rtermConstant_wf rmul-identity1 rdiv_functionality rneq-by-function rneq-symmetry req_wf assert-rat-term-eq2 rtermDivide_wf rtermMultiply_wf rtermVar_wf rinv-mul-as-rdiv mdist-max-metric-mul iff_weakening_equal squash_wf true_wf real_wf subtype_rel_self equal_functionality_wrt_subtype_rel2 rmul_functionality rabs-of-nonneg sq_stable__rless rless-implies-rless rleq_weakening_rless rsub_wf real-vec-norm-mul rabs_wf rmul-rinv3 req_transitivity rinv_wf2 real-vec-mul_wf rdiv_wf minimal-not-not-excluded-middle minimal-double-negation-hyp-elim stable__meq false_wf not_wf unit-cube-to-unit-ball real_term_value_var_lemma real_term_value_const_lemma real_term_value_mul_lemma real_term_value_sub_lemma real_polynomial_null req-iff-rsub-is-0 rless_functionality rleq_functionality real-vec-dist-symmetry req_weakening mdist-symm req_functionality itermMultiply_wf itermSubtract_wf rless_transitivity1 rless_wf decidable__lt rless-int rmul_preserves_rless rleq-int scale-metric_wf real-vec-dist_wf real-vec-dist-from-zero nat_plus_wf rmul_wf meq_wf mfun_wf metric-on-subtype max-metric_wf is-mfun_wf unit-ball-to-unit-cube rn-metric-leq-max-metric nat_plus_subtype_nat max-metric-leq-rn-metric rleq_wf rleq_weakening rleq_transitivity real-vec-norm_wf rn-metric_wf istype-le int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma istype-int intformless_wf itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_plus_properties real-vec_wf mdist_wf req_inversion int_seg_wf int-to-real_wf
Rules used in proof :  addEquality multiplyEquality hyp_replacement applyLambdaEquality inlFormation_alt instantiate universeEquality imageMemberEquality baseClosed imageElimination equalityIstype inrFormation_alt unionEquality functionEquality unionIsType functionIsType productIsType closedConclusion setEquality equalitySymmetry equalityTransitivity functionExtensionality applyEquality inhabitedIsType setIsType voidElimination isect_memberEquality_alt int_eqEquality dependent_pairFormation_alt independent_functionElimination approximateComputation independent_isectElimination unionElimination dependent_functionElimination because_Cache dependent_set_memberEquality_alt independent_pairFormation hypothesisEquality natural_numberEquality universeIsType hypothesis productElimination rename setElimination thin isectElimination sqequalHypSubstitution extract_by_obid introduction lambdaEquality_alt sqequalRule cut lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  homeomorphic+(\{q:\mBbbR{}\^{}n|  mdist(rn-metric(n);\mlambda{}i.r0;q)  \mleq{}  r1\}  ;rn-metric(n);\{q:\mBbbR{}\^{}n|  mdist(max-metri\000Cc(n);\mlambda{}i.r0;q)  \mleq{}  r1\}  ;max-metric(n))



Date html generated: 2019_10_30-AM-11_26_21
Last ObjectModification: 2019_10_29-PM-01_08_07

Theory : real!vectors


Home Index