Nuprl Lemma : es-class-def_wf

[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[X:EClass(B)]. ∀[R:E ─→ A ─→ ℙ]. ∀[F:e:E ─→ {a:A| R[e;a]}  ─→ B].
  (∀a,e such that R[e;a]
     e∈with value  F[e;a]  ∈ ℙ)


Definitions occuring in Statement :  es-class-def: es-class-def eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E uall: [x:A]. B[x] prop: so_apply: x[s1;s2] member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x] universe: Type
Lemmas :  all_wf iff_wf assert_wf in-eclass_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype top_wf exists_wf eclass-val_wf es-E-interface-property eclass_wf event-ordering+_wf

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[X:EClass(B)].  \mforall{}[R:E  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[F:e:E
                                                                                                                                                                    {}\mrightarrow{}  \{a:A|  R[e;a]\} 
                                                                                                                                                                    {}\mrightarrow{}  B].
    (\mforall{}a,e  such  that  R[e;a]
          e\mmember{}X  with  value    F[e;a]    \mmember{}  \mBbbP{})

Date html generated: 2015_07_21-PM-03_26_00
Last ObjectModification: 2015_01_27-PM-06_41_02

Home Index