:: by Jessica Enright and Piotr Rudnicki

::

:: Received January 10, 2008

:: Copyright (c) 2008-2018 Association of Mizar Users

definition

let p, q be FinSequence;

ex b_{1} being FinSequence st

( b_{1} is_a_prefix_of p & b_{1} is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of b_{1} ) )

for b_{1}, b_{2} being FinSequence st b_{1} is_a_prefix_of p & b_{1} is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of b_{1} ) & b_{2} is_a_prefix_of p & b_{2} is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of b_{2} ) holds

b_{1} = b_{2}
;

commutativity

for b_{1}, p, q being FinSequence st b_{1} is_a_prefix_of p & b_{1} is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of b_{1} ) holds

( b_{1} is_a_prefix_of q & b_{1} is_a_prefix_of p & ( for r being FinSequence st r is_a_prefix_of q & r is_a_prefix_of p holds

r is_a_prefix_of b_{1} ) )
;

end;
func maxPrefix (p,q) -> FinSequence means :Def1: :: HELLY:def 1

( it is_a_prefix_of p & it is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of it ) );

existence ( it is_a_prefix_of p & it is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of it ) );

ex b

( b

r is_a_prefix_of b

proof end;

uniqueness for b

r is_a_prefix_of b

r is_a_prefix_of b

b

commutativity

for b

r is_a_prefix_of b

( b

r is_a_prefix_of b

:: deftheorem Def1 defines maxPrefix HELLY:def 1 :

for p, q, b_{3} being FinSequence holds

( b_{3} = maxPrefix (p,q) iff ( b_{3} is_a_prefix_of p & b_{3} is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of b_{3} ) ) );

for p, q, b

( b

r is_a_prefix_of b

theorem :: HELLY:2

theorem Th6: :: HELLY:6

for p, q being FinSequence

for j being Nat st j <= len (maxPrefix (p,q)) holds

(maxPrefix (p,q)) . j = p . j

for j being Nat st j <= len (maxPrefix (p,q)) holds

(maxPrefix (p,q)) . j = p . j

proof end;

theorem Th9: :: HELLY:9

for p, q being FinSequence st not p is_a_prefix_of q & not q is_a_prefix_of p holds

p . ((len (maxPrefix (p,q))) + 1) <> q . ((len (maxPrefix (p,q))) + 1)

p . ((len (maxPrefix (p,q))) + 1) <> q . ((len (maxPrefix (p,q))) + 1)

proof end;

theorem :: HELLY:11

for G being _Graph

for W being Walk of G

for m, n being Nat st not W .cut (m,n) is trivial holds

not W is trivial

for W being Walk of G

for m, n being Nat st not W .cut (m,n) is trivial holds

not W is trivial

proof end;

theorem Th12: :: HELLY:12

for G being _Graph

for W being Walk of G

for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds

ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

for W being Walk of G

for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds

ex j being odd Nat st

( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )

proof end;

registration

let G be _Graph;

correctness

coherence

for b_{1} being Walk of G holds not b_{1} is empty ;

by CARD_1:27;

end;
correctness

coherence

for b

by CARD_1:27;

theorem Th13: :: HELLY:13

for G being _Graph

for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds

W1 .vertices() c= W2 .vertices()

for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds

W1 .vertices() c= W2 .vertices()

proof end;

theorem :: HELLY:14

for G being _Graph

for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds

W1 .edges() c= W2 .edges()

for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds

W1 .edges() c= W2 .edges()

proof end;

theorem Th16: :: HELLY:16

for G being _Graph

for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds

W1 .append W2 = W2

for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds

W1 .append W2 = W2

proof end;

theorem Th17: :: HELLY:17

for G being _Graph

for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds

W1 .append W2 is Trail-like

for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds

W1 .append W2 is Trail-like

proof end;

theorem Th18: :: HELLY:18

for G being _Graph

for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} holds

P1 .append P2 is Path-like

for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} holds

P1 .append P2 is Path-like

proof end;

theorem Th19: :: HELLY:19

for G being _Graph

for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds

( P1 .append P2 is open & P1 .append P2 is Path-like )

for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds

( P1 .append P2 is open & P1 .append P2 is Path-like )

proof end;

theorem Th20: :: HELLY:20

for G being _Graph

for P1, P2 being Path of G st P1 .last() = P2 .first() & P2 .last() = P1 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} holds

P1 .append P2 is Cycle-like

for P1, P2 being Path of G st P1 .last() = P2 .first() & P2 .last() = P1 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} holds

