---

Step * of Lemma int_upper_ind

∀i:ℤ. ∀[E:{i...} ⟶ ℙ{u}]. (E[i] ⇒ (∀k:{i + 1...}. (E[k - 1] ⇒ E[k])) ⇒ {∀k:{i...}. E[k]})
BY
{ (UnivCD THENA Auto) }

1
1. i : ℤ
2. [E] : {i...} ⟶ ℙ{u}
3. E[i]
4. ∀k:{i + 1...}. (E[k - 1] ⇒ E[k])
⊢ ∀k:{i...}. E[k]

---

Latex:

---

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}[E:\{i...\}  {}\mrightarrow{}  \mBbbP{}\{u\}].  (E[i]  {}\mRightarrow{}  (\mforall{}k:\{i  +  1...\}.  (E[k  -  1]  {}\mRightarrow{}  E[k]))  {}\mRightarrow{}  \{\mforall{}k:\{i...\}.  E[k]\})


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index