Nuprl Lemma : max-metric-complete

n:ℕmcomplete(ℝ^n with max-metric(n))


Proof




Definitions occuring in Statement :  max-metric: max-metric(n) real-vec: ^n mcomplete: mcomplete(M) mk-metric-space: with d nat: all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T rn-prod-metric: rn-prod-metric(n) implies:  Q nat: decidable: Dec(P) or: P ∨ Q uimplies: supposing a sq_type: SQType(T) guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True prop: cand: c∧ B metric-leq: d1 ≤ d2 max-metric: max-metric(n) scale-metric: c*d top: Top prod-metric: prod-metric(k;d) subtract: m mdist: mdist(d;x;y) rmetric: rmetric() so_lambda: λ2x.t[x] so_apply: x[s] le: A ≤ B not: ¬A false: False uiff: uiff(P;Q) subtype_rel: A ⊆B exists: x:A. B[x] req_int_terms: t1 ≡ t2 nat_plus: + ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) rneq: x ≠ y rless: x < y sq_exists: x:A [B[x]] rat_term_to_real: rat_term_to_real(f;t) rtermVar: rtermVar(var) rat_term_ind: rat_term_ind pi1: fst(t) rtermDivide: num "/" denom rtermConstant: "const" pi2: snd(t) rev_uimplies: rev_uimplies(P;Q) label: ...$L... t rge: x ≥ y
Lemmas referenced :  equiv-metrics-preserve-complete real-vec_wf rn-prod-metric_wf max-metric_wf decidable__equal_int subtype_base_sq int_subtype_base mcomplete-rn-prod-metric istype-nat rless-int int-to-real_wf rless_wf primrec0_lemma istype-void rsum-empty rleq_weakening rmul_wf istype-le itermSubtract_wf itermMultiply_wf itermConstant_wf req-iff-rsub-is-0 metric-leq_wf scale-metric_wf rleq-int istype-false rleq_wf subtype_rel_sets_simple real_wf rleq_weakening_rless real_polynomial_null istype-int real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_const_lemma rless-int-fractions2 nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf intformeq_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-less_than int_term_value_mul_lemma rdiv_wf nat_plus_properties rleq-int-fractions2 decidable__le rneq-int scale-metric-leq-iff rn-prod-metric-le-max-metric assert-rat-term-eq2 rtermDivide_wf rtermConstant_wf rtermVar_wf mdist_wf rleq_functionality req_weakening rmul_functionality max-metric-leq-rn-metric rn-metric-leq-rn-prod-metric rn-metric_wf rleq-implies-rleq rsub_wf rleq_functionality_wrt_implies rleq_weakening_equal real_term_value_var_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination setElimination rename natural_numberEquality unionElimination instantiate cumulativity intEquality independent_isectElimination because_Cache productElimination sqequalRule equalityTransitivity equalitySymmetry independent_pairFormation imageMemberEquality baseClosed dependent_set_memberEquality_alt universeIsType isect_memberEquality_alt voidElimination minusEquality inhabitedIsType productIsType applyEquality lambdaEquality_alt dependent_pairFormation_alt approximateComputation int_eqEquality multiplyEquality closedConclusion inrFormation_alt

Latex:
\mforall{}n:\mBbbN{}.  mcomplete(\mBbbR{}\^{}n  with  max-metric(n))



Date html generated: 2019_10_30-AM-08_38_41
Last ObjectModification: 2019_10_02-AM-11_03_51

Theory : reals


Home Index