### Nuprl Lemma : rless_functionality

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

Proof

Definitions occuring in Statement :  rless: `x < y` req: `x = y` real: `ℝ` uimplies: `b supposing a` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` req: `x = y` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` prop: `ℙ` rev_implies: `P `` 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 b then t else f 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

Latex:
\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