---

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


1. k : ℤ
2. [%1] : 0 < k
3. ∀Z:i:ℕk - 1 ⟶ {z:ℝ| z ∈ [r0, r1)} . ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk - 1. ((Z i) ≤ z)
4. Z : i:ℕk ⟶ {z:ℝ| z ∈ [r0, r1)} 
⊢ ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk. ((Z i) ≤ z)
BY
{ ((InstHyp [⌜Z⌝] (-2)⋅ THENA Auto) THEN ExRepD) }

1
1. k : ℤ
2. [%1] : 0 < k
3. ∀Z:i:ℕk - 1 ⟶ {z:ℝ| z ∈ [r0, r1)} . ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk - 1. ((Z i) ≤ z)
4. Z : i:ℕk ⟶ {z:ℝ| z ∈ [r0, r1)} 
5. z : {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 
6. ∀i:ℕk - 1. ((Z i) ≤ z)
⊢ ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk. ((Z i) ≤ z)

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  [\%1]  :  0  <  k
3.  \mforall{}Z:i:\mBbbN{}k  -  1  {}\mrightarrow{}  \{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mexists{}z:\{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\}  .  \mforall{}i:\mBbbN{}k  -  1.  ((Z  i)  \mleq{}  z)
4.  Z  :  i:\mBbbN{}k  {}\mrightarrow{}  \{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\} 
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\}  .  \mforall{}i:\mBbbN{}k.  ((Z  i)  \mleq{}  z)


By

---

Latex:
((InstHyp  [\mkleeneopen{}Z\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index