:: On the Decomposition of a Simple Closed Curve into Two Arcs
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received September 16, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem :: JORDAN16:1
canceled;
theorem :: JORDAN16:2
for
a,
b,
c,
X being
set st
a in X &
b in X &
c in X holds
{a,b,c} c= X
theorem :: JORDAN16:3
canceled;
theorem :: JORDAN16:4
theorem Th5: :: JORDAN16:5
theorem :: JORDAN16:6
canceled;
theorem Th7: :: JORDAN16:7
theorem Th8: :: JORDAN16:8
theorem Th9: :: JORDAN16:9
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 holds
(
q1 in Segment A,
p1,
p2,
q1,
q2 &
q2 in Segment A,
p1,
p2,
q1,
q2 )
theorem :: JORDAN16:10
theorem :: JORDAN16:11
theorem Th12: :: JORDAN16:12
theorem Th13: :: JORDAN16:13
theorem Th14: :: JORDAN16:14
theorem Th15: :: JORDAN16:15
theorem Th16: :: JORDAN16:16
theorem :: JORDAN16:17
theorem :: JORDAN16:18
theorem Th19: :: JORDAN16:19
theorem Th20: :: JORDAN16:20
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 holds
ex
g being
Function of
I[01] ,
((TOP-REAL 2) | A) ex
s1,
s2 being
Real st
(
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 &
0 <= s1 &
s1 <= s2 &
s2 <= 1 )
theorem Th21: :: JORDAN16:21
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 &
q1 <> q2 holds
ex
g being
Function of
I[01] ,
((TOP-REAL 2) | A) ex
s1,
s2 being
Real st
(
g is
being_homeomorphism &
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 &
g . s2 = q2 &
0 <= s1 &
s1 < s2 &
s2 <= 1 )
theorem :: JORDAN16:22
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 holds
not
Segment A,
p1,
p2,
q1,
q2 is
empty
theorem :: JORDAN16:23
:: deftheorem JORDAN16:def 1 :
canceled;
:: deftheorem JORDAN16:def 2 :
canceled;
:: deftheorem Def3 defines AffineMap JORDAN16:def 3 :
theorem :: JORDAN16:24
theorem Th25: :: JORDAN16:25
theorem Th26: :: JORDAN16:26
theorem Th27: :: JORDAN16:27
theorem :: JORDAN16:28
theorem :: JORDAN16:29
theorem Th30: :: JORDAN16:30
theorem :: JORDAN16:31
theorem Th32: :: JORDAN16:32
theorem Th33: :: JORDAN16:33
theorem Th34: :: JORDAN16:34
theorem Th35: :: JORDAN16:35
theorem Th36: :: JORDAN16:36
for
A being
Subset of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
A is_an_arc_of p1,
p2 &
LE q1,
q2,
A,
p1,
p2 &
q1 <> q2 holds
Segment A,
p1,
p2,
q1,
q2 is_an_arc_of q1,
q2
theorem :: JORDAN16:37
theorem :: JORDAN16:38
theorem :: JORDAN16:39