:: by Adam Grabowski

::

:: Received August 7, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

registration
end;

::$CT 3

theorem Th1: :: BORSUK_4:4

for f, g being Function

for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} holds

f +* g is one-to-one

for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} holds

f +* g is one-to-one

proof end;

theorem Th2: :: BORSUK_4:5

for f, g being Function

for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} & f . a = g . a holds

(f +* g) " = (f ") +* (g ")

for a being set st f is one-to-one & g is one-to-one & (dom f) /\ (dom g) = {a} & (rng f) /\ (rng g) = {(f . a)} & f . a = g . a holds

(f +* g) " = (f ") +* (g ")

proof end;

theorem Th3: :: 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

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

proof end;

theorem :: BORSUK_4:7

for s1, s3, s4, l being Real st s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 holds

s1 <= ((1 - l) * s3) + (l * s4)

s1 <= ((1 - l) * s3) + (l * s4)

proof end;

theorem Th5: :: BORSUK_4:8

for A being Subset of I[01]

for a, b being Real st a < b & A = ].a,b.[ holds

[.a,b.] c= the carrier of I[01]

for a, b being Real st a < b & A = ].a,b.[ holds

[.a,b.] c= the carrier of I[01]

proof end;

theorem Th6: :: BORSUK_4:9

for A being Subset of I[01]

for a, b being Real st a < b & A = ].a,b.] holds

[.a,b.] c= the carrier of I[01]

for a, b being Real st a < b & A = ].a,b.] holds

[.a,b.] c= the carrier of I[01]

proof end;

theorem Th7: :: BORSUK_4:10

for A being Subset of I[01]

for a, b being Real st a < b & A = [.a,b.[ holds

[.a,b.] c= the carrier of I[01]

for a, b being Real st a < b & A = [.a,b.[ holds

[.a,b.] c= the carrier of I[01]

proof end;

theorem Th14: :: BORSUK_4:17

for A, B being Subset of I[01]

for a, b, c being Real st a < b & b < c & A = [.a,b.[ & B = ].b,c.] holds

A,B are_separated

for a, b, c being Real st a < b & b < c & A = [.a,b.[ & B = ].b,c.] holds

A,B are_separated

proof end;

theorem :: BORSUK_4:18

theorem Th18: :: 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 & b <= c & a in A & c in A holds

b in A

for a, b, c being Point of I[01] st a <= b & b <= c & a in A & c in A holds

b in A

proof end;

theorem Th19: :: BORSUK_4:22

for A being non empty connected Subset of I[01]

for a, b being Real st a in A & b in A holds

[.a,b.] c= A

for a, b being Real st a in A & b in A holds

[.a,b.] c= A

proof end;

theorem Th21: :: 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]

[.p1,p2.] is non empty connected compact Subset of I[01]

proof end;

theorem Th22: :: BORSUK_4:25

for X being Subset of I[01]

for X9 being Subset of REAL st X9 = X holds

( X9 is bounded_above & X9 is bounded_below )

for X9 being Subset of REAL st X9 = X holds

( X9 is bounded_above & X9 is bounded_below )

proof end;

theorem Th23: :: BORSUK_4:26

for X being Subset of I[01]

for X9 being Subset of REAL

for x being Real st x in X9 & X9 = X holds

( lower_bound X9 <= x & x <= upper_bound X9 )

for X9 being Subset of REAL

for x being Real st x in X9 & X9 = X holds

( lower_bound X9 <= x & x <= upper_bound X9 )

proof end;

Lm1: I[01] is closed SubSpace of R^1

by TOPMETR:20, TREAL_1:2;

theorem Th24: :: 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 )

for B being Subset of I[01] st A = B holds

( A is closed iff B is closed )

proof end;

theorem Th26: :: BORSUK_4:29

for C being non empty connected compact Subset of I[01]

for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds

[.(lower_bound C9),(upper_bound C9).] = C9

for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds

[.(lower_bound C9),(upper_bound C9).] = C9

proof end;

theorem Th27: :: BORSUK_4:30

for C being non empty connected compact Subset of I[01] holds C is non empty closed_interval Subset of REAL

proof end;

theorem Th28: :: 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 & C = [.p1,p2.] )

( p1 <= p2 & C = [.p1,p2.] )

proof end;

definition

existence

ex b_{1} being strict SubSpace of I[01] st the carrier of b_{1} = ].0,1.[

for b_{1}, b_{2} being strict SubSpace of I[01] st the carrier of b_{1} = ].0,1.[ & the carrier of b_{2} = ].0,1.[ holds

b_{1} = b_{2}
by TSEP_1:5;

end;
ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines I(01) BORSUK_4:def 1 :

for b_{1} being strict SubSpace of I[01] holds

( b_{1} = I(01) iff the carrier of b_{1} = ].0,1.[ );

for b

( b

theorem :: BORSUK_4:32

registration
end;

theorem :: BORSUK_4:38

for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square,(TOP-REAL 2) | D are_homeomorphic

proof end;

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

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

proof end;

theorem Th37: :: 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

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

proof end;

theorem :: BORSUK_4:41

theorem Th39: :: BORSUK_4:42

for E being Subset of I(01) st ex p1, p2 being Point of I[01] st

( p1 < p2 & E = [.p1,p2.] ) holds

I[01] ,I(01) | E are_homeomorphic

( p1 < p2 & E = [.p1,p2.] ) holds

I[01] ,I(01) | E are_homeomorphic

proof end;

theorem Th40: :: 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 & 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.] & f is being_homeomorphism & f . a = p & f . b = q )

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 & 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.] & f is being_homeomorphism & f . a = p & f . b = q )

