Nuprl Lemma : strict-inc-subtype

`∀m:ℕ. (StrictInc ⊆r {s:ℕm ⟶ ℕ| strictly-increasing-seq(m;s)} )`

Proof

Definitions occuring in Statement :  strict-inc: `StrictInc` strictly-increasing-seq: `strictly-increasing-seq(n;s)` int_seg: `{i..j-}` nat: `ℕ` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` member: `t ∈ T` strict-inc: `StrictInc` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` nat: `ℕ` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` strictly-increasing-seq: `strictly-increasing-seq(n;s)` int_seg: `{i..j-}` guard: `{T}`
Lemmas referenced :  strict-inc_wf nat_wf subtype_rel_dep_function int_seg_wf int_seg_subtype_nat false_wf subtype_rel_self strictly-increasing-seq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation lambdaEquality sqequalHypSubstitution setElimination thin rename cut hypothesis lemma_by_obid dependent_set_memberEquality hypothesisEquality applyEquality isectElimination sqequalRule natural_numberEquality independent_isectElimination independent_pairFormation because_Cache intEquality dependent_functionElimination

Latex:
\mforall{}m:\mBbbN{}.  (StrictInc  \msubseteq{}r  \{s:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}|  strictly-increasing-seq(m;s)\}  )

Date html generated: 2016_05_14-PM-09_47_21
Last ObjectModification: 2015_12_26-PM-09_47_33

Theory : continuity

Home Index