---

Step * of Lemma fpf-union-join-dom

∀[A:Type]
  ∀eq:EqDecider(A). ∀f,g:a:A fp-> Top. ∀x:A. ∀R:Top.
    (↑x ∈ dom(fpf-union-join(eq;R;f;g)) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
BY
{ (UnivCD THENA Auto) }

1
1. [A] : Type
2. eq : EqDecider(A)@i
3. f : a:A fp-> Top@i
4. g : a:A fp-> Top@i
5. x : A@i
6. R : Top@i
⊢ ↑x ∈ dom(fpf-union-join(eq;R;f;g)) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g))

---

Latex:


\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A).  \mforall{}f,g:a:A  fp->  Top.  \mforall{}x:A.  \mforall{}R:Top.
        (\muparrow{}x  \mmember{}  dom(fpf-union-join(eq;R;f;g))  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))  \mvee{}  (\muparrow{}x  \mmember{}  dom(g)))


By

(UnivCD  THENA  Auto)

---

Home Index