Nuprl Lemma : rminimum_functionality_wrt_rleq

[n,m:ℤ].
  ∀[x,y:{n..m 1-} ⟶ ℝ].
    rminimum(n;m;k.x[k]) ≤ rminimum(n;m;k.y[k]) supposing ∀k:ℤ((n ≤ k)  (k ≤ m)  (x[k] ≤ y[k])) 
  supposing n ≤ m


Proof




Definitions occuring in Statement :  rminimum: rminimum(n;m;k.x[k]) rleq: x ≤ y real: int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] le: A ≤ B all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] add: m natural_number: $n int:
Definitions unfolded in proof :  true: True less_than': less_than'(a;b) subtract: m rev_implies:  Q iff: ⇐⇒ Q squash: T less_than: a < b cand: c∧ B bfalse: ff ifthenelse: if then else fi  subtype_rel: A ⊆B btrue: tt it: unit: Unit bool: 𝔹 req_int_terms: t1 ≡ t2 uiff: uiff(P;Q) rge: x ≥ y rev_uimplies: rev_uimplies(P;Q) lelt: i ≤ j < k int_seg: {i..j-} so_apply: x[s] le: A ≤ B rnonneg: rnonneg(x) rleq: x ≤ y sq_type: SQType(T) ge: i ≥  guard: {T} prop: and: P ∧ Q top: Top false: False exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) implies:  Q not: ¬A or: P ∨ Q decidable: Dec(P) all: x:A. B[x] nat: rminimum: rminimum(n;m;k.x[k]) uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  subtract-add-cancel int_seg_properties rmin_wf primrec_wf rmin_functionality_wrt_rleq subtype_rel_self le-add-cancel add-commutes add-zero zero-add zero-mul add-mul-special minus-one-mul-top add-swap minus-one-mul minus-add add-associates condition-implies-le not-le-2 istype-false le_reflexive int_seg_subtype subtype_rel_function primrec-unroll assert_of_le_int bnot_of_lt_int assert_functionality_wrt_uiff eqff_to_assert bnot_wf le_wf le_int_wf assert_of_lt_int eqtt_to_assert less_than_wf assert_wf bool_wf equal-wf-base uiff_transitivity lt_int_wf real_term_value_const_lemma real_term_value_var_lemma real_term_value_sub_lemma int-to-real_wf real_polynomial_null req-iff-rsub-is-0 rleq_weakening rleq_weakening_equal rleq_functionality_wrt_implies real_wf int_seg_wf decidable__lt rleq_wf subtract-1-ge-0 primrec0_lemma le_witness_for_triv istype-less_than ge_wf int_formula_prop_less_lemma intformless_wf int_term_value_add_lemma int_formula_prop_eq_lemma itermAdd_wf intformeq_wf decidable__equal_int nat_properties int_subtype_base subtype_base_sq istype-le int_formula_prop_wf int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma istype-int itermVar_wf itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le subtract_wf
Rules used in proof :  multiplyEquality minusEquality imageElimination baseClosed closedConclusion baseApply equalityElimination isectIsTypeImplies productIsType addEquality applyEquality functionIsType equalityIstype functionIsTypeImplies productElimination intWeakElimination because_Cache rename setElimination applyLambdaEquality equalitySymmetry equalityTransitivity intEquality cumulativity instantiate lambdaFormation_alt inhabitedIsType universeIsType independent_pairFormation voidElimination isect_memberEquality_alt int_eqEquality lambdaEquality_alt dependent_pairFormation_alt independent_functionElimination approximateComputation independent_isectElimination unionElimination natural_numberEquality dependent_functionElimination hypothesis hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid dependent_set_memberEquality_alt sqequalRule thin cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n,m:\mBbbZ{}].
    \mforall{}[x,y:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].
        rminimum(n;m;k.x[k])  \mleq{}  rminimum(n;m;k.y[k]) 
        supposing  \mforall{}k:\mBbbZ{}.  ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  m)  {}\mRightarrow{}  (x[k]  \mleq{}  y[k])) 
    supposing  n  \mleq{}  m



Date html generated: 2019_11_06-PM-00_29_51
Last ObjectModification: 2019_11_05-PM-00_10_36

Theory : reals


Home Index