Nuprl Lemma : eclass_wf3

[f:Name ─→ Type]. ∀[T:Type].  (EClass(T) ∈ 𝕌')


Proof




Definitions occuring in Statement :  Message: Message(f) eclass: EClass(A[eo; e]) name: Name uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  eclass_wf Message_wf es-E_wf event-ordering+_subtype event-ordering+_wf name_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[T:Type].    (EClass(T)  \mmember{}  \mBbbU{}')



Date html generated: 2015_07_21-PM-04_48_29
Last ObjectModification: 2015_01_28-AM-08_46_26

Home Index