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))


Definitions occuring in Statement :  disjoint-union-comb: (+) 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: supposing a uall: [x:A]. B[x] inr: inr  union: left right universe: Type equal: 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

\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