Nuprl Lemma : iproper-approx

I:Interval
  (iproper(I)  (∀n:ℕ+(icompact(i-approx(I;n))  (icompact(i-approx(I;n 1)) ∧ iproper(i-approx(I;n 1))))))


Proof




Definitions occuring in Statement :  icompact: icompact(I) i-approx: i-approx(I;n) iproper: iproper(I) interval: Interval nat_plus: + all: x:A. B[x] implies:  Q and: P ∧ Q add: m natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q and: P ∧ Q cand: c∧ B member: t ∈ T prop: uall: [x:A]. B[x] true: True less_than': less_than'(a;b) le: A ≤ B top: Top subtype_rel: A ⊆B subtract: m uimplies: supposing a uiff: uiff(P;Q) false: False rev_implies:  Q not: ¬A iff: ⇐⇒ Q or: P ∨ Q decidable: Dec(P) nat_plus: + exists: x:A. B[x] i-nonvoid: i-nonvoid(I) icompact: icompact(I) guard: {T} satisfiable_int_formula: satisfiable_int_formula(fmla) rless: x < y sq_exists: x:{A| B[x]} iproper: iproper(I) interval: Interval i-approx: i-approx(I;n) i-finite: i-finite(I) rccint: [l, u] isl: isl(x) assert: b ifthenelse: if then else fi  btrue: tt right-endpoint: right-endpoint(I) left-endpoint: left-endpoint(I) endpoints: endpoints(I) outl: outl(x) pi1: fst(t) pi2: snd(t) real: bfalse: ff rge: x ≥ y rneq: x ≠ y rsub: y squash: T less_than: a < b itermConstant: "const" req_int_terms: t1 ≡ t2 rdiv: (x/y)
Lemmas referenced :  icompact_wf i-approx_wf nat_plus_wf iproper_wf less_than_wf le-add-cancel add-zero add-associates add_functionality_wrt_le add-commutes minus-one-mul-top zero-add minus-one-mul minus-add condition-implies-le less-iff-le not-lt-2 false_wf decidable__lt i-approx-compact int_formula_prop_wf int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma itermConstant_wf itermAdd_wf itermVar_wf intformle_wf intformnot_wf satisfiable-full-omega-tt decidable__le nat_plus_properties i-approx-monotonic icompact-endpoints-rleq rless-int-fractions intformless_wf itermMultiply_wf int_formula_prop_less_lemma int_term_value_mul_lemma rless-int left_endpoint_rccint_lemma right_endpoint_rccint_lemma intformand_wf itermMinus_wf int_formula_prop_and_lemma int_term_value_minus_lemma i-finite_wf rleq_weakening_equal rless_functionality_wrt_implies rless_wf int-to-real_wf rdiv_wf radd_wf radd_comm rless_functionality equal_wf radd-preserves-rless real_wf rsub_wf radd-assoc req_inversion radd-ac radd-rminus-assoc req_weakening radd-rminus-both req_transitivity radd_functionality radd-zero-both rminus_wf rleq_wf rsub_functionality_wrt_rleq radd-int rmul_functionality rmul-distrib2 rmul-identity1 rleq_functionality uiff_transitivity rmul_wf radd-preserves-rleq rmul_comm rmul_preserves_rless regular-int-seq_wf rleq_weakening_rless rless_transitivity2 rless_transitivity1 rinv_wf2 rinv-as-rdiv real_term_polynomial itermSubtract_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_add_lemma real_term_value_minus_lemma real_term_value_var_lemma real_term_value_mul_lemma req-iff-rsub-is-0
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut independent_pairFormation hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache minusEquality intEquality voidEquality isect_memberEquality lambdaEquality applyEquality sqequalRule independent_isectElimination independent_functionElimination voidElimination unionElimination natural_numberEquality rename setElimination addEquality dependent_set_memberEquality dependent_functionElimination productElimination computeAll int_eqEquality dependent_pairFormation multiplyEquality inrFormation equalitySymmetry equalityTransitivity levelHypothesis addLevel baseClosed imageMemberEquality functionExtensionality

Latex:
\mforall{}I:Interval
    (iproper(I)
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}
                (icompact(i-approx(I;n))  {}\mRightarrow{}  (icompact(i-approx(I;n  +  1))  \mwedge{}  iproper(i-approx(I;n  +  1))))))



Date html generated: 2017_10_03-AM-09_34_12
Last ObjectModification: 2017_07_28-AM-07_52_06

Theory : reals


Home Index