---

Step * 1 2 1 1 of Lemma member-listify


1. [T] : Type
2. d : ℤ
3. [%1] : 0 < d
4. ∀m:ℤ. ∀n:{m..m + (d - 1)-}. ∀f:{m..n-} ⟶ T. ∀x:T.  ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
5. m : ℤ
6. n : {m..m + d-}
7. ¬(n ≤ m)
8. f : {m..n-} ⟶ T
9. x : T
10. (x = (f m) ∈ T) ∨ (∃i:{m + 1..n-}. (x = (f i) ∈ T))
⊢ ∃i:{m..n-}. (x = (f i) ∈ T)
BY
{ xxx(D -1 THEN Auto)xxx }

1
1. [T] : Type
2. d : ℤ
3. [%1] : 0 < d
4. ∀m:ℤ. ∀n:{m..m + (d - 1)-}. ∀f:{m..n-} ⟶ T. ∀x:T.  ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
5. m : ℤ
6. n : {m..m + d-}
7. ¬(n ≤ m)
8. f : {m..n-} ⟶ T
9. x : T
10. ∃i:{m + 1..n-}. (x = (f i) ∈ T)
⊢ ∃i:{m..n-}. (x = (f i) ∈ T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  d  :  \mBbbZ{}
3.  [\%1]  :  0  <  d
4.  \mforall{}m:\mBbbZ{}.  \mforall{}n:\{m..m  +  (d  -  1)\msupminus{}\}.  \mforall{}f:\{m..n\msupminus{}\}  {}\mrightarrow{}  T.  \mforall{}x:T.
          ((x  \mmember{}  listify(f;m;n))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i)))
5.  m  :  \mBbbZ{}
6.  n  :  \{m..m  +  d\msupminus{}\}
7.  \mneg{}(n  \mleq{}  m)
8.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
9.  x  :  T
10.  (x  =  (f  m))  \mvee{}  (\mexists{}i:\{m  +  1..n\msupminus{}\}.  (x  =  (f  i)))
\mvdash{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i))


By

---

Latex:
xxx(D  -1  THEN  Auto)xxx

---

Home Index