Nuprl Lemma : rational-lower-approx-property

x:ℝ. ∀n:ℕ+.  (((below within 1/n) ≤ x) ∧ (x ≤ ((below within 1/n) (r1/r(n)))))


Proof




Definitions occuring in Statement :  rational-lower-approx: (below within 1/n) rdiv: (x/y) rleq: x ≤ y radd: b int-to-real: r(n) real: nat_plus: + all: x:A. B[x] and: P ∧ Q natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T nat_plus: + uall: [x:A]. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop: rational-approx: (x within 1/n) rational-lower-approx: (below within 1/n) real: has-value: (a)↓ int_nzero: -o nequal: a ≠ b ∈  subtype_rel: A ⊆B rneq: x ≠ y guard: {T} iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) rat_term_to_real: rat_term_to_real(f;t) rtermSubtract: left "-" right rat_term_ind: rat_term_ind rtermDivide: num "/" denom rtermConstant: "const" rtermVar: rtermVar(var) pi1: fst(t) true: True pi2: snd(t) cand: c∧ B rge: x ≥ y req_int_terms: t1 ≡ t2
Lemmas referenced :  rational-approx-property nat_plus_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermMultiply_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_wf istype-less_than nat_plus_wf real_wf value-type-has-value int-value-type subtract_wf int-rdiv_wf intformeq_wf int_formula_prop_eq_lemma int_subtype_base nequal_wf int-to-real_wf rsub_wf rdiv_wf rless-int rless_wf req_functionality int-rdiv_functionality req_inversion rsub-int req_weakening int-rdiv-req rsub_functionality req-int-fractions nat_plus_inc_int_nzero decidable__equal_int assert-rat-term-eq2 rtermDivide_wf rtermSubtract_wf rtermVar_wf rtermConstant_wf rleq_wf radd_wf rabs_wf iff_weakening_uiff rleq_functionality radd_functionality rabs-difference-bound-rleq rleq_functionality_wrt_implies rleq_weakening_equal itermAdd_wf int_term_value_add_lemma req_transitivity radd-rdiv rdiv_functionality radd-int req_wf rleq_weakening itermSubtract_wf req-iff-rsub-is-0 real_polynomial_null real_term_value_sub_lemma real_term_value_add_lemma real_term_value_var_lemma real_term_value_const_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality dependent_set_memberEquality_alt multiplyEquality natural_numberEquality setElimination rename hypothesis isectElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType intEquality applyEquality because_Cache inhabitedIsType equalityIstype equalityTransitivity equalitySymmetry callbyvalueReduce baseApply closedConclusion baseClosed sqequalBase inrFormation_alt productElimination applyLambdaEquality promote_hyp addEquality

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (((below  x  within  1/n)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  ((below  x  within  1/n)  +  (r1/r(n)))))



Date html generated: 2019_10_29-AM-10_01_11
Last ObjectModification: 2019_04_02-AM-10_01_41

Theory : reals


Home Index