Nuprl Lemma : all-class-values_wf
[Info:Type]. [es:EO+(Info)]. [T:Type]. [A:EClass(T)]. [P:T 
]. (all-class-values{i:l}(Info;es;T;A;t.P[t]) 
')
Proof not projected
Definitions occuring in Statement :
all-class-values: all-class-values{i:l}(Info;es;T;A;t.P[t]),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
member: t T,
equal: s = t,
isect: 
x:A. B[x],
function: x:A B[x],
universe: Type,
prop: ,
uall: [x:A]. B[x],
eclass: EClass(A[eo; e]),
so_lambda: 
x y.t[x; y],
event-ordering+: EO+(Info),
all-class-values: all-class-values{i:l}(Info;es;T;A;t.P[t]),
so_apply: x[s],
apply: f a,
axiom: Ax,
all: x:A. B[x],
lambda: x.A[x],
es-E: E,
event_ordering: EO,
subtype: S 
T,
so_lambda: x.t[x],
uimplies: b supposing a,
classrel: v X(e)
Lemmas :
classrel_wf,
uall_wf,
event-ordering+_inc,
es-E_wf,
event-ordering+_wf,
eclass_wf
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[T:Type]. \mforall{}[A:EClass(T)]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}].
(all-class-values\{i:l\}(Info;es;T;A;t.P[t]) \mmember{} \mBbbP{}')
Date html generated:
2011_10_20-PM-04_56_02
Last ObjectModification:
2011_06_21-PM-02_39_04
Home
Index