---

Step * 2 1 1 1 1 of Lemma member-listify


1. [T] : Type
2. ∀d:ℕ. ∀m:ℤ. ∀n:{m..m + d-}. ∀f:{m..n-} ⟶ T. ∀x:T.  ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
3. m : ℤ
4. n : {n:ℤ| n ≥ m } 
5. f : {m..n-} ⟶ T
6. [x] : T
7. ∀x:T. ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
8. i : ℕ
9. i < ||listify(f;m;n)||
10. x = listify(f;m;n)[i] ∈ T
⊢ ∃i:{m..n-}. (x = (f i) ∈ T)
BY
{ xxx(InstHyp [⌜listify(f;m;n)[i]⌝] (-4)⋅ THENA Auto)xxx }

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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mforall{}d:\mBbbN{}.  \mforall{}m:\mBbbZ{}.  \mforall{}n:\{m..m  +  d\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)))
3.  m  :  \mBbbZ{}
4.  n  :  \{n:\mBbbZ{}|  n  \mgeq{}  m  \} 
5.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
6.  [x]  :  T
7.  \mforall{}x:T.  ((x  \mmember{}  listify(f;m;n))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i)))
8.  i  :  \mBbbN{}
9.  i  <  ||listify(f;m;n)||
10.  x  =  listify(f;m;n)[i]
\mvdash{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i))


By

---

Latex:
xxx(InstHyp  [\mkleeneopen{}listify(f;m;n)[i]\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)xxx

---

Home Index