### Nuprl Lemma : disjoint-union-comb-single-val

`∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].`
`  (single-valued-classrel(es;X (+) Y;A + B)) supposing `
`     (disjoint-classrel(es;A;X;B;Y) and `
`     single-valued-classrel(es;Y;B) and `
`     single-valued-classrel(es;X;A))`

Proof

Definitions occuring in Statement :  disjoint-union-comb: `X (+) Y` single-valued-classrel: `single-valued-classrel(es;X;T)` disjoint-classrel: `disjoint-classrel(es;A;X;B;Y)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` union: `left + right` universe: `Type`
Lemmas :  parallel-class-single-val simple-comb-1_wf lifting-1_wf simple-comb-1-single-val disjoint-classrel-symm simple-comb-1-disjoint-classrel classrel_wf disjoint-union-comb_wf es-E_wf event-ordering+_subtype disjoint-classrel_wf single-valued-classrel_wf eclass_wf event-ordering+_wf

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
(single-valued-classrel(es;X  (+)  Y;A  +  B))  supposing
(disjoint-classrel(es;A;X;B;Y)  and
single-valued-classrel(es;Y;B)  and
single-valued-classrel(es;X;A))

Date html generated: 2015_07_22-PM-00_19_21
Last ObjectModification: 2015_01_28-AM-10_42_35

Home Index