:: On Some Points of a Simple Closed Curve
:: by Artur Korni{\l}owicz
::
:: Received October 6, 2004
:: Copyright (c) 2004 Association of Mizar Users
Lm1:
dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm2:
for r being real number
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
Lm4:
for A, B, C, D being set st A misses D & B misses D & C misses D holds
(A \/ B) \/ C misses D
theorem :: JORDAN21:1
theorem Th2: :: JORDAN21:2
theorem Th3: :: JORDAN21:3
theorem Th4: :: JORDAN21:4
theorem Th5: :: JORDAN21:5
theorem :: JORDAN21:6
theorem :: JORDAN21:7
theorem :: JORDAN21:8
theorem :: JORDAN21:9
theorem :: JORDAN21:10
theorem Th11: :: JORDAN21:11
for
P being
Subset of the
carrier of
(TOP-REAL 2) for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
P is_an_arc_of p1,
p2 &
p1 <> q1 &
p2 <> q2 holds
( not
p1 in Segment P,
p1,
p2,
q1,
q2 & not
p2 in Segment P,
p1,
p2,
q1,
q2 )
:: deftheorem Def1 defines with_the_max_arc JORDAN21:def 1 :
theorem Th12: :: JORDAN21:12
theorem Th13: :: JORDAN21:13
theorem :: JORDAN21:14
canceled;
theorem :: JORDAN21:15
canceled;
theorem :: JORDAN21:16
canceled;
theorem :: JORDAN21:17
canceled;
theorem :: JORDAN21:18
canceled;
theorem :: JORDAN21:19
canceled;
theorem :: JORDAN21:20
canceled;
theorem :: JORDAN21:21
canceled;
theorem :: JORDAN21:22
canceled;
theorem Th23: :: JORDAN21:23
theorem Th24: :: JORDAN21:24
theorem :: JORDAN21:25
theorem Th26: :: JORDAN21:26
theorem Th27: :: JORDAN21:27
theorem Th28: :: JORDAN21:28
theorem Th29: :: JORDAN21:29
theorem Th30: :: JORDAN21:30
theorem Th31: :: JORDAN21:31
theorem :: JORDAN21:32
:: deftheorem defines UMP JORDAN21:def 2 :
:: deftheorem defines LMP JORDAN21:def 3 :
theorem :: JORDAN21:33
canceled;
theorem :: JORDAN21:34
canceled;
theorem :: JORDAN21:35
canceled;
theorem :: JORDAN21:36
canceled;
theorem Th37: :: JORDAN21:37
theorem Th38: :: JORDAN21:38
theorem Th39: :: JORDAN21:39
theorem Th40: :: JORDAN21:40
theorem :: JORDAN21:41
theorem :: JORDAN21:42
theorem Th43: :: JORDAN21:43
theorem Th44: :: JORDAN21:44
theorem Th45: :: JORDAN21:45
theorem Th46: :: JORDAN21:46
theorem Th47: :: JORDAN21:47
theorem Th48: :: JORDAN21:48
theorem Th49: :: JORDAN21:49
theorem Th50: :: JORDAN21:50
theorem Th51: :: JORDAN21:51
theorem Th52: :: JORDAN21:52
theorem Th53: :: JORDAN21:53
theorem Th54: :: JORDAN21:54
theorem Th55: :: JORDAN21:55
theorem :: JORDAN21:56
theorem :: JORDAN21:57
theorem :: JORDAN21:58
theorem :: JORDAN21:59
theorem :: JORDAN21:60
theorem :: JORDAN21:61
theorem :: JORDAN21:62
theorem :: JORDAN21:63