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