:: On the Decompositions of Intervals and Simple Closed Curves
:: by Adam Grabowski
::
:: Received August 7, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

registration
cluster being_simple_closed_curve  ->  non trivial for Element of bool the carrier of (TOP-REAL 2);
coherence
 for b1 being Simple_closed_curve holds not b1 is trivial
proofend;
end;

theorem Th1: :: BORSUK_4:1
for X being non empty set
for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x} by SUBSET_1:47;

theorem Th2: :: BORSUK_4:2
for X being non trivial set
for p being set ex q being Element of X st q <> p
proofend;

theorem Th3: :: BORSUK_4:3
for T being non trivial set
for X being non trivial Subset of T
for p being set ex q being Element of T st
( q in X &amp; q <> p )
proofend;

theorem Th4: :: BORSUK_4:4
for f, g being Function
for a being set st f is one-to-one &amp; g is one-to-one &amp; (dom f) /\ (dom g) = {a} &amp; (rng f) /\ (rng g) = {(f . a)} holds
f +* g is one-to-one
proofend;

theorem Th5: :: BORSUK_4:5
for f, g being Function
for a being set st f is one-to-one &amp; g is one-to-one &amp; (dom f) /\ (dom g) = {a} &amp; (rng f) /\ (rng g) = {(f . a)} &amp; f . a = g . a holds
(f +* g) " = (f ") +* (g ")
proofend;

theorem Th6: :: BORSUK_4:6
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q holds
not A \ {p} is empty
proofend;

theorem :: BORSUK_4:7
for s1, s3, s4, l being real number st s1 <= s3 &amp; s1 < s4 &amp; 0 <= l &amp; l <= 1 holds
s1 <= ((1 - l) * s3) + (l * s4)
proofend;

theorem Th8: :: BORSUK_4:8
for A being Subset of I[01]
for a, b being real number st a < b &amp; A = ].a,b.[ holds
[.a,b.] c= the carrier of I[01]
proofend;

theorem Th9: :: BORSUK_4:9
for A being Subset of I[01]
for a, b being real number st a < b &amp; A = ].a,b.] holds
[.a,b.] c= the carrier of I[01]
proofend;

theorem Th10: :: BORSUK_4:10
for A being Subset of I[01]
for a, b being real number st a < b &amp; A = [.a,b.[ holds
[.a,b.] c= the carrier of I[01]
proofend;

theorem Th11: :: BORSUK_4:11
for a, b being real number st a <> b holds
Cl ].a,b.] = [.a,b.]
proofend;

theorem Th12: :: BORSUK_4:12
for a, b being real number st a <> b holds
Cl [.a,b.[ = [.a,b.]
proofend;

theorem :: BORSUK_4:13
for A being Subset of I[01]
for a, b being real number st a < b &amp; A = ].a,b.[ holds
Cl A = [.a,b.]
proofend;

theorem Th14: :: BORSUK_4:14
for A being Subset of I[01]
for a, b being real number st a < b &amp; A = ].a,b.] holds
Cl A = [.a,b.]
proofend;

