Nuprl Lemma : comp-nat-ind-ext
∀[P:ℕ ⟶ ℙ]. ((∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
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 :
member: t ∈ T,
complete_nat_ind,
any: any x
Lemmas referenced :
complete_nat_ind
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{}i:\mBbbN{}. ((\mforall{}j:\mBbbN{}i. P[j]) {}\mRightarrow{} P[i])) {}\mRightarrow{} (\mforall{}i:\mBbbN{}. P[i]))
Date html generated:
2018_05_21-PM-09_04_03
Last ObjectModification:
2018_05_19-PM-05_08_30
Theory : general
Home
Index