### Nuprl 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))`

Proof

Definitions occuring in Statement :  fpf-union-join: `fpf-union-join(eq;R;f;g)` fpf-ap: `f(x)` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` l_member: `(x ∈ l)` list: `T List` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` isect: `∩x:A. B[x]` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  assert_witness fpf-dom_wf fpf-union-join_wf subtype-fpf2 top_wf subtype_top list_wf l_member_wf fpf-ap_wf assert_wf bool_wf fpf_wf deq_wf fpf-union-join-ap eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot false_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse nil_wf btrue_neq_bfalse member_append filter_wf5 subtype_rel_dep_function subtype_rel_self set_wf member_filter or_wf true_wf
\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))

Date html generated: 2015_07_17-AM-11_07_33
Last ObjectModification: 2015_01_28-AM-07_48_39

Home Index