### Nuprl Lemma : increasing-sequence-prop1

`∀a:ℕ ⟶ ℕ. (increasing-sequence(a) `` (∀n,m:ℕ.  ((n ≤ m) `` ((a n) ≤ (a m)))))`

Proof

Definitions occuring in Statement :  increasing-sequence: `increasing-sequence(a)` nat: `ℕ` le: `A ≤ B` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  increasing-sequence: `increasing-sequence(a)` subtype_rel: `A ⊆r B` le: `A ≤ B` guard: `{T}` sq_type: `SQType(T)` prop: `ℙ` and: `P ∧ Q` top: `Top` not: `¬A` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` uall: `∀[x:A]. B[x]` nat: `ℕ` member: `t ∈ T` exists: `∃x:A. B[x]` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  and_wf less_than'_wf less_than_wf ge_wf int_formula_prop_less_lemma intformless_wf increasing-sequence_wf nat_wf int_subtype_base subtype_base_sq equal_wf int_term_value_add_lemma int_formula_prop_eq_lemma itermAdd_wf intformeq_wf decidable__equal_int le_wf 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 int_formula_prop_and_lemma itermVar_wf itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties subtract_wf
Rules used in proof :  applyLambdaEquality hyp_replacement axiomEquality independent_pairEquality intWeakElimination functionEquality applyEquality functionExtensionality independent_functionElimination equalitySymmetry equalityTransitivity cumulativity instantiate promote_hyp productElimination addEquality computeAll independent_pairFormation sqequalRule voidEquality voidElimination isect_memberEquality intEquality int_eqEquality lambdaEquality independent_isectElimination unionElimination natural_numberEquality dependent_functionElimination hypothesisEquality hypothesis because_Cache rename setElimination thin isectElimination sqequalHypSubstitution extract_by_obid introduction dependent_set_memberEquality dependent_pairFormation cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (increasing-sequence(a)  {}\mRightarrow{}  (\mforall{}n,m:\mBbbN{}.    ((n  \mleq{}  m)  {}\mRightarrow{}  ((a  n)  \mleq{}  (a  m)))))

Date html generated: 2017_04_20-AM-07_36_37
Last ObjectModification: 2017_04_18-AM-05_58_51

Theory : continuity

Home Index