---

Step * of Lemma fset-constrained-image-union

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[P:A ⟶ 𝔹]. ∀[x,y:fset(T)].
  (f"(x ⋃ y) s.t. P = f"(x) s.t. P ⋃ f"(y) s.t. P ∈ 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. P : A ⟶ 𝔹
7. x : fset(T)
8. y : fset(T)
9. a : A
10. a ∈ f"(x ⋃ y) s.t. P
⊢ a ∈ f"(x) s.t. P ∨ a ∈ f"(y) s.t. P

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  FsetExt)

---

Home Index