Step
*
1
1
of Lemma
comp_nat_ind_tp
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) 
⇒ P[i])
3. i : ℕ
⊢ P[i]
BY
{ PushArgs [`hn`,int_to_arg 3] }
1
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) 
⇒ P[i])
3. i : ℕ
⊢ P[i]
Latex:
Latex:
1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}
2.  \mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}.  P[j]  supposing  j  <  i)  {}\mRightarrow{}  P[i])
3.  i  :  \mBbbN{}
\mvdash{}  P[i]
By
Latex:
PushArgs  [`hn`,int\_to\_arg  3]
Home
Index