---

Step * of Lemma member-fset-map

∀[T:Type]. ∀[eqT:EqDecider(T)]. ∀[X:Type]. ∀[eqX:EqDecider(X)]. ∀[f:T ⟶ X]. ∀[s:fset(T)]. ∀[x:X].
  uiff(x ∈ fset-map(f;s);↓∃y:T. (y ∈ s ∧ (x = (f y) ∈ X)))
BY
{ Auto }

1
1. T : Type
2. eqT : EqDecider(T)
3. X : Type
4. eqX : EqDecider(X)
5. f : T ⟶ X
6. s : fset(T)
7. x : X
8. x ∈ fset-map(f;s)
⊢ ↓∃y:T. (y ∈ s ∧ (x = (f y) ∈ X))

2
1. T : Type
2. eqT : EqDecider(T)
3. X : Type
4. eqX : EqDecider(X)
5. f : T ⟶ X
6. s : fset(T)
7. x : X
8. ↓∃y:T. (y ∈ s ∧ (x = (f y) ∈ X))
⊢ x ∈ fset-map(f;s)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eqT:EqDecider(T)].  \mforall{}[X:Type].  \mforall{}[eqX:EqDecider(X)].  \mforall{}[f:T  {}\mrightarrow{}  X].  \mforall{}[s:fset(T)].  \mforall{}[x:X].
    uiff(x  \mmember{}  fset-map(f;s);\mdownarrow{}\mexists{}y:T.  (y  \mmember{}  s  \mwedge{}  (x  =  (f  y))))


By

---

Latex:
Auto

---

Home Index