### 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 e and Y is functional at e)`

Proof

Definitions occuring in Statement :  eclass3: `eclass3(X;Y)` classfun-res: `X@e` es-functional-class-at: `X is functional at e` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-E: `E` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = 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

Latex:
\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