Nuprl Lemma : classfun-res-eclass3

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


Definitions occuring in Statement :  eclass3: eclass3(X;Y) classfun-res: X@e es-functional-class-at: is functional at e eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  sv-bag-only-combine bag-map_wf single-valued-classrel-implies-bag member-eclass-iff-size single-valued-bag-map bag-size-map equal_wf sv-bag-only_wf es-functional-class-at_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf sv-bag-only-map2 iff_weakening_equal

\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  C)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (eclass3(X;Y)@e  =  (X@e  Y@e))  supposing  (X  is  functional  at  e  and  Y  is  functional  at  e)

Date html generated: 2015_07_23-AM-11_29_19
Last ObjectModification: 2015_02_04-PM-04_44_40

Home Index