Nuprl Lemma : rational-upper-approx_wf

[x:ℕ+ ⟶ ℤ]. ∀[n:ℕ+].  (above within 1/n ∈ ℝ)


Proof




Definitions occuring in Statement :  rational-upper-approx: above within 1/n real: nat_plus: + uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rational-upper-approx: above within 1/n has-value: (a)↓ uimplies: supposing a nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True and: P ∧ Q prop: int_nzero: -o nequal: a ≠ b ∈  not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False all: x:A. B[x] top: Top subtype_rel: A ⊆B
Lemmas referenced :  value-type-has-value int-value-type nat_plus_wf mul_nat_plus less_than_wf int-rdiv_wf nat_plus_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermMultiply_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf equal-wf-base int_subtype_base nequal_wf int-to-real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule callbyvalueReduce extract_by_obid sqequalHypSubstitution isectElimination thin intEquality independent_isectElimination hypothesis multiplyEquality natural_numberEquality setElimination rename hypothesisEquality because_Cache addEquality applyEquality functionExtensionality dependent_set_memberEquality independent_pairFormation imageMemberEquality baseClosed lambdaFormation dependent_pairFormation lambdaEquality int_eqEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality computeAll baseApply closedConclusion axiomEquality equalityTransitivity equalitySymmetry functionEquality

Latex:
\mforall{}[x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (above  x  within  1/n  \mmember{}  \mBbbR{})



Date html generated: 2017_01_09-AM-08_55_45
Last ObjectModification: 2016_11_26-PM-01_34_24

Theory : reals


Home Index