---

Step * of Lemma member-listify

∀[T:Type]. ∀m:ℤ. ∀n:{n:ℤ| n ≥ m } . ∀f:{m..n-} ⟶ T.  ∀[x:T]. ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
BY
{ ((D 0 THENA Auto)
   THEN Assert  ⌜∀d:ℕ. ∀m:ℤ. ∀n:{m..m + d-}. ∀f:{m..n-} ⟶ T. ∀x:T.
                   ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))⌝⋅
   ) }

1
.....assertion..... 
1. [T] : Type
⊢ ∀d:ℕ. ∀m:ℤ. ∀n:{m..m + d-}. ∀f:{m..n-} ⟶ T. ∀x:T.  ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))

2
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))
⊢ ∀m:ℤ. ∀n:{n:ℤ| n ≥ m } . ∀f:{m..n-} ⟶ T.  ∀[x:T]. ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}m:\mBbbZ{}.  \mforall{}n:\{n:\mBbbZ{}|  n  \mgeq{}  m  \}  .  \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)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Assert    \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}
  )

---

Home Index