Nuprl Lemma : classfun-res-parallel-class-right

[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)]. ∀[e:E].
  (X || Y@e Y@e) supposing (disjoint-classrel(es;A;X;A;Y) and (↑e ∈b Y))


Definitions occuring in Statement :  parallel-class: || Y classfun-res: X@e 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] universe: Type sqequal: t
Lemmas :  empty-bag-iff-no-member equal-empty-bag assert-member-eclass empty_bag_append_lemma disjoint-classrel_wf assert_wf member-eclass_wf es-E_wf event-ordering+_subtype eclass_wf event-ordering+_wf

\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(A)].  \mforall{}[e:E].
    (X  ||  Y@e  \msim{}  Y@e)  supposing  (disjoint-classrel(es;A;X;A;Y)  and  (\muparrow{}e  \mmember{}\msubb{}  Y))

Date html generated: 2015_07_23-AM-11_29_04
Last ObjectModification: 2015_01_28-PM-11_12_50

Home Index