theorem Th15: :: BORSUK_4:15
for A being Subset of I[01]
for a, b being real number st a < b &amp; A = [.a,b.[ holds
Cl A = [.a,b.]
proofend;

theorem Th16: :: BORSUK_4:16
for A being Subset of I[01]
for a, b being real number st a <= b &amp; A = [.a,b.] holds
( 0 <= a &amp; b <= 1 )
proofend;

theorem Th17: :: BORSUK_4:17
for A, B being Subset of I[01]
for a, b, c being real number st a < b &amp; b < c &amp; A = [.a,b.[ &amp; B = ].b,c.] holds
A,B are_separated
proofend;

theorem :: BORSUK_4:18
for p1, p2 being Point of I[01] holds [.p1,p2.] is Subset of I[01] by BORSUK_1:40, XXREAL_2:def_12;

theorem Th19: :: BORSUK_4:19
for a, b being Point of I[01] holds ].a,b.[ is Subset of I[01]
proofend;

begin

theorem :: BORSUK_4:20
for p being real number holds {p} is non empty closed_interval Subset of REAL
proofend;

theorem Th21: :: BORSUK_4:21
for A being non empty connected Subset of I[01]
for a, b, c being Point of I[01] st a <= b &amp; b <= c &amp; a in A &amp; c in A holds
b in A
proofend;

theorem Th22: :: BORSUK_4:22
for A being non empty connected Subset of I[01]
for a, b being real number st a in A &amp; b in A holds
[.a,b.] c= A
proofend;

theorem Th23: :: BORSUK_4:23
for a, b being real number
for A being Subset of I[01] st A = [.a,b.] holds
A is closed
proofend;

theorem Th24: :: BORSUK_4:24
for p1, p2 being Point of I[01] st p1 <= p2 holds
[.p1,p2.] is non empty connected compact Subset of I[01]
proofend;

theorem Th25: :: BORSUK_4:25
for X being Subset of I[01]
for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above &amp; X9 is bounded_below )
proofend;

theorem Th26: :: BORSUK_4:26
for X being Subset of I[01]
for X9 being Subset of REAL
for x being real number st x in X9 &amp; X9 = X holds
( lower_bound X9 <= x &amp; x <= upper_bound X9 )
proofend;

Lm1:  I[01] is closed SubSpace of R^1
by TOPMETR:20, TREAL_1:2;

theorem Th27: :: BORSUK_4:27
for A being Subset of REAL
for B being Subset of I[01] st A = B holds
( A is closed iff B is closed )
proofend;

theorem Th28: :: BORSUK_4:28
for C being non empty closed_interval Subset of REAL holds lower_bound C <= upper_bound C
proofend;

theorem Th29: :: BORSUK_4:29
for C being non empty connected compact Subset of I[01]
for C9 being Subset of REAL st C = C9 &amp; [.(lower_bound C9),(upper_bound C9).] c= C9 holds
[.(lower_bound C9),(upper_bound C9).] = C9
proofend;

theorem Th30: :: BORSUK_4:30
for C being non empty connected compact Subset of I[01] holds C is non empty closed_interval Subset of REAL
proofend;

theorem Th31: :: BORSUK_4:31
for C being non empty connected compact Subset of I[01] ex p1, p2 being Point of I[01] st
( p1 <= p2 &amp; C = [.p1,p2.] )
proofend;

begin

definition
func I(01)  ->  strict SubSpace of I[01]  means :Def1: :: BORSUK_4:def 1
 the carrier of it = ].0,1.[;
existence
 ex b1 being strict SubSpace of I[01] st the carrier of b1 = ].0,1.[
proofend;
uniqueness
 for b1, b2 being strict SubSpace of I[01] st the carrier of b1 = ].0,1.[ &amp; the carrier of b2 = ].0,1.[ holds
b1 = b2 by TSEP_1:5;
end;

:: deftheorem Def1 defines I(01) BORSUK_4:def_1_:_
 for b1 being strict SubSpace of I[01] holds
( b1 = I(01) iff the carrier of b1 = ].0,1.[ );

registration
cluster I(01)  ->  non empty strict ;
coherence
 not I(01) is empty
proofend;
end;

theorem :: BORSUK_4:32
for A being Subset of I[01] st A = the carrier of I(01) holds
I(01) = I[01] | A by PRE_TOPC:8, TSEP_1:5;

theorem Th33: :: BORSUK_4:33
the carrier of I(01) = the carrier of I[01] \ {0,1}
proofend;

registration
cluster I(01)  ->  strict open ;
coherence
 I(01) is open by Th33, JORDAN6:34, TSEP_1:def_1;
end;

theorem :: BORSUK_4:34
I(01) is open ;

theorem Th35: :: BORSUK_4:35
for r being real number holds
( r in the carrier of I(01) iff ( 0 < r &amp; r < 1 ) )
proofend;

theorem Th36: :: BORSUK_4:36
for a, b being Point of I[01] st a < b &amp; b <> 1 holds
].a,b.] is non empty Subset of I(01)
proofend;

