---

Step * of Lemma bag-member-map

∀[T,U:Type].  ∀x:U. ∀f:T ⟶ U. ∀bs:bag(T).  uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))
BY
{ ((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. bs : bag(T)
6. x ↓∈ bag-map(f;bs)
⊢ ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))

2
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. bs : bag(T)
6. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
⊢ x ↓∈ bag-map(f;bs)

---

Latex:

---

Latex:
\mforall{}[T,U:Type].    \mforall{}x:U.  \mforall{}f:T  {}\mrightarrow{}  U.  \mforall{}bs:bag(T).    uiff(x  \mdownarrow{}\mmember{}  bag-map(f;bs);\mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index