---

Step * of Lemma fpf-domain-join

∀[A:Type]
  ∀f,g:a:A fp-> Top. ∀eq:EqDecider(A). ∀x:A.  ((x ∈ fpf-domain(f ⊕ g)) ⇐⇒ (x ∈ fpf-domain(f)) ∨ (x ∈ fpf-domain(g)))
BY
{ ((UnivCD THENA Auto)
   THEN ((InstLemma `member-fpf-domain` [⌈A⌉; ⌈f⌉; ⌈eq⌉; ⌈x⌉])⋅ THENA Auto)
   THEN ((InstLemma `member-fpf-domain` [⌈A⌉; ⌈g⌉; ⌈eq⌉; ⌈x⌉])⋅ THENA Auto)
   THEN ((InstLemma `member-fpf-domain` [⌈A⌉; ⌈f ⊕ g⌉; ⌈eq⌉; ⌈x⌉])⋅ THENA Auto)) }

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

---

Latex:


\mforall{}[A:Type]
    \mforall{}f,g:a:A  fp->  Top.  \mforall{}eq:EqDecider(A).  \mforall{}x:A.
        ((x  \mmember{}  fpf-domain(f  \moplus{}  g))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  fpf-domain(f))  \mvee{}  (x  \mmember{}  fpf-domain(g)))


By

((UnivCD  THENA  Auto)
  THEN  ((InstLemma  `member-fpf-domain`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `member-fpf-domain`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}g\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `member-fpf-domain`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f  \moplus{}  g\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index