P1 .append P2 is Cycle-like

proof end;

theorem :: HELLY:21

for G being simple _Graph

for W1, W2 being Walk of G

for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) holds

for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

for W1, W2 being Walk of G

for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds

W1 . j = W2 . j ) holds

for j being Nat st 1 <= j & j <= k holds

W1 . j = W2 . j

proof end;

theorem Th22: :: HELLY:22

for G being _Graph

for W1, W2 being Walk of G st W1 .first() = W2 .first() holds

len (maxPrefix (W1,W2)) is odd

for W1, W2 being Walk of G st W1 .first() = W2 .first() holds

len (maxPrefix (W1,W2)) is odd

proof end;

theorem Th23: :: HELLY:23

for G being _Graph

for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 holds

(len (maxPrefix (W1,W2))) + 2 <= len W1

for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 holds

(len (maxPrefix (W1,W2))) + 2 <= len W1

proof end;

theorem Th24: :: HELLY:24

for G being non-multi _Graph

for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 holds

W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2)

for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 holds

W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2)

proof end;

definition
end;

registration

let T be _Tree;

correctness

coherence

for b_{1} being Walk of T st b_{1} is Trail-like holds

b_{1} is Path-like ;

end;
correctness

coherence

for b

b

proof end;

theorem Th25: :: HELLY:25

for T being _Tree

for P being Path of T st not P is trivial holds

P is open by GLIB_001:def 31, GLIB_002:def 2;

for P being Path of T st not P is trivial holds

P is open by GLIB_001:def 31, GLIB_002:def 2;

registration

let T be _Tree;

correctness

coherence

for b_{1} being Path of T st not b_{1} is trivial holds

b_{1} is open ;

by Th25;

end;
correctness

coherence

for b

b

by Th25;

theorem Th26: :: HELLY:26

for T being _Tree

for P being Path of T

for i, j being odd Nat st i < j & j <= len P holds

P . i <> P . j

for P being Path of T

for i, j being odd Nat st i < j & j <= len P holds

P . i <> P . j

proof end;

theorem Th27: :: HELLY:27

for T being _Tree

for a, b being Vertex of T

for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds

P1 = P2

for a, b being Vertex of T

for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds

P1 = P2

proof end;

definition

let T be _Tree;

let a, b be Vertex of T;

existence

ex b_{1} being Path of T st b_{1} is_Walk_from a,b

for b_{1}, b_{2} being Path of T st b_{1} is_Walk_from a,b & b_{2} is_Walk_from a,b holds

b_{1} = b_{2}
by Th27;

end;
let a, b be Vertex of T;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines .pathBetween HELLY:def 2 :

for T being _Tree

for a, b being Vertex of T

for b_{4} being Path of T holds

( b_{4} = T .pathBetween (a,b) iff b_{4} is_Walk_from a,b );

for T being _Tree

for a, b being Vertex of T

for b

( b

theorem Th28: :: HELLY:28

for T being _Tree

for a, b being Vertex of T holds

( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )

for a, b being Vertex of T holds

( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )

proof end;

:: more theorems about pathBetween ?

theorem Th29: :: HELLY:29

for T being _Tree

for a, b being Vertex of T holds

( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() )

for a, b being Vertex of T holds

( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() )

proof end;

registration

let T be _Tree;

let a be Vertex of T;

correctness

coherence

T .pathBetween (a,a) is closed ;

by Def2, GLIB_001:119;

end;
let a be Vertex of T;

correctness

coherence

T .pathBetween (a,a) is closed ;

by Def2, GLIB_001:119;

registration
end;

theorem Th31: :: HELLY:31

for T being _Tree

for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a)

for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a)

proof end;

theorem Th32: :: HELLY:32

for T being _Tree

for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()

for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()

proof end;

theorem Th33: :: HELLY:33

for T being _Tree

for a, b being Vertex of T

for t being _Subtree of T

for a9, b9 being Vertex of t st a = a9 & b = b9 holds

T .pathBetween (a,b) = t .pathBetween (a9,b9)

for a, b being Vertex of T

for t being _Subtree of T

for a9, b9 being Vertex of t st a = a9 & b = b9 holds

T .pathBetween (a,b) = t .pathBetween (a9,b9)

proof end;

theorem Th34: :: HELLY:34

for T being _Tree

for a, b being Vertex of T

for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds

