:: JGRAPH_1 semantic presentation

theorem Th1: :: JGRAPH_1:1

canceled;

theorem Th2: :: JGRAPH_1:2

for b₁, b₂ being Real holds sqrt ((b₁ ^2 ) + (b₂ ^2 )) <= (abs b₁) + (abs b₂)

proof end;

theorem Th3: :: JGRAPH_1:3

for b₁, b₂ being Real holds
( abs b₁ <= sqrt ((b₁ ^2 ) + (b₂ ^2 )) & abs b₂ <= sqrt ((b₁ ^2 ) + (b₂ ^2 )) )

proof end;

theorem Th4: :: JGRAPH_1:4

for b₁ being Graph
for b₂ being oriented Chain of b₁
for b₃ being FinSequence of the Vertices of b₁ st b₂ is Simple & b₃ is_oriented_vertex_seq_of b₂ holds
for b₄, b₅ being Nat st 1 <= b₄ & b₄ < b₅ & b₅ <= len b₃ & b₃ . b₄ = b₃ . b₅ holds
( b₄ = 1 & b₅ = len b₃ )

proof end;

definition

let c₁ be set ;
func PGraph c₁ -> MultiGraphStruct equals :: JGRAPH_1:def 1
MultiGraphStruct(# a₁,[:a₁,a₁:],(pr1 a₁,a₁),(pr2 a₁,a₁) #);
coherence ;

end;

:: deftheorem Def1 defines PGraph JGRAPH_1:def 1 :

theorem Th5: :: JGRAPH_1:5

for b₁ being non empty set holds PGraph b₁ is Graph by GRAPH_1:def 1;

theorem Th6: :: JGRAPH_1:6

for b₁ being set holds the Vertices of (PGraph b₁) = b₁ ;

definition

let c₁ be FinSequence;
func PairF c₁ -> FinSequence means :Def2: :: JGRAPH_1:def 2
( len a₂ = (len a₁) -' 1 & ( for b₁ being Nat st 1 <= b₁ & b₁ < len a₁ holds
a₂ . b₁ = [(a₁ . b₁),(a₁ . (b₁ + 1))] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines PairF JGRAPH_1:def 2 :

registration

let c₁ be non empty set ;
cluster PGraph a₁ -> Graph-like ;
coherence by Th5;

end;

theorem Th7: :: JGRAPH_1:7

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds b₂ is FinSequence of the Vertices of (PGraph b₁) ;

theorem Th8: :: JGRAPH_1:8

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds PairF b₂ is FinSequence of the Edges of (PGraph b₁)

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
redefine func PairF as PairF c₂ -> FinSequence of the Edges of (PGraph a₁);
coherence by Th8;

end;

theorem Th9: :: JGRAPH_1:9

for b₁ being non empty set
for b₂ being Nat
for b₃ being FinSequence of b₁ st 1 <= b₂ & b₂ <= len (PairF b₃) holds
(PairF b₃) . b₂ in the Edges of (PGraph b₁)

proof end;

theorem Th10: :: JGRAPH_1:10

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds PairF b₂ is oriented Chain of PGraph b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
redefine func PairF as PairF c₂ -> oriented Chain of PGraph a₁;
coherence by Th10;

end;

theorem Th11: :: JGRAPH_1:11

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being FinSequence of the Vertices of (PGraph b₁) st len b₂ >= 1 & b₂ = b₃ holds
b₃ is_oriented_vertex_seq_of PairF b₂

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be FinSequence of c₁;
pred c₃ is_Shortcut_of c₂ means :Def3: :: JGRAPH_1:def 3
( a₂ . 1 = a₃ . 1 & a₂ . (len a₂) = a₃ . (len a₃) & ex b₁ being FinSubsequence of PairF a₂ex b₂ being FinSubsequence of a₂ex b₃ being oriented simple Chain of PGraph a₁ex b₄ being FinSequence of the Vertices of (PGraph a₁) st
( Seq b₁ = b₃ & Seq b₂ = a₃ & b₄ = a₃ & b₄ is_oriented_vertex_seq_of b₃ ) );

end;

:: deftheorem Def3 defines is_Shortcut_of JGRAPH_1:def 3 :

theorem Th12: :: JGRAPH_1:12

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₃ is_Shortcut_of b₂ holds
( 1 <= len b₃ & len b₃ <= len b₂ )

proof end;

theorem Th13: :: JGRAPH_1:13

for b₁ being non empty set
for b₂ being FinSequence of b₁ st len b₂ >= 1 holds
ex b₃ being FinSequence of b₁ st b₃ is_Shortcut_of b₂

proof end;

theorem Th14: :: JGRAPH_1:14

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₃ is_Shortcut_of b₂ holds
rng (PairF b₃) c= rng (PairF b₂)

proof end;

theorem Th15: :: JGRAPH_1:15

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st b₂ . 1 <> b₂ . (len b₂) & b₃ is_Shortcut_of b₂ holds
( b₃ is one-to-one & rng (PairF b₃) c= rng (PairF b₂) & b₃ . 1 = b₂ . 1 & b₃ . (len b₃) = b₂ . (len b₂) )

proof end;

definition

let c₁ be Nat;
let c₂ be FinSequence of (TOP-REAL c₁);
attr a₂ is nodic means :Def4: :: JGRAPH_1:def 4
for b₁, b₂ being Nat holds
( not LSeg a₂,b₁ meets LSeg a₂,b₂ or ( (LSeg a₂,b₁) /\ (LSeg a₂,b₂) = {(a₂ . b₁)} & ( a₂ . b₁ = a₂ . b₂ or a₂ . b₁ = a₂ . (b₂ + 1) ) ) or ( (LSeg a₂,b₁) /\ (LSeg a₂,b₂) = {(a₂ . (b₁ + 1))} & ( a₂ . (b₁ + 1) = a₂ . b₂ or a₂ . (b₁ + 1) = a₂ . (b₂ + 1) ) ) or LSeg a₂,b₁ = LSeg a₂,b₂ );

end;

:: deftheorem Def4 defines nodic JGRAPH_1:def 4 :

theorem Th16: :: JGRAPH_1:16

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is s.n.c. holds
b₁ is s.c.c.

proof end;

theorem Th17: :: JGRAPH_1:17

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is s.c.c. & LSeg b₁,1 misses LSeg b₁,((len b₁) -' 1) holds
b₁ is s.n.c.

proof end;

theorem Th18: :: JGRAPH_1:18

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is nodic & PairF b₁ is Simple holds
b₁ is s.c.c.

proof end;

theorem Th19: :: JGRAPH_1:19

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is nodic & PairF b₁ is Simple & b₁ . 1 <> b₁ . (len b₁) holds
b₁ is s.n.c.

proof end;

theorem Th20: :: JGRAPH_1:20

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds
( for b₅ being set holds
( not b₅ <> b₃ or not b₅ in (LSeg b₂,b₃) /\ (LSeg b₃,b₄) ) or b₂ in LSeg b₃,b₄ or b₄ in LSeg b₂,b₃ )

proof end;

theorem Th21: :: JGRAPH_1:21

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is s.n.c. & (LSeg b₁,1) /\ (LSeg b₁,(1 + 1)) c= {(b₁ /. (1 + 1))} & (LSeg b₁,((len b₁) -' 2)) /\ (LSeg b₁,((len b₁) -' 1)) c= {(b₁ /. ((len b₁) -' 1))} holds
b₁ is unfolded

proof end;

theorem Th22: :: JGRAPH_1:22

for b₁ being non empty set
for b₂ being FinSequence of b₁ st PairF b₂ is Simple & b₂ . 1 <> b₂ . (len b₂) holds
( b₂ is one-to-one & len b₂ <> 1 )

proof end;

theorem Th23: :: JGRAPH_1:23

for b₁ being non empty set
for b₂ being FinSequence of b₁ st b₂ is one-to-one & len b₂ > 1 holds
( PairF b₂ is Simple & b₂ . 1 <> b₂ . (len b₂) )

proof end;

theorem Th24: :: JGRAPH_1:24

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is nodic & PairF b₁ is Simple & b₁ . 1 <> b₁ . (len b₁) holds
b₁ is unfolded

proof end;

theorem Th25: :: JGRAPH_1:25

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Nat st b₂ is_Shortcut_of b₁ & 1 <= b₃ & b₃ + 1 <= len b₂ holds
ex b₄ being Nat st
( 1 <= b₄ & b₄ + 1 <= len b₁ & b₁ /. b₄ = b₂ /. b₃ & b₁ /. (b₄ + 1) = b₂ /. (b₃ + 1) & b₁ . b₄ = b₂ . b₃ & b₁ . (b₄ + 1) = b₂ . (b₃ + 1) )

proof end;

theorem Th26: :: JGRAPH_1:26

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₂ is_Shortcut_of b₁ holds
rng b₂ c= rng b₁

proof end;

theorem Th27: :: JGRAPH_1:27

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₂ is_Shortcut_of b₁ holds
L~ b₂ c= L~ b₁

proof end;

theorem Th28: :: JGRAPH_1:28

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is special & b₂ is_Shortcut_of b₁ holds
b₂ is special

proof end;

theorem Th29: :: JGRAPH_1:29

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is special & 2 <= len b₁ & b₁ . 1 <> b₁ . (len b₁) holds
ex b₂ being FinSequence of (TOP-REAL 2) st
( 2 <= len b₂ & b₂ is special & b₂ is one-to-one & L~ b₂ c= L~ b₁ & b₁ . 1 = b₂ . 1 & b₁ . (len b₁) = b₂ . (len b₂) & rng b₂ c= rng b₁ )

proof end;

theorem Th30: :: JGRAPH_1:30

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is special & b₂ is special & 2 <= len b₁ & 2 <= len b₂ & b₁ . 1 <> b₁ . (len b₁) & b₂ . 1 <> b₂ . (len b₂) & X_axis b₁ lies_between (X_axis b₁) . 1,(X_axis b₁) . (len b₁) & X_axis b₂ lies_between (X_axis b₁) . 1,(X_axis b₁) . (len b₁) & Y_axis b₁ lies_between (Y_axis b₂) . 1,(Y_axis b₂) . (len b₂) & Y_axis b₂ lies_between (Y_axis b₂) . 1,(Y_axis b₂) . (len b₂) holds
L~ b₁ meets L~ b₂

proof end;

theorem Th31: :: JGRAPH_1:31

for b₁, b₂, b₃, b₄ being Real st b₁ <= b₃ & b₃ <= b₂ & b₁ <= b₄ & b₄ <= b₂ holds
abs (b₃ - b₄) <= b₂ - b₁

proof end;

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
redefine func |.c₂.| -> Element of REAL means :Def5: :: JGRAPH_1:def 5
for b₁ being Element of REAL a₁ st a₂ = b₁ holds
a₃ = |.b₁.|;
compatibility

proof end;

end;

:: deftheorem Def5 defines |. JGRAPH_1:def 5 :

theorem Th32: :: JGRAPH_1:32

canceled;

theorem Th33: :: JGRAPH_1:33

canceled;

theorem Th34: :: JGRAPH_1:34

canceled;

theorem Th35: :: JGRAPH_1:35

canceled;

theorem Th36: :: JGRAPH_1:36

canceled;

theorem Th37: :: JGRAPH_1:37

canceled;

theorem Th38: :: JGRAPH_1:38

canceled;

theorem Th39: :: JGRAPH_1:39

canceled;

theorem Th40: :: JGRAPH_1:40

canceled;

theorem Th41: :: JGRAPH_1:41

canceled;

theorem Th42: :: JGRAPH_1:42

canceled;

theorem Th43: :: JGRAPH_1:43

canceled;

theorem Th44: :: JGRAPH_1:44

canceled;

theorem Th45: :: JGRAPH_1:45

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄, b₅ being Point of (Euclid b₁) st b₄ = b₂ & b₅ = b₃ holds
|.(b₂ - b₃).| = dist b₄,b₅

proof end;

theorem Th46: :: JGRAPH_1:46

for b₁ being Point of (TOP-REAL 2) holds |.b₁.| ^2 = ((b₁ `1 ) ^2 ) + ((b₁ `2 ) ^2 )

proof end;

theorem Th47: :: JGRAPH_1:47

for b₁ being Point of (TOP-REAL 2) holds |.b₁.| = sqrt (((b₁ `1 ) ^2 ) + ((b₁ `2 ) ^2 ))

proof end;

theorem Th48: :: JGRAPH_1:48

for b₁ being Point of (TOP-REAL 2) holds |.b₁.| <= (abs (b₁ `1 )) + (abs (b₁ `2 ))

proof end;

theorem Th49: :: JGRAPH_1:49

for b₁, b₂ being Point of (TOP-REAL 2) holds |.(b₁ - b₂).| <= (abs ((b₁ `1 ) - (b₂ `1 ))) + (abs ((b₁ `2 ) - (b₂ `2 )))

proof end;

theorem Th50: :: JGRAPH_1:50

for b₁ being Point of (TOP-REAL 2) holds
( abs (b₁ `1 ) <= |.b₁.| & abs (b₁ `2 ) <= |.b₁.| )

proof end;

theorem Th51: :: JGRAPH_1:51

for b₁, b₂ being Point of (TOP-REAL 2) holds
( abs ((b₁ `1 ) - (b₂ `1 )) <= |.(b₁ - b₂).| & abs ((b₁ `2 ) - (b₂ `2 )) <= |.(b₁ - b₂).| )

proof end;

theorem Th52: :: JGRAPH_1:52

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in LSeg b₃,b₄ holds
ex b₅ being Real st
( 0 <= b₅ & b₅ <= 1 & b₂ = ((1 - b₅) * b₃) + (b₅ * b₄) )

proof end;

theorem Th53: :: JGRAPH_1:53

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in LSeg b₃,b₄ holds
( |.(b₂ - b₃).| <= |.(b₃ - b₄).| & |.(b₂ - b₄).| <= |.(b₃ - b₄).| )

proof end;

theorem Th54: :: JGRAPH_1:54

for b₁ being non empty MetrSpace
for b₂, b₃ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact & b₃ <> {} & b₃ is compact holds
min_dist_min b₂,b₃ >= 0

proof end;

theorem Th55: :: JGRAPH_1:55

for b₁ being non empty MetrSpace
for b₂, b₃ being Subset of (TopSpaceMetr b₁) st b₂ <> {} & b₂ is compact & b₃ <> {} & b₃ is compact holds
( b₂ misses b₃ iff min_dist_min b₂,b₃ > 0 )

proof end;

theorem Th56: :: JGRAPH_1:56

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃, b₄ being Real st 1 <= len b₁ & X_axis b₁ lies_between (X_axis b₁) . 1,(X_axis b₁) . (len b₁) & Y_axis b₁ lies_between b₃,b₄ & b₂ > 0 & ( for b₅ being Nat st 1 <= b₅ & b₅ + 1 <= len b₁ holds
|.((b₁ /. b₅) - (b₁ /. (b₅ + 1))).| < b₂ ) holds
ex b₅ being FinSequence of (TOP-REAL 2) st
( b₅ is special & b₅ . 1 = b₁ . 1 & b₅ . (len b₅) = b₁ . (len b₁) & len b₅ >= len b₁ & X_axis b₅ lies_between (X_axis b₁) . 1,(X_axis b₁) . (len b₁) & Y_axis b₅ lies_between b₃,b₄ & ( for b₆ being Nat st b₆ in dom b₅ holds
ex b₇ being Nat st
( b₇ in dom b₁ & |.((b₅ /. b₆) - (b₁ /. b₇)).| < b₂ ) ) & ( for b₆ being Nat st 1 <= b₆ & b₆ + 1 <= len b₅ holds
|.((b₅ /. b₆) - (b₅ /. (b₆ + 1))).| < b₂ ) )

proof end;

theorem Th57: :: JGRAPH_1:57

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃, b₄ being Real st 1 <= len b₁ & Y_axis b₁ lies_between (Y_axis b₁) . 1,(Y_axis b₁) . (len b₁) & X_axis b₁ lies_between b₃,b₄ & b₂ > 0 & ( for b₅ being Nat st 1 <= b₅ & b₅ + 1 <= len b₁ holds
|.((b₁ /. b₅) - (b₁ /. (b₅ + 1))).| < b₂ ) holds
ex b₅ being FinSequence of (TOP-REAL 2) st
( b₅ is special & b₅ . 1 = b₁ . 1 & b₅ . (len b₅) = b₁ . (len b₁) & len b₅ >= len b₁ & Y_axis b₅ lies_between (Y_axis b₁) . 1,(Y_axis b₁) . (len b₁) & X_axis b₅ lies_between b₃,b₄ & ( for b₆ being Nat st b₆ in dom b₅ holds
ex b₇ being Nat st
( b₇ in dom b₁ & |.((b₅ /. b₆) - (b₁ /. b₇)).| < b₂ ) ) & ( for b₆ being Nat st 1 <= b₆ & b₆ + 1 <= len b₅ holds
|.((b₅ /. b₆) - (b₅ /. (b₆ + 1))).| < b₂ ) )

proof end;

theorem Th58: :: JGRAPH_1:58

canceled;

theorem Th59: :: JGRAPH_1:59

for b₁ being FinSequence of (TOP-REAL 2) st 1 <= len b₁ holds
( len (X_axis b₁) = len b₁ & (X_axis b₁) . 1 = (b₁ /. 1) `1 & (X_axis b₁) . (len b₁) = (b₁ /. (len b₁)) `1 )

proof end;

theorem Th60: :: JGRAPH_1:60

for b₁ being FinSequence of (TOP-REAL 2) st 1 <= len b₁ holds
( len (Y_axis b₁) = len b₁ & (Y_axis b₁) . 1 = (b₁ /. 1) `2 & (Y_axis b₁) . (len b₁) = (b₁ /. (len b₁)) `2 )

proof end;

theorem Th61: :: JGRAPH_1:61

for b₁ being Nat
for b₂ being FinSequence of (TOP-REAL 2) st b₁ in dom b₂ holds
( (X_axis b₂) . b₁ = (b₂ /. b₁) `1 & (Y_axis b₂) . b₁ = (b₂ /. b₁) `2 )

proof end;

theorem Th62: :: JGRAPH_1:62

for b₁, b₂ being non empty Subset of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₃,b₄ & b₂ is_an_arc_of b₅,b₆ & ( for b₇ being Point of (TOP-REAL 2) st b₇ in b₁ holds
( b₃ `1 <= b₇ `1 & b₇ `1 <= b₄ `1 ) ) & ( for b₇ being Point of (TOP-REAL 2) st b₇ in b₂ holds
( b₃ `1 <= b₇ `1 & b₇ `1 <= b₄ `1 ) ) & ( for b₇ being Point of (TOP-REAL 2) st b₇ in b₁ holds
( b₅ `2 <= b₇ `2 & b₇ `2 <= b₆ `2 ) ) & ( for b₇ being Point of (TOP-REAL 2) st b₇ in b₂ holds
( b₅ `2 <= b₇ `2 & b₇ `2 <= b₆ `2 ) ) holds
b₁ meets b₂

proof end;

theorem Th63: :: JGRAPH_1:63

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being non empty Subset of b₂
for b₅ being Function of b₁,(b₂ | b₄) st b₃ = b₅ & b₃ is continuous holds
b₅ is continuous

proof end;

theorem Th64: :: JGRAPH_1:64

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being non empty Subset of b₂ st b₁ is compact & b₂ is_T2 & b₃ is continuous & b₃ is one-to-one & b₄ = rng b₃ holds
ex b₅ being Function of b₁,(b₂ | b₄) st
( b₃ = b₅ & b₅ is_homeomorphism )

proof end;

theorem Th65: :: JGRAPH_1:65

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number
for b₇, b₈ being Point of I[01] st b₇ = 0 & b₈ = 1 & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & (b₁ . b₇) `1 = b₃ & (b₁ . b₈) `1 = b₄ & (b₂ . b₇) `2 = b₅ & (b₂ . b₈) `2 = b₆ & ( for b₉ being Point of I[01] holds
( b₃ <= (b₁ . b₉) `1 & (b₁ . b₉) `1 <= b₄ & b₃ <= (b₂ . b₉) `1 & (b₂ . b₉) `1 <= b₄ & b₅ <= (b₁ . b₉) `2 & (b₁ . b₉) `2 <= b₆ & b₅ <= (b₂ . b₉) `2 & (b₂ . b₉) `2 <= b₆ ) ) holds
rng b₁ meets rng b₂

proof end;