Step
*
1
1
of Lemma
bag-member-map
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. L : T List
⊢ x ↓∈ bag-map(f;L)
⇒ (↓∃v:T. (v ↓∈ L ∧ (x = (f v) ∈ U)))
BY
{ ListInd (-1) }
1
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
⊢ x ↓∈ bag-map(f;[])
⇒ (↓∃v:T. (v ↓∈ [] ∧ (x = (f v) ∈ U)))
2
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. u : T
6. v : T List
7. x ↓∈ bag-map(f;v)
⇒ (↓∃v@0:T. (v@0 ↓∈ v ∧ (x = (f v@0) ∈ U)))
⊢ x ↓∈ bag-map(f;[u / v])
⇒ (↓∃v@0:T. (v@0 ↓∈ [u / v] ∧ (x = (f v@0) ∈ U)))
Latex:
Latex:
1. T : Type
2. U : Type
3. x : U
4. f : T {}\mrightarrow{} U
5. L : T List
\mvdash{} x \mdownarrow{}\mmember{} bag-map(f;L) {}\mRightarrow{} (\mdownarrow{}\mexists{}v:T. (v \mdownarrow{}\mmember{} L \mwedge{} (x = (f v))))
By
Latex:
ListInd (-1)
Home
Index