proof end;

theorem Th41: :: 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 & C is SubSpace of B holds

for h being Function of (A | X),C st h = f | X holds

h is continuous

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 & C is SubSpace of B holds

for h being Function of (A | X),C st h = f | X holds

h is continuous

proof end;

theorem Th46: :: 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 & a < b & 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.] & f is being_homeomorphism & f . b = q )

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 & a < b & 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.] & f is being_homeomorphism & f . b = q )

proof end;

theorem Th47: :: 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 & a < b & 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.[ & f is being_homeomorphism & f . a = p )

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 & a < b & 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.[ & f is being_homeomorphism & f . a = p )

proof end;

theorem Th48: :: 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 & B is_an_arc_of q,p & A /\ B = {p,q} & p <> q holds

I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic

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 & B is_an_arc_of q,p & A /\ B = {p,q} & p <> q holds

I(01) ,(TOP-REAL n) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic

proof end;

theorem Th49: :: 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

for p being Point of (TOP-REAL 2) st p in D holds

(TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic

proof end;

theorem :: BORSUK_4:53

for D being Simple_closed_curve

for p, q being Point of (TOP-REAL 2) st p in D & q in D holds

(TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic

for p, q being Point of (TOP-REAL 2) st p in D & q in D holds

(TOP-REAL 2) | (D \ {p}),(TOP-REAL 2) | (D \ {q}) are_homeomorphic

proof end;

theorem Th51: :: 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 & E = [.p1,p2.] ) & 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

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 & E = [.p1,p2.] ) & 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

proof end;

theorem Th52: :: 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 & C c= Dp & ex p1, p2 being Point of I[01] st

( p1 < p2 & f .: C = [.p1,p2.] ) holds

ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2

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 & C c= Dp & ex p1, p2 being Point of I[01] st

( p1 < p2 & f .: C = [.p1,p2.] ) holds

ex s1, s2 being Point of (TOP-REAL 2) st C is_an_arc_of s1,s2

proof end;

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} )

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} )

proof end;

theorem Th54: :: 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 & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D )

ex D being non empty closed_interval Subset of REAL st

( C c= D & D c= ].0,1.[ & lower_bound C = lower_bound D & upper_bound C = upper_bound D )

proof end;

theorem Th55: :: 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 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )

ex p1, p2 being Point of I[01] st

( p1 <= p2 & C c= [.p1,p2.] & [.p1,p2.] c= ].0,1.[ )

proof end;

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 & C c= B & B c= D )

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 & C c= B & B c= D )

proof end;