:: Connectedness Conditions Using Polygonal Arcs
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: deftheorem Def1 defines is_S-P_arc_joining TOPREAL4:def 1 :
:: deftheorem defines being_special_polygon TOPREAL4:def 2 :
:: deftheorem Def3 defines being_Region TOPREAL4:def 3 :
theorem :: TOPREAL4:1
canceled;
theorem Th2: :: TOPREAL4:2
theorem Th3: :: TOPREAL4:3
theorem Th4: :: TOPREAL4:4
theorem :: TOPREAL4:5
theorem :: TOPREAL4:6
theorem Th7: :: TOPREAL4:7
theorem Th8: :: TOPREAL4:8
theorem Th9: :: TOPREAL4:9
for
p,
q being
Point of
(TOP-REAL 2) for
f being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
p `1 <> q `1 &
p `2 <> q `2 &
p in Ball u,
r &
q in Ball u,
r &
|[(p `1 ),(q `2 )]| in Ball u,
r &
f = <*p,|[(p `1 ),(q `2 )]|,q*> holds
(
f is
being_S-Seq &
f /. 1
= p &
f /. (len f) = q &
L~ f is_S-P_arc_joining p,
q &
L~ f c= Ball u,
r )
theorem Th10: :: TOPREAL4:10
for
p,
q being
Point of
(TOP-REAL 2) for
f being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st
p `1 <> q `1 &
p `2 <> q `2 &
p in Ball u,
r &
q in Ball u,
r &
|[(q `1 ),(p `2 )]| in Ball u,
r &
f = <*p,|[(q `1 ),(p `2 )]|,q*> holds
(
f is
being_S-Seq &
f /. 1
= p &
f /. (len f) = q &
L~ f is_S-P_arc_joining p,
q &
L~ f c= Ball u,
r )
theorem Th11: :: TOPREAL4:11
theorem Th12: :: TOPREAL4:12
theorem Th13: :: TOPREAL4:13
theorem Th14: :: TOPREAL4:14
theorem Th15: :: TOPREAL4:15
theorem Th16: :: TOPREAL4:16
theorem Th17: :: TOPREAL4:17
theorem Th18: :: TOPREAL4:18
theorem Th19: :: TOPREAL4:19
theorem Th20: :: TOPREAL4:20
theorem Th21: :: TOPREAL4:21
for
p being
Point of
(TOP-REAL 2) for
f,
h being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st not
f /. 1
in Ball u,
r &
f /. (len f) in Ball u,
r &
p in Ball u,
r &
|[(p `1 ),((f /. (len f)) `2 )]| in Ball u,
r &
f is
being_S-Seq &
p `1 <> (f /. (len f)) `1 &
p `2 <> (f /. (len f)) `2 &
h = f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|,p*> &
((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p)) /\ (L~ f) = {(f /. (len f))} holds
(
L~ h is_S-P_arc_joining f /. 1,
p &
L~ h c= (L~ f) \/ (Ball u,r) )
theorem Th22: :: TOPREAL4:22
for
p being
Point of
(TOP-REAL 2) for
f,
h being
FinSequence of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st not
f /. 1
in Ball u,
r &
f /. (len f) in Ball u,
r &
p in Ball u,
r &
|[((f /. (len f)) `1 ),(p `2 )]| in Ball u,
r &
f is
being_S-Seq &
p `1 <> (f /. (len f)) `1 &
p `2 <> (f /. (len f)) `2 &
h = f ^ <*|[((f /. (len f)) `1 ),(p `2 )]|,p*> &
((LSeg (f /. (len f)),|[((f /. (len f)) `1 ),(p `2 )]|) \/ (LSeg |[((f /. (len f)) `1 ),(p `2 )]|,p)) /\ (L~ f) = {(f /. (len f))} holds
(
L~ h is_S-P_arc_joining f /. 1,
p &
L~ h c= (L~ f) \/ (Ball u,r) )
theorem Th23: :: TOPREAL4:23
theorem Th24: :: TOPREAL4:24
Lm1:
TopSpaceMetr (Euclid 2) = TOP-REAL 2
by EUCLID:def 8;
theorem Th25: :: TOPREAL4:25
theorem Th26: :: TOPREAL4:26
theorem Th27: :: TOPREAL4:27
theorem Th28: :: TOPREAL4:28
theorem :: TOPREAL4:29
theorem :: TOPREAL4:30