---

Step * 1 2 1 1 2 1 1 of Lemma path-end-mem-basic


1. Z : i:ℕ0 ⟶ {z:ℝ| z ∈ [r0, r1)} 
⊢ ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕ0. ((Z i) ≤ z)
BY
{ (D 0 With ⌜r0⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  Z  :  i:\mBbbN{}0  {}\mrightarrow{}  \{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\} 
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\}  .  \mforall{}i:\mBbbN{}0.  ((Z  i)  \mleq{}  z)


By

---

Latex:
(D  0  With  \mkleeneopen{}r0\mkleeneclose{}    THEN  Auto)

---

Home Index