---

Step * 1 of Lemma fpf-union-contains2


1. [A] : Type
2. [V] : Type
3. [B] : A ─→ Type
4. ∀a:A. (B[a] ⊆r V)
5. eq : EqDecider(A)@i
6. f : x:A fp-> B[x] List@i
7. g : x:A fp-> B[x] List@i
8. fpf-single-valued(A;eq;x.B[x];V;g)
9. x : A@i
10. R : (V List) ─→ V ─→ 𝔹@i
11. fpf-union-compatible(A;V;x.B[x];eq;R;f;g)@i
12. ↑x ∈ dom(g)
13. ↑x ∈ dom(f)
14. B[x] ⊆r V
⊢ g(x) ⊆ f(x) @ filter(R f(x);g(x))
BY
{ (All (Unfold `so_apply`)⋅
   THEN Unfold `l_contains` 0
   THEN BLemma `l_all_iff`
   THEN Auto
   THEN Try ((DoSubsume 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 : x:A fp-> (B x) List@i
7. g : x:A fp-> (B x) List@i
8. fpf-single-valued(A;eq;x.B x;V;g)
9. x : A@i
10. R : (V List) ─→ V ─→ 𝔹@i
11. fpf-union-compatible(A;V;x.B x;eq;R;f;g)@i
12. ↑x ∈ dom(g)
13. ↑x ∈ dom(f)
14. (B x) ⊆r V
15. a : B x@i
16. (a ∈ g(x))@i
⊢ (a ∈ f(x) @ filter(R f(x);g(x)))

---

Latex:



1.  [A]  :  Type
2.  [V]  :  Type
3.  [B]  :  A  {}\mrightarrow{}  Type
4.  \mforall{}a:A.  (B[a]  \msubseteq{}r  V)
5.  eq  :  EqDecider(A)@i
6.  f  :  x:A  fp->  B[x]  List@i
7.  g  :  x:A  fp->  B[x]  List@i
8.  fpf-single-valued(A;eq;x.B[x];V;g)
9.  x  :  A@i
10.  R  :  (V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}@i
11.  fpf-union-compatible(A;V;x.B[x];eq;R;f;g)@i
12.  \muparrow{}x  \mmember{}  dom(g)
13.  \muparrow{}x  \mmember{}  dom(f)
14.  B[x]  \msubseteq{}r  V
\mvdash{}  g(x)  \msubseteq{}  f(x)  @  filter(R  f(x);g(x))


By

(All  (Unfold  `so\_apply`)\mcdot{}
  THEN  Unfold  `l\_contains`  0
  THEN  BLemma  `l\_all\_iff`
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto)))

---

Home Index