### Nuprl Lemma : min-inc-seq_wf

`∀[a:ℕ ⟶ ℕ]. ∀[n,k:ℕ].  (min-inc-seq(a;n;k) ∈ ℕ)`

Proof

Definitions occuring in Statement :  min-inc-seq: `min-inc-seq(a;n;k)` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` min-inc-seq: `min-inc-seq(a;n;k)` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  min-increasing-sequence_wf nat_wf unit_wf2 equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis unionEquality lambdaFormation equalityTransitivity equalitySymmetry unionElimination dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality because_Cache functionEquality

Latex:
\mforall{}[a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[n,k:\mBbbN{}].    (min-inc-seq(a;n;k)  \mmember{}  \mBbbN{})

Date html generated: 2019_06_20-PM-03_07_17
Last ObjectModification: 2018_08_21-PM-01_57_20

Theory : continuity

Home Index