---

Step * of Lemma member-concat-map

∀[T,S:Type].  ∀f:T ⟶ (S List). ∀L:T List. ∀x:S.  ((x ∈ concat(map(f;L))) ⇐⇒ (∃t∈L. (x ∈ f t)))
BY
{ (InductionOnList THEN Reduce 0 THEN (RWW "concat-cons map_append_sq concat_append" 0 THEN Reduce 0) THEN Auto) }

1
1. [T] : Type
2. [S] : Type
3. f : T ⟶ (S List)@i
4. x : S@i
5. (∃t∈[]. (x ∈ f t))@i
⊢ (x ∈ [])

2
1. [T] : Type
2. [S] : Type
3. f : T ⟶ (S List)@i
4. u : T@i
5. v : T List@i
6. ∀x:S. ((x ∈ concat(map(f;v))) ⇐⇒ (∃t∈v. (x ∈ f t)))@i
7. x : S@i
8. (x ∈ (f u) @ concat(map(f;v)))@i
⊢ (∃t∈[u / v]. (x ∈ f t))

3
1. [T] : Type
2. [S] : Type
3. f : T ⟶ (S List)@i
4. u : T@i
5. v : T List@i
6. ∀x:S. ((x ∈ concat(map(f;v))) ⇐⇒ (∃t∈v. (x ∈ f t)))@i
7. x : S@i
8. (∃t∈[u / v]. (x ∈ f t))@i
⊢ (x ∈ (f u) @ concat(map(f;v)))

---

Latex:

---

Latex:
\mforall{}[T,S:Type].    \mforall{}f:T  {}\mrightarrow{}  (S  List).  \mforall{}L:T  List.  \mforall{}x:S.    ((x  \mmember{}  concat(map(f;L)))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}t\mmember{}L.  (x  \mmember{}  f  t)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  (RWW  "concat-cons  map\_append\_sq  concat\_append"  0  THEN  Reduce  0)
  THEN  Auto)

---

Home Index