---

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


1. [A] : Type
2. eq : EqDecider(A)
3. [B] : A ⟶ Type
4. f : a:A fp-> B[a] List
5. g : a:A fp-> B[a] List
6. R : ⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹)
7. a : A
8. ↑a ∈ dom(fpf-union-join(eq;R;f;g))
9. x : B[a]
10. (x ∈ fpf-union-join(eq;R;f;g)(a))
⊢ ((↑a ∈ dom(f)) ∧ (x ∈ f(a))) ∨ ((↑a ∈ dom(g)) ∧ (x ∈ g(a)))
BY
{ xxx((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)xxx }

1
1. [A] : Type
2. eq : EqDecider(A)
3. [B] : A ⟶ Type
4. f : a:A fp-> B[a] List
5. g : a:A fp-> B[a] List
6. R : ⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹)
7. a : A
8. ↑a ∈ dom(fpf-union-join(eq;R;f;g))
9. x : B[a]
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)))
⊢ (True ∧ (x ∈ f(a))) ∨ (True ∧ (x ∈ g(a)))

---

Latex:

---

Latex:

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


By

---

Latex:
xxx((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)xxx

---

Home Index