:: On the Decomposition of a Simple Closed Curve into Two Arcs
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received September 16, 2002
:: Copyright (c) 2002-2011 Association of Mizar Users


begin

registration
let n be Element of NAT ;
cluster trivial Element of K6( the carrier of (TOP-REAL n));
existence
ex b1 being Subset of (TOP-REAL n) st b1 is trivial
proof end;
end;

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
proof end;

theorem :: JORDAN16:3
canceled;

theorem :: JORDAN16:4
for C being Simple_closed_curve holds Lower_Arc C <> Upper_Arc C
proof end;

theorem Th5: :: JORDAN16:5
for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (A,p1,p2,q1,q2) c= A
proof end;

theorem :: JORDAN16:6
canceled;

theorem Th7: :: JORDAN16:7
for A being Subset of (TOP-REAL 2)
for q, p1, p2 being Point of (TOP-REAL 2) st q in A holds
q in L_Segment (A,p1,p2,q)
proof end;

theorem Th8: :: JORDAN16:8
for A being Subset of (TOP-REAL 2)
for q, p1, p2 being Point of (TOP-REAL 2) st q in A holds
q in R_Segment (A,p1,p2,q)
proof end;

theorem Th9: :: JORDAN16:9
for A being Subset of (TOP-REAL 2)
for q1, q2, p1, p2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds
( q1 in Segment (A,p1,p2,q1,q2) & q2 in Segment (A,p1,p2,q1,q2) )
proof end;

theorem :: JORDAN16:10
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) holds Segment (p,q,C) c= C
proof end;

theorem :: JORDAN16:11
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds
LE q,p,C
proof end;

theorem Th12: :: JORDAN16:12
for X, Y being non empty TopSpace
for Y0 being non empty SubSpace of Y
for f being Function of X,Y
for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
proof end;

theorem Th13: :: JORDAN16:13
for S, T being non empty TopSpace
for S0 being non empty SubSpace of S
for T0 being non empty SubSpace of T
for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
proof end;

theorem Th14: :: JORDAN16:14
for P1, P2, P3 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 holds
P1 = P3
proof end;

theorem Th15: :: JORDAN16:15
for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds
( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )
proof end;

theorem Th16: :: JORDAN16:16
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds
A1 <> A2
proof end;

theorem :: JORDAN16:17
for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds
A1 \/ A2 = C
proof end;

theorem :: JORDAN16:18
for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds
for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2
proof end;

theorem Th19: :: JORDAN16:19
for C being Simple_closed_curve
for A being non empty Subset of (TOP-REAL 2) st A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C holds
A = Upper_Arc C
proof end;

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 )
proof end;

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 )
proof end;

theorem :: JORDAN16:22
for A being Subset of (TOP-REAL 2)
for q1, q2, p1, p2 being Point of (TOP-REAL 2) st LE q1,q2,A,p1,p2 holds
not Segment (A,p1,p2,q1,q2) is empty
proof end;

theorem :: JORDAN16:23
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in C holds
( p in Segment (p,(W-min C),C) & W-min C in Segment (p,(W-min C),C) )
proof end;

definition
canceled;
canceled;
let a, b be real number ;
func AffineMap (a,b) -> Function of REAL,REAL means :Def3: :: JORDAN16:def 3
for x being real number holds it . x = (a * x) + b;
existence
ex b1 being Function of REAL,REAL st
for x being real number holds b1 . x = (a * x) + b
proof end;
uniqueness
for b1, b2 being Function of REAL,REAL st ( for x being real number holds b1 . x = (a * x) + b ) & ( for x being real number holds b2 . x = (a * x) + b ) holds
b1 = b2
proof end;
end;

:: deftheorem JORDAN16:def 1 :
canceled;

:: deftheorem JORDAN16:def 2 :
canceled;

:: deftheorem Def3 defines AffineMap JORDAN16:def 3 :
for a, b being real number
for b3 being Function of REAL,REAL holds
( b3 = AffineMap (a,b) iff for x being real number holds b3 . x = (a * x) + b );

registration
let a, b be real number ;
cluster AffineMap (a,b) -> continuous ;
coherence
AffineMap (a,b) is continuous
proof end;
end;

registration
cluster non empty Relation-like REAL -defined REAL -valued Function-like continuous total quasi_total V149() V150() V151() Element of K6(K7(REAL,REAL));
existence
ex b1 being Function of REAL,REAL st b1 is continuous
proof end;
end;

theorem :: JORDAN16:24
for f, g being continuous PartFunc of REAL,REAL holds g * f is continuous PartFunc of REAL,REAL ;

theorem Th25: :: JORDAN16:25
for a, b being real number holds (AffineMap (a,b)) . 0 = b
proof end;

theorem Th26: :: JORDAN16:26
for a, b being real number holds (AffineMap (a,b)) . 1 = a + b
proof end;

theorem Th27: :: JORDAN16:27
for a, b being real number st a <> 0 holds
AffineMap (a,b) is one-to-one
proof end;

theorem :: JORDAN16:28
for a, b, x, y being real number st a > 0 & x < y holds
(AffineMap (a,b)) . x < (AffineMap (a,b)) . y
proof end;

theorem :: JORDAN16:29
for a, b, x, y being real number st a < 0 & x < y holds
(AffineMap (a,b)) . x > (AffineMap (a,b)) . y
proof end;

theorem Th30: :: JORDAN16:30
for a, b, x, y being real number st a >= 0 & x <= y holds
(AffineMap (a,b)) . x <= (AffineMap (a,b)) . y
proof end;

theorem :: JORDAN16:31
for a, b, x, y being real number st a <= 0 & x <= y holds
(AffineMap (a,b)) . x >= (AffineMap (a,b)) . y
proof end;

theorem Th32: :: JORDAN16:32
for a, b being real number st a <> 0 holds
rng (AffineMap (a,b)) = REAL
proof end;

theorem Th33: :: JORDAN16:33
for a, b being real number st a <> 0 holds
(AffineMap (a,b)) " = AffineMap ((a "),(- (b / a)))
proof end;

theorem Th34: :: JORDAN16:34
for a, b being real number st a > 0 holds
(AffineMap (a,b)) .: [.0,1.] = [.b,(a + b).]
proof end;

theorem Th35: :: JORDAN16:35
for f being Function of R^1,R^1
for a, b being Real st a <> 0 & f = AffineMap (a,b) holds
f is being_homeomorphism
proof end;

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
proof end;

theorem :: JORDAN16:37
for C being Simple_closed_curve
for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P
proof end;

theorem :: JORDAN16:38
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds
ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {p1,p2} )
proof end;

theorem :: JORDAN16:39
for P being non empty Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & p1 <> q1 holds
Segment (P,p1,p2,p1,q1) is_an_arc_of p1,q1
proof end;