Nuprl Lemma : monotone-labeled-graph
[F:Type 
Type]. Monotone(T.LabeledGraph(F[T])) supposing Monotone(T.F[T])
Proof not projected
Definitions occuring in Statement :
labeled-graph: LabeledGraph(T),
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
function: x:A B[x],
universe: Type
Definitions :
all: x:A. B[x],
so_lambda: 
x.t[x],
member: t 
T,
labeled-graph: LabeledGraph(T),
so_apply: x[s],
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: 
,
guard: {T}
Lemmas :
subtype_rel_simple_product,
subtype_rel_list,
subtype_rel_self,
Error :dep-isect-subtype2,
length_wf,
int_seg_wf,
top_wf,
type-monotone_wf
\mforall{}[F:Type {}\mrightarrow{} Type]. Monotone(T.LabeledGraph(F[T])) supposing Monotone(T.F[T])
Date html generated:
2012_01_23-PM-12_36_29
Last ObjectModification:
2011_12_13-PM-05_05_54
Home
Index