---

Step * of Lemma fpf-join-range

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[df:x:A fp-> Type]. ∀[f:x:A fp-> df(x)?Top]. ∀[dg:x:A fp-> Type].
∀[g:x:A fp-> dg(x)?Top].
  (f ⊕ g ∈ x:A fp-> df ⊕ dg(x)?Top) supposing 
     ((∀x:A. ((↑x ∈ dom(g)) ⇒ (↑x ∈ dom(dg)))) and 
     (∀x:A. ((↑x ∈ dom(f)) ⇒ (↑x ∈ dom(df)))) and 
     df || dg)
BY
{ TACTIC:(UnivCD THENA Auto) }

1
1. A : Type
2. eq : EqDecider(A)
3. df : x:A fp-> Type
4. f : x:A fp-> df(x)?Top
5. dg : x:A fp-> Type
6. g : x:A fp-> dg(x)?Top
7. df || dg
8. ∀x:A. ((↑x ∈ dom(f)) ⇒ (↑x ∈ dom(df)))
9. ∀x:A. ((↑x ∈ dom(g)) ⇒ (↑x ∈ dom(dg)))
⊢ f ⊕ g ∈ x:A fp-> df ⊕ dg(x)?Top

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[df:x:A  fp->  Type].  \mforall{}[f:x:A  fp->  df(x)?Top].  \mforall{}[dg:x:A  fp->  Type].
\mforall{}[g:x:A  fp->  dg(x)?Top].
    (f  \moplus{}  g  \mmember{}  x:A  fp->  df  \moplus{}  dg(x)?Top)  supposing 
          ((\mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(g))  {}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(dg))))  and 
          (\mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(f))  {}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(df))))  and 
          df  ||  dg)


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index