---

Step * of Lemma member-f-union

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[g:T ⟶ fset(A)]. ∀[s:fset(T)]. ∀[a:A].
  uiff(a ∈ f-union(eqt;eqa;s;x.g[x]);↓∃x:T. (x ∈ s ∧ a ∈ g[x]))
BY
{ Auto }

1
1. T : Type
2. A : Type
3. eqt : EqDecider(T)
4. eqa : EqDecider(A)
5. g : T ⟶ fset(A)
6. s : fset(T)
7. a : A
8. a ∈ f-union(eqt;eqa;s;x.g[x])
⊢ ↓∃x:T. (x ∈ s ∧ a ∈ g[x])

2
1. T : Type
2. A : Type
3. eqt : EqDecider(T)
4. eqa : EqDecider(A)
5. g : T ⟶ fset(A)
6. s : fset(T)
7. a : A
8. ↓∃x:T. (x ∈ s ∧ a ∈ g[x])
⊢ a ∈ f-union(eqt;eqa;s;x.g[x])

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[eqt:EqDecider(T)].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[g:T  {}\mrightarrow{}  fset(A)].  \mforall{}[s:fset(T)].  \mforall{}[a:A].
    uiff(a  \mmember{}  f-union(eqt;eqa;s;x.g[x]);\mdownarrow{}\mexists{}x:T.  (x  \mmember{}  s  \mwedge{}  a  \mmember{}  g[x]))


By

---

Latex:
Auto

---

Home Index