Step * 1 1 of Lemma comp_nat_ind_tp


1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ((∀j:ℕP[j] supposing j < i)  P[i])
3. : ℕ
⊢ P[i]
BY
PushArgs [`hn`,int_to_arg 3] }

1
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ((∀j:ℕP[j] supposing j < i)  P[i])
3. : ℕ
⊢ 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