---

Step * of Lemma mem_map

∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀x:|s|. ∀as:|s| List.  ((↑(x ∈b as)) ⇒ (↑((f x) ∈b map(f;as))))
BY
{ TACTIC:(InductionOnListA THEN Reduce 0 THEN Auto THEN (All (RW bool_to_propC) THENA Auto)) }

1
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)))

---

Latex:

---

Latex:
\mforall{}s,s':DSet.  \mforall{}f:|s|  {}\mrightarrow{}  |s'|.  \mforall{}x:|s|.  \mforall{}as:|s|  List.    ((\muparrow{}(x  \mmember{}\msubb{}  as))  {}\mRightarrow{}  (\muparrow{}((f  x)  \mmember{}\msubb{}  map(f;as))))


By

---

Latex:
TACTIC:(InductionOnListA  THEN  Reduce  0  THEN  Auto  THEN  (All  (RW  bool\_to\_propC)  THENA  Auto))

---

Home Index