:: Weighted and Labeled Graphs
:: by Gilbert Lee
::
:: Received February 22, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem :: GLIB_003:1
theorem Th2: :: GLIB_003:2
:: deftheorem defines WeightSelector GLIB_003:def 1 :
:: deftheorem defines ELabelSelector GLIB_003:def 2 :
:: deftheorem defines VLabelSelector GLIB_003:def 3 :
:: deftheorem Def4 defines [Weighted] GLIB_003:def 4 :
:: deftheorem Def5 defines [ELabeled] GLIB_003:def 5 :
:: deftheorem Def6 defines [VLabeled] GLIB_003:def 6 :
:: deftheorem defines the_Weight_of GLIB_003:def 7 :
:: deftheorem defines the_ELabel_of GLIB_003:def 8 :
:: deftheorem defines the_VLabel_of GLIB_003:def 9 :
Lm1:
for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G
Lm2:
for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G
Lm3:
for G being _Graph
for X being set holds
( G .set WeightSelector ,X == G & G .set ELabelSelector ,X == G & G .set VLabelSelector ,X == G )
:: deftheorem Def10 defines weight-inheriting GLIB_003:def 10 :
:: deftheorem Def11 defines elabel-inheriting GLIB_003:def 11 :
:: deftheorem Def12 defines vlabel-inheriting GLIB_003:def 12 :
:: deftheorem Def13 defines real-weighted GLIB_003:def 13 :
:: deftheorem Def14 defines nonnegative-weighted GLIB_003:def 14 :
:: deftheorem Def15 defines real-elabeled GLIB_003:def 15 :
:: deftheorem Def16 defines real-vlabeled GLIB_003:def 16 :
:: deftheorem Def17 defines real-WEV GLIB_003:def 17 :
:: deftheorem Def18 defines .weightSeq() GLIB_003:def 18 :
:: deftheorem defines .cost() GLIB_003:def 19 :
Lm4:
for x, y, X, Y being set
for f being PartFunc of X,Y st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
:: deftheorem defines .labeledE() GLIB_003:def 20 :
:: deftheorem Def21 defines .labelEdge GLIB_003:def 21 :
:: deftheorem Def22 defines .labelVertex GLIB_003:def 22 :
:: deftheorem defines .labeledV() GLIB_003:def 23 :
:: deftheorem Def24 defines [Weighted] GLIB_003:def 24 :
:: deftheorem Def25 defines [ELabeled] GLIB_003:def 25 :
:: deftheorem Def26 defines [VLabeled] GLIB_003:def 26 :
:: deftheorem Def27 defines real-weighted GLIB_003:def 27 :
:: deftheorem Def28 defines nonnegative-weighted GLIB_003:def 28 :
:: deftheorem Def29 defines real-elabeled GLIB_003:def 29 :
:: deftheorem Def30 defines real-vlabeled GLIB_003:def 30 :
:: deftheorem Def31 defines real-WEV GLIB_003:def 31 :
theorem :: GLIB_003:3
theorem :: GLIB_003:4
theorem :: GLIB_003:5
canceled;
theorem :: GLIB_003:6
theorem :: GLIB_003:7
theorem :: GLIB_003:8
theorem :: GLIB_003:9
canceled;
theorem :: GLIB_003:10
canceled;
theorem :: GLIB_003:11
canceled;
theorem :: GLIB_003:12
canceled;
theorem :: GLIB_003:13
canceled;
theorem :: GLIB_003:14
canceled;
theorem :: GLIB_003:15
theorem :: GLIB_003:16
theorem :: GLIB_003:17
theorem :: GLIB_003:18
theorem Th19: :: GLIB_003:19
theorem :: GLIB_003:20
theorem Th21: :: GLIB_003:21
theorem Th22: :: GLIB_003:22
theorem Th23: :: GLIB_003:23
theorem Th24: :: GLIB_003:24
theorem Th25: :: GLIB_003:25
theorem Th26: :: GLIB_003:26
theorem Th27: :: GLIB_003:27
theorem :: GLIB_003:28
theorem :: GLIB_003:29
theorem :: GLIB_003:30
theorem :: GLIB_003:31
theorem :: GLIB_003:32
theorem :: GLIB_003:33
theorem :: GLIB_003:34
theorem Th35: :: GLIB_003:35
theorem :: GLIB_003:36
theorem :: GLIB_003:37
theorem :: GLIB_003:38
theorem Th39: :: GLIB_003:39
theorem :: GLIB_003:40
theorem :: GLIB_003:41
theorem :: GLIB_003:42
theorem Th43: :: GLIB_003:43
theorem :: GLIB_003:44
theorem Th45: :: GLIB_003:45
theorem :: GLIB_003:46
theorem :: GLIB_003:47
theorem :: GLIB_003:48
theorem Th49: :: GLIB_003:49
theorem :: GLIB_003:50
theorem :: GLIB_003:51
theorem Th52: :: GLIB_003:52
theorem :: GLIB_003:53
theorem :: GLIB_003:54
theorem :: GLIB_003:55
theorem :: GLIB_003:56
theorem :: GLIB_003:57
theorem :: GLIB_003:58
theorem Th59: :: GLIB_003:59
theorem :: GLIB_003:60
theorem :: GLIB_003:61
theorem :: GLIB_003:62
theorem :: GLIB_003:63
theorem :: GLIB_003:64