---

Step * of Lemma int_seg_ind

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

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

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index