Nuprl Lemma : outr-or-class
[Info,A,B:Type]. [X:EClass(A)]. [Y:EClass(B)]. (outr-class(or-class(X;Y)) = Y)
Proof not projected
Definitions occuring in Statement :
or-class: or-class(X;Y),
outr-class: outr-class(X),
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
eclass: EClass(A[eo; e]),
outr-class: outr-class(X),
or-class: or-class(X;Y),
member: t 
T,
all: x:A. B[x],
so_lambda: 
x y.t[x; y],
eclass-compose1: f o X,
parallel-class: X || Y,
inl-class: inl-class(X),
inr-class: inr-class(X),
eclass-compose2: eclass-compose2(f;X;Y),
implies: P 
Q,
bag-mapfilter: bag-mapfilter(f;P;bs),
pi2: snd(t),
bag-separate: bag-separate(bs),
so_apply: x[s1;s2],
uimplies: b supposing a,
subtype: S 
T,
bag-merge: bag-merge(as;bs)
Lemmas :
eclass-ext,
es-E_wf,
event-ordering+_inc,
outr-class_wf,
or-class_wf,
top_wf,
es-interface-top,
bag_wf,
eclass_wf,
event-ordering+_wf,
bag-separate-merge,
bag-subtype-list
\mforall{}[Info,A,B:Type]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. (outr-class(or-class(X;Y)) = Y)
Date html generated:
2012_01_23-PM-12_25_26
Last ObjectModification:
2011_12_31-AM-11_53_44
Home
Index