---

Step * of Lemma int_lt_to_int_upper_uniform

∀i:ℤ. ∀[A:{i + 1...} ⟶ ℙ]. ({∀[j:ℤ]. A[j] supposing i < j} ⇐⇒ {∀[j:{i + 1...}]. A[j]})
BY
{ Unfold `guard` 0 }

1
∀i:ℤ. ∀[A:{i + 1...} ⟶ ℙ]. (∀[j:ℤ]. A[j] supposing i < j ⇐⇒ ∀[j:{i + 1...}]. 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:
Unfold  `guard`  0

---

Home Index