Nuprl Lemma : eclass_subtype_rel

[T,A,B:Type].  EClass(A) ⊆EClass(B) supposing A ⊆B


Proof




Definitions occuring in Statement :  eclass: EClass(A[eo; e]) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Lemmas :  subtype_rel_dep_function event-ordering+_wf es-E_wf event-ordering+_subtype bag_wf subtype_rel_bag subtype_rel_wf
\mforall{}[T,A,B:Type].    EClass(A)  \msubseteq{}r  EClass(B)  supposing  A  \msubseteq{}r  B



Date html generated: 2015_07_17-PM-00_14_04
Last ObjectModification: 2015_01_28-AM-00_05_32

Home Index