environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, PRE_POLY, TARSKI, CARD_1, UPROOTS, CARD_3, ARYTM_3, FINSEQ_1, NAT_1, XXREAL_0, FINSET_1, SUBSET_1, FINSEQ_2, ARYTM_1, GLIB_003, TREES_1, GLIB_000, GLIB_001, REAL_1, PBOOLE, ZFMISC_1, FUNCT_2, ABIAN, PARTFUN1, MCART_1, GLIB_002, WAYBEL_0, RELAT_2, RCOMP_1, GRAPH_1, GLIB_004;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, XFAMILY, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, DOMAIN_1, MCART_1, XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, RELSET_1, PARTFUN1, FUNCT_1, FINSEQ_1, FINSEQ_2, PBOOLE, FUNCT_2, RVSUM_1, ABIAN, UPROOTS, FINSET_1, NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, GLIB_002, GLIB_003, RFUNCT_3, PRE_POLY;
definitions TARSKI;
theorems CARD_1, CARD_2, FUNCOP_1, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSET_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, GLIB_002, GLIB_003, ABIAN, INT_1, JORDAN12, NAT_1, PARTFUN1, PBOOLE, RELAT_1, RVSUM_1, TARSKI, TREES_1, UPROOTS, XBOOLE_0, XBOOLE_1, XREAL_0, ZFMISC_1, XREAL_1, XXREAL_0, ORDINAL1, FINSOP_1, FUNCT_7, MCART_1, RELSET_1, PRE_POLY;
schemes NAT_1, SUBSET_1, RECDEF_1, CQC_SIM1, PBOOLE, PRE_CIRC;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FRAENKEL, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, CARD_1, GLIB_000, ABIAN, GLIB_001, GLIB_002, GLIB_003, VALUED_0, RELSET_1, PRE_POLY, INT_1, FINSEQ_1, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, BINOP_2, FINSOP_1, RVSUM_1, GRAPH_2, RFUNCT_3, UPROOTS, GLIB_002, GLIB_003, XXREAL_2, RELSET_1, XTUPLE_0, WSIERP_1, XFAMILY;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities GLIB_000, GLIB_003, RVSUM_1, FUNCOP_1, CARD_1, ORDINAL1;
expansions TARSKI, GLIB_000, GLIB_003;
Lm1:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Lm2:
for F being Function
for x, y, z being set st z in dom (F +* (x .--> y)) & not z in dom F holds
x = z
theorem Th5:
for
A being
set for
b1,
b2 being
Rbag of
A st ( for
x being
set st
x in A holds
b1 . x <= b2 . x ) holds
Sum b1 <= Sum b2
theorem
for
A being
set for
b1,
b2 being
Rbag of
A st ( for
x being
set st
x in A holds
b1 . x = b2 . x ) holds
Sum b1 = Sum b2
theorem
for
A1,
A2 being
set for
b1 being
Rbag of
A1 for
b2 being
Rbag of
A2 st
b1 = b2 holds
Sum b1 = Sum b2
Lm3:
for G being WGraph holds WGraphSelectors c= dom G
Lm4:
for G being WGraph holds
( G == G | WGraphSelectors & the_Weight_of G = the_Weight_of (G | WGraphSelectors) )
Lm5:
for G being WGraph holds dom (G | WGraphSelectors) = WGraphSelectors
definition
let G be
real-weighted WGraph;
let L be
DIJK:Labeling of
G;
existence
ex b1 being Subset of (the_Edges_of G) st
for e1 being set holds
( e1 in b1 iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds
((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e1 being set holds
( e1 in b1 iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds
((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds
((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) holds
b1 = b2
end;
definition
let G be
real-weighted WGraph;
let L be
PRIM:Labeling of
G;
existence
ex b1 being Subset of (the_Edges_of G) st
for e1 being set holds
( e1 in b1 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e1 being set holds
( e1 in b1 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) holds
b1 = b2
end;