---

Step * 1 of Lemma int_lt_to_int_upper_uniform


∀i:ℤ. ∀[A:{i + 1...} ⟶ ℙ]. (∀[j:ℤ]. A[j] supposing i < j ⇐⇒ ∀[j:{i + 1...}]. A[j])
BY
{ (GenUnivCD THENA Auto) }

1
1. i : ℤ@i
2. [A] : {i + 1...} ⟶ ℙ
3. ∀[j:ℤ]. A[j] supposing i < j@i
4. [j] : {i + 1...}
⊢ A[j]

2
1. i : ℤ@i
2. [A] : {i + 1...} ⟶ ℙ
3. ∀[j:{i + 1...}]. A[j]@i
4. [j] : ℤ
5. i < j
⊢ A[j]

---

Latex:

---

Latex:

\mforall{}i:\mBbbZ{}.  \mforall{}[A:\{i  +  1...\}  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}[j:\mBbbZ{}].  A[j]  supposing  i  <  j  \mLeftarrow{}{}\mRightarrow{}  \mforall{}[j:\{i  +  1...\}].  A[j])


By

---

Latex:
(GenUnivCD  THENA  Auto)

---

Home Index