Nuprl Lemma : lower-right-endpoint_wf

[a,b:ℝ]. ∀[n:ℕ+].  (lower-right-endpoint(a;b;n) ∈ ℝ)


Proof




Definitions occuring in Statement :  lower-right-endpoint: lower-right-endpoint(a;b;n) real: nat_plus: + uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T lower-right-endpoint: lower-right-endpoint(a;b;n) int_nzero: -o nat_plus: + nequal: a ≠ b ∈  not: ¬A implies:  Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False all: x:A. B[x] top: Top and: P ∧ Q prop:
Lemmas referenced :  real_wf nat_plus_wf int-rmul_wf radd_wf nequal_wf equal_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_and_lemma intformless_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf intformand_wf satisfiable-full-omega-tt nat_plus_properties int-rdiv_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin dependent_set_memberEquality addEquality setElimination rename hypothesisEquality natural_numberEquality hypothesis lambdaFormation independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll axiomEquality equalityTransitivity equalitySymmetry because_Cache

Latex:
\mforall{}[a,b:\mBbbR{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (lower-right-endpoint(a;b;n)  \mmember{}  \mBbbR{})



Date html generated: 2016_05_18-AM-08_38_06
Last ObjectModification: 2016_01_17-AM-02_23_02

Theory : reals


Home Index