:: Helly property for subtrees
:: by Jessica Enright and Piotr Rudnicki
::
:: Received January 10, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem :: HELLY:1
:: deftheorem Def1 defines maxPrefix HELLY:def 1 :
theorem :: HELLY:2
theorem Th3: :: HELLY:3
theorem Th4: :: HELLY:4
theorem Th5: :: HELLY:5
theorem Th6: :: HELLY:6
theorem Th7: :: HELLY:7
theorem Th8: :: HELLY:8
theorem Th9: :: HELLY:9
theorem Th10: :: HELLY:10
theorem :: HELLY:11
theorem Th12: :: HELLY:12
theorem Th13: :: HELLY:13
theorem :: HELLY:14
theorem Th15: :: HELLY:15
theorem Th15a: :: HELLY:16
theorem Th16: :: HELLY:17
theorem Th17: :: HELLY:18
theorem Th18: :: HELLY:19
theorem Th19: :: HELLY:20
theorem :: HELLY:21
theorem Th21: :: HELLY:22
theorem Th22: :: HELLY:23
theorem Th23: :: HELLY:24
theorem Th24: :: HELLY:25
theorem Th25: :: HELLY:26
theorem Th26: :: HELLY:27
:: deftheorem Def2 defines .pathBetween HELLY:def 2 :
theorem Th27: :: HELLY:28
theorem Th28: :: HELLY:29
theorem Th29: :: HELLY:30
theorem Th30: :: HELLY:31
theorem Th31: :: HELLY:32
theorem Th32: :: HELLY:33
theorem Th33: :: HELLY:34
theorem Th34: :: HELLY:35
theorem Th35: :: HELLY:36
theorem Th36: :: HELLY:37
theorem Th37: :: HELLY:38
theorem Th38: :: HELLY:39
theorem Th39: :: HELLY:40
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}
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)))}
definition
let T be
_Tree;
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
ex b1 being Vertex of T st (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {b1}
uniqueness
for b1, b2 being Vertex of T st (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {b1} & (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {b2} holds
b1 = b2
by ZFMISC_1:6;
end;
:: deftheorem Def3 defines MiddleVertex HELLY:def 3 :
theorem Th40: :: HELLY:41
theorem Th41: :: HELLY:42
theorem :: HELLY:43
theorem Th43: :: HELLY:44
theorem :: HELLY:45
theorem Th45: :: HELLY:46
theorem :: HELLY:47
theorem Th47: :: HELLY:48
theorem Th48: :: HELLY:49
theorem :: HELLY:50
theorem Th50: :: HELLY:51
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))
theorem Th52: :: HELLY:53
:: deftheorem defines with_Helly_property HELLY:def 4 :
theorem :: HELLY:54