---

Step * of Lemma fpf-contains-union-join-right2

∀[A,V:Type]. ∀[B:A ─→ Type].
  ∀eq:EqDecider(A). ∀f,h,g:a:A fp-> B[a] List. ∀R:(V List) ─→ V ─→ 𝔹.
    fpf-union-compatible(A;V;x.B[x];eq;R;f;g) ⇒ h ⊆⊆ g ⇒ h ⊆⊆ fpf-union-join(eq;R;f;g) 
    supposing fpf-single-valued(A;eq;x.B[x];V;g) 
  supposing ∀a:A. (B[a] ⊆r V)
BY
{ (Auto THEN RepeatFor 3 (ParallelLast) THEN Auto) }

1
1. [A] : Type
2. [V] : Type
3. [B] : A ─→ Type
4. ∀a:A. (B[a] ⊆r V)
5. eq : EqDecider(A)@i
6. f : a:A fp-> B[a] List@i
7. h : a:A fp-> B[a] List@i
8. g : a:A fp-> B[a] List@i
9. R : (V List) ─→ V ─→ 𝔹@i
10. fpf-single-valued(A;eq;x.B[x];V;g)
11. fpf-union-compatible(A;V;x.B[x];eq;R;f;g)@i
12. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(g)) c∧ h(x) ⊆ g(x)))@i
13. x : A@i
14. ↑x ∈ dom(h)@i
15. (↑x ∈ dom(g)) c∧ h(x) ⊆ g(x)
⊢ ↑x ∈ dom(fpf-union-join(eq;R;f;g))

2
1. [A] : Type
2. [V] : Type
3. [B] : A ─→ Type
4. ∀a:A. (B[a] ⊆r V)
5. eq : EqDecider(A)@i
6. f : a:A fp-> B[a] List@i
7. h : a:A fp-> B[a] List@i
8. g : a:A fp-> B[a] List@i
9. R : (V List) ─→ V ─→ 𝔹@i
10. fpf-single-valued(A;eq;x.B[x];V;g)
11. fpf-union-compatible(A;V;x.B[x];eq;R;f;g)@i
12. ∀x:A. ((↑x ∈ dom(h)) ⇒ ((↑x ∈ dom(g)) c∧ h(x) ⊆ g(x)))@i
13. x : A@i
14. ↑x ∈ dom(h)@i
15. (↑x ∈ dom(g)) c∧ h(x) ⊆ g(x)
16. ↑x ∈ dom(fpf-union-join(eq;R;f;g))
⊢ h(x) ⊆ fpf-union-join(eq;R;f;g)(x)

---

Latex:


\mforall{}[A,V:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f,h,g:a:A  fp->  B[a]  List.  \mforall{}R:(V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}.
        fpf-union-compatible(A;V;x.B[x];eq;R;f;g)  {}\mRightarrow{}  h  \msubseteq{}\msubseteq{}  g  {}\mRightarrow{}  h  \msubseteq{}\msubseteq{}  fpf-union-join(eq;R;f;g) 
        supposing  fpf-single-valued(A;eq;x.B[x];V;g) 
    supposing  \mforall{}a:A.  (B[a]  \msubseteq{}r  V)


By

(Auto  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index