Nuprl Lemma : fpf-join-list-domain2

{

[A:Type]

eq:EqDecider(A).

L:a:A fp-> Top List.

x:A.
((x

fpf-domain(

(L)))

(

f

L. (x

fpf-domain(f)))) }

{ Proof }

Definitions occuring in Statement : fpf-join-list:

(L), fpf-domain: fpf-domain(f), fpf: a:A fp-> B[a], uall:

[x:A]. B[x], top: Top, all:

x:A. B[x], iff: P

Q, list: type List, universe: Type, l_exists: (

x

L. P[x]), l_member: (x

l), deq: EqDecider(T)
Definitions : uall:

[x:A]. B[x], all:

x:A. B[x], member: t

T, so_lambda:

x.t[x], iff: P

Q, l_exists: (

x

L. P[x]), prop:

, and: P

Q, implies: P

Q, rev_implies: P

Q, exists:

x:A. B[x], cand: A c

B, so_apply: x[s]
Lemmas : fpf-join-list-dom2, fpf_wf, top_wf, deq_wf, assert_wf, fpf-dom_wf, fpf-join-list_wf, l_member_wf, fpf-domain_wf, l_exists_wf, iff_functionality_wrt_iff, member-fpf-domain

\mforall{}[A:Type] \mforall{}eq:EqDecider(A). \mforall{}L:a:A fp-> Top List. \mforall{}x:A. ((x \mmember{} fpf-domain(\moplus{}(L))) \mLeftarrow{}{}\mRightarrow{} (\mexists{}f\mmember{}L. (x \mmember{} fpf-domain(f)))) Date html generated: 2011_08_10-AM-08_01_06 Last ObjectModification: 2011_06_18-AM-08_19_50 Home Index