Nuprl Lemma : lg-size-map
[T,S:Type]. [f:T 
S]. [g:LabeledGraph(T)]. (lg-size(lg-map(f;g)) = lg-size(g))
Proof not projected
Definitions occuring in Statement :
lg-map: lg-map(f;g),
lg-size: lg-size(g),
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
function: x:A B[x],
int: 
,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
lg-size: lg-size(g),
lg-map: lg-map(f;g),
member: t 
T,
top: Top,
labeled-graph: LabeledGraph(T)
Lemmas :
length-map-sq,
length_wf,
top_wf,
labeled-graph_wf
\mforall{}[T,S:Type]. \mforall{}[f:T {}\mrightarrow{} S]. \mforall{}[g:LabeledGraph(T)]. (lg-size(lg-map(f;g)) = lg-size(g))
Date html generated:
2012_01_23-PM-12_38_40
Last ObjectModification:
2012_01_05-PM-02_25_33
Home
Index