Nuprl Lemma : eclass3-functional

[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)].
  (eclass3(X;Y) is functional) supposing (X is functional and is functional)


Definitions occuring in Statement :  eclass3: eclass3(X;Y) es-functional-class: is functional eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) uimplies: supposing a uall: [x:A]. B[x] function: x:A ─→ B[x] universe: Type
Lemmas :  eclass3-single-val eclass3-total classrel_wf eclass3_wf es-E_wf event-ordering+_subtype less_than_wf bag-size_wf class-ap_wf nat_wf es-functional-class_wf event-ordering+_wf eclass_wf
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  C)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].
    (eclass3(X;Y)  is  functional)  supposing  (X  is  functional  and  Y  is  functional)

Date html generated: 2015_07_17-PM-00_38_01
Last ObjectModification: 2015_01_27-PM-11_13_41

Home Index