theorem Th37: :: BORSUK_4:37
for a, b being Point of I[01] st a < b &amp; a <> 0 holds
[.a,b.[ is non empty Subset of I(01)
proofend;

theorem :: BORSUK_4:38
for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | D are_homeomorphic
proofend;

theorem :: BORSUK_4:39
for n being Element of NAT
for D being non empty Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I(01) ,(TOP-REAL n) | (D \ {p1,p2}) are_homeomorphic
proofend;

theorem Th40: :: BORSUK_4:40
for n being Element of NAT
for D being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st D is_an_arc_of p1,p2 holds
I[01] ,(TOP-REAL n) | D are_homeomorphic
proofend;

theorem :: BORSUK_4:41
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
I[01] ,(TOP-REAL n) | (LSeg (p1,p2)) are_homeomorphic by Th40, TOPREAL1:9;

theorem Th42: :: BORSUK_4:42
for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 &amp; E = [.p1,p2.] ) holds
I[01] ,I(01) | E are_homeomorphic
proofend;

theorem Th43: :: BORSUK_4:43
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q &amp; a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] &amp; f is being_homeomorphism &amp; f . a = p &amp; f . b = q )
proofend;

theorem Th44: :: BORSUK_4:44
for A being TopSpace
for B being non empty TopSpace
for f being Function of A,B
for C being TopSpace
for X being Subset of A st f is continuous &amp; C is SubSpace of B holds
for h being Function of (A | X),C st h = f | X holds
h is continuous
proofend;

theorem Th45: :: BORSUK_4:45
for X being Subset of I[01]
for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
proofend;

theorem Th46: :: BORSUK_4:46
for X being Subset of I(01)
for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
proofend;

theorem Th47: :: BORSUK_4:47
for X being Subset of I(01)
for a being Point of I[01] st X = ].0,a.] holds
X is closed
proofend;

theorem Th48: :: BORSUK_4:48
for X being Subset of I(01)
for a being Point of I[01] st X = [.a,1.[ holds
X is closed
proofend;

theorem Th49: :: BORSUK_4:49
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q &amp; a < b &amp; b <> 1 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {p})) st
( E = ].a,b.] &amp; f is being_homeomorphism &amp; f . b = q )
proofend;

theorem Th50: :: BORSUK_4:50
for n being Element of NAT
for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q &amp; a < b &amp; a <> 0 holds
ex E being non empty Subset of I(01) ex f being Function of (I(01) | E),((TOP-REAL n) | (A \ {q})) st
( E = [.a,b.[ &amp; f is being_homeomorphism &amp; f . a = p )
proofend;

theorem Th51: :: BORSUK_4:51
for n being Element of NAT
for A, B being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st A is_an_arc_of p,q &amp; B is_an_arc_of q,p &amp; A /\ B = {p,q} &amp; p <> q holds
I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
proofend;

theorem Th52: :: BORSUK_4:52
for D being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in D holds
(TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
proofend;

theorem :: BORSUK_4:53
for D being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p in D &amp; q in D holds
(TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic
proofend;

theorem Th54: :: BORSUK_4:54
for n being Element of NAT
for C being non empty Subset of (TOP-REAL n)
for E being Subset of I(01) st ex p1, p2 being Point of I[01] st
( p1 < p2 &amp; E = [.p1,p2.] ) &amp; I(01) | E,(TOP-REAL n) | C are_homeomorphic holds
ex s1, s2 being Point of (TOP-REAL n) st C is_an_arc_of s1,s2
proofend;

theorem Th55: :: BORSUK_4:55
for Dp being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | Dp),I(01)
for C being non empty Subset of (TOP-REAL 2) st f is being_homeomorphism &amp; C c= Dp &amp; ex p1, p2 being Point of I[01] st
( p1 < p2 &amp; f .: C = [.p1,p2.] ) holds
ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2
proofend;

theorem :: BORSUK_4:56
for D being Simple_closed_curve
for C being non empty connected compact Subset of (TOP-REAL 2) holds
( not C c= D or C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
proofend;

begin

theorem Th57: :: BORSUK_4:57
for C being non empty compact Subset of I[01] st C c= ].0,1.[ holds
ex D being non empty closed_interval Subset of REAL st
( C c= D &amp; D c= ].0,1.[ &amp; lower_bound C = lower_bound D &amp; upper_bound C = upper_bound D )
proofend;

theorem Th58: :: BORSUK_4:58
for C being non empty compact Subset of I[01] st C c= ].0,1.[ holds
ex p1, p2 being Point of I[01] st
( p1 <= p2 &amp; C c= [.p1,p2.] &amp; [.p1,p2.] c= ].0,1.[ )
proofend;

theorem :: BORSUK_4:59
for D being Simple_closed_curve
for C being closed Subset of (TOP-REAL 2) st C c< D holds
ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 &amp; C c= B &amp; B c= D )
proofend;