---

Step * of Lemma member-mapl

∀[T,T':Type].  ∀L:T List. ∀y:T'. ∀f:{x:T| (x ∈ L)}  ⟶ T'.  ((y ∈ mapl(f;L)) ⇐⇒ ∃a:T. ((a ∈ L) c∧ (y = (f a) ∈ T')))
BY
{ (InductionOnList THEN Unfold `mapl` 0 THEN Reduce 0 THEN Try (Fold `mapl` 0)) }

1
1. [T] : Type
2. [T'] : Type
⊢ ∀y:T'. ∀f:{x:T| (x ∈ [])}  ⟶ T'.  ((y ∈ []) ⇐⇒ ∃a:T. ((a ∈ []) c∧ (y = (f a) ∈ T')))

2
1. [T] : Type
2. [T'] : Type
3. u : T
4. v : T List
5. ∀y:T'. ∀f:{x:T| (x ∈ v)}  ⟶ T'.  ((y ∈ mapl(f;v)) ⇐⇒ ∃a:T. ((a ∈ v) c∧ (y = (f a) ∈ T')))
⊢ ∀y:T'. ∀f:{x:T| (x ∈ [u / v])}  ⟶ T'.  ((y ∈ [f u / mapl(f;v)]) ⇐⇒ ∃a:T. ((a ∈ [u / v]) c∧ (y = (f a) ∈ T')))

---

Latex:

---

Latex:
\mforall{}[T,T':Type].
    \mforall{}L:T  List.  \mforall{}y:T'.  \mforall{}f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  T'.    ((y  \mmember{}  mapl(f;L))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:T.  ((a  \mmember{}  L)  c\mwedge{}  (y  =  (f  a))))


By

---

Latex:
(InductionOnList  THEN  Unfold  `mapl`  0  THEN  Reduce  0  THEN  Try  (Fold  `mapl`  0))

---

Home Index