---

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

.....wf..... 
1. k : ℤ
2. 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)
⊢ rmax(z;Z (k - 1)) ∈ {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 
BY
{ ((GenConclTerm ⌜Z (k - 1)⌝⋅ THENA Auto) THEN All Thin) }

1
1. z : {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 
2. v : {z:ℝ| z ∈ [r0, r1)} 
⊢ rmax(z;v) ∈ {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 

---

Latex:

---

Latex:
.....wf..... 
1.  k  :  \mBbbZ{}
2.  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)\} 
5.  z  :  \{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\} 
6.  \mforall{}i:\mBbbN{}k  -  1.  ((Z  i)  \mleq{}  z)
\mvdash{}  rmax(z;Z  (k  -  1))  \mmember{}  \{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\} 


By

---

Latex:
((GenConclTerm  \mkleeneopen{}Z  (k  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index