---

Step * 1 of Lemma fpf-union-join-member


1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. f : a:A fp-> B[a] List@i
5. g : a:A fp-> B[a] List@i
6. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
7. a : A@i
8. ↑a ∈ dom(fpf-union-join(eq;R;f;g))
9. x : B[a]@i
10. (x ∈ fpf-union-join(eq;R;f;g)(a))@i
⊢ ((↑a ∈ dom(f)) ∧ (x ∈ f(a))) ∨ ((↑a ∈ dom(g)) ∧ (x ∈ g(a)))
BY
{ ((IsectHD ⌈a⌉ 6⋅ THENA Auto)
   THEN (RWO "fpf-union-join-ap" (-2) THENA Auto)
   THEN MoveToConcl (-2)
   THEN Unfold `fpf-union` (0)
   THEN Unfold `fpf-cap` 0
   THEN AutoBoolCase ⌈a ∈ dom(f)⌉⋅
   THEN AutoBoolCase ⌈a ∈ dom(g)⌉⋅
   THEN Auto) }

1
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. f : a:A fp-> B[a] List@i
5. g : a:A fp-> B[a] List@i
6. R : ∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹)@i
7. a : A@i
8. ↑a ∈ dom(fpf-union-join(eq;R;f;g))
9. x : B[a]@i
10. R ∈ (B[a] List) ─→ B[a] ─→ 𝔹
11. ↑a ∈ dom(f)
12. ↑a ∈ dom(g)
13. (x ∈ f(a) @ filter(R f(a);g(a)))@i
⊢ (True ∧ (x ∈ f(a))) ∨ (True ∧ (x ∈ g(a)))

---

Latex:



1.  [A]  :  Type
2.  eq  :  EqDecider(A)@i
3.  [B]  :  A  {}\mrightarrow{}  Type
4.  f  :  a:A  fp->  B[a]  List@i
5.  g  :  a:A  fp->  B[a]  List@i
6.  R  :  \mcap{}a:A.  ((B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{})@i
7.  a  :  A@i
8.  \muparrow{}a  \mmember{}  dom(fpf-union-join(eq;R;f;g))
9.  x  :  B[a]@i
10.  (x  \mmember{}  fpf-union-join(eq;R;f;g)(a))@i
\mvdash{}  ((\muparrow{}a  \mmember{}  dom(f))  \mwedge{}  (x  \mmember{}  f(a)))  \mvee{}  ((\muparrow{}a  \mmember{}  dom(g))  \mwedge{}  (x  \mmember{}  g(a)))


By

((IsectHD  \mkleeneopen{}a\mkleeneclose{}  6\mcdot{}  THENA  Auto)
  THEN  (RWO  "fpf-union-join-ap"  (-2)  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  Unfold  `fpf-union`  (0)
  THEN  Unfold  `fpf-cap`  0
  THEN  AutoBoolCase  \mkleeneopen{}a  \mmember{}  dom(f)\mkleeneclose{}\mcdot{}
  THEN  AutoBoolCase  \mkleeneopen{}a  \mmember{}  dom(g)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index