Nuprl Lemma : complete-nat-induction-ext
∀[P:ℕ ⟶ ℙ]. ((∀n:ℕ. ((∀m:ℕn. P[m])
⇒ P[n]))
⇒ (∀n:ℕ. P[n]))
Proof
Definitions occuring in Statement :
int_seg: {i..j-}
,
nat: ℕ
,
uall: ∀[x:A]. B[x]
,
prop: ℙ
,
so_apply: x[s]
,
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
function: x:A ⟶ B[x]
,
natural_number: $n
Definitions unfolded in proof :
complete-nat-induction,
member: t ∈ T
,
so_apply: x[s1;s2]
,
natrec: natrec,
genrec: genrec
Lemmas referenced :
complete-nat-induction
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[P:\mBbbN{} {}\mrightarrow{} \mBbbP{}]. ((\mforall{}n:\mBbbN{}. ((\mforall{}m:\mBbbN{}n. P[m]) {}\mRightarrow{} P[n])) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. P[n]))
Date html generated:
2019_06_20-PM-01_04_59
Last ObjectModification:
2019_06_20-PM-01_02_13
Theory : int_1
Home
Index