---

Step * of Lemma int_upper_ind_uniform

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

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

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index