Nuprl Lemma : outl-or-class

[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].  (outl-class(or-class(X;Y)) X ∈ EClass(A))


Proof




Definitions occuring in Statement :  or-class: or-class(X;Y) outl-class: outl-class(X) eclass: EClass(A[eo; e]) uall: [x:A]. B[x] universe: Type equal: t ∈ T
Lemmas :  eclass-ext es-E_wf event-ordering+_subtype outl-class_wf or-class_wf top_wf es-interface-subtype_rel2 bag_wf eclass_wf event-ordering+_wf bag-separate-merge bag-subtype-list

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].    (outl-class(or-class(X;Y))  =  X)



Date html generated: 2015_07_20-PM-03_22_52
Last ObjectModification: 2015_01_27-PM-10_21_51

Home Index