---

Step * of Lemma int_lt_to_int_upper

∀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