---

Step * of Lemma fset-image-union

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[x,y:fset(T)].
  (f"(x ⋃ y) = f"(x) ⋃ f"(y) ∈ fset(A))
BY
{ (Auto THEN FsetExt) }

1
1. T : Type
2. A : Type
3. eqt : EqDecider(T)
4. eqa : EqDecider(A)
5. f : T ⟶ A
6. x : fset(T)
7. y : fset(T)
8. a : A
9. a ∈ f"(x ⋃ y)
⊢ a ∈ f"(x) ∨ a ∈ f"(y)

2
1. T : Type
2. A : Type
3. eqt : EqDecider(T)
4. eqa : EqDecider(A)
5. f : T ⟶ A
6. x : fset(T)
7. y : fset(T)
8. a : A
9. a ∈ f"(x) ∨ a ∈ f"(y)
⊢ a ∈ f"(x ⋃ y)

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[eqt:EqDecider(T)].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[x,y:fset(T)].
    (f"(x  \mcup{}  y)  =  f"(x)  \mcup{}  f"(y))


By

---

Latex:
(Auto  THEN  FsetExt)

---

Home Index