Step * of Lemma comp_nat_ind_a

[P:ℕ ⟶ ℙ{k}]. ((∀i:ℕ((∀j:ℕP[j] supposing j < i)  P[i]))  {∀i:ℕP[i]})
BY
((Unfold `guard` THEN RepD) THENA Auto) }

1
1. [P] : ℕ ⟶ ℙ{k}
2. ∀i:ℕ((∀j:ℕP[j] supposing j < i)  P[i])
3. : ℕ
⊢ P[i]


Latex:


Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}].  ((\mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}.  P[j]  supposing  j  <  i)  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  \{\mforall{}i:\mBbbN{}.  P[i]\})


By


Latex:
((Unfold  `guard`  0  THEN  RepD)  THENA  Auto)




Home Index