Nuprl Lemma : rless_functionality

x1,x2,y1,y2:ℝ.  (x1 < y1 ⇐⇒ x2 < y2) supposing ((y1 y2) and (x1 x2))


Definitions occuring in Statement :  rless: x < y req: y real: uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ Q
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] implies:  Q iff: ⇐⇒ Q and: P ∧ Q req: y nat_plus: + less_than: a < b squash: T less_than': less_than'(a;b) true: True prop: rev_implies:  Q exists: x:A. B[x] int_upper: {i...} le: A ≤ B guard: {T} decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top real: so_lambda: λ2x.t[x] so_apply: x[s] ifthenelse: if then else fi  btrue: tt uiff: uiff(P;Q) sq_type: SQType(T) bfalse: ff
Lemmas referenced :  assert_of_bnot iff_weakening_uiff iff_transitivity eqff_to_assert assert_of_lt_int eqtt_to_assert bool_subtype_base bool_wf subtype_base_sq bool_cases int_term_value_minus_lemma itermMinus_wf minus-is-int-iff not_wf bnot_wf assert_wf false_wf int_term_value_subtract_lemma int_term_value_constant_lemma int_term_value_add_lemma int_formula_prop_less_lemma itermSubtract_wf itermConstant_wf itermAdd_wf intformless_wf subtract-is-int-iff decidable__lt lt_int_wf real_wf req_wf rless_wf all_wf int_upper_wf subtract_wf absval_ifthenelse int_formula_prop_wf int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_plus_properties int_upper_properties less_than_transitivity1 rless-iff4 less_than_wf rless-iff-large-diff req_witness
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis rename independent_pairFormation dependent_functionElimination productElimination dependent_set_memberEquality natural_numberEquality sqequalRule imageMemberEquality baseClosed dependent_pairFormation setElimination independent_isectElimination unionElimination lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll because_Cache applyEquality addEquality equalityTransitivity equalitySymmetry pointwiseFunctionality promote_hyp baseApply closedConclusion imageElimination instantiate cumulativity impliesFunctionality

\mforall{}x1,x2,y1,y2:\mBbbR{}.    (x1  <  y1  \mLeftarrow{}{}\mRightarrow{}  x2  <  y2)  supposing  ((y1  =  y2)  and  (x1  =  x2))

Date html generated: 2016_05_18-AM-07_04_57
Last ObjectModification: 2016_01_17-AM-01_51_25

Theory : reals

Home Index