Nuprl Lemma : fpf-join-dom-da

f,g:x:Knd fp-> Type. ∀x:Knd.  (↑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] Kind-deq: KindDeq Knd: Knd assert: b all: x:A. B[x] iff: ⇐⇒ Q or: P ∨ Q universe: Type
Lemmas :  Knd_wf fpf_wf or_wf assert_wf fpf-dom_wf Kind-deq_wf subtype-fpf2 top_wf subtype_top fpf-join-dom fpf-join_wf iff_wf
\mforall{}f,g:x:Knd  fp->  Type.  \mforall{}x:Knd.    (\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-11_13_41
Last ObjectModification: 2015_01_28-AM-07_41_04

Home Index