Nuprl Lemma : classfun-res-disjoint-union-comb-right
∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].
(X (+) Y@e = (inr Y@e ) ∈ (A + B)) supposing
(single-valued-classrel(es;Y;B) and
disjoint-classrel(es;A;X;B;Y) and
(↑e ∈b Y))
Proof
Definitions occuring in Statement :
disjoint-union-comb: X (+) Y,
classfun-res: X@e,
single-valued-classrel: single-valued-classrel(es;X;T),
disjoint-classrel: disjoint-classrel(es;A;X;B;Y),
member-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
inr: inr x ,
union: left + right,
universe: Type,
equal: s = t ∈ T
Lemmas :
member-eclass-simple-comb-1,
lifting-1_wf,
assert-bag-null,
bag-combine-null,
single-bag_wf,
null_cons_lemma,
decidable__assert,
bag-member-not-bag-null,
assert_wf,
bag-null_wf,
bag-combine_wf,
lifting1_wf,
bag_wf,
not_wf,
bag-combine-single-right-as-map,
sv-bag-only-map,
member-eclass-iff-size,
single-valued-classrel-implies-bag
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. \mforall{}[e:E].
(X (+) Y@e = (inr Y@e )) supposing
(single-valued-classrel(es;Y;B) and
disjoint-classrel(es;A;X;B;Y) and
(\muparrow{}e \mmember{}\msubb{} Y))
Date html generated:
2015_07_23-AM-11_29_12
Last ObjectModification:
2015_01_28-PM-11_13_37
Home
Index