Nuprl Lemma : es-component_wf
∀[Info,A,B:Type]. (ComponentSpec(A;B) ∈ 𝕌')
Proof
Definitions occuring in Statement :
es-component: ComponentSpec(A;B),
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type
Lemmas :
event-ordering+_wf,
eclass_wf,
es-E_wf,
event-ordering+_subtype
Latex:
\mforall{}[Info,A,B:Type]. (ComponentSpec(A;B) \mmember{} \mBbbU{}')
Date html generated:
2015_07_21-PM-04_06_55
Last ObjectModification:
2015_01_27-PM-05_44_23
Home
Index