---

Step * of Lemma int_le_to_int_upper

∀i:ℤ. ∀[A:{i...} ⟶ ℙ]. ({∀j:ℤ. A[j] supposing i ≤ j} ⇐⇒ {∀j:{i...}. A[j]})
BY
{ (Unfold `guard` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}[A:\{i...\}  {}\mrightarrow{}  \mBbbP{}].  (\{\mforall{}j:\mBbbZ{}.  A[j]  supposing  i  \mleq{}  j\}  \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}j:\{i...\}.  A[j]\})


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index