---

Step * of Lemma int_le_to_int_upper_uniform

∀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