Nuprl Lemma : is-max-f-class

[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[e:E].
  (e ∈b (v from with maximum f[v]) e ∈b X)


Definitions occuring in Statement :  max-f-class: (v from with maximum f[v]) in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E uall: [x:A]. B[x] top: Top so_apply: x[s] universe: Type sqequal: t
Lemmas :  is-accum-class es-interface-subtype_rel2 es-E_wf event-ordering+_subtype eclass_wf event-ordering+_wf top_wf

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[f:Top].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (e  \mmember{}\msubb{}  (v  from  X  with  maximum  f[v])  \msim{}  e  \mmember{}\msubb{}  X)

Date html generated: 2015_07_20-PM-03_49_46
Last ObjectModification: 2015_01_27-PM-10_07_01

Home Index