---

Step * 1 of Lemma mem_map


1. s : DSet
2. s' : DSet
3. f : |s| ⟶ |s'|
4. x : |s|
5. a : |s|
6. as : |s| List
7. (↑(x ∈b as)) ⇒ (↑((f x) ∈b map(f;as)))
8. (a = x ∈ |s|) ∨ (↑(x ∈b as))
⊢ ((f a) = (f x) ∈ |s'|) ∨ (↑((f x) ∈b map(f;as)))
BY
{ TACTIC:(ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  s'  :  DSet
3.  f  :  |s|  {}\mrightarrow{}  |s'|
4.  x  :  |s|
5.  a  :  |s|
6.  as  :  |s|  List
7.  (\muparrow{}(x  \mmember{}\msubb{}  as))  {}\mRightarrow{}  (\muparrow{}((f  x)  \mmember{}\msubb{}  map(f;as)))
8.  (a  =  x)  \mvee{}  (\muparrow{}(x  \mmember{}\msubb{}  as))
\mvdash{}  ((f  a)  =  (f  x))  \mvee{}  (\muparrow{}((f  x)  \mmember{}\msubb{}  map(f;as)))


By

---

Latex:
TACTIC:(ParallelLast  THEN  Auto)

---

Home Index