Nuprl Lemma : lg-edge-map

[T,S:Type].

f:T

S.

g:LabeledGraph(T).

a,b:

lg-size(g). (lg-edge(lg-map(f;g);a;b)

lg-edge(g;a;b))

Proof not projected

Definitions occuring in Statement : lg-map: lg-map(f;g), lg-edge: lg-edge(g;a;b), lg-size: lg-size(g), labeled-graph: LabeledGraph(T), int_seg: {i..j

}, uall:

[x:A]. B[x], all:

x:A. B[x], iff: P

Q, function: x:A

B[x], natural_number: $n, universe: Type
Definitions : uall:

[x:A]. B[x], all:

x:A. B[x], lg-size: lg-size(g), iff: P

Q, lg-edge: lg-edge(g;a;b), lg-map: lg-map(f;g), lg-in-edges: lg-in-edges(g;x), spreadn: spread3, pi1: fst(t), pi2: snd(t), top: Top, member: t

T, le: A

B, not:

A, implies: P

Q, false: False, and: P

Q, rev_implies: P

Q, subtype: S

T, labeled-graph: LabeledGraph(T), int_seg: {i..j

}, uimplies: b supposing a, lelt: i

j < k, nat:

, prop:

Lemmas : select-map, select_wf, int_seg_wf, l_member_wf, lg-size_wf, nat_wf, labeled-graph_wf

\mforall{}[T,S:Type]. \mforall{}f:T {}\mrightarrow{} S. \mforall{}g:LabeledGraph(T). \mforall{}a,b:\mBbbN{}lg-size(g). (lg-edge(lg-map(f;g);a;b) \mLeftarrow{}{}\mRightarrow{} lg-edge(g;a;b)) Date html generated: 2012_01_23-PM-12_38_50 Last ObjectModification: 2012_01_05-PM-02_49_26 Home Index