### Nuprl Lemma : fpf-join-dom

`∀[A:Type]. ∀[B:A ─→ Type].`
`  ∀eq:EqDecider(A). ∀f,g:a:A fp-> B[a]. ∀x:A.  (↑x ∈ dom(f ⊕ g) `⇐⇒` (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))`

Proof

Definitions occuring in Statement :  fpf-join: `f ⊕ g` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` assert: `↑b` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  deq-member_wf bool_wf eqtt_to_assert assert-deq-member l_member_wf or_wf false_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot true_wf member_filter bnot_wf assert_wf filter_wf5 iff_wf member_append append_wf list_wf deq_wf
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
\mforall{}eq:EqDecider(A).  \mforall{}f,g:a:A  fp->  B[a].  \mforall{}x:A.    (\muparrow{}x  \mmember{}  dom(f  \moplus{}  g)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))  \mvee{}  (\muparrow{}x  \mmember{}  dom(g)))

Date html generated: 2015_07_17-AM-09_19_40
Last ObjectModification: 2015_01_28-AM-07_49_56

Home Index