---

Step * of Lemma fpf-cap-join-subtype

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Type]. ∀[a:A].  (f ⊕ g(a)?Top ⊆r f(a)?Top)
BY
{ Auto }

1
1. A : Type
2. eq : EqDecider(A)
3. f : a:A fp-> Type
4. g : a:A fp-> Type
5. a : A
⊢ f ⊕ g(a)?Top ⊆r f(a)?Top

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:A  fp->  Type].  \mforall{}[a:A].    (f  \moplus{}  g(a)?Top  \msubseteq{}r  f(a)?Top)


By

Auto

---

Home Index