---

Step * 2 2 of Lemma map-l-union


1. T : Type
2. T' : Type
3. f : T ⟶ T'
4. eq : EqDecider(T)
5. eq' : EqDecider(T')
6. u : T
7. v : T List
8. ∀as:T List. (Inj({x:T| (x ∈ as ⋃ v)} ;T';f) ⇒ (map(f;as ⋃ v) ~ map(f;as) ⋃ map(f;v)))
9. as : T List
10. ¬(u ∈ as ⋃ v)
11. Inj({x:T| (x ∈ insert(u;as ⋃ v))} ;T';f)
12. (f u ∈ map(f;as ⋃ v))
⊢ [f u / map(f;as ⋃ v)] ~ map(f;as ⋃ v)
BY
{ ((RWO "member-map" (-1) THENA Auto) THEN ExRepD) }

1
1. T : Type
2. T' : Type
3. f : T ⟶ T'
4. eq : EqDecider(T)
5. eq' : EqDecider(T')
6. u : T
7. v : T List
8. ∀as:T List. (Inj({x:T| (x ∈ as ⋃ v)} ;T';f) ⇒ (map(f;as ⋃ v) ~ map(f;as) ⋃ map(f;v)))
9. as : T List
10. ¬(u ∈ as ⋃ v)
11. Inj({x:T| (x ∈ insert(u;as ⋃ v))} ;T';f)
12. y : T
13. (y ∈ as ⋃ v)
14. (f u) = (f y) ∈ T'
⊢ [f u / map(f;as ⋃ v)] ~ map(f;as ⋃ v)

---

Latex:

---

Latex:

1.  T  :  Type
2.  T'  :  Type
3.  f  :  T  {}\mrightarrow{}  T'
4.  eq  :  EqDecider(T)
5.  eq'  :  EqDecider(T')
6.  u  :  T
7.  v  :  T  List
8.  \mforall{}as:T  List.  (Inj(\{x:T|  (x  \mmember{}  as  \mcup{}  v)\}  ;T';f)  {}\mRightarrow{}  (map(f;as  \mcup{}  v)  \msim{}  map(f;as)  \mcup{}  map(f;v)))
9.  as  :  T  List
10.  \mneg{}(u  \mmember{}  as  \mcup{}  v)
11.  Inj(\{x:T|  (x  \mmember{}  insert(u;as  \mcup{}  v))\}  ;T';f)
12.  (f  u  \mmember{}  map(f;as  \mcup{}  v))
\mvdash{}  [f  u  /  map(f;as  \mcup{}  v)]  \msim{}  map(f;as  \mcup{}  v)


By

---

Latex:
((RWO  "member-map"  (-1)  THENA  Auto)  THEN  ExRepD)

---

Home Index