---

Step * 1 1 of Lemma fpf-join-sub2


1. A : Type@i'
2. B : A ─→ Type@i'
3. eq : EqDecider(A)@i
4. f1 : a:A fp-> B[a]@i
5. g : a:A fp-> B[a]@i
6. f2 : a:A fp-> B[a]@i
7. ∀[g2:a:A fp-> B[a]]. (f1 ⊕ f2 ⊆ g ⊕ g2) supposing (f2 ⊆ g2 and f1 ⊆ g and f2 || g)
8. f1 ⊆ g@i
9. f2 ⊆ g@i
⊢ f1 ⊕ f2 ⊆ g
BY
{ (Subst ⌈g = g ⊕ g ∈ a:A fp-> B[a]⌉ 0⋅ THENA Auto) }

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

---

Latex:



1.  A  :  Type@i'
2.  B  :  A  {}\mrightarrow{}  Type@i'
3.  eq  :  EqDecider(A)@i
4.  f1  :  a:A  fp->  B[a]@i
5.  g  :  a:A  fp->  B[a]@i
6.  f2  :  a:A  fp->  B[a]@i
7.  \mforall{}[g2:a:A  fp->  B[a]].  (f1  \moplus{}  f2  \msubseteq{}  g  \moplus{}  g2)  supposing  (f2  \msubseteq{}  g2  and  f1  \msubseteq{}  g  and  f2  ||  g)
8.  f1  \msubseteq{}  g@i
9.  f2  \msubseteq{}  g@i
\mvdash{}  f1  \moplus{}  f2  \msubseteq{}  g


By

(Subst  \mkleeneopen{}g  =  g  \moplus{}  g\mkleeneclose{}  0\mcdot{}  THENA  Auto)

---

Home Index