Nuprl Lemma : classfun-res-eclass1

[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ C]. ∀[es:EO+(Info)]. ∀[e:E].
  ((f X)@e (f loc(e) X@e) ∈ C) supposing (single-valued-classrel(es;X;B) and (↑e ∈b X))


Definitions occuring in Statement :  eclass1: (f X) classfun-res: X@e single-valued-classrel: single-valued-classrel(es;X;T) member-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-loc: loc(e) es-E: E Id: Id assert: b uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  sv-bag-only-map2 es-loc_wf single-valued-classrel-implies-bag member-eclass-iff-size single-valued-classrel_wf assert_wf member-eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf Id_wf eclass_wf

\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    ((f  o  X)@e  =  (f  loc(e)  X@e))  supposing  (single-valued-classrel(es;X;B)  and  (\muparrow{}e  \mmember{}\msubb{}  X))

Date html generated: 2015_07_23-AM-11_29_15
Last ObjectModification: 2015_01_28-PM-11_13_00

Home Index