---

Step * 1 of Lemma fpf-join-sub2


∀A:Type. ∀B:A ⟶ Type. ∀eq:EqDecider(A). ∀f1,g,f2:a:A fp-> B[a].  (f1 ⊆ g ⇒ f2 ⊆ g ⇒ f1 ⊕ f2 ⊆ g)
BY
{ xxx((InstLemma `fpf-join-sub` []) THEN RepeatFor 6 (ParallelLast) THEN Auto)xxx }

1
1. A : Type
2. B : A ⟶ Type
3. eq : EqDecider(A)
4. f1 : a:A fp-> B[a]
5. g : a:A fp-> B[a]
6. f2 : a:A fp-> B[a]
7. ∀[g2:a:A fp-> B[a]]. (f1 ⊕ f2 ⊆ g ⊕ g2) supposing (f2 ⊆ g2 and f1 ⊆ g and f2 || g)
8. f1 ⊆ g
9. f2 ⊆ g
⊢ f1 ⊕ f2 ⊆ g

---

Latex:

---

Latex:

\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}eq:EqDecider(A).  \mforall{}f1,g,f2:a:A  fp->  B[a].    (f1  \msubseteq{}  g  {}\mRightarrow{}  f2  \msubseteq{}  g  {}\mRightarrow{}  f1  \moplus{}  f2  \msubseteq{}  g)


By

---

Latex:
xxx((InstLemma  `fpf-join-sub`  [])  THEN  RepeatFor  6  (ParallelLast)  THEN  Auto)xxx

---

Home Index