---

Step * of Lemma fpf-union-join-member

∀[A:Type]
  ∀eq:EqDecider(A)
    ∀[B:A ⟶ Type]
      ∀f,g:a:A fp-> B[a] List. ∀R:⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹). ∀a:A.
        ∀x:B[a]. ((x ∈ fpf-union-join(eq;R;f;g)(a)) ⇒ (((↑a ∈ dom(f)) ∧ (x ∈ f(a))) ∨ ((↑a ∈ dom(g)) ∧ (x ∈ g(a))))) 
        supposing ↑a ∈ dom(fpf-union-join(eq;R;f;g))
BY
{ 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. (x ∈ fpf-union-join(eq;R;f;g)(a))@i
⊢ ((↑a ∈ dom(f)) ∧ (x ∈ f(a))) ∨ ((↑a ∈ dom(g)) ∧ (x ∈ g(a)))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A)
        \mforall{}[B:A  {}\mrightarrow{}  Type]
            \mforall{}f,g:a:A  fp->  B[a]  List.  \mforall{}R:\mcap{}a:A.  ((B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{}).  \mforall{}a:A.
                \mforall{}x:B[a]
                    ((x  \mmember{}  fpf-union-join(eq;R;f;g)(a))
                    {}\mRightarrow{}  (((\muparrow{}a  \mmember{}  dom(f))  \mwedge{}  (x  \mmember{}  f(a)))  \mvee{}  ((\muparrow{}a  \mmember{}  dom(g))  \mwedge{}  (x  \mmember{}  g(a))))) 
                supposing  \muparrow{}a  \mmember{}  dom(fpf-union-join(eq;R;f;g))


By

---

Latex:
Auto

---

Home Index