(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

for a, b being Vertex of T

for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds

(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t

proof end;

theorem Th35: :: HELLY:35

for T being _Tree

for P being Path of T

for a, b being Vertex of T

for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

for P being Path of T

for a, b being Vertex of T

for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds

T .pathBetween (a,b) = P .cut (i,j)

proof end;

theorem Th36: :: HELLY:36

for T being _Tree

for a, b, c being Vertex of T holds

( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )

for a, b, c being Vertex of T holds

( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )

proof end;

theorem Th37: :: HELLY:37

for T being _Tree

for a, b, c being Vertex of T holds

( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) )

for a, b, c being Vertex of T holds

( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) )

proof end;

theorem Th38: :: HELLY:38

for T being _Tree

for P1, P2 being Path of T st P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds

P1 .append P2 is Path-like

for P1, P2 being Path of T st P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds

P1 .append P2 is Path-like

proof end;

theorem Th39: :: HELLY:39

for T being _Tree

for a, b, c being Vertex of T holds

( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} )

for a, b, c being Vertex of T holds

( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} )

proof end;

theorem Th40: :: HELLY:40

for T being _Tree

for a, b, c, d being Vertex of T

for P1, P2 being Path of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix (P1,P2))) holds

((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d}

for a, b, c, d being Vertex of T

for P1, P2 being Path of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix (P1,P2))) holds

((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d}

proof end;

Lm1: for T being _Tree

for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds

(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c}

proof end;

Lm2: for T being _Tree

for a, b, c being Vertex of T

for P1, P4 being Path of T st P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 holds

((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))}

proof end;

definition

let T be _Tree;

let a, b, c be Vertex of T;

ex b_{1} being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b_{1}}

for b_{1}, b_{2} being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b_{1}} & (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b_{2}} holds

b_{1} = b_{2}
by ZFMISC_1:3;

end;
let a, b, c be Vertex of T;

func MiddleVertex (a,b,c) -> Vertex of T means :Def3: :: HELLY:def 3

(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {it};

existence (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {it};

ex b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines MiddleVertex HELLY:def 3 :

for T being _Tree

for a, b, c, b_{5} being Vertex of T holds

( b_{5} = MiddleVertex (a,b,c) iff (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b_{5}} );

for T being _Tree

for a, b, c, b

( b

theorem Th46: :: HELLY:46

for T being _Tree

for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds

MiddleVertex (a,b,c) = c

for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds

MiddleVertex (a,b,c) = c

proof end;

theorem Th51: :: HELLY:51

for T being _Tree

for P1, P2 being Path of T

for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds

MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))

for P1, P2 being Path of T

for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds

MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))

proof end;

theorem :: HELLY:52

for T being _Tree

for P1, P2, P3, P4 being Path of T

for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & P3 = T .pathBetween (b,a) & P4 = T .pathBetween (b,c) & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds

P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4)))

for P1, P2, P3, P4 being Path of T

for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & P3 = T .pathBetween (b,a) & P4 = T .pathBetween (b,c) & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds

P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4)))

proof end;

theorem Th53: :: HELLY:53

for T being _Tree

for a, b, c being Vertex of T

for S being non empty set st ( for s being set st s in S holds

( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) holds

meet S <> {}

for a, b, c being Vertex of T

for S being non empty set st ( for s being set st s in S holds

( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) holds

meet S <> {}

proof end;

:: deftheorem defines with_Helly_property HELLY:def 4 :

for F being set holds

( F is with_Helly_property iff for H being non empty set st H c= F & ( for x, y being set st x in H & y in H holds

x meets y ) holds

meet H <> {} );

for F being set holds

( F is with_Helly_property iff for H being non empty set st H c= F & ( for x, y being set st x in H & y in H holds

x meets y ) holds

meet H <> {} );

:: At some point one would like to define allSubtrees of a Tree

:: The claim below does not hold when T is infinite and we consider

:: infinite families of subtrees. Example: half-line tree with

:: subtrees T_i = {j >= i}.

:: main Prop4p7:

:: The claim below does not hold when T is infinite and we consider

:: infinite families of subtrees. Example: half-line tree with

:: subtrees T_i = {j >= i}.

:: main Prop4p7:

theorem :: HELLY:54

for T being _Tree

for X being finite set st ( for x being set st x in X holds

ex t being _Subtree of T st x = the_Vertices_of t ) holds

X is with_Helly_property

for X being finite set st ( for x being set st x in X holds

ex t being _Subtree of T st x = the_Vertices_of t ) holds

X is with_Helly_property

proof end;