Nuprl Lemma : is-dag-map

[T,S:Type].

[f:T

S].

[g:LabeledGraph(T)]. is-dag(lg-map(f;g)) supposing is-dag(g)

Proof not projected

Definitions occuring in Statement : lg-map: lg-map(f;g), is-dag: is-dag(g), labeled-graph: LabeledGraph(T), uimplies: b supposing a, uall:

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

B[x], universe: Type
Definitions : uall:

[x:A]. B[x], uimplies: b supposing a, is-dag: is-dag(g), member: t

T, all:

x:A. B[x], int_seg: {i..j

}, implies: P

Q, lelt: i

j < k, and: P

Q, le: A

B, not:

A, false: False, prop:

, iff: P

Q, nat:

Lemmas : lg-size-map, lelt_wf, lg-edge-map, lg-edge_wf, lg-map_wf, int_seg_wf, lg-size_wf, nat_wf, is-dag_wf, labeled-graph_wf

\mforall{}[T,S:Type]. \mforall{}[f:T {}\mrightarrow{} S]. \mforall{}[g:LabeledGraph(T)]. is-dag(lg-map(f;g)) supposing is-dag(g) Date html generated: 2012_01_23-PM-12_39_00 Last ObjectModification: 2012_01_05-PM-02_50_01 Home Index