borsuk_6.miz
begin
scheme ::
BORSUK_6:sch1
ExFunc3CondD { C() -> non
empty
set , P,Q,R[
set], F,G,H(
set) ->
set } :
ex f be
Function st (
dom f)
= C() & for c be
Element of C() holds (P[c] implies (f
. c)
= F(c)) & (Q[c] implies (f
. c)
= G(c)) & (R[c] implies (f
. c)
= H(c))
provided
A1: for c be
Element of C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (Q[c] implies not R[c])
and
A2: for c be
Element of C() holds P[c] or Q[c] or R[c];
A3: for c be
set st c
in C() holds P[c] or Q[c] or R[c] by
A2;
A4: for c be
set st c
in C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (Q[c] implies not R[c]) by
A1;
ex f be
Function st (
dom f)
= C() & for c be
set st c
in C() holds (P[c] implies (f
. c)
= F(c)) & (Q[c] implies (f
. c)
= G(c)) & (R[c] implies (f
. c)
= H(c)) from
RECDEF_2:sch 1(
A4,
A3);
then
consider f be
Function such that
A5: (
dom f)
= C() and
A6: for c be
set st c
in C() holds (P[c] implies (f
. c)
= F(c)) & (Q[c] implies (f
. c)
= G(c)) & (R[c] implies (f
. c)
= H(c));
take f;
thus (
dom f)
= C() by
A5;
let c be
Element of C();
thus thesis by
A6;
end;
theorem ::
BORSUK_6:1
Th1: the
carrier of
[:
I[01] ,
I[01] :]
=
[:
[.
0 , 1.],
[.
0 , 1.]:] by
BORSUK_1: 40,
BORSUK_1:def 2;
theorem ::
BORSUK_6:2
Th2: for a,b,x be
Real st a
<= x & x
<= b holds ((x
- a)
/ (b
- a))
in the
carrier of (
Closed-Interval-TSpace (
0 ,1))
proof
let a,b,x be
Real;
assume that
A1: a
<= x and
A2: x
<= b;
A3: a
<= b by
A1,
A2,
XXREAL_0: 2;
A4: (x
- a)
<= (b
- a) by
A2,
XREAL_1: 9;
A5: ((x
- a)
/ (b
- a))
<= 1
proof
per cases by
A3,
XREAL_1: 48;
suppose (b
- a)
=
0 ;
hence thesis by
XCMPLX_1: 49;
end;
suppose (b
- a)
>
0 ;
hence thesis by
A4,
XREAL_1: 185;
end;
end;
A6: (x
- a)
>=
0 by
A1,
XREAL_1: 48;
(b
- a)
>=
0 by
A3,
XREAL_1: 48;
then ((x
- a)
/ (b
- a))
in
[.
0 , 1.] by
A5,
A6,
XXREAL_1: 1;
hence thesis by
TOPMETR: 18;
end;
theorem ::
BORSUK_6:3
Th3: for x be
Point of
I[01] st x
<= (1
/ 2) holds (2
* x) is
Point of
I[01]
proof
let x be
Point of
I[01] ;
assume x
<= (1
/ 2);
then
A1: (2
* x)
<= (2
* (1
/ 2)) by
XREAL_1: 64;
0
<= x by
BORSUK_1: 43;
hence thesis by
A1,
BORSUK_1: 43;
end;
theorem ::
BORSUK_6:4
Th4: for x be
Point of
I[01] st x
>= (1
/ 2) holds ((2
* x)
- 1) is
Point of
I[01]
proof
let x be
Point of
I[01] ;
x
<= 1 by
BORSUK_1: 43;
then (2
* x)
<= (2
* 1) by
XREAL_1: 64;
then
A1: ((2
* x)
- 1)
<= (2
- 1) by
XREAL_1: 9;
assume x
>= (1
/ 2);
then (2
* x)
>= (2
* (1
/ 2)) by
XREAL_1: 64;
then ((2
* x)
- 1)
>= (1
- 1) by
XREAL_1: 9;
hence thesis by
A1,
BORSUK_1: 43;
end;
theorem ::
BORSUK_6:5
Th5: for p,q be
Point of
I[01] holds (p
* q) is
Point of
I[01]
proof
let p,q be
Point of
I[01] ;
A1:
0
<= p by
BORSUK_1: 43;
p
<= 1 & q
<= 1 by
BORSUK_1: 43;
then
0
<= q & (p
* q)
<= 1 by
A1,
BORSUK_1: 43,
XREAL_1: 160;
hence thesis by
A1,
BORSUK_1: 43;
end;
theorem ::
BORSUK_6:6
Th6: for x be
Point of
I[01] holds ((1
/ 2)
* x) is
Point of
I[01]
proof
let x be
Point of
I[01] ;
x
<= 1 by
BORSUK_1: 43;
then ((1
/ 2)
* x)
<= ((1
/ 2)
* 1) by
XREAL_1: 64;
then x
>=
0 & ((1
/ 2)
* x)
<= 1 by
BORSUK_1: 43,
XXREAL_0: 2;
hence thesis by
BORSUK_1: 43;
end;
theorem ::
BORSUK_6:7
Th7: for x be
Point of
I[01] st x
>= (1
/ 2) holds (x
- (1
/ 4)) is
Point of
I[01]
proof
let x be
Point of
I[01] ;
x
<= 1 by
BORSUK_1: 43;
then x
<= (1
+ (1
/ 4)) by
XXREAL_0: 2;
then
A1: (x
- (1
/ 4))
<= 1 by
XREAL_1: 20;
assume x
>= (1
/ 2);
then x
>= ((1
/ 4)
+
0 ) by
XXREAL_0: 2;
then (x
- (1
/ 4))
>=
0 by
XREAL_1: 19;
hence thesis by
A1,
BORSUK_1: 43;
end;
theorem ::
BORSUK_6:8
Th8: (
id
I[01] ) is
Path of
0[01] ,
1[01]
proof
set f = (
id
I[01] );
(f
.
0 )
=
0[01] & (f
. 1)
=
1[01] by
BORSUK_1:def 14,
BORSUK_1:def 15,
FUNCT_1: 18;
hence thesis by
BORSUK_2:def 4;
end;
theorem ::
BORSUK_6:9
Th9: for a,b,c,d be
Point of
I[01] st a
<= b & c
<= d holds
[:
[.a, b.],
[.c, d.]:] is
compact non
empty
Subset of
[:
I[01] ,
I[01] :]
proof
let a,b,c,d be
Point of
I[01] ;
[.a, b.] is
Subset of
I[01] &
[.c, d.] is
Subset of
I[01] by
BORSUK_4: 18;
then
A1:
[:
[.a, b.],
[.c, d.]:]
c=
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
ZFMISC_1: 96;
assume
A2: a
<= b & c
<= d;
then a
in
[.a, b.] & c
in
[.c, d.] by
XXREAL_1: 1;
then
reconsider Ewa =
[:
[.a, b.],
[.c, d.]:] as non
empty
Subset of
[:
I[01] ,
I[01] :] by
A1,
BORSUK_1:def 2;
[.a, b.] is
compact
Subset of
I[01] &
[.c, d.] is
compact
Subset of
I[01] by
A2,
BORSUK_4: 24;
then Ewa is
compact
Subset of
[:
I[01] ,
I[01] :] by
BORSUK_3: 23;
hence thesis;
end;
begin
theorem ::
BORSUK_6:10
Th10: for S,T be
Subset of (
TOP-REAL 2) st S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= ((2
* (p
`1 ))
- 1) } & T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (p
`1 ) } holds ((
AffineMap (1,
0 ,(1
/ 2),(1
/ 2)))
.: S)
= T
proof
set f = (
AffineMap (1,
0 ,(1
/ 2),(1
/ 2)));
set A = 1, B =
0 , C = (1
/ 2), D = (1
/ 2);
let S,T be
Subset of (
TOP-REAL 2);
assume that
A1: S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= ((2
* (p
`1 ))
- 1) } and
A2: T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (p
`1 ) };
(f
.: S)
= T
proof
thus (f
.: S)
c= T
proof
let x be
object;
assume x
in (f
.: S);
then
consider y be
object such that y
in (
dom f) and
A3: y
in S and
A4: x
= (f
. y) by
FUNCT_1:def 6;
consider p be
Point of (
TOP-REAL 2) such that
A5: y
= p and
A6: (p
`2 )
<= ((2
* (p
`1 ))
- 1) by
A1,
A3;
set b = (f
. p);
(f
. p)
=
|[((A
* (p
`1 ))
+ B), ((C
* (p
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then
A7: (b
`1 )
= ((A
* (p
`1 ))
+ B) & (b
`2 )
= ((C
* (p
`2 ))
+ D) by
EUCLID: 52;
(C
* (p
`2 ))
<= (C
* ((2
* (p
`1 ))
- 1)) by
A6,
XREAL_1: 64;
then ((C
* (p
`2 ))
+ D)
<= (((p
`1 )
- C)
+ D) by
XREAL_1: 6;
hence thesis by
A2,
A4,
A5,
A7;
end;
let x be
object;
assume
A8: x
in T;
then
A9: ex p be
Point of (
TOP-REAL 2) st x
= p & (p
`2 )
<= (p
`1 ) by
A2;
f is
onto by
JORDAN1K: 36;
then (
rng f)
= the
carrier of (
TOP-REAL 2) by
FUNCT_2:def 3;
then
consider y be
object such that
A10: y
in (
dom f) and
A11: x
= (f
. y) by
A8,
FUNCT_1:def 3;
reconsider y as
Point of (
TOP-REAL 2) by
A10;
set b = (f
. y);
A12: (f
. y)
=
|[((A
* (y
`1 ))
+ B), ((C
* (y
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then (b
`1 )
= (y
`1 ) by
EUCLID: 52;
then (2
* (b
`2 ))
<= (2
* (y
`1 )) by
A9,
A11,
XREAL_1: 64;
then
A13: ((2
* (b
`2 ))
- 1)
<= ((2
* (y
`1 ))
- 1) by
XREAL_1: 9;
(b
`2 )
= ((C
* (y
`2 ))
+ D) by
A12,
EUCLID: 52;
then y
in S by
A1,
A13;
hence thesis by
A10,
A11,
FUNCT_1:def 6;
end;
hence thesis;
end;
theorem ::
BORSUK_6:11
Th11: for S,T be
Subset of (
TOP-REAL 2) st S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= ((2
* (p
`1 ))
- 1) } & T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (p
`1 ) } holds ((
AffineMap (1,
0 ,(1
/ 2),(1
/ 2)))
.: S)
= T
proof
set f = (
AffineMap (1,
0 ,(1
/ 2),(1
/ 2)));
set A = 1, B =
0 , C = (1
/ 2), D = (1
/ 2);
let S,T be
Subset of (
TOP-REAL 2);
assume that
A1: S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= ((2
* (p
`1 ))
- 1) } and
A2: T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (p
`1 ) };
(f
.: S)
= T
proof
thus (f
.: S)
c= T
proof
let x be
object;
assume x
in (f
.: S);
then
consider y be
object such that y
in (
dom f) and
A3: y
in S and
A4: x
= (f
. y) by
FUNCT_1:def 6;
consider p be
Point of (
TOP-REAL 2) such that
A5: y
= p and
A6: (p
`2 )
>= ((2
* (p
`1 ))
- 1) by
A1,
A3;
A7: (C
* (p
`2 ))
>= (C
* ((2
* (p
`1 ))
- 1)) by
A6,
XREAL_1: 64;
set b = (f
. p);
A8: (f
. p)
=
|[((A
* (p
`1 ))
+ B), ((C
* (p
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then
A9: (b
`1 )
= ((A
* (p
`1 ))
+ B) by
EUCLID: 52;
(b
`2 )
= ((C
* (p
`2 ))
+ D) by
A8,
EUCLID: 52;
then (b
`2 )
>= (((p
`1 )
- C)
+ D) by
A7,
XREAL_1: 6;
hence thesis by
A2,
A4,
A5,
A9;
end;
let x be
object;
assume
A10: x
in T;
then
A11: ex p be
Point of (
TOP-REAL 2) st x
= p & (p
`2 )
>= (p
`1 ) by
A2;
f is
onto by
JORDAN1K: 36;
then (
rng f)
= the
carrier of (
TOP-REAL 2) by
FUNCT_2:def 3;
then
consider y be
object such that
A12: y
in (
dom f) and
A13: x
= (f
. y) by
A10,
FUNCT_1:def 3;
reconsider y as
Point of (
TOP-REAL 2) by
A12;
set b = (f
. y);
A14: (f
. y)
=
|[((A
* (y
`1 ))
+ B), ((C
* (y
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then (b
`1 )
= (y
`1 ) by
EUCLID: 52;
then (2
* (b
`2 ))
>= (2
* (y
`1 )) by
A11,
A13,
XREAL_1: 64;
then
A15: ((2
* (b
`2 ))
- 1)
>= ((2
* (y
`1 ))
- 1) by
XREAL_1: 9;
(b
`2 )
= ((C
* (y
`2 ))
+ D) by
A14,
EUCLID: 52;
then y
in S by
A1,
A15;
hence thesis by
A12,
A13,
FUNCT_1:def 6;
end;
hence thesis;
end;
theorem ::
BORSUK_6:12
Th12: for S,T be
Subset of (
TOP-REAL 2) st S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (1
- (2
* (p
`1 ))) } & T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (
- (p
`1 )) } holds ((
AffineMap (1,
0 ,(1
/ 2),(
- (1
/ 2))))
.: S)
= T
proof
set f = (
AffineMap (1,
0 ,(1
/ 2),(
- (1
/ 2))));
set A = 1, B =
0 , C = (1
/ 2), D = (
- (1
/ 2));
let S,T be
Subset of (
TOP-REAL 2);
assume that
A1: S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (1
- (2
* (p
`1 ))) } and
A2: T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (
- (p
`1 )) };
(f
.: S)
= T
proof
thus (f
.: S)
c= T
proof
let x be
object;
assume x
in (f
.: S);
then
consider y be
object such that y
in (
dom f) and
A3: y
in S and
A4: x
= (f
. y) by
FUNCT_1:def 6;
consider p be
Point of (
TOP-REAL 2) such that
A5: y
= p and
A6: (p
`2 )
>= (1
- (2
* (p
`1 ))) by
A1,
A3;
set b = (f
. p);
(C
* (p
`2 ))
>= (C
* (1
- (2
* (p
`1 )))) by
A6,
XREAL_1: 64;
then
A7: ((C
* (p
`2 ))
+ D)
>= ((C
- (p
`1 ))
+ D) by
XREAL_1: 6;
A8: (f
. p)
=
|[((A
* (p
`1 ))
+ B), ((C
* (p
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then (b
`1 )
= ((A
* (p
`1 ))
+ B) by
EUCLID: 52;
then (b
`2 )
>= (
- (b
`1 )) by
A8,
A7,
EUCLID: 52;
hence thesis by
A2,
A4,
A5;
end;
let x be
object;
assume
A9: x
in T;
then
A10: ex p be
Point of (
TOP-REAL 2) st x
= p & (p
`2 )
>= (
- (p
`1 )) by
A2;
f is
onto by
JORDAN1K: 36;
then (
rng f)
= the
carrier of (
TOP-REAL 2) by
FUNCT_2:def 3;
then
consider y be
object such that
A11: y
in (
dom f) and
A12: x
= (f
. y) by
A9,
FUNCT_1:def 3;
reconsider y as
Point of (
TOP-REAL 2) by
A11;
set b = (f
. y);
A13: (f
. y)
=
|[((A
* (y
`1 ))
+ B), ((C
* (y
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then (b
`1 )
= (y
`1 ) by
EUCLID: 52;
then (2
* (b
`2 ))
>= (2
* (
- (y
`1 ))) by
A10,
A12,
XREAL_1: 64;
then
A14: ((2
* (b
`2 ))
+ 1)
>= ((2
* (
- (y
`1 )))
+ 1) by
XREAL_1: 6;
(b
`2 )
= ((C
* (y
`2 ))
+ D) by
A13,
EUCLID: 52;
then (y
`2 )
>= (1
- (2
* (y
`1 ))) by
A14;
then y
in S by
A1;
hence thesis by
A11,
A12,
FUNCT_1:def 6;
end;
hence thesis;
end;
theorem ::
BORSUK_6:13
Th13: for S,T be
Subset of (
TOP-REAL 2) st S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (1
- (2
* (p
`1 ))) } & T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (
- (p
`1 )) } holds ((
AffineMap (1,
0 ,(1
/ 2),(
- (1
/ 2))))
.: S)
= T
proof
set f = (
AffineMap (1,
0 ,(1
/ 2),(
- (1
/ 2))));
set A = 1, B =
0 , C = (1
/ 2), D = (
- (1
/ 2));
let S,T be
Subset of (
TOP-REAL 2);
assume that
A1: S
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (1
- (2
* (p
`1 ))) } and
A2: T
= { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (
- (p
`1 )) };
(f
.: S)
= T
proof
thus (f
.: S)
c= T
proof
let x be
object;
assume x
in (f
.: S);
then
consider y be
object such that y
in (
dom f) and
A3: y
in S and
A4: x
= (f
. y) by
FUNCT_1:def 6;
consider p be
Point of (
TOP-REAL 2) such that
A5: y
= p and
A6: (p
`2 )
<= (1
- (2
* (p
`1 ))) by
A1,
A3;
set b = (f
. p);
(C
* (p
`2 ))
<= (C
* (1
- (2
* (p
`1 )))) by
A6,
XREAL_1: 64;
then
A7: ((C
* (p
`2 ))
+ D)
<= ((C
- (p
`1 ))
+ D) by
XREAL_1: 6;
A8: (f
. p)
=
|[((A
* (p
`1 ))
+ B), ((C
* (p
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then (b
`1 )
= ((A
* (p
`1 ))
+ B) by
EUCLID: 52;
then (b
`2 )
<= (
- (b
`1 )) by
A8,
A7,
EUCLID: 52;
hence thesis by
A2,
A4,
A5;
end;
let x be
object;
assume
A9: x
in T;
then
A10: ex p be
Point of (
TOP-REAL 2) st x
= p & (p
`2 )
<= (
- (p
`1 )) by
A2;
f is
onto by
JORDAN1K: 36;
then (
rng f)
= the
carrier of (
TOP-REAL 2) by
FUNCT_2:def 3;
then
consider y be
object such that
A11: y
in (
dom f) and
A12: x
= (f
. y) by
A9,
FUNCT_1:def 3;
reconsider y as
Point of (
TOP-REAL 2) by
A11;
set b = (f
. y);
A13: (f
. y)
=
|[((A
* (y
`1 ))
+ B), ((C
* (y
`2 ))
+ D)]| by
JGRAPH_2:def 2;
then (b
`1 )
= (y
`1 ) by
EUCLID: 52;
then (2
* (b
`2 ))
<= (2
* (
- (y
`1 ))) by
A10,
A12,
XREAL_1: 64;
then
A14: ((2
* (b
`2 ))
+ 1)
<= ((2
* (
- (y
`1 )))
+ 1) by
XREAL_1: 6;
(b
`2 )
= ((C
* (y
`2 ))
+ D) by
A13,
EUCLID: 52;
then (y
`2 )
<= (1
- (2
* (y
`1 ))) by
A14;
then y
in S by
A1;
hence thesis by
A11,
A12,
FUNCT_1:def 6;
end;
hence thesis;
end;
begin
theorem ::
BORSUK_6:14
for T be non
empty
1-sorted holds T is
real-membered iff for x be
Element of T holds x is
real
proof
let T be non
empty
1-sorted;
thus T is
real-membered implies for x be
Element of T holds x is
real;
assume for x be
Element of T holds x is
real;
then for x be
object st x
in the
carrier of T holds x is
real;
then the
carrier of T is
real-membered by
MEMBERED:def 3;
hence thesis by
TOPMETR:def 8;
end;
registration
cluster non
empty
real-membered for
1-sorted;
existence
proof
take
I[01] ;
thus thesis;
end;
cluster non
empty
real-membered for
TopSpace;
existence
proof
take
I[01] ;
thus thesis;
end;
end
registration
let T be
real-membered
1-sorted;
cluster ->
real for
Element of T;
coherence ;
end
registration
let T be
real-membered
TopStruct;
cluster ->
real-membered for
SubSpace of T;
coherence ;
end
registration
let S,T be
real-membered non
empty
TopSpace, p be
Element of
[:S, T:];
cluster (p
`1 ) ->
real;
coherence
proof
p
in the
carrier of
[:S, T:];
then p
in
[:the
carrier of S, the
carrier of T:] by
BORSUK_1:def 2;
then (p
`1 )
in the
carrier of S by
MCART_1: 10;
hence thesis;
end;
cluster (p
`2 ) ->
real;
coherence
proof
p
in the
carrier of
[:S, T:];
then p
in
[:the
carrier of S, the
carrier of T:] by
BORSUK_1:def 2;
then (p
`2 )
in the
carrier of T by
MCART_1: 10;
hence thesis;
end;
end
registration
let T be non
empty
SubSpace of
[:
I[01] ,
I[01] :], x be
Point of T;
cluster (x
`1 ) ->
real;
coherence
proof
the
carrier of T
c= the
carrier of
[:
I[01] ,
I[01] :] & x
in the
carrier of T by
BORSUK_1: 1;
then
reconsider x9 = x as
Point of
[:
I[01] ,
I[01] :];
(x9
`1 ) is
real;
hence thesis;
end;
cluster (x
`2 ) ->
real;
coherence
proof
the
carrier of T
c= the
carrier of
[:
I[01] ,
I[01] :] & x
in the
carrier of T by
BORSUK_1: 1;
then
reconsider x9 = x as
Point of
[:
I[01] ,
I[01] :];
(x9
`2 ) is
real;
hence thesis;
end;
end
begin
theorem ::
BORSUK_6:15
Th15: { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= ((2
* (p
`1 ))
- 1) } is
closed
Subset of (
TOP-REAL 2)
proof
reconsider L = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (p
`1 ) } as
closed
Subset of (
TOP-REAL 2) by
JGRAPH_2: 46;
set f = (
AffineMap (1,
0 ,(1
/ 2),(1
/ 2)));
defpred
P[
Point of (
TOP-REAL 2)] means ($1
`2 )
<= ((2
* ($1
`1 ))
- 1);
{ p where p be
Point of (
TOP-REAL 2) :
P[p] } is
Subset of (
TOP-REAL 2) from
JGRAPH_2:sch 1;
then
reconsider K = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= ((2
* (p
`1 ))
- 1) } as
Subset of (
TOP-REAL 2);
K
c= the
carrier of (
TOP-REAL 2);
then
A1: K
c= (
dom f) by
FUNCT_2:def 1;
A2: (f
.: K)
= L by
Th10;
f is
one-to-one by
JGRAPH_2: 44;
then K
= (f
" (f
.: K)) by
A1,
FUNCT_1: 94;
hence thesis by
A2,
PRE_TOPC:def 6;
end;
theorem ::
BORSUK_6:16
Th16: { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= ((2
* (p
`1 ))
- 1) } is
closed
Subset of (
TOP-REAL 2)
proof
reconsider L = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (p
`1 ) } as
closed
Subset of (
TOP-REAL 2) by
JGRAPH_2: 46;
set f = (
AffineMap (1,
0 ,(1
/ 2),(1
/ 2)));
defpred
P[
Point of (
TOP-REAL 2)] means ($1
`2 )
>= ((2
* ($1
`1 ))
- 1);
{ p where p be
Point of (
TOP-REAL 2) :
P[p] } is
Subset of (
TOP-REAL 2) from
JGRAPH_2:sch 1;
then
reconsider K = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= ((2
* (p
`1 ))
- 1) } as
Subset of (
TOP-REAL 2);
K
c= the
carrier of (
TOP-REAL 2);
then
A1: K
c= (
dom f) by
FUNCT_2:def 1;
A2: (f
.: K)
= L by
Th11;
f is
one-to-one by
JGRAPH_2: 44;
then K
= (f
" (f
.: K)) by
A1,
FUNCT_1: 94;
hence thesis by
A2,
PRE_TOPC:def 6;
end;
theorem ::
BORSUK_6:17
Th17: { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (1
- (2
* (p
`1 ))) } is
closed
Subset of (
TOP-REAL 2)
proof
reconsider L = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (
- (p
`1 )) } as
closed
Subset of (
TOP-REAL 2) by
JGRAPH_2: 47;
set f = (
AffineMap (1,
0 ,(1
/ 2),(
- (1
/ 2))));
defpred
P[
Point of (
TOP-REAL 2)] means ($1
`2 )
<= (1
- (2
* ($1
`1 )));
{ p where p be
Point of (
TOP-REAL 2) :
P[p] } is
Subset of (
TOP-REAL 2) from
JGRAPH_2:sch 1;
then
reconsider K = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
<= (1
- (2
* (p
`1 ))) } as
Subset of (
TOP-REAL 2);
K
c= the
carrier of (
TOP-REAL 2);
then
A1: K
c= (
dom f) by
FUNCT_2:def 1;
A2: (f
.: K)
= L by
Th13;
f is
one-to-one by
JGRAPH_2: 44;
then K
= (f
" (f
.: K)) by
A1,
FUNCT_1: 94;
hence thesis by
A2,
PRE_TOPC:def 6;
end;
theorem ::
BORSUK_6:18
Th18: { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (1
- (2
* (p
`1 ))) } is
closed
Subset of (
TOP-REAL 2)
proof
reconsider L = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (
- (p
`1 )) } as
closed
Subset of (
TOP-REAL 2) by
JGRAPH_2: 47;
set f = (
AffineMap (1,
0 ,(1
/ 2),(
- (1
/ 2))));
defpred
P[
Point of (
TOP-REAL 2)] means ($1
`2 )
>= (1
- (2
* ($1
`1 )));
{ p where p be
Point of (
TOP-REAL 2) :
P[p] } is
Subset of (
TOP-REAL 2) from
JGRAPH_2:sch 1;
then
reconsider K = { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (1
- (2
* (p
`1 ))) } as
Subset of (
TOP-REAL 2);
K
c= the
carrier of (
TOP-REAL 2);
then
A1: K
c= (
dom f) by
FUNCT_2:def 1;
A2: (f
.: K)
= L by
Th12;
f is
one-to-one by
JGRAPH_2: 44;
then K
= (f
" (f
.: K)) by
A1,
FUNCT_1: 94;
hence thesis by
A2,
PRE_TOPC:def 6;
end;
theorem ::
BORSUK_6:19
Th19: { p where p be
Point of (
TOP-REAL 2) : (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1) } is
closed
Subset of (
TOP-REAL 2)
proof
defpred
R[
Point of (
TOP-REAL 2)] means ($1
`2 )
>= ((2
* ($1
`1 ))
- 1);
reconsider L = { p where p be
Point of (
TOP-REAL 2) :
R[p] } as
closed
Subset of (
TOP-REAL 2) by
Th16;
defpred
P[
Point of (
TOP-REAL 2)] means ($1
`2 )
>= (1
- (2
* ($1
`1 )));
reconsider K = { p where p be
Point of (
TOP-REAL 2) :
P[p] } as
closed
Subset of (
TOP-REAL 2) by
Th18;
set T = { p where p be
Point of (
TOP-REAL 2) :
P[p] &
R[p] };
{ p where p be
Point of (
TOP-REAL 2) :
P[p] &
R[p] }
= ({ p where p be
Point of (
TOP-REAL 2) :
P[p] }
/\ { p where p be
Point of (
TOP-REAL 2) :
R[p] }) from
DOMAIN_1:sch 10;
then T
= (K
/\ L);
hence thesis;
end;
theorem ::
BORSUK_6:20
Th20: ex f be
Function of
[:
R^1 ,
R^1 :], (
TOP-REAL 2) st for x,y be
Real holds (f
.
[x, y])
=
<*x, y*>
proof
defpred
P[
Element of
REAL ,
Element of
REAL ,
set] means ex c be
Element of (
REAL 2) st c
= $3 & $3
=
<*$1, $2*>;
A1: for x,y be
Element of
REAL holds ex u be
Element of (
REAL 2) st
P[x, y, u]
proof
let x,y be
Element of
REAL ;
take
<*x, y*>;
<*x, y*> is
Element of (
REAL 2) by
FINSEQ_2: 137;
hence thesis;
end;
consider f be
Function of
[:
REAL ,
REAL :], (
REAL 2) such that
A2: for x,y be
Element of
REAL holds
P[x, y, (f
. (x,y))] from
BINOP_1:sch 3(
A1);
the
carrier of
[:
R^1 ,
R^1 :]
=
[:the
carrier of
R^1 , the
carrier of
R^1 :] by
BORSUK_1:def 2;
then
reconsider f as
Function of
[:
R^1 ,
R^1 :], (
TOP-REAL 2) by
EUCLID: 22,
TOPMETR: 17;
take f;
for x,y be
Real holds (f
.
[x, y])
=
<*x, y*>
proof
let x,y be
Real;
reconsider x, y as
Element of
REAL by
XREAL_0:def 1;
P[x, y, (f
. (x,y))] by
A2;
hence thesis;
end;
hence thesis;
end;
theorem ::
BORSUK_6:21
Th21: { p where p be
Point of
[:
R^1 ,
R^1 :] : (p
`2 )
<= (1
- (2
* (p
`1 ))) } is
closed
Subset of
[:
R^1 ,
R^1 :]
proof
set GG =
[:
R^1 ,
R^1 :], SS = (
TOP-REAL 2);
defpred
P[
Point of GG] means ($1
`2 )
<= (1
- (2
* ($1
`1 )));
defpred
R[
Point of SS] means ($1
`2 )
<= (1
- (2
* ($1
`1 )));
reconsider K = { p where p be
Point of GG :
P[p] } as
Subset of GG from
DOMAIN_1:sch 7;
reconsider L = { p where p be
Point of SS :
R[p] } as
Subset of SS from
DOMAIN_1:sch 7;
consider f be
Function of GG, SS such that
A1: for x,y be
Real holds (f
.
[x, y])
=
<*x, y*> by
Th20;
A2: L
c= (f
.: K)
proof
let x be
object;
assume x
in L;
then
consider z be
Point of SS such that
A3: z
= x and
A4:
R[z];
the
carrier of SS
= (
REAL 2) by
EUCLID: 22;
then z is
Tuple of 2,
REAL by
FINSEQ_2: 131;
then
consider x1,y1 be
Element of
REAL such that
A5: z
=
<*x1, y1*> by
FINSEQ_2: 100;
(z
`1 )
= x1 by
A5,
EUCLID: 52;
then
A6: y1
<= (1
- (2
* x1)) by
A4,
A5,
EUCLID: 52;
set Y =
[x1, y1];
A7: Y
in
[:
REAL ,
REAL :] by
ZFMISC_1: 87;
then
A8: Y
in the
carrier of GG by
BORSUK_1:def 2,
TOPMETR: 17;
reconsider Y as
Point of GG by
A7,
BORSUK_1:def 2,
TOPMETR: 17;
A9: Y
in (
dom f) by
A8,
FUNCT_2:def 1;
(Y
`1 )
= x1 & (Y
`2 )
= y1;
then
A10: Y
in K by
A6;
x
= (f
. Y) by
A1,
A3,
A5;
hence thesis by
A10,
A9,
FUNCT_1:def 6;
end;
A11: f is
being_homeomorphism by
A1,
TOPREAL6: 76;
(f
.: K)
c= L
proof
let x be
object;
assume x
in (f
.: K);
then
consider y be
object such that y
in (
dom f) and
A12: y
in K and
A13: x
= (f
. y) by
FUNCT_1:def 6;
consider z be
Point of GG such that
A14: z
= y and
A15:
P[z] by
A12;
z
in the
carrier of GG;
then z
in
[:the
carrier of
R^1 , the
carrier of
R^1 :] by
BORSUK_1:def 2;
then
consider x1,y1 be
object such that
A16: x1
in the
carrier of
R^1 & y1
in the
carrier of
R^1 and
A17: z
=
[x1, y1] by
ZFMISC_1:def 2;
reconsider x1, y1 as
Real by
A16;
A18: x
=
|[x1, y1]| by
A1,
A13,
A14,
A17;
then
reconsider x9 = x as
Point of SS;
A19: (z
`1 )
= x1 & (z
`2 )
= y1 by
A17;
(x9
`1 )
= x1 & (x9
`2 )
= y1 by
A18,
FINSEQ_1: 44;
hence thesis by
A15,
A19;
end;
then (f
.: K)
= L by
A2;
hence thesis by
A11,
Th17,
TOPS_2: 58;
end;
theorem ::
BORSUK_6:22
Th22: { p where p be
Point of
[:
R^1 ,
R^1 :] : (p
`2 )
<= ((2
* (p
`1 ))
- 1) } is
closed
Subset of
[:
R^1 ,
R^1 :]
proof
set GG =
[:
R^1 ,
R^1 :], SS = (
TOP-REAL 2);
defpred
P[
Point of GG] means ($1
`2 )
<= ((2
* ($1
`1 ))
- 1);
defpred
R[
Point of SS] means ($1
`2 )
<= ((2
* ($1
`1 ))
- 1);
reconsider K = { p where p be
Point of GG :
P[p] } as
Subset of GG from
DOMAIN_1:sch 7;
reconsider L = { p where p be
Point of SS :
R[p] } as
Subset of SS from
DOMAIN_1:sch 7;
consider f be
Function of GG, SS such that
A1: for x,y be
Real holds (f
.
[x, y])
=
<*x, y*> by
Th20;
A2: L
c= (f
.: K)
proof
let x be
object;
assume x
in L;
then
consider z be
Point of SS such that
A3: z
= x and
A4:
R[z];
the
carrier of SS
= (
REAL 2) by
EUCLID: 22;
then z is
Tuple of 2,
REAL by
FINSEQ_2: 131;
then
consider x1,y1 be
Element of
REAL such that
A5: z
=
<*x1, y1*> by
FINSEQ_2: 100;
(z
`1 )
= x1 by
A5,
EUCLID: 52;
then
A6: y1
<= ((2
* x1)
- 1) by
A4,
A5,
EUCLID: 52;
set Y =
[x1, y1];
A7: Y
in
[:the
carrier of
R^1 , the
carrier of
R^1 :] by
TOPMETR: 17,
ZFMISC_1: 87;
then
A8: Y
in the
carrier of GG by
BORSUK_1:def 2;
reconsider Y as
Point of GG by
A7,
BORSUK_1:def 2;
A9: Y
in (
dom f) by
A8,
FUNCT_2:def 1;
(Y
`1 )
= x1 & (Y
`2 )
= y1;
then
A10: Y
in K by
A6;
x
= (f
. Y) by
A1,
A3,
A5;
hence thesis by
A10,
A9,
FUNCT_1:def 6;
end;
A11: f is
being_homeomorphism by
A1,
TOPREAL6: 76;
(f
.: K)
c= L
proof
let x be
object;
assume x
in (f
.: K);
then
consider y be
object such that y
in (
dom f) and
A12: y
in K and
A13: x
= (f
. y) by
FUNCT_1:def 6;
consider z be
Point of GG such that
A14: z
= y and
A15:
P[z] by
A12;
z
in the
carrier of GG;
then z
in
[:the
carrier of
R^1 , the
carrier of
R^1 :] by
BORSUK_1:def 2;
then
consider x1,y1 be
object such that
A16: x1
in the
carrier of
R^1 & y1
in the
carrier of
R^1 and
A17: z
=
[x1, y1] by
ZFMISC_1:def 2;
reconsider x1, y1 as
Real by
A16;
A18: x
=
|[x1, y1]| by
A1,
A13,
A14,
A17;
then
reconsider x9 = x as
Point of SS;
A19: (z
`1 )
= x1 & (z
`2 )
= y1 by
A17;
(x9
`1 )
= x1 & (x9
`2 )
= y1 by
A18,
FINSEQ_1: 44;
hence thesis by
A15,
A19;
end;
then (f
.: K)
= L by
A2;
hence thesis by
A11,
Th15,
TOPS_2: 58;
end;
theorem ::
BORSUK_6:23
Th23: { p where p be
Point of
[:
R^1 ,
R^1 :] : (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1) } is
closed
Subset of
[:
R^1 ,
R^1 :]
proof
set GG =
[:
R^1 ,
R^1 :], SS = (
TOP-REAL 2);
defpred
P[
Point of GG] means ($1
`2 )
>= (1
- (2
* ($1
`1 ))) & ($1
`2 )
>= ((2
* ($1
`1 ))
- 1);
defpred
R[
Point of SS] means ($1
`2 )
>= (1
- (2
* ($1
`1 ))) & ($1
`2 )
>= ((2
* ($1
`1 ))
- 1);
reconsider K = { p where p be
Point of GG :
P[p] } as
Subset of GG from
DOMAIN_1:sch 7;
reconsider L = { p where p be
Point of SS :
R[p] } as
Subset of SS from
DOMAIN_1:sch 7;
consider f be
Function of GG, SS such that
A1: for x,y be
Real holds (f
.
[x, y])
=
<*x, y*> by
Th20;
A2: L
c= (f
.: K)
proof
let x be
object;
assume x
in L;
then
consider z be
Point of SS such that
A3: z
= x and
A4:
R[z];
the
carrier of SS
= (
REAL 2) by
EUCLID: 22;
then z is
Tuple of 2,
REAL by
FINSEQ_2: 131;
then
consider x1,y1 be
Element of
REAL such that
A5: z
=
<*x1, y1*> by
FINSEQ_2: 100;
(z
`1 )
= x1 by
A5,
EUCLID: 52;
then
A6: y1
>= (1
- (2
* x1)) & y1
>= ((2
* x1)
- 1) by
A4,
A5,
EUCLID: 52;
set Y =
[x1, y1];
A7: Y
in
[:the
carrier of
R^1 , the
carrier of
R^1 :] by
TOPMETR: 17,
ZFMISC_1: 87;
then
A8: Y
in the
carrier of GG by
BORSUK_1:def 2;
reconsider Y as
Point of GG by
A7,
BORSUK_1:def 2;
A9: Y
in (
dom f) by
A8,
FUNCT_2:def 1;
(Y
`1 )
= x1 & (Y
`2 )
= y1;
then
A10: Y
in K by
A6;
x
= (f
. Y) by
A1,
A3,
A5;
hence thesis by
A10,
A9,
FUNCT_1:def 6;
end;
A11: f is
being_homeomorphism by
A1,
TOPREAL6: 76;
(f
.: K)
c= L
proof
let x be
object;
assume x
in (f
.: K);
then
consider y be
object such that y
in (
dom f) and
A12: y
in K and
A13: x
= (f
. y) by
FUNCT_1:def 6;
consider z be
Point of GG such that
A14: z
= y and
A15:
P[z] by
A12;
z
in the
carrier of GG;
then z
in
[:the
carrier of
R^1 , the
carrier of
R^1 :] by
BORSUK_1:def 2;
then
consider x1,y1 be
object such that
A16: x1
in the
carrier of
R^1 & y1
in the
carrier of
R^1 and
A17: z
=
[x1, y1] by
ZFMISC_1:def 2;
reconsider x1, y1 as
Real by
A16;
A18: x
=
|[x1, y1]| by
A1,
A13,
A14,
A17;
then
reconsider x9 = x as
Point of SS;
A19: (z
`1 )
= x1 & (z
`2 )
= y1 by
A17;
(x9
`1 )
= x1 & (x9
`2 )
= y1 by
A18,
FINSEQ_1: 44;
hence thesis by
A15,
A19;
end;
then (f
.: K)
= L by
A2;
hence thesis by
A11,
Th19,
TOPS_2: 58;
end;
theorem ::
BORSUK_6:24
Th24: { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
<= (1
- (2
* (p
`1 ))) } is
closed non
empty
Subset of
[:
I[01] ,
I[01] :]
proof
set GG =
[:
I[01] ,
I[01] :], SS =
[:
R^1 ,
R^1 :];
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
[
0 ,
0 ]
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
ZFMISC_1: 87;
then
reconsider x =
[
0 ,
0 ] as
Point of GG by
BORSUK_1:def 2;
reconsider PA = { p where p be
Point of SS : (p
`2 )
<= (1
- (2
* (p
`1 ))) } as
closed
Subset of SS by
Th21;
set P0 = { p where p be
Point of GG : (p
`2 )
<= (1
- (2
* (p
`1 ))) };
A1: GG is
SubSpace of SS by
BORSUK_3: 21;
A2: P0
= (PA
/\ (
[#] GG))
proof
thus P0
c= (PA
/\ (
[#] GG))
proof
let x be
object;
A3: the
carrier of GG
c= the
carrier of SS by
A1,
BORSUK_1: 1;
assume x
in P0;
then
A4: ex p be
Point of GG st x
= p & (p
`2 )
<= (1
- (2
* (p
`1 )));
then x
in the
carrier of GG;
then
reconsider a = x as
Point of SS by
A3;
(a
`2 )
<= (1
- (2
* (a
`1 ))) by
A4;
then x
in PA;
hence thesis by
A4,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A5: x
in (PA
/\ (
[#] GG));
then x
in PA by
XBOOLE_0:def 4;
then ex p be
Point of SS st x
= p & (p
`2 )
<= (1
- (2
* (p
`1 )));
hence thesis by
A5;
end;
(x
`2 )
<= (1
- (2
* (x
`1 )));
then x
in P0;
hence thesis by
A1,
A2,
PRE_TOPC: 13;
end;
theorem ::
BORSUK_6:25
Th25: { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1) } is
closed non
empty
Subset of
[:
I[01] ,
I[01] :]
proof
set GG =
[:
I[01] ,
I[01] :], SS =
[:
R^1 ,
R^1 :];
1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
[1, 1]
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
ZFMISC_1: 87;
then
reconsider x =
[1, 1] as
Point of GG by
BORSUK_1:def 2;
reconsider PA = { p where p be
Point of SS : (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1) } as
closed
Subset of SS by
Th23;
set P0 = { p where p be
Point of GG : (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1) };
A1: (x
`2 )
>= ((2
* (x
`1 ))
- 1);
A2: GG is
SubSpace of SS by
BORSUK_3: 21;
A3: P0
= (PA
/\ (
[#] GG))
proof
thus P0
c= (PA
/\ (
[#] GG))
proof
let x be
object;
A4: the
carrier of GG
c= the
carrier of SS by
A2,
BORSUK_1: 1;
assume x
in P0;
then
A5: ex p be
Point of GG st x
= p & (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1);
then x
in the
carrier of GG;
then
reconsider a = x as
Point of SS by
A4;
(a
`2 )
>= (1
- (2
* (a
`1 ))) by
A5;
then x
in PA by
A5;
hence thesis by
A5,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A6: x
in (PA
/\ (
[#] GG));
then x
in PA by
XBOOLE_0:def 4;
then ex p be
Point of SS st x
= p & (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1);
hence thesis by
A6;
end;
(x
`2 )
>= (1
- (2
* (x
`1 )));
then x
in P0 by
A1;
hence thesis by
A2,
A3,
PRE_TOPC: 13;
end;
theorem ::
BORSUK_6:26
Th26: { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
<= ((2
* (p
`1 ))
- 1) } is
closed non
empty
Subset of
[:
I[01] ,
I[01] :]
proof
set GG =
[:
I[01] ,
I[01] :], SS =
[:
R^1 ,
R^1 :];
0
in the
carrier of
I[01] & 1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
[1,
0 ]
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
ZFMISC_1: 87;
then
reconsider x =
[1,
0 ] as
Point of GG by
BORSUK_1:def 2;
reconsider PA = { p where p be
Point of SS : (p
`2 )
<= ((2
* (p
`1 ))
- 1) } as
closed
Subset of SS by
Th22;
set P0 = { p where p be
Point of GG : (p
`2 )
<= ((2
* (p
`1 ))
- 1) };
A1: GG is
SubSpace of SS by
BORSUK_3: 21;
A2: P0
= (PA
/\ (
[#] GG))
proof
thus P0
c= (PA
/\ (
[#] GG))
proof
let x be
object;
A3: the
carrier of GG
c= the
carrier of SS by
A1,
BORSUK_1: 1;
assume x
in P0;
then
A4: ex p be
Point of GG st x
= p & (p
`2 )
<= ((2
* (p
`1 ))
- 1);
then x
in the
carrier of GG;
then
reconsider a = x as
Point of SS by
A3;
(a
`2 )
<= ((2
* (a
`1 ))
- 1) by
A4;
then x
in PA;
hence thesis by
A4,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A5: x
in (PA
/\ (
[#] GG));
then x
in PA by
XBOOLE_0:def 4;
then ex p be
Point of SS st x
= p & (p
`2 )
<= ((2
* (p
`1 ))
- 1);
hence thesis by
A5;
end;
(x
`2 )
<= ((2
* (x
`1 ))
- 1);
then x
in P0;
hence thesis by
A1,
A2,
PRE_TOPC: 13;
end;
theorem ::
BORSUK_6:27
Th27: for S,T be non
empty
TopSpace, p be
Point of
[:S, T:] holds (p
`1 ) is
Point of S & (p
`2 ) is
Point of T
proof
let S,T be non
empty
TopSpace, p be
Point of
[:S, T:];
p
in the
carrier of
[:S, T:];
then p
in
[:the
carrier of S, the
carrier of T:] by
BORSUK_1:def 2;
hence thesis by
MCART_1: 10;
end;
theorem ::
BORSUK_6:28
Th28: for A,B be
Subset of
[:
I[01] ,
I[01] :] st A
=
[:
[.
0 , (1
/ 2).],
[.
0 , 1.]:] & B
=
[:
[.(1
/ 2), 1.],
[.
0 , 1.]:] holds ((
[#] (
[:
I[01] ,
I[01] :]
| A))
\/ (
[#] (
[:
I[01] ,
I[01] :]
| B)))
= (
[#]
[:
I[01] ,
I[01] :])
proof
let A,B be
Subset of
[:
I[01] ,
I[01] :];
assume
A1: A
=
[:
[.
0 , (1
/ 2).],
[.
0 , 1.]:] & B
=
[:
[.(1
/ 2), 1.],
[.
0 , 1.]:];
((
[#] (
[:
I[01] ,
I[01] :]
| A))
\/ (
[#] (
[:
I[01] ,
I[01] :]
| B)))
= (A
\/ (
[#] (
[:
I[01] ,
I[01] :]
| B))) by
PRE_TOPC:def 5
.= (A
\/ B) by
PRE_TOPC:def 5
.=
[:(
[.
0 , (1
/ 2).]
\/
[.(1
/ 2), 1.]),
[.
0 , 1.]:] by
A1,
ZFMISC_1: 97
.=
[:
[.
0 , 1.],
[.
0 , 1.]:] by
XXREAL_1: 174
.= (
[#]
[:
I[01] ,
I[01] :]) by
BORSUK_1: 40,
BORSUK_1:def 2;
hence thesis;
end;
theorem ::
BORSUK_6:29
Th29: for A,B be
Subset of
[:
I[01] ,
I[01] :] st A
=
[:
[.
0 , (1
/ 2).],
[.
0 , 1.]:] & B
=
[:
[.(1
/ 2), 1.],
[.
0 , 1.]:] holds ((
[#] (
[:
I[01] ,
I[01] :]
| A))
/\ (
[#] (
[:
I[01] ,
I[01] :]
| B)))
=
[:
{(1
/ 2)},
[.
0 , 1.]:]
proof
let A,B be
Subset of
[:
I[01] ,
I[01] :];
assume
A1: A
=
[:
[.
0 , (1
/ 2).],
[.
0 , 1.]:] & B
=
[:
[.(1
/ 2), 1.],
[.
0 , 1.]:];
((
[#] (
[:
I[01] ,
I[01] :]
| A))
/\ (
[#] (
[:
I[01] ,
I[01] :]
| B)))
= (A
/\ (
[#] (
[:
I[01] ,
I[01] :]
| B))) by
PRE_TOPC:def 5
.= (A
/\ B) by
PRE_TOPC:def 5
.=
[:(
[.
0 , (1
/ 2).]
/\
[.(1
/ 2), 1.]),
[.
0 , 1.]:] by
A1,
ZFMISC_1: 99
.=
[:
{(1
/ 2)},
[.
0 , 1.]:] by
XXREAL_1: 418;
hence thesis;
end;
begin
registration
let T be
TopStruct;
cluster
empty
compact for
Subset of T;
existence
proof
take (
{} T);
thus thesis;
end;
end
theorem ::
BORSUK_6:30
Th30: for T be
TopStruct holds
{} is
empty
compact
Subset of T
proof
let T be
TopStruct;
(
{} T)
c= the
carrier of T;
hence thesis;
end;
theorem ::
BORSUK_6:31
Th31: for T be
TopStruct, a,b be
Real st a
> b holds
[.a, b.] is
empty
compact
Subset of T
proof
let T be
TopStruct, a,b be
Real;
assume a
> b;
then
[.a, b.]
= (
{} T) by
XXREAL_1: 29;
hence thesis;
end;
theorem ::
BORSUK_6:32
for a,b,c,d be
Point of
I[01] holds
[:
[.a, b.],
[.c, d.]:] is
compact
Subset of
[:
I[01] ,
I[01] :]
proof
let a,b,c,d be
Point of
I[01] ;
per cases ;
suppose a
<= b & c
<= d;
hence thesis by
Th9;
end;
suppose a
> b & c
<= d;
then
reconsider A =
[.a, b.] as
empty
Subset of
I[01] by
Th31;
[:A,
[.c, d.]:]
=
{} ;
hence thesis by
Th30;
end;
suppose a
> b & c
> d;
then
reconsider A =
[.c, d.] as
empty
Subset of
I[01] by
Th31;
[:
[.a, b.], A:]
=
{} ;
hence thesis by
Th30;
end;
suppose a
<= b & c
> d;
then
reconsider A =
[.c, d.] as
empty
Subset of
I[01] by
Th31;
[:
[.a, b.], A:]
=
{} ;
hence thesis by
Th30;
end;
end;
begin
definition
let a,b,c,d be
Real;
::
BORSUK_6:def1
func
L[01] (a,b,c,d) ->
Function of (
Closed-Interval-TSpace (a,b)), (
Closed-Interval-TSpace (c,d)) equals ((
L[01] ((
(#) (c,d)),((c,d)
(#) )))
* (
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) ))));
correctness ;
end
theorem ::
BORSUK_6:33
Th33: for a,b,c,d be
Real st a
< b & c
< d holds ((
L[01] (a,b,c,d))
. a)
= c & ((
L[01] (a,b,c,d))
. b)
= d
proof
let a,b,c,d be
Real;
assume that
A1: a
< b and
A2: c
< d;
a
in
[.a, b.] by
A1,
XXREAL_1: 1;
then a
in the
carrier of (
Closed-Interval-TSpace (a,b)) by
A1,
TOPMETR: 18;
then a
in (
dom (
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) )))) by
FUNCT_2:def 1;
hence ((
L[01] (a,b,c,d))
. a)
= ((
L[01] ((
(#) (c,d)),((c,d)
(#) )))
. ((
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) )))
. a)) by
FUNCT_1: 13
.= ((
L[01] ((
(#) (c,d)),((c,d)
(#) )))
. ((
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) )))
. (
(#) (a,b)))) by
A1,
TREAL_1:def 1
.= ((
L[01] ((
(#) (c,d)),((c,d)
(#) )))
. (
(#) (
0 ,1))) by
A1,
TREAL_1: 13
.= (
(#) (c,d)) by
A2,
TREAL_1: 9
.= c by
A2,
TREAL_1:def 1;
b
in
[.a, b.] by
A1,
XXREAL_1: 1;
then b
in the
carrier of (
Closed-Interval-TSpace (a,b)) by
A1,
TOPMETR: 18;
then b
in (
dom (
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) )))) by
FUNCT_2:def 1;
hence ((
L[01] (a,b,c,d))
. b)
= ((
L[01] ((
(#) (c,d)),((c,d)
(#) )))
. ((
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) )))
. b)) by
FUNCT_1: 13
.= ((
L[01] ((
(#) (c,d)),((c,d)
(#) )))
. ((
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) )))
. ((a,b)
(#) ))) by
A1,
TREAL_1:def 2
.= ((
L[01] ((
(#) (c,d)),((c,d)
(#) )))
. ((
0 ,1)
(#) )) by
A1,
TREAL_1: 13
.= ((c,d)
(#) ) by
A2,
TREAL_1: 9
.= d by
A2,
TREAL_1:def 2;
end;
theorem ::
BORSUK_6:34
Th34: for a,b,c,d be
Real st a
< b & c
<= d holds (
L[01] (a,b,c,d)) is
continuous
Function of (
Closed-Interval-TSpace (a,b)), (
Closed-Interval-TSpace (c,d))
proof
let a,b,c,d be
Real;
assume a
< b & c
<= d;
then (
L[01] ((
(#) (c,d)),((c,d)
(#) ))) is
continuous
Function of (
Closed-Interval-TSpace (
0 ,1)), (
Closed-Interval-TSpace (c,d)) & (
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) ))) is
continuous
Function of (
Closed-Interval-TSpace (a,b)), (
Closed-Interval-TSpace (
0 ,1)) by
TREAL_1: 8,
TREAL_1: 12;
hence thesis;
end;
theorem ::
BORSUK_6:35
Th35: for a,b,c,d be
Real st a
< b & c
<= d holds for x be
Real st a
<= x & x
<= b holds ((
L[01] (a,b,c,d))
. x)
= ((((d
- c)
/ (b
- a))
* (x
- a))
+ c)
proof
A1:
0
= (
(#) (
0 ,1)) & 1
= ((
0 ,1)
(#) ) by
TREAL_1:def 1,
TREAL_1:def 2;
let a,b,c,d be
Real;
assume
A2: a
< b;
set G = (
P[01] (a,b,(
(#) (
0 ,1)),((
0 ,1)
(#) )));
set F = (
L[01] ((
(#) (c,d)),((c,d)
(#) )));
set f = (
L[01] (a,b,c,d));
assume
A3: c
<= d;
then
A4: (
(#) (c,d))
= c & ((c,d)
(#) )
= d by
TREAL_1:def 1,
TREAL_1:def 2;
let x be
Real;
assume
A5: a
<= x;
set X = ((x
- a)
/ (b
- a));
assume
A6: x
<= b;
then
A7: X
in the
carrier of (
Closed-Interval-TSpace (
0 ,1)) by
A5,
Th2;
x
in
[.a, b.] by
A5,
A6,
XXREAL_1: 1;
then
A8: x
in the
carrier of (
Closed-Interval-TSpace (a,b)) by
A2,
TOPMETR: 18;
then x
in (
dom G) by
FUNCT_2:def 1;
then (f
. x)
= (F
. (G
. x)) by
FUNCT_1: 13
.= (F
. ((((b
- x)
*
0 )
+ ((x
- a)
* 1))
/ (b
- a))) by
A2,
A8,
A1,
TREAL_1:def 4
.= (((1
- X)
* c)
+ (X
* d)) by
A3,
A4,
A7,
TREAL_1:def 3
.= ((((d
- c)
/ (b
- a))
* (x
- a))
+ c) by
XCMPLX_1: 234;
hence thesis;
end;
theorem ::
BORSUK_6:36
Th36: for f1,f2 be
Function of
[:
I[01] ,
I[01] :],
I[01] st f1 is
continuous & f2 is
continuous & (for p be
Point of
[:
I[01] ,
I[01] :] holds ((f1
. p)
* (f2
. p)) is
Point of
I[01] ) holds ex g be
Function of
[:
I[01] ,
I[01] :],
I[01] st (for p be
Point of
[:
I[01] ,
I[01] :], r1,r2 be
Real st (f1
. p)
= r1 & (f2
. p)
= r2 holds (g
. p)
= (r1
* r2)) & g is
continuous
proof
reconsider A =
[.
0 , 1.] as non
empty
Subset of
R^1 by
TOPMETR: 17,
XXREAL_1: 1;
set X =
[:
I[01] ,
I[01] :];
let f1,f2 be
Function of
[:
I[01] ,
I[01] :],
I[01] ;
assume that
A1: f1 is
continuous & f2 is
continuous and
A2: for p be
Point of
[:
I[01] ,
I[01] :] holds ((f1
. p)
* (f2
. p)) is
Point of
I[01] ;
reconsider f19 = f1, f29 = f2 as
Function of X,
R^1 by
BORSUK_1: 40,
FUNCT_2: 7,
TOPMETR: 17;
f19 is
continuous & f29 is
continuous by
A1,
PRE_TOPC: 26;
then
consider g be
Function of X,
R^1 such that
A3: for p be
Point of X, r1,r2 be
Real st (f19
. p)
= r1 & (f29
. p)
= r2 holds (g
. p)
= (r1
* r2) and
A4: g is
continuous by
JGRAPH_2: 25;
A5: (
rng g)
c=
[.
0 , 1.]
proof
let x be
object;
assume x
in (
rng g);
then
consider y be
object such that
A6: y
in (
dom g) and
A7: x
= (g
. y) by
FUNCT_1:def 3;
reconsider y as
Point of X by
A6;
(g
. y)
= ((f1
. y)
* (f2
. y)) by
A3;
then (g
. y) is
Point of
I[01] by
A2;
hence thesis by
A7,
BORSUK_1: 40;
end;
[.
0 , 1.]
= the
carrier of (
R^1
| A) & (
dom g)
= the
carrier of X by
FUNCT_2:def 1,
PRE_TOPC: 8;
then
reconsider g as
Function of X, (
R^1
| A) by
A5,
FUNCT_2: 2;
(
R^1
| A)
=
I[01] by
BORSUK_1:def 13,
TOPMETR:def 6;
then
reconsider g as
continuous
Function of X,
I[01] by
A4,
JGRAPH_1: 45;
take g;
thus thesis by
A3;
end;
theorem ::
BORSUK_6:37
Th37: for f1,f2 be
Function of
[:
I[01] ,
I[01] :],
I[01] st f1 is
continuous & f2 is
continuous & (for p be
Point of
[:
I[01] ,
I[01] :] holds ((f1
. p)
+ (f2
. p)) is
Point of
I[01] ) holds ex g be
Function of
[:
I[01] ,
I[01] :],
I[01] st (for p be
Point of
[:
I[01] ,
I[01] :], r1,r2 be
Real st (f1
. p)
= r1 & (f2
. p)
= r2 holds (g
. p)
= (r1
+ r2)) & g is
continuous
proof
reconsider A =
[.
0 , 1.] as non
empty
Subset of
R^1 by
TOPMETR: 17,
XXREAL_1: 1;
set X =
[:
I[01] ,
I[01] :];
let f1,f2 be
Function of
[:
I[01] ,
I[01] :],
I[01] ;
assume that
A1: f1 is
continuous & f2 is
continuous and
A2: for p be
Point of
[:
I[01] ,
I[01] :] holds ((f1
. p)
+ (f2
. p)) is
Point of
I[01] ;
reconsider f19 = f1, f29 = f2 as
Function of X,
R^1 by
BORSUK_1: 40,
FUNCT_2: 7,
TOPMETR: 17;
f19 is
continuous & f29 is
continuous by
A1,
PRE_TOPC: 26;
then
consider g be
Function of X,
R^1 such that
A3: for p be
Point of X, r1,r2 be
Real st (f19
. p)
= r1 & (f29
. p)
= r2 holds (g
. p)
= (r1
+ r2) and
A4: g is
continuous by
JGRAPH_2: 19;
A5: (
rng g)
c=
[.
0 , 1.]
proof
let x be
object;
assume x
in (
rng g);
then
consider y be
object such that
A6: y
in (
dom g) and
A7: x
= (g
. y) by
FUNCT_1:def 3;
reconsider y as
Point of X by
A6;
(g
. y)
= ((f1
. y)
+ (f2
. y)) by
A3;
then (g
. y) is
Point of
I[01] by
A2;
hence thesis by
A7,
BORSUK_1: 40;
end;
[.
0 , 1.]
= the
carrier of (
R^1
| A) & (
dom g)
= the
carrier of X by
FUNCT_2:def 1,
PRE_TOPC: 8;
then
reconsider g as
Function of X, (
R^1
| A) by
A5,
FUNCT_2: 2;
(
R^1
| A)
=
I[01] by
BORSUK_1:def 13,
TOPMETR:def 6;
then
reconsider g as
continuous
Function of X,
I[01] by
A4,
JGRAPH_1: 45;
take g;
thus thesis by
A3;
end;
theorem ::
BORSUK_6:38
for f1,f2 be
Function of
[:
I[01] ,
I[01] :],
I[01] st f1 is
continuous & f2 is
continuous & (for p be
Point of
[:
I[01] ,
I[01] :] holds ((f1
. p)
- (f2
. p)) is
Point of
I[01] ) holds ex g be
Function of
[:
I[01] ,
I[01] :],
I[01] st (for p be
Point of
[:
I[01] ,
I[01] :], r1,r2 be
Real st (f1
. p)
= r1 & (f2
. p)
= r2 holds (g
. p)
= (r1
- r2)) & g is
continuous
proof
reconsider A =
[.
0 , 1.] as non
empty
Subset of
R^1 by
TOPMETR: 17,
XXREAL_1: 1;
set X =
[:
I[01] ,
I[01] :];
let f1,f2 be
Function of
[:
I[01] ,
I[01] :],
I[01] ;
assume that
A1: f1 is
continuous & f2 is
continuous and
A2: for p be
Point of
[:
I[01] ,
I[01] :] holds ((f1
. p)
- (f2
. p)) is
Point of
I[01] ;
reconsider f19 = f1, f29 = f2 as
Function of X,
R^1 by
BORSUK_1: 40,
FUNCT_2: 7,
TOPMETR: 17;
f19 is
continuous & f29 is
continuous by
A1,
PRE_TOPC: 26;
then
consider g be
Function of X,
R^1 such that
A3: for p be
Point of X, r1,r2 be
Real st (f19
. p)
= r1 & (f29
. p)
= r2 holds (g
. p)
= (r1
- r2) and
A4: g is
continuous by
JGRAPH_2: 21;
A5: (
rng g)
c=
[.
0 , 1.]
proof
let x be
object;
assume x
in (
rng g);
then
consider y be
object such that
A6: y
in (
dom g) and
A7: x
= (g
. y) by
FUNCT_1:def 3;
reconsider y as
Point of X by
A6;
(g
. y)
= ((f1
. y)
- (f2
. y)) by
A3;
then (g
. y) is
Point of
I[01] by
A2;
hence thesis by
A7,
BORSUK_1: 40;
end;
[.
0 , 1.]
= the
carrier of (
R^1
| A) & (
dom g)
= the
carrier of X by
FUNCT_2:def 1,
PRE_TOPC: 8;
then
reconsider g as
Function of X, (
R^1
| A) by
A5,
FUNCT_2: 2;
(
R^1
| A)
=
I[01] by
BORSUK_1:def 13,
TOPMETR:def 6;
then
reconsider g as
continuous
Function of X,
I[01] by
A4,
JGRAPH_1: 45;
take g;
thus thesis by
A3;
end;
begin
reserve T for non
empty
TopSpace,
a,b,c,d for
Point of T;
theorem ::
BORSUK_6:39
Th39: for P be
Path of a, b st P is
continuous holds (P
* (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1))))) is
continuous
Function of
I[01] , T
proof
reconsider g = (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1)))) as
Function of
I[01] ,
I[01] by
TOPMETR: 20;
let P be
Path of a, b such that
A1: P is
continuous;
reconsider f = (P
* g) as
Function of
I[01] , T;
g is
continuous by
TOPMETR: 20,
TREAL_1: 8;
then f is
continuous by
A1;
hence thesis;
end;
theorem ::
BORSUK_6:40
Th40: for X be non
empty
TopStruct, a,b be
Point of X, P be
Path of a, b st (P
.
0 )
= a & (P
. 1)
= b holds ((P
* (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1)))))
.
0 )
= b & ((P
* (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1)))))
. 1)
= a
proof
A1:
0
in
[.
0 , 1.] by
XXREAL_1: 1;
set e = (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1))));
let X be non
empty
TopStruct, a,b be
Point of X;
let P be
Path of a, b such that
A2: (P
.
0 )
= a and
A3: (P
. 1)
= b;
A4: the
carrier of (
Closed-Interval-TSpace (
0 ,1))
=
[.
0 , 1.] by
TOPMETR: 18;
(e
.
0 )
= (e
. (
(#) (
0 ,1))) by
TREAL_1:def 1
.= ((
0 ,1)
(#) ) by
TREAL_1: 9
.= 1 by
TREAL_1:def 2;
hence ((P
* e)
.
0 )
= b by
A3,
A4,
A1,
FUNCT_2: 15;
A5: 1
in
[.
0 , 1.] by
XXREAL_1: 1;
(e
. 1)
= (e
. ((
0 ,1)
(#) )) by
TREAL_1:def 2
.= (
(#) (
0 ,1)) by
TREAL_1: 9
.=
0 by
TREAL_1:def 1;
hence thesis by
A2,
A4,
A5,
FUNCT_2: 15;
end;
theorem ::
BORSUK_6:41
Th41: for P be
Path of a, b st P is
continuous & (P
.
0 )
= a & (P
. 1)
= b holds (
- P) is
continuous & ((
- P)
.
0 )
= b & ((
- P)
. 1)
= a
proof
let P be
Path of a, b such that
A1: P is
continuous and
A2: (P
.
0 )
= a & (P
. 1)
= b;
A3: ((P
* (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1)))))
. 1)
= a by
A2,
Th40;
(P
* (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1))))) is
continuous
Function of
I[01] , T & ((P
* (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1)))))
.
0 )
= b by
A1,
A2,
Th39,
Th40;
then (b,a)
are_connected by
A3;
hence thesis by
BORSUK_2:def 2;
end;
definition
let T be non
empty
TopSpace, a,b be
Point of T;
:: original:
are_connected
redefine
pred a,b
are_connected ;
reflexivity
proof
let a be
Point of T;
thus (a,a)
are_connected ;
end;
symmetry
proof
let a,b be
Point of T;
set P = the
Path of a, b;
assume
A1: (a,b)
are_connected ;
then
A2: (P
. 1)
= b by
BORSUK_2:def 2;
take (
- P);
P is
continuous & (P
.
0 )
= a by
A1,
BORSUK_2:def 2;
hence thesis by
A2,
Th41;
end;
end
theorem ::
BORSUK_6:42
Th42: (a,b)
are_connected & (b,c)
are_connected implies (a,c)
are_connected
proof
assume that
A1: (a,b)
are_connected and
A2: (b,c)
are_connected ;
set P = the
Path of a, b, R = the
Path of b, c;
A3: P is
continuous & (P
.
0 )
= a by
A1,
BORSUK_2:def 2;
take (P
+ R);
A4: (R
.
0 )
= b & (R
. 1)
= c by
A2,
BORSUK_2:def 2;
(P
. 1)
= b & R is
continuous by
A1,
A2,
BORSUK_2:def 2;
hence thesis by
A3,
A4,
BORSUK_2: 14;
end;
theorem ::
BORSUK_6:43
Th43: (a,b)
are_connected implies for A be
Path of a, b holds A
= (
- (
- A))
proof
set I = the
carrier of
I[01] ;
assume
A1: (a,b)
are_connected ;
let A be
Path of a, b;
for x be
Element of I holds (A
. x)
= ((
- (
- A))
. x)
proof
let x be
Element of I;
reconsider z = (1
- x) as
Point of
I[01] by
JORDAN5B: 4;
thus ((
- (
- A))
. x)
= ((
- A)
. (1
- x)) by
A1,
BORSUK_2:def 6
.= (A
. (1
- z)) by
A1,
BORSUK_2:def 6
.= (A
. x);
end;
hence thesis by
FUNCT_2: 63;
end;
theorem ::
BORSUK_6:44
for T be non
empty
pathwise_connected
TopSpace, a,b be
Point of T holds for A be
Path of a, b holds A
= (
- (
- A)) by
Th43,
BORSUK_2:def 3;
begin
definition
let T be non
empty
pathwise_connected
TopSpace;
let a,b,c be
Point of T;
let P be
Path of a, b, Q be
Path of b, c;
:: original:
+
redefine
::
BORSUK_6:def2
func P
+ Q means for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (it
. t)
= (P
. (2
* t))) & ((1
/ 2)
<= t implies (it
. t)
= (Q
. ((2
* t)
- 1)));
compatibility
proof
let X be
Path of a, c;
(a,b)
are_connected & (b,c)
are_connected by
BORSUK_2:def 3;
hence thesis by
BORSUK_2:def 5;
end;
end
definition
let T be non
empty
pathwise_connected
TopSpace;
let a,b be
Point of T;
let P be
Path of a, b;
:: original:
-
redefine
::
BORSUK_6:def3
func
- P means
:
Def3: for t be
Point of
I[01] holds (it
. t)
= (P
. (1
- t));
compatibility
proof
let X be
Path of b, a;
(b,a)
are_connected by
BORSUK_2:def 3;
hence thesis by
BORSUK_2:def 6;
end;
end
begin
definition
let T be non
empty
TopSpace, a,b be
Point of T;
let P be
Path of a, b;
let f be
continuous
Function of
I[01] ,
I[01] ;
assume that
A1: (f
.
0 )
=
0 and
A2: (f
. 1)
= 1 and
A3: (a,b)
are_connected ;
::
BORSUK_6:def4
func
RePar (P,f) ->
Path of a, b equals
:
Def4: (P
* f);
coherence
proof
set PF = (P
* f);
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
0
in (
dom f) by
FUNCT_2:def 1;
then
A4: (PF
.
0 )
= (P
. (f
.
0 )) by
FUNCT_1: 13
.= a by
A1,
A3,
BORSUK_2:def 2;
1
in the
carrier of
I[01] by
BORSUK_1: 43;
then 1
in (
dom f) by
FUNCT_2:def 1;
then
A5: (PF
. 1)
= (P
. (f
. 1)) by
FUNCT_1: 13
.= b by
A2,
A3,
BORSUK_2:def 2;
P is
continuous by
A3,
BORSUK_2:def 2;
hence thesis by
A3,
A4,
A5,
BORSUK_2:def 2;
end;
end
theorem ::
BORSUK_6:45
Th45: for P be
Path of a, b, f be
continuous
Function of
I[01] ,
I[01] st (f
.
0 )
=
0 & (f
. 1)
= 1 & (a,b)
are_connected holds ((
RePar (P,f)),P)
are_homotopic
proof
set X =
[:
I[01] ,
I[01] :];
reconsider G2 = (
pr2 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of X,
I[01] by
YELLOW12: 40;
reconsider F2 = (
pr1 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of X,
I[01] by
YELLOW12: 39;
reconsider f3 = (
pr1 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of X,
I[01] by
YELLOW12: 39;
reconsider f4 = (
pr2 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of X,
I[01] by
YELLOW12: 40;
reconsider ID = (
id
I[01] ) as
Path of
0[01] ,
1[01] by
Th8;
let P be
Path of a, b, f be
continuous
Function of
I[01] ,
I[01] ;
assume that
A1: (f
.
0 )
=
0 and
A2: (f
. 1)
= 1 and
A3: (a,b)
are_connected ;
reconsider f2 = (f
* F2) as
continuous
Function of X,
I[01] ;
set G1 = (
- ID);
reconsider f1 = (G1
* G2) as
continuous
Function of X,
I[01] ;
A4: for s,t be
Point of
I[01] holds (f1
.
[s, t])
= (1
- t)
proof
let s,t be
Point of
I[01] ;
A5: (1
- t)
in the
carrier of
I[01] by
JORDAN5B: 4;
[s, t]
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
ZFMISC_1: 87;
then
[s, t]
in (
dom G2) by
FUNCT_2:def 1;
then (f1
.
[s, t])
= (G1
. (G2
. (s,t))) by
FUNCT_1: 13
.= (G1
. t) by
FUNCT_3:def 5
.= (ID
. (1
- t)) by
Def3
.= (1
- t) by
A5,
FUNCT_1: 18;
hence thesis;
end;
for p be
Point of X holds ((f3
. p)
* (f4
. p)) is
Point of
I[01] by
Th5;
then
consider g2 be
Function of X,
I[01] such that
A6: for p be
Point of X, r1,r2 be
Real st (f3
. p)
= r1 & (f4
. p)
= r2 holds (g2
. p)
= (r1
* r2) and
A7: g2 is
continuous by
Th36;
for p be
Point of X holds ((f1
. p)
* (f2
. p)) is
Point of
I[01] by
Th5;
then
consider g1 be
Function of X,
I[01] such that
A8: for p be
Point of X, r1,r2 be
Real st (f1
. p)
= r1 & (f2
. p)
= r2 holds (g1
. p)
= (r1
* r2) and
A9: g1 is
continuous by
Th36;
A10: for s,t be
Point of
I[01] holds (f2
. (s,t))
= (f
. s)
proof
let s,t be
Point of
I[01] ;
[s, t]
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
ZFMISC_1: 87;
then
[s, t]
in (
dom F2) by
FUNCT_2:def 1;
hence (f2
. (s,t))
= (f
. (F2
. (s,t))) by
FUNCT_1: 13
.= (f
. s) by
FUNCT_3:def 4;
end;
A11: for t,s be
Point of
I[01] holds (g1
.
[s, t])
= ((1
- t)
* (f
. s))
proof
let t,s be
Point of
I[01] ;
(f1
. (s,t))
= (1
- t) & (f2
. (s,t))
= (f
. s) by
A4,
A10;
hence thesis by
A8;
end;
A12: for t,s be
Point of
I[01] holds (g2
.
[s, t])
= (t
* s)
proof
let t,s be
Point of
I[01] ;
(f3
. (s,t))
= s & (f4
. (s,t))
= t by
FUNCT_3:def 4,
FUNCT_3:def 5;
hence thesis by
A6;
end;
for p be
Point of X holds ((g1
. p)
+ (g2
. p)) is
Point of
I[01]
proof
let p be
Point of X;
p
in the
carrier of
[:
I[01] ,
I[01] :];
then p
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
consider s,t be
object such that
A13: s
in the
carrier of
I[01] & t
in the
carrier of
I[01] and
A14: p
=
[s, t] by
ZFMISC_1:def 2;
reconsider s, t as
Point of
I[01] by
A13;
set a = (f
. s);
per cases ;
suppose
A15: (f
. s)
<= s;
A16: s
<= 1 by
BORSUK_1: 40,
XXREAL_1: 1;
A17: t
<= 1 by
BORSUK_1: 40,
XXREAL_1: 1;
then (((1
- t)
* a)
+ (t
* s))
<= s by
A15,
XREAL_1: 172;
then
A18:
0
<= a & (((1
- t)
* a)
+ (t
* s))
<= 1 by
A16,
BORSUK_1: 40,
XXREAL_0: 2,
XXREAL_1: 1;
0
<= t by
BORSUK_1: 40,
XXREAL_1: 1;
then
A19: a
<= (((1
- t)
* a)
+ (t
* s)) by
A15,
A17,
XREAL_1: 173;
((g1
. p)
+ (g2
. p))
= (((1
- t)
* (f
. s))
+ (g2
. p)) by
A11,
A14
.= (((1
- t)
* (f
. s))
+ (t
* s)) by
A12,
A14;
hence thesis by
A19,
A18,
BORSUK_1: 40,
XXREAL_1: 1;
end;
suppose
A20: a
> s;
set j = (1
- t);
A21: a
<= 1 by
BORSUK_1: 40,
XXREAL_1: 1;
A22: j
in the
carrier of
I[01] by
JORDAN5B: 4;
then
A23: j
<= 1 by
BORSUK_1: 43;
then (((1
- j)
* s)
+ (j
* a))
<= a by
A20,
XREAL_1: 172;
then
A24:
0
<= s & (((1
- t)
* a)
+ (t
* s))
<= 1 by
A21,
BORSUK_1: 40,
XXREAL_0: 2,
XXREAL_1: 1;
0
<= j by
A22,
BORSUK_1: 43;
then
A25: s
<= (((1
- j)
* s)
+ (j
* a)) by
A20,
A23,
XREAL_1: 173;
((g1
. p)
+ (g2
. p))
= (((1
- t)
* (f
. s))
+ (g2
. p)) by
A11,
A14
.= (((1
- t)
* (f
. s))
+ (t
* s)) by
A12,
A14;
hence thesis by
A25,
A24,
BORSUK_1: 40,
XXREAL_1: 1;
end;
end;
then
consider h be
Function of X,
I[01] such that
A26: for p be
Point of X, r1,r2 be
Real st (g1
. p)
= r1 & (g2
. p)
= r2 holds (h
. p)
= (r1
+ r2) and
A27: h is
continuous by
A9,
A7,
Th37;
A28: for t,s be
Point of
I[01] holds (h
.
[s, t])
= (((1
- t)
* (f
. s))
+ (t
* s))
proof
let t,s be
Point of
I[01] ;
(g1
.
[s, t])
= ((1
- t)
* (f
. s)) & (g2
.
[s, t])
= (t
* s) by
A11,
A12;
hence thesis by
A26;
end;
A29: for t be
Point of
I[01] holds (h
.
[1, t])
= 1
proof
reconsider oo = 1 as
Point of
I[01] by
BORSUK_1: 43;
let t be
Point of
I[01] ;
thus (h
.
[1, t])
= (((1
- t)
* (f
. oo))
+ (t
* 1)) by
A28
.= 1 by
A2;
end;
set H = (P
* h);
A30: (
dom h)
= the
carrier of
[:
I[01] ,
I[01] :] by
FUNCT_2:def 1
.=
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
set Q = (
RePar (P,f));
A31: 1 is
Point of
I[01] by
BORSUK_1: 43;
A32: for s be
Point of
I[01] holds (h
.
[s, 1])
= s
proof
let s be
Point of
I[01] ;
thus (h
.
[s, 1])
= (((1
- 1)
* (f
. s))
+ (1
* s)) by
A31,
A28
.= s;
end;
A33:
0 is
Point of
I[01] by
BORSUK_1: 43;
A34: for s be
Point of
I[01] holds (h
.
[s,
0 ])
= (f
. s)
proof
let s be
Point of
I[01] ;
thus (h
.
[s,
0 ])
= (((1
-
0 )
* (f
. s))
+ (
0
* s)) by
A33,
A28
.= (f
. s);
end;
A35: for s be
Point of
I[01] holds (H
. (s,
0 ))
= (Q
. s) & (H
. (s,1))
= (P
. s)
proof
let s be
Point of
I[01] ;
s
in the
carrier of
I[01] ;
then
A36: s
in (
dom f) by
FUNCT_2:def 1;
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
[s,
0 ]
in (
dom h) by
A30,
ZFMISC_1: 87;
hence (H
. (s,
0 ))
= (P
. (h
.
[s,
0 ])) by
FUNCT_1: 13
.= (P
. (f
. s)) by
A34
.= ((P
* f)
. s) by
A36,
FUNCT_1: 13
.= (Q
. s) by
A1,
A2,
A3,
Def4;
1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
[s, 1]
in (
dom h) by
A30,
ZFMISC_1: 87;
hence (H
. (s,1))
= (P
. (h
.
[s, 1])) by
FUNCT_1: 13
.= (P
. s) by
A32;
end;
A37: for t be
Point of
I[01] holds (h
.
[
0 , t])
=
0
proof
reconsider oo =
0 as
Point of
I[01] by
BORSUK_1: 43;
let t be
Point of
I[01] ;
thus (h
.
[
0 , t])
= (((1
- t)
* (f
. oo))
+ (t
*
0 )) by
A28
.=
0 by
A1;
end;
A38: for t be
Point of
I[01] holds (H
. (
0 ,t))
= a & (H
. (1,t))
= b
proof
let t be
Point of
I[01] ;
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
[
0 , t]
in (
dom h) by
A30,
ZFMISC_1: 87;
hence (H
. (
0 ,t))
= (P
. (h
.
[
0 , t])) by
FUNCT_1: 13
.= (P
.
0 ) by
A37
.= a by
A3,
BORSUK_2:def 2;
1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
[1, t]
in (
dom h) by
A30,
ZFMISC_1: 87;
hence (H
. (1,t))
= (P
. (h
.
[1, t])) by
FUNCT_1: 13
.= (P
. 1) by
A29
.= b by
A3,
BORSUK_2:def 2;
end;
P is
continuous by
A3,
BORSUK_2:def 2;
hence thesis by
A27,
A35,
A38;
end;
theorem ::
BORSUK_6:46
for T be non
empty
pathwise_connected
TopSpace, a,b be
Point of T, P be
Path of a, b, f be
continuous
Function of
I[01] ,
I[01] st (f
.
0 )
=
0 & (f
. 1)
= 1 holds ((
RePar (P,f)),P)
are_homotopic by
Th45,
BORSUK_2:def 3;
definition
::
BORSUK_6:def5
func
1RP ->
Function of
I[01] ,
I[01] means
:
Def5: for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (it
. t)
= (2
* t)) & (t
> (1
/ 2) implies (it
. t)
= 1);
existence
proof
deffunc
G(
set) = 1;
deffunc
F(
Real) = (2
* $1);
defpred
P[
Real] means $1
<= (1
/ 2);
consider f be
Function such that
A1: (
dom f)
= the
carrier of
I[01] & for x be
Element of
I[01] holds (
P[x] implies (f
. x)
=
F(x)) & ( not
P[x] implies (f
. x)
=
G(x)) from
PARTFUN1:sch 4;
for x be
object st x
in the
carrier of
I[01] holds (f
. x)
in the
carrier of
I[01]
proof
let x be
object;
assume x
in the
carrier of
I[01] ;
then
reconsider x as
Point of
I[01] ;
per cases ;
suppose
A2:
P[x];
then (f
. x)
= (2
* x) by
A1;
then (f
. x) is
Point of
I[01] by
A2,
Th3;
hence thesis;
end;
suppose not
P[x];
then (f
. x)
=
G(x) by
A1;
hence thesis by
BORSUK_1: 43;
end;
end;
then
reconsider f as
Function of
I[01] ,
I[01] by
A1,
FUNCT_2: 3;
for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (f
. t)
= (2
* t)) & (t
> (1
/ 2) implies (f
. t)
= 1) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of
I[01] ,
I[01] ;
assume that
A3: for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (f1
. t)
= (2
* t)) & (t
> (1
/ 2) implies (f1
. t)
= 1) and
A4: for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (f2
. t)
= (2
* t)) & (t
> (1
/ 2) implies (f2
. t)
= 1);
for t be
Point of
I[01] holds (f1
. t)
= (f2
. t)
proof
let t be
Point of
I[01] ;
per cases ;
suppose
A5: t
<= (1
/ 2);
then (f1
. t)
= (2
* t) by
A3
.= (f2
. t) by
A4,
A5;
hence thesis;
end;
suppose
A6: t
> (1
/ 2);
then (f1
. t)
= 1 by
A3
.= (f2
. t) by
A4,
A6;
hence thesis;
end;
end;
hence thesis by
FUNCT_2: 63;
end;
end
registration
cluster
1RP ->
continuous;
coherence
proof
A1: (1
/ 2) is
Point of
I[01] by
BORSUK_1: 43;
1 is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider B =
[.(1
/ 2), 1.] as non
empty
compact
Subset of
I[01] by
A1,
BORSUK_4: 24;
0 is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider A =
[.
0 , (1
/ 2).] as non
empty
compact
Subset of
I[01] by
A1,
BORSUK_4: 24;
set T1 = (
I[01]
| A), T2 = (
I[01]
| B), T =
I[01] ;
reconsider g = (T2
-->
1[01] ) as
continuous
Function of T2,
I[01] ;
T1
= (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
TOPMETR: 24;
then
reconsider f = (
L[01] (
0 ,(1
/ 2),
0 ,1)) as
continuous
Function of T1,
I[01] by
Th34,
TOPMETR: 20;
A2: for p be
set st p
in ((
[#] T1)
/\ (
[#] T2)) holds (f
. p)
= (g
. p)
proof
let p be
set;
assume p
in ((
[#] T1)
/\ (
[#] T2));
then p
in (
[.
0 , (1
/ 2).]
/\ (
[#] T2)) by
PRE_TOPC:def 5;
then p
in (
[.
0 , (1
/ 2).]
/\
[.(1
/ 2), 1.]) by
PRE_TOPC:def 5;
then p
in
{(1
/ 2)} by
XXREAL_1: 418;
then
A3: p
= (1
/ 2) by
TARSKI:def 1;
then p
in
[.(1
/ 2), 1.] by
XXREAL_1: 1;
then
A4: p
in the
carrier of T2 by
PRE_TOPC: 8;
(f
. p)
= ((((1
-
0 )
/ ((1
/ 2)
-
0 ))
* ((1
/ 2)
-
0 ))
+
0 ) by
A3,
Th35
.= (g
. p) by
A4,
BORSUK_1:def 15,
FUNCOP_1: 7;
hence thesis;
end;
A5: for x be
Element of
I[01] holds (
1RP
. x)
= ((f
+* g)
. x)
proof
let x be
Element of
I[01] ;
A6: (
dom g)
= the
carrier of T2 by
FUNCT_2:def 1
.=
[.(1
/ 2), 1.] by
PRE_TOPC: 8;
per cases by
XXREAL_0: 1;
suppose
A7: x
< (1
/ 2);
0
<= x by
BORSUK_1: 43;
then
A8: (f
. x)
= ((((1
-
0 )
/ ((1
/ 2)
-
0 ))
* (x
-
0 ))
+
0 ) by
A7,
Th35
.= ((1
/ (1
/ 2))
* x);
A9: not x
in (
dom g) by
A6,
A7,
XXREAL_1: 1;
thus (
1RP
. x)
= (2
* x) by
A7,
Def5
.= ((f
+* g)
. x) by
A9,
A8,
FUNCT_4: 11;
end;
suppose
A10: x
= (1
/ 2);
then
A11: x
in (
dom g) by
A6,
XXREAL_1: 1;
thus (
1RP
. x)
= (2
* (1
/ 2)) by
A10,
Def5
.= (g
. x) by
A11,
BORSUK_1:def 15,
FUNCOP_1: 7
.= ((f
+* g)
. x) by
A11,
FUNCT_4: 13;
end;
suppose
A12: x
> (1
/ 2);
x
<= 1 by
BORSUK_1: 43;
then
A13: x
in (
dom g) by
A6,
A12,
XXREAL_1: 1;
thus (
1RP
. x)
= 1 by
A12,
Def5
.= (g
. x) by
A13,
BORSUK_1:def 15,
FUNCOP_1: 7
.= ((f
+* g)
. x) by
A13,
FUNCT_4: 13;
end;
end;
((
[#] T1)
\/ (
[#] T2))
= (
[.
0 , (1
/ 2).]
\/ (
[#] T2)) by
PRE_TOPC:def 5
.= (
[.
0 , (1
/ 2).]
\/
[.(1
/ 2), 1.]) by
PRE_TOPC:def 5
.= (
[#] T) by
BORSUK_1: 40,
XXREAL_1: 174;
then ex h be
Function of
I[01] ,
I[01] st h
= (f
+* g) & h is
continuous by
A2,
BORSUK_2: 1;
hence thesis by
A5,
FUNCT_2: 63;
end;
end
theorem ::
BORSUK_6:47
Th47: (
1RP
.
0 )
=
0 & (
1RP
. 1)
= 1
proof
reconsider x =
0 , y = 1 as
Point of
I[01] by
BORSUK_1: 43;
thus (
1RP
.
0 )
= (2
* x) by
Def5
.=
0 ;
thus (
1RP
. 1)
= (
1RP
. y)
.= 1 by
Def5;
end;
definition
::
BORSUK_6:def6
func
2RP ->
Function of
I[01] ,
I[01] means
:
Def6: for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (it
. t)
=
0 ) & (t
> (1
/ 2) implies (it
. t)
= ((2
* t)
- 1));
existence
proof
deffunc
F(
set) =
0 ;
deffunc
G(
Real) = ((2
* $1)
- 1);
defpred
P[
Real] means $1
<= (1
/ 2);
consider f be
Function such that
A1: (
dom f)
= the
carrier of
I[01] & for x be
Element of
I[01] holds (
P[x] implies (f
. x)
=
F(x)) & ( not
P[x] implies (f
. x)
=
G(x)) from
PARTFUN1:sch 4;
for x be
object st x
in the
carrier of
I[01] holds (f
. x)
in the
carrier of
I[01]
proof
let x be
object;
assume x
in the
carrier of
I[01] ;
then
reconsider x as
Point of
I[01] ;
per cases ;
suppose
P[x];
then (f
. x)
=
0 by
A1;
hence thesis by
BORSUK_1: 43;
end;
suppose
A2: not
P[x];
then (f
. x)
=
G(x) by
A1;
then (f
. x) is
Point of
I[01] by
A2,
Th4;
hence thesis;
end;
end;
then
reconsider f as
Function of
I[01] ,
I[01] by
A1,
FUNCT_2: 3;
for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (f
. t)
=
0 ) & (t
> (1
/ 2) implies (f
. t)
= ((2
* t)
- 1)) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of
I[01] ,
I[01] ;
assume that
A3: for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (f1
. t)
=
0 ) & (t
> (1
/ 2) implies (f1
. t)
= ((2
* t)
- 1)) and
A4: for t be
Point of
I[01] holds (t
<= (1
/ 2) implies (f2
. t)
=
0 ) & (t
> (1
/ 2) implies (f2
. t)
= ((2
* t)
- 1));
for t be
Point of
I[01] holds (f1
. t)
= (f2
. t)
proof
let t be
Point of
I[01] ;
per cases ;
suppose
A5: t
<= (1
/ 2);
then (f1
. t)
=
0 by
A3
.= (f2
. t) by
A4,
A5;
hence thesis;
end;
suppose
A6: t
> (1
/ 2);
then (f1
. t)
= ((2
* t)
- 1) by
A3
.= (f2
. t) by
A4,
A6;
hence thesis;
end;
end;
hence thesis by
FUNCT_2: 63;
end;
end
registration
cluster
2RP ->
continuous;
coherence
proof
A1: (1
/ 2) is
Point of
I[01] by
BORSUK_1: 43;
1 is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider B =
[.(1
/ 2), 1.] as non
empty
compact
Subset of
I[01] by
A1,
BORSUK_4: 24;
0 is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider A =
[.
0 , (1
/ 2).] as non
empty
compact
Subset of
I[01] by
A1,
BORSUK_4: 24;
set T1 = (
I[01]
| A), T2 = (
I[01]
| B), T =
I[01] ;
reconsider g = (T1
-->
0[01] ) as
continuous
Function of T1,
I[01] ;
T2
= (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 24;
then
reconsider f = (
L[01] ((1
/ 2),1,
0 ,1)) as
continuous
Function of T2,
I[01] by
Th34,
TOPMETR: 20;
A2: for p be
set st p
in ((
[#] T2)
/\ (
[#] T1)) holds (f
. p)
= (g
. p)
proof
let p be
set;
assume p
in ((
[#] T2)
/\ (
[#] T1));
then p
in (
[.
0 , (1
/ 2).]
/\ (
[#] T2)) by
PRE_TOPC:def 5;
then p
in (
[.
0 , (1
/ 2).]
/\
[.(1
/ 2), 1.]) by
PRE_TOPC:def 5;
then p
in
{(1
/ 2)} by
XXREAL_1: 418;
then
A3: p
= (1
/ 2) by
TARSKI:def 1;
then p
in
[.
0 , (1
/ 2).] by
XXREAL_1: 1;
then
A4: p
in the
carrier of T1 by
PRE_TOPC: 8;
(f
. p)
= ((((1
-
0 )
/ (1
- (1
/ 2)))
* ((1
/ 2)
- (1
/ 2)))
+
0 ) by
A3,
Th35
.= (g
. p) by
A4,
BORSUK_1:def 14,
FUNCOP_1: 7;
hence thesis;
end;
A5: for x be
Element of
I[01] holds (
2RP
. x)
= ((g
+* f)
. x)
proof
let x be
Element of
I[01] ;
A6: (
dom f)
= the
carrier of T2 by
FUNCT_2:def 1
.=
[.(1
/ 2), 1.] by
PRE_TOPC: 8;
per cases by
XXREAL_0: 1;
suppose
A7: x
> (1
/ 2);
1
>= x by
BORSUK_1: 43;
then
A8: (f
. x)
= ((((1
-
0 )
/ (1
- (1
/ 2)))
* (x
- (1
/ 2)))
+
0 ) by
A7,
Th35
.= ((2
* x)
- 1);
x
<= 1 by
BORSUK_1: 43;
then
A9: x
in (
dom f) by
A6,
A7,
XXREAL_1: 1;
thus (
2RP
. x)
= ((2
* x)
- 1) by
A7,
Def6
.= ((g
+* f)
. x) by
A9,
A8,
FUNCT_4: 13;
end;
suppose
A10: x
= (1
/ 2);
then
A11: x
in (
dom f) by
A6,
XXREAL_1: 1;
thus (
2RP
. x)
= ((((1
-
0 )
/ (1
- (1
/ 2)))
* ((1
/ 2)
- (1
/ 2)))
+
0 ) by
A10,
Def6
.= (f
. x) by
A10,
Th35
.= ((g
+* f)
. x) by
A11,
FUNCT_4: 13;
end;
suppose
A12: x
< (1
/ 2);
x
>=
0 by
BORSUK_1: 43;
then x
in
[.
0 , (1
/ 2).] by
A12,
XXREAL_1: 1;
then
A13: x
in the
carrier of T1 by
PRE_TOPC: 8;
A14: not x
in (
dom f) by
A6,
A12,
XXREAL_1: 1;
thus (
2RP
. x)
=
0 by
A12,
Def6
.= (g
. x) by
A13,
BORSUK_1:def 14,
FUNCOP_1: 7
.= ((g
+* f)
. x) by
A14,
FUNCT_4: 11;
end;
end;
((
[#] T2)
\/ (
[#] T1))
= (
[.
0 , (1
/ 2).]
\/ (
[#] T2)) by
PRE_TOPC:def 5
.= (
[.
0 , (1
/ 2).]
\/
[.(1
/ 2), 1.]) by
PRE_TOPC:def 5
.= (
[#] T) by
BORSUK_1: 40,
XXREAL_1: 174;
then ex h be
Function of
I[01] ,
I[01] st h
= (g
+* f) & h is
continuous by
A2,
BORSUK_2: 1;
hence thesis by
A5,
FUNCT_2: 63;
end;
end
theorem ::
BORSUK_6:48
Th48: (
2RP
.
0 )
=
0 & (
2RP
. 1)
= 1
proof
reconsider x =
0 , y = 1 as
Point of
I[01] by
BORSUK_1: 43;
thus (
2RP
.
0 )
= (
2RP
. x)
.=
0 by
Def6;
thus (
2RP
. 1)
= ((2
* y)
- 1) by
Def6
.= 1;
end;
definition
::
BORSUK_6:def7
func
3RP ->
Function of
I[01] ,
I[01] means
:
Def7: for x be
Point of
I[01] holds (x
<= (1
/ 2) implies (it
. x)
= ((1
/ 2)
* x)) & (x
> (1
/ 2) & x
<= (3
/ 4) implies (it
. x)
= (x
- (1
/ 4))) & (x
> (3
/ 4) implies (it
. x)
= ((2
* x)
- 1));
existence
proof
deffunc
H(
Real) = ((2
* $1)
- 1);
deffunc
G(
Real) = ($1
- (1
/ 4));
deffunc
F(
Real) = ((1
/ 2)
* $1);
defpred
R[
Real] means $1
> (3
/ 4);
defpred
Q[
Real] means $1
> (1
/ 2) & $1
<= (3
/ 4);
defpred
P[
Real] means $1
<= (1
/ 2);
A1: for c be
Element of
I[01] holds
P[c] or
Q[c] or
R[c];
A2: for c be
Element of
I[01] holds (
P[c] implies not
Q[c]) & (
P[c] implies not
R[c]) & (
Q[c] implies not
R[c]) by
XXREAL_0: 2;
consider f be
Function such that
A3: (
dom f)
= the
carrier of
I[01] & for c be
Element of
I[01] holds (
P[c] implies (f
. c)
=
F(c)) & (
Q[c] implies (f
. c)
=
G(c)) & (
R[c] implies (f
. c)
=
H(c)) from
ExFunc3CondD(
A2,
A1);
for x be
object st x
in the
carrier of
I[01] holds (f
. x)
in the
carrier of
I[01]
proof
let x be
object;
assume x
in the
carrier of
I[01] ;
then
reconsider x as
Point of
I[01] ;
per cases ;
suppose
P[x];
then (f
. x)
= ((1
/ 2)
* x) by
A3;
then (f
. x) is
Point of
I[01] by
Th6;
hence thesis;
end;
suppose
A4:
Q[x];
then (f
. x)
=
G(x) by
A3;
then (f
. x) is
Point of
I[01] by
A4,
Th7;
hence thesis;
end;
suppose
A5:
R[x];
then (f
. x)
= ((2
* x)
- 1) by
A3;
then (f
. x) is
Point of
I[01] by
A5,
Th4,
XXREAL_0: 2;
hence thesis;
end;
end;
then
reconsider f as
Function of
I[01] ,
I[01] by
A3,
FUNCT_2: 3;
for x be
Point of
I[01] holds (x
<= (1
/ 2) implies (f
. x)
= ((1
/ 2)
* x)) & (x
> (1
/ 2) & x
<= (3
/ 4) implies (f
. x)
= (x
- (1
/ 4))) & (x
> (3
/ 4) implies (f
. x)
= ((2
* x)
- 1)) by
A3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of
I[01] ,
I[01] ;
assume that
A6: for x be
Point of
I[01] holds (x
<= (1
/ 2) implies (f1
. x)
= ((1
/ 2)
* x)) & (x
> (1
/ 2) & x
<= (3
/ 4) implies (f1
. x)
= (x
- (1
/ 4))) & (x
> (3
/ 4) implies (f1
. x)
= ((2
* x)
- 1)) and
A7: for x be
Point of
I[01] holds (x
<= (1
/ 2) implies (f2
. x)
= ((1
/ 2)
* x)) & (x
> (1
/ 2) & x
<= (3
/ 4) implies (f2
. x)
= (x
- (1
/ 4))) & (x
> (3
/ 4) implies (f2
. x)
= ((2
* x)
- 1));
for x be
Point of
I[01] holds (f1
. x)
= (f2
. x)
proof
let x be
Point of
I[01] ;
per cases ;
suppose
A8: x
<= (1
/ 2);
then (f1
. x)
= ((1
/ 2)
* x) by
A6
.= (f2
. x) by
A7,
A8;
hence thesis;
end;
suppose
A9: x
> (1
/ 2) & x
<= (3
/ 4);
then (f1
. x)
= (x
- (1
/ 4)) by
A6
.= (f2
. x) by
A7,
A9;
hence thesis;
end;
suppose
A10: x
> (3
/ 4);
then (f1
. x)
= ((2
* x)
- 1) by
A6
.= (f2
. x) by
A7,
A10;
hence thesis;
end;
end;
hence thesis by
FUNCT_2: 63;
end;
end
registration
cluster
3RP ->
continuous;
coherence
proof
A1: (1
/ 2) is
Point of
I[01] by
BORSUK_1: 43;
A2: (3
/ 4) is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider B =
[.(1
/ 2), (3
/ 4).] as non
empty
compact
Subset of
I[01] by
A1,
BORSUK_4: 24;
A3:
0 is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider A =
[.
0 , (1
/ 2).] as non
empty
compact
Subset of
I[01] by
A1,
BORSUK_4: 24;
reconsider G =
[.
0 , (3
/ 4).] as non
empty
compact
Subset of
I[01] by
A3,
A2,
BORSUK_4: 24;
A4: (1
/ 4) is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider E =
[.(1
/ 4), (1
/ 2).] as non
empty
compact
Subset of
I[01] by
A1,
BORSUK_4: 24;
reconsider F =
[.
0 , (1
/ 4).] as non
empty
compact
Subset of
I[01] by
A3,
A4,
BORSUK_4: 24;
A5: 1 is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider C =
[.(3
/ 4), 1.] as non
empty
compact
Subset of
I[01] by
A2,
BORSUK_4: 24;
reconsider D =
[.(1
/ 2), 1.] as non
empty
compact
Subset of
I[01] by
A1,
A5,
BORSUK_4: 24;
set T =
I[01] ;
set T1 = (T
| A), T2 = (T
| B), T3 = (T
| C), T4 = (T
| D), T5 = (T
| E), T6 = (T
| F);
set f = (
L[01] (
0 ,(1
/ 2),
0 ,(1
/ 4)));
set g = (
L[01] ((1
/ 2),(3
/ 4),(1
/ 4),(1
/ 2)));
set h = (
L[01] ((3
/ 4),1,(1
/ 2),1));
reconsider TT1 = T1, TT2 = T2 as
SubSpace of (T
| G) by
TOPMETR: 22,
XXREAL_1: 34;
(
Closed-Interval-TSpace ((3
/ 4),1))
= T3 & (
Closed-Interval-TSpace ((1
/ 2),1))
= T4 by
TOPMETR: 24;
then
reconsider h as
continuous
Function of T3, T4 by
Th34;
reconsider h as
continuous
Function of T3, T by
JORDAN6: 3;
A6: for x be
Point of T3 holds (h
. x)
= ((2
* x)
- 1)
proof
let x be
Point of T3;
x
in the
carrier of T3;
then x
in C by
PRE_TOPC: 8;
then (3
/ 4)
<= x & x
<= 1 by
XXREAL_1: 1;
then (h
. x)
= ((((1
- (1
/ 2))
/ (1
- (3
/ 4)))
* (x
- (3
/ 4)))
+ (1
/ 2)) by
Th35
.= ((2
* x)
- 1);
hence thesis;
end;
(
Closed-Interval-TSpace (
0 ,(1
/ 4)))
= T6 & (
Closed-Interval-TSpace (
0 ,(1
/ 2)))
= T1 by
TOPMETR: 24;
then
reconsider f as
continuous
Function of T1, T6 by
Th34;
(
Closed-Interval-TSpace ((1
/ 4),(1
/ 2)))
= T5 & (
Closed-Interval-TSpace ((1
/ 2),(3
/ 4)))
= T2 by
TOPMETR: 24;
then
reconsider g as
continuous
Function of T2, T5 by
Th34;
reconsider g as
continuous
Function of T2, T by
JORDAN6: 3;
reconsider f as
continuous
Function of T1, T by
JORDAN6: 3;
set f1 = f, g1 = g;
A7: for x be
Point of T2 holds (g
. x)
= (x
- (1
/ 4))
proof
let x be
Point of T2;
x
in the
carrier of T2;
then x
in B by
PRE_TOPC: 8;
then (1
/ 2)
<= x & x
<= (3
/ 4) by
XXREAL_1: 1;
then (g
. x)
= (((((1
/ 2)
- (1
/ 4))
/ ((3
/ 4)
- (1
/ 2)))
* (x
- (1
/ 2)))
+ (1
/ 4)) by
Th35
.= (x
- (1
/ 4));
hence thesis;
end;
A8: ((
[#] TT1)
/\ (
[#] TT2))
= (A
/\ (
[#] TT2)) by
PRE_TOPC:def 5
.= (A
/\ B) by
PRE_TOPC:def 5
.=
{(1
/ 2)} by
XXREAL_1: 418;
A9: for p be
set st p
in ((
[#] TT1)
/\ (
[#] TT2)) holds (f1
. p)
= (g1
. p)
proof
let p be
set;
assume p
in ((
[#] TT1)
/\ (
[#] TT2));
then
A10: p
= (1
/ 2) by
A8,
TARSKI:def 1;
then
reconsider p as
Point of
I[01] by
BORSUK_1: 40,
XXREAL_1: 1;
(f1
. p)
= (((((1
/ 4)
-
0 )
/ ((1
/ 2)
-
0 ))
* (p
-
0 ))
+
0 ) by
A10,
Th35
.= (((((1
/ 2)
- (1
/ 4))
/ ((3
/ 4)
- (1
/ 2)))
* (p
- (1
/ 2)))
+ (1
/ 4)) by
A10
.= (g1
. p) by
A10,
Th35;
hence thesis;
end;
((
[#] TT1)
\/ (
[#] TT2))
= (A
\/ (
[#] TT2)) by
PRE_TOPC:def 5
.= (A
\/ B) by
PRE_TOPC:def 5
.=
[.
0 , (3
/ 4).] by
XXREAL_1: 174
.= (
[#] (T
| G)) by
PRE_TOPC:def 5;
then
consider FF be
Function of (T
| G), T such that
A11: FF
= (f1
+* g1) and
A12: FF is
continuous by
A9,
BORSUK_2: 1;
A13: ((
[#] (T
| G))
/\ (
[#] T3))
= (G
/\ (
[#] T3)) by
PRE_TOPC:def 5
.= (G
/\ C) by
PRE_TOPC:def 5
.=
{(3
/ 4)} by
XXREAL_1: 418;
A14: for p be
set st p
in ((
[#] (T
| G))
/\ (
[#] T3)) holds (FF
. p)
= (h
. p)
proof
let p be
set;
assume p
in ((
[#] (T
| G))
/\ (
[#] T3));
then
A15: p
= (3
/ 4) by
A13,
TARSKI:def 1;
then
reconsider p as
Point of T by
BORSUK_1: 43;
p
in
[.(1
/ 2), (3
/ 4).] by
A15,
XXREAL_1: 1;
then p
in the
carrier of T2 by
PRE_TOPC: 8;
then p
in (
dom g) by
FUNCT_2:def 1;
then (FF
. p)
= (g
. p) by
A11,
FUNCT_4: 13
.= (1
/ 2) by
A15,
Th33
.= (h
. p) by
A15,
Th33;
hence thesis;
end;
((
[#] (T
| G))
\/ (
[#] T3))
= (G
\/ (
[#] T3)) by
PRE_TOPC:def 5
.= (G
\/ C) by
PRE_TOPC:def 5
.= (
[#] T) by
BORSUK_1: 40,
XXREAL_1: 174;
then
consider HH be
Function of T, T such that
A16: HH
= (FF
+* h) and
A17: HH is
continuous by
A12,
A14,
BORSUK_2: 1;
A18: for x be
Point of T1 holds (f
. x)
= ((1
/ 2)
* x)
proof
let x be
Point of T1;
x
in the
carrier of T1;
then x
in A by
PRE_TOPC: 8;
then
0
<= x & x
<= (1
/ 2) by
XXREAL_1: 1;
then (f
. x)
= (((((1
/ 4)
-
0 )
/ ((1
/ 2)
-
0 ))
* (x
-
0 ))
+
0 ) by
Th35
.= ((1
/ 2)
* x);
hence thesis;
end;
for x be
Element of T holds (HH
. x)
= (
3RP
. x)
proof
let x be
Element of T;
A19:
0
<= x by
BORSUK_1: 43;
A20: x
<= 1 by
BORSUK_1: 43;
per cases by
XXREAL_0: 1;
suppose
A21: x
< (1
/ 2);
then not x
in
[.(1
/ 2), (3
/ 4).] by
XXREAL_1: 1;
then not x
in the
carrier of T2 by
PRE_TOPC: 8;
then
A22: not x
in (
dom g);
x
in
[.
0 , (1
/ 2).] by
A19,
A21,
XXREAL_1: 1;
then
A23: x is
Point of T1 by
PRE_TOPC: 8;
x
< (3
/ 4) by
A21,
XXREAL_0: 2;
then not x
in
[.(3
/ 4), 1.] by
XXREAL_1: 1;
then not x
in the
carrier of T3 by
PRE_TOPC: 8;
then not x
in (
dom h);
then (HH
. x)
= (FF
. x) by
A16,
FUNCT_4: 11
.= (f
. x) by
A11,
A22,
FUNCT_4: 11
.= ((1
/ 2)
* x) by
A18,
A23
.= (
3RP
. x) by
A21,
Def7;
hence thesis;
end;
suppose
A24: x
= (1
/ 2);
then x
in
[.(1
/ 2), (3
/ 4).] by
XXREAL_1: 1;
then x
in the
carrier of T2 by
PRE_TOPC: 8;
then
A25: x
in (
dom g) by
FUNCT_2:def 1;
not x
in
[.(3
/ 4), 1.] by
A24,
XXREAL_1: 1;
then not x
in the
carrier of T3 by
PRE_TOPC: 8;
then not x
in (
dom h);
then (HH
. x)
= (FF
. x) by
A16,
FUNCT_4: 11
.= (g
. x) by
A11,
A25,
FUNCT_4: 13
.= ((1
/ 2)
* x) by
A24,
Th33
.= (
3RP
. x) by
A24,
Def7;
hence thesis;
end;
suppose
A26: x
> (1
/ 2) & x
< (3
/ 4);
then x
in
[.(1
/ 2), (3
/ 4).] by
XXREAL_1: 1;
then
A27: x
in the
carrier of T2 by
PRE_TOPC: 8;
then
A28: x
in (
dom g) by
FUNCT_2:def 1;
not x
in
[.(3
/ 4), 1.] by
A26,
XXREAL_1: 1;
then not x
in the
carrier of T3 by
PRE_TOPC: 8;
then not x
in (
dom h);
then (HH
. x)
= (FF
. x) by
A16,
FUNCT_4: 11
.= (g
. x) by
A11,
A28,
FUNCT_4: 13
.= (x
- (1
/ 4)) by
A7,
A27
.= (
3RP
. x) by
A26,
Def7;
hence thesis;
end;
suppose
A29: x
= (3
/ 4);
then x
in
[.(3
/ 4), 1.] by
XXREAL_1: 1;
then x
in the
carrier of T3 by
PRE_TOPC: 8;
then x
in (
dom h) by
FUNCT_2:def 1;
then (HH
. x)
= (h
. x) by
A16,
FUNCT_4: 13
.= (x
- (1
/ 4)) by
A29,
Th33
.= (
3RP
. x) by
A29,
Def7;
hence thesis;
end;
suppose
A30: x
> (3
/ 4);
then x
in
[.(3
/ 4), 1.] by
A20,
XXREAL_1: 1;
then
A31: x
in the
carrier of T3 by
PRE_TOPC: 8;
then x
in (
dom h) by
FUNCT_2:def 1;
then (HH
. x)
= (h
. x) by
A16,
FUNCT_4: 13
.= ((2
* x)
- 1) by
A6,
A31
.= (
3RP
. x) by
A30,
Def7;
hence thesis;
end;
end;
hence thesis by
A17,
FUNCT_2: 63;
end;
end
theorem ::
BORSUK_6:49
Th49: (
3RP
.
0 )
=
0 & (
3RP
. 1)
= 1
proof
0 is
Point of
I[01] by
BORSUK_1: 43;
hence (
3RP
.
0 )
= ((1
/ 2)
*
0 ) by
Def7
.=
0 ;
1 is
Point of
I[01] by
BORSUK_1: 43;
hence (
3RP
. 1)
= ((2
* 1)
- 1) by
Def7
.= 1;
end;
theorem ::
BORSUK_6:50
Th50: for P be
Path of a, b, Q be
constant
Path of b, b st (a,b)
are_connected holds (
RePar (P,
1RP ))
= (P
+ Q)
proof
let P be
Path of a, b, Q be
constant
Path of b, b;
set f = (
RePar (P,
1RP )), g = (P
+ Q);
assume
A1: (a,b)
are_connected ;
A2: (b,b)
are_connected ;
for p be
Element of
I[01] holds (f
. p)
= (g
. p)
proof
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A3:
0
in (
dom Q) by
FUNCT_2:def 1;
let p be
Element of
I[01] ;
p
in the
carrier of
I[01] ;
then
A4: p
in (
dom
1RP ) by
FUNCT_2:def 1;
A5: (f
. p)
= ((P
*
1RP )
. p) by
A1,
Def4,
Th47
.= (P
. (
1RP
. p)) by
A4,
FUNCT_1: 13;
per cases ;
suppose
A6: p
<= (1
/ 2);
then (f
. p)
= (P
. (2
* p)) by
A5,
Def5
.= (g
. p) by
A1,
A6,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A7: p
> (1
/ 2);
then ((2
* p)
- 1) is
Point of
I[01] by
Th4;
then ((2
* p)
- 1)
in the
carrier of
I[01] ;
then
A8: ((2
* p)
- 1)
in (
dom Q) by
FUNCT_2:def 1;
(f
. p)
= (P
. 1) by
A5,
A7,
Def5
.= b by
A1,
BORSUK_2:def 2
.= (Q
.
0 ) by
A2,
BORSUK_2:def 2
.= (Q
. ((2
* p)
- 1)) by
A3,
A8,
FUNCT_1:def 10
.= (g
. p) by
A1,
A7,
BORSUK_2:def 5;
hence thesis;
end;
end;
hence thesis by
FUNCT_2: 63;
end;
theorem ::
BORSUK_6:51
Th51: for P be
Path of a, b, Q be
constant
Path of a, a st (a,b)
are_connected holds (
RePar (P,
2RP ))
= (Q
+ P)
proof
let P be
Path of a, b, Q be
constant
Path of a, a;
assume
A1: (a,b)
are_connected ;
set f = (
RePar (P,
2RP )), g = (Q
+ P);
A2: (a,a)
are_connected ;
for p be
Element of
I[01] holds (f
. p)
= (g
. p)
proof
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A3:
0
in (
dom Q) by
FUNCT_2:def 1;
let p be
Element of
I[01] ;
p
in the
carrier of
I[01] ;
then
A4: p
in (
dom
2RP ) by
FUNCT_2:def 1;
A5: (f
. p)
= ((P
*
2RP )
. p) by
A1,
Def4,
Th48
.= (P
. (
2RP
. p)) by
A4,
FUNCT_1: 13;
per cases ;
suppose
A6: p
<= (1
/ 2);
then (2
* p) is
Point of
I[01] by
Th3;
then (2
* p)
in the
carrier of
I[01] ;
then
A7: (2
* p)
in (
dom Q) by
FUNCT_2:def 1;
(f
. p)
= (P
.
0 ) by
A5,
A6,
Def6
.= a by
A1,
BORSUK_2:def 2
.= (Q
.
0 ) by
A2,
BORSUK_2:def 2
.= (Q
. (2
* p)) by
A3,
A7,
FUNCT_1:def 10
.= (g
. p) by
A1,
A6,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A8: p
> (1
/ 2);
then (f
. p)
= (P
. ((2
* p)
- 1)) by
A5,
Def6
.= (g
. p) by
A1,
A8,
BORSUK_2:def 5;
hence thesis;
end;
end;
hence thesis by
FUNCT_2: 63;
end;
theorem ::
BORSUK_6:52
Th52: for P be
Path of a, b, Q be
Path of b, c, R be
Path of c, d st (a,b)
are_connected & (b,c)
are_connected & (c,d)
are_connected holds (
RePar (((P
+ Q)
+ R),
3RP ))
= (P
+ (Q
+ R))
proof
let P be
Path of a, b, Q be
Path of b, c, R be
Path of c, d;
assume that
A1: (a,b)
are_connected and
A2: (b,c)
are_connected and
A3: (c,d)
are_connected ;
set F = ((P
+ Q)
+ R);
set f = (
RePar (F,
3RP )), g = (P
+ (Q
+ R));
A4: (a,c)
are_connected by
A1,
A2,
Th42;
A5: (b,d)
are_connected by
A2,
A3,
Th42;
for x be
Point of
I[01] holds (f
. x)
= (g
. x)
proof
let x be
Point of
I[01] ;
x
in the
carrier of
I[01] ;
then
A6: x
in (
dom
3RP ) by
FUNCT_2:def 1;
A7: (f
. x)
= ((F
*
3RP )
. x) by
A3,
A4,
Def4,
Th42,
Th49
.= (F
. (
3RP
. x)) by
A6,
FUNCT_1: 13;
per cases ;
suppose
A8: x
<= (1
/ 2);
reconsider y = ((1
/ 2)
* x) as
Point of
I[01] by
Th6;
((1
/ 2)
* x)
<= ((1
/ 2)
* (1
/ 2)) by
A8,
XREAL_1: 64;
then
A9: y
<= (1
/ 2) by
XXREAL_0: 2;
reconsider z = (2
* y) as
Point of
I[01] ;
(f
. x)
= (F
. y) by
A7,
A8,
Def7
.= ((P
+ Q)
. z) by
A3,
A4,
A9,
BORSUK_2:def 5
.= (P
. (2
* x)) by
A1,
A2,
A8,
BORSUK_2:def 5
.= (g
. x) by
A1,
A5,
A8,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A10: x
> (1
/ 2) & x
<= (3
/ 4);
then
A11: ((1
/ 2)
- (1
/ 4))
<= (x
- (1
/ 4)) by
XREAL_1: 9;
A12: (x
- (1
/ 4))
<= ((3
/ 4)
- (1
/ 4)) by
A10,
XREAL_1: 9;
then (x
- (1
/ 4))
<= 1 by
XXREAL_0: 2;
then
reconsider y = (x
- (1
/ 4)) as
Point of
I[01] by
A11,
BORSUK_1: 43;
reconsider z = (2
* y) as
Point of
I[01] by
A12,
Th3;
A13: (2
* y)
>= (2
* (1
/ 4)) by
A11,
XREAL_1: 64;
reconsider w = ((2
* x)
- 1) as
Point of
I[01] by
A10,
Th4;
(2
* x)
<= (2
* (3
/ 4)) by
A10,
XREAL_1: 64;
then
A14: ((2
* x)
- 1)
<= ((3
/ 2)
- 1) by
XREAL_1: 9;
(f
. x)
= (F
. y) by
A7,
A10,
Def7
.= ((P
+ Q)
. z) by
A3,
A4,
A12,
BORSUK_2:def 5
.= (Q
. ((2
* z)
- 1)) by
A1,
A2,
A13,
BORSUK_2:def 5
.= (Q
. (2
* w))
.= ((Q
+ R)
. w) by
A2,
A3,
A14,
BORSUK_2:def 5
.= (g
. x) by
A1,
A5,
A10,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A15: x
> (3
/ 4);
then
reconsider w = ((2
* x)
- 1) as
Point of
I[01] by
Th4,
XXREAL_0: 2;
(2
* x)
> (2
* (3
/ 4)) by
A15,
XREAL_1: 68;
then
A16: ((2
* x)
- 1)
> ((2
* (3
/ 4))
- 1) by
XREAL_1: 14;
reconsider y = ((2
* x)
- 1) as
Point of
I[01] by
A15,
Th4,
XXREAL_0: 2;
A17: x
> (1
/ 2) by
A15,
XXREAL_0: 2;
(f
. x)
= (F
. y) by
A7,
A15,
Def7
.= (R
. ((2
* y)
- 1)) by
A3,
A4,
A16,
BORSUK_2:def 5
.= ((Q
+ R)
. w) by
A2,
A3,
A16,
BORSUK_2:def 5
.= (g
. x) by
A1,
A5,
A17,
BORSUK_2:def 5;
hence thesis;
end;
end;
hence thesis by
FUNCT_2: 63;
end;
begin
definition
::
BORSUK_6:def8
func
LowerLeftUnitTriangle ->
Subset of
[:
I[01] ,
I[01] :] means
:
Def8: for x be
set holds x
in it iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= (1
- (2
* a));
existence
proof
defpred
P[
object] means ex a,b be
Point of
I[01] st $1
=
[a, b] & b
<= (1
- (2
* a));
consider X be
set such that
A1: for x be
object holds x
in X iff x
in the
carrier of
[:
I[01] ,
I[01] :] &
P[x] from
XBOOLE_0:sch 1;
X
c= the
carrier of
[:
I[01] ,
I[01] :] by
A1;
then
reconsider X as
Subset of
[:
I[01] ,
I[01] :];
take X;
thus thesis by
A1;
end;
uniqueness
proof
let X1,X2 be
Subset of
[:
I[01] ,
I[01] :] such that
A2: for x be
set holds x
in X1 iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= (1
- (2
* a)) and
A3: for x be
set holds x
in X2 iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= (1
- (2
* a));
X1
= X2
proof
thus X1
c= X2
proof
let x be
object;
assume x
in X1;
then ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= (1
- (2
* a)) by
A2;
hence thesis by
A3;
end;
let x be
object;
assume x
in X2;
then ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= (1
- (2
* a)) by
A3;
hence thesis by
A2;
end;
hence thesis;
end;
end
notation
synonym
IAA for
LowerLeftUnitTriangle ;
end
definition
::
BORSUK_6:def9
func
UpperUnitTriangle ->
Subset of
[:
I[01] ,
I[01] :] means
:
Def9: for x be
set holds x
in it iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
>= (1
- (2
* a)) & b
>= ((2
* a)
- 1);
existence
proof
defpred
P[
object] means ex a,b be
Point of
I[01] st $1
=
[a, b] & b
>= (1
- (2
* a)) & b
>= ((2
* a)
- 1);
consider X be
set such that
A1: for x be
object holds x
in X iff x
in the
carrier of
[:
I[01] ,
I[01] :] &
P[x] from
XBOOLE_0:sch 1;
X
c= the
carrier of
[:
I[01] ,
I[01] :] by
A1;
then
reconsider X as
Subset of
[:
I[01] ,
I[01] :];
take X;
thus thesis by
A1;
end;
uniqueness
proof
let X1,X2 be
Subset of
[:
I[01] ,
I[01] :] such that
A2: for x be
set holds x
in X1 iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
>= (1
- (2
* a)) & b
>= ((2
* a)
- 1) and
A3: for x be
set holds x
in X2 iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
>= (1
- (2
* a)) & b
>= ((2
* a)
- 1);
X1
= X2
proof
thus X1
c= X2
proof
let x be
object;
assume x
in X1;
then ex a,b be
Point of
I[01] st x
=
[a, b] & b
>= (1
- (2
* a)) & b
>= ((2
* a)
- 1) by
A2;
hence thesis by
A3;
end;
let x be
object;
assume x
in X2;
then ex a,b be
Point of
I[01] st x
=
[a, b] & b
>= (1
- (2
* a)) & b
>= ((2
* a)
- 1) by
A3;
hence thesis by
A2;
end;
hence thesis;
end;
end
notation
synonym
IBB for
UpperUnitTriangle ;
end
definition
::
BORSUK_6:def10
func
LowerRightUnitTriangle ->
Subset of
[:
I[01] ,
I[01] :] means
:
Def10: for x be
set holds x
in it iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= ((2
* a)
- 1);
existence
proof
defpred
P[
object] means ex a,b be
Point of
I[01] st $1
=
[a, b] & b
<= ((2
* a)
- 1);
consider X be
set such that
A1: for x be
object holds x
in X iff x
in the
carrier of
[:
I[01] ,
I[01] :] &
P[x] from
XBOOLE_0:sch 1;
X
c= the
carrier of
[:
I[01] ,
I[01] :] by
A1;
then
reconsider X as
Subset of
[:
I[01] ,
I[01] :];
take X;
thus thesis by
A1;
end;
uniqueness
proof
let X1,X2 be
Subset of
[:
I[01] ,
I[01] :] such that
A2: for x be
set holds x
in X1 iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= ((2
* a)
- 1) and
A3: for x be
set holds x
in X2 iff ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= ((2
* a)
- 1);
X1
= X2
proof
thus X1
c= X2
proof
let x be
object;
assume x
in X1;
then ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= ((2
* a)
- 1) by
A2;
hence thesis by
A3;
end;
let x be
object;
assume x
in X2;
then ex a,b be
Point of
I[01] st x
=
[a, b] & b
<= ((2
* a)
- 1) by
A3;
hence thesis by
A2;
end;
hence thesis;
end;
end
notation
synonym
ICC for
LowerRightUnitTriangle ;
end
theorem ::
BORSUK_6:53
Th53:
IAA
= { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
<= (1
- (2
* (p
`1 ))) }
proof
set P = { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
<= (1
- (2
* (p
`1 ))) };
thus
IAA
c= P
proof
let x be
object;
assume
A1: x
in
IAA ;
then
reconsider x9 = x as
Point of
[:
I[01] ,
I[01] :];
consider a,b be
Point of
I[01] such that
A2: x
=
[a, b] and
A3: b
<= (1
- (2
* a)) by
A1,
Def8;
(x9
`1 )
= a & (x9
`2 )
= b by
A2;
hence thesis by
A3;
end;
let x be
object;
assume x
in P;
then
consider p be
Point of
[:
I[01] ,
I[01] :] such that
A4: p
= x and
A5: (p
`2 )
<= (1
- (2
* (p
`1 )));
x
in the
carrier of
[:
I[01] ,
I[01] :] by
A4;
then x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A6: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
(p
`1 ) is
Point of
I[01] & (p
`2 ) is
Point of
I[01] by
Th27;
hence thesis by
A4,
A5,
A6,
Def8;
end;
theorem ::
BORSUK_6:54
Th54:
IBB
= { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1) }
proof
set P = { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1) };
thus
IBB
c= P
proof
let x be
object;
assume
A1: x
in
IBB ;
then
reconsider x9 = x as
Point of
[:
I[01] ,
I[01] :];
consider a,b be
Point of
I[01] such that
A2: x
=
[a, b] and
A3: b
>= (1
- (2
* a)) & b
>= ((2
* a)
- 1) by
A1,
Def9;
(x9
`1 )
= a & (x9
`2 )
= b by
A2;
hence thesis by
A3;
end;
let x be
object;
assume x
in P;
then
consider p be
Point of
[:
I[01] ,
I[01] :] such that
A4: p
= x and
A5: (p
`2 )
>= (1
- (2
* (p
`1 ))) & (p
`2 )
>= ((2
* (p
`1 ))
- 1);
x
in the
carrier of
[:
I[01] ,
I[01] :] by
A4;
then x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A6: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
(p
`1 ) is
Point of
I[01] & (p
`2 ) is
Point of
I[01] by
Th27;
hence thesis by
A4,
A5,
A6,
Def9;
end;
theorem ::
BORSUK_6:55
Th55:
ICC
= { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
<= ((2
* (p
`1 ))
- 1) }
proof
set P = { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
<= ((2
* (p
`1 ))
- 1) };
thus
ICC
c= P
proof
let x be
object;
assume
A1: x
in
ICC ;
then
reconsider x9 = x as
Point of
[:
I[01] ,
I[01] :];
consider a,b be
Point of
I[01] such that
A2: x
=
[a, b] and
A3: b
<= ((2
* a)
- 1) by
A1,
Def10;
(x9
`1 )
= a & (x9
`2 )
= b by
A2;
hence thesis by
A3;
end;
let x be
object;
assume x
in P;
then
consider p be
Point of
[:
I[01] ,
I[01] :] such that
A4: p
= x and
A5: (p
`2 )
<= ((2
* (p
`1 ))
- 1);
x
in the
carrier of
[:
I[01] ,
I[01] :] by
A4;
then x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A6: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
(p
`1 ) is
Point of
I[01] & (p
`2 ) is
Point of
I[01] by
Th27;
hence thesis by
A4,
A5,
A6,
Def10;
end;
registration
cluster
IAA ->
closed non
empty;
coherence by
Th24,
Th53;
cluster
IBB ->
closed non
empty;
coherence by
Th25,
Th54;
cluster
ICC ->
closed non
empty;
coherence by
Th26,
Th55;
end
theorem ::
BORSUK_6:56
Th56: ((
IAA
\/
IBB )
\/
ICC )
=
[:
[.
0 , 1.],
[.
0 , 1.]:]
proof
thus ((
IAA
\/
IBB )
\/
ICC )
c=
[:
[.
0 , 1.],
[.
0 , 1.]:] by
Th1;
let x be
object;
assume
A1: x
in
[:
[.
0 , 1.],
[.
0 , 1.]:];
then
reconsider q = (x
`1 ), p = (x
`2 ) as
Point of
I[01] by
BORSUK_1: 40,
MCART_1: 10;
A2: x
=
[q, p] by
A1,
MCART_1: 21;
x
in
IAA or x
in
IBB or x
in
ICC
proof
per cases ;
suppose
A3: p
>= (1
- (2
* q));
now
per cases ;
suppose p
>= ((2
* q)
- 1);
hence thesis by
A2,
A3,
Def9;
end;
suppose p
< ((2
* q)
- 1);
hence thesis by
A2,
Def10;
end;
end;
hence thesis;
end;
suppose p
< (1
- (2
* q));
hence thesis by
A2,
Def8;
end;
end;
then x
in (
IAA
\/
IBB ) or x
in
ICC by
XBOOLE_0:def 3;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
BORSUK_6:57
Th57: (
IAA
/\
IBB )
= { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
= (1
- (2
* (p
`1 ))) }
proof
set KK = { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
= (1
- (2
* (p
`1 ))) };
thus (
IAA
/\
IBB )
c= KK
proof
let x be
object;
assume
A1: x
in (
IAA
/\
IBB );
then x
in
IAA by
XBOOLE_0:def 4;
then
consider p be
Point of
[:
I[01] ,
I[01] :] such that
A2: x
= p and
A3: (p
`2 )
<= (1
- (2
* (p
`1 ))) by
Th53;
x
in
IBB by
A1,
XBOOLE_0:def 4;
then ex q be
Point of
[:
I[01] ,
I[01] :] st x
= q & (q
`2 )
>= (1
- (2
* (q
`1 ))) & (q
`2 )
>= ((2
* (q
`1 ))
- 1) by
Th54;
then (p
`2 )
= (1
- (2
* (p
`1 ))) by
A2,
A3,
XXREAL_0: 1;
hence thesis by
A2;
end;
let x be
object;
assume x
in KK;
then
consider p be
Point of
[:
I[01] ,
I[01] :] such that
A4: p
= x and
A5: (p
`2 )
= (1
- (2
* (p
`1 )));
x
in the
carrier of
[:
I[01] ,
I[01] :] by
A4;
then
A6: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A7: x
=
[(p
`1 ), (p
`2 )] & (p
`1 )
in the
carrier of
I[01] by
A4,
MCART_1: 10,
MCART_1: 21;
A8: (p
`2 )
in the
carrier of
I[01] by
A4,
A6,
MCART_1: 10;
then
A9: x
in
IAA by
A5,
A7,
Def8;
(1
- (2
* (p
`1 )))
>=
0 by
A5,
A8,
BORSUK_1: 43;
then (
0
+ (2
* (p
`1 )))
<= 1 by
XREAL_1: 19;
then ((2
* (p
`1 ))
/ 2)
<= (1
/ 2) by
XREAL_1: 72;
then ((2
* (p
`1 ))
- 1)
<=
0 &
0
<= (1
- (2
* (p
`1 ))) by
XREAL_1: 217,
XREAL_1: 218;
then x
in
IBB by
A5,
A7,
A8,
Def9;
hence thesis by
A9,
XBOOLE_0:def 4;
end;
theorem ::
BORSUK_6:58
Th58: (
ICC
/\
IBB )
= { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
= ((2
* (p
`1 ))
- 1) }
proof
set KK = { p where p be
Point of
[:
I[01] ,
I[01] :] : (p
`2 )
= ((2
* (p
`1 ))
- 1) };
thus (
ICC
/\
IBB )
c= KK
proof
let x be
object;
assume
A1: x
in (
ICC
/\
IBB );
then x
in
ICC by
XBOOLE_0:def 4;
then
consider p be
Point of
[:
I[01] ,
I[01] :] such that
A2: x
= p and
A3: (p
`2 )
<= ((2
* (p
`1 ))
- 1) by
Th55;
x
in
IBB by
A1,
XBOOLE_0:def 4;
then ex q be
Point of
[:
I[01] ,
I[01] :] st x
= q & (q
`2 )
>= (1
- (2
* (q
`1 ))) & (q
`2 )
>= ((2
* (q
`1 ))
- 1) by
Th54;
then (p
`2 )
= ((2
* (p
`1 ))
- 1) by
A2,
A3,
XXREAL_0: 1;
hence thesis by
A2;
end;
let x be
object;
assume x
in KK;
then
consider p be
Point of
[:
I[01] ,
I[01] :] such that
A4: p
= x and
A5: (p
`2 )
= ((2
* (p
`1 ))
- 1);
x
in the
carrier of
[:
I[01] ,
I[01] :] by
A4;
then
A6: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A7: x
=
[(p
`1 ), (p
`2 )] & (p
`1 )
in the
carrier of
I[01] by
A4,
MCART_1: 10,
MCART_1: 21;
A8: (p
`2 )
in the
carrier of
I[01] by
A4,
A6,
MCART_1: 10;
then
A9: x
in
ICC by
A5,
A7,
Def10;
((2
* (p
`1 ))
- 1)
>=
0 by
A5,
A8,
BORSUK_1: 43;
then (2
* (p
`1 ))
>= (
0
+ 1) by
XREAL_1: 19;
then ((2
* (p
`1 ))
/ 2)
>= (1
/ 2) by
XREAL_1: 72;
then ((2
* (p
`1 ))
- 1)
>=
0 &
0
>= (1
- (2
* (p
`1 ))) by
XREAL_1: 219,
XREAL_1: 220;
then x
in
IBB by
A5,
A7,
A8,
Def9;
hence thesis by
A9,
XBOOLE_0:def 4;
end;
theorem ::
BORSUK_6:59
Th59: for x be
Point of
[:
I[01] ,
I[01] :] st x
in
IAA holds (x
`1 )
<= (1
/ 2)
proof
set GG =
[:
I[01] ,
I[01] :];
let x be
Point of GG;
assume x
in
IAA ;
then
consider a,b be
Point of
I[01] such that
A1: x
=
[a, b] and
A2: b
<= (1
- (2
* a)) by
Def8;
b
>=
0 by
BORSUK_1: 43;
then 1
>= (
0
+ (2
* a)) by
A2,
XREAL_1: 19;
then
A3: (1
/ 2)
>= ((2
* a)
/ 2) by
XREAL_1: 72;
thus thesis by
A1,
A3;
end;
theorem ::
BORSUK_6:60
Th60: for x be
Point of
[:
I[01] ,
I[01] :] st x
in
ICC holds (x
`1 )
>= (1
/ 2)
proof
set GG =
[:
I[01] ,
I[01] :];
let x be
Point of GG;
assume x
in
ICC ;
then
consider a,b be
Point of
I[01] such that
A1: x
=
[a, b] and
A2: b
<= ((2
* a)
- 1) by
Def10;
b
>=
0 by
BORSUK_1: 43;
then (
0
+ 1)
<= (2
* a) by
A2,
XREAL_1: 19;
then
A3: (1
/ 2)
<= ((2
* a)
/ 2) by
XREAL_1: 72;
thus thesis by
A1,
A3;
end;
theorem ::
BORSUK_6:61
Th61: for x be
Point of
I[01] holds
[
0 , x]
in
IAA
proof
let x be
Point of
I[01] ;
0 is
Point of
I[01] & x
<= (1
- (2
*
0 )) by
BORSUK_1: 43;
hence thesis by
Def8;
end;
theorem ::
BORSUK_6:62
Th62: for s be
set holds
[
0 , s]
in
IBB implies s
= 1
proof
let s be
set;
assume
[
0 , s]
in
IBB ;
then
consider a,b be
Point of
I[01] such that
A1:
[
0 , s]
=
[a, b] and
A2: b
>= (1
- (2
* a)) and b
>= ((2
* a)
- 1) by
Def9;
A3: b
<= 1 by
BORSUK_1: 43;
a
=
0 & b
= s by
A1,
XTUPLE_0: 1;
hence thesis by
A2,
A3,
XXREAL_0: 1;
end;
theorem ::
BORSUK_6:63
Th63: for s be
set holds
[s, 1]
in
ICC implies s
= 1
proof
let s be
set;
assume
[s, 1]
in
ICC ;
then
consider a,b be
Point of
I[01] such that
A1:
[s, 1]
=
[a, b] and
A2: b
<= ((2
* a)
- 1) by
Def10;
b
= 1 by
A1,
XTUPLE_0: 1;
then (1
+ 1)
<= (2
* a) by
A2,
XREAL_1: 19;
then
A3: (2
/ 2)
<= ((2
* a)
/ 2) by
XREAL_1: 72;
a
<= 1 & a
= s by
A1,
BORSUK_1: 43,
XTUPLE_0: 1;
hence thesis by
A3,
XXREAL_0: 1;
end;
theorem ::
BORSUK_6:64
Th64:
[
0 , 1]
in
IBB
proof
A1: 1
>= (1
- (2
*
0 )) & 1
>= ((2
*
0 )
- 1);
0 is
Point of
I[01] & 1 is
Point of
I[01] by
BORSUK_1: 43;
hence thesis by
A1,
Def9;
end;
theorem ::
BORSUK_6:65
Th65: for x be
Point of
I[01] holds
[x, 1]
in
IBB
proof
let x be
Point of
I[01] ;
x
<= 1 by
BORSUK_1: 43;
then (2
* x)
<= (2
* 1) by
XREAL_1: 64;
then
A1: 1 is
Point of
I[01] & ((2
* x)
- 1)
<= ((2
* 1)
- 1) by
BORSUK_1: 43,
XREAL_1: 13;
x
>=
0 by
BORSUK_1: 43;
then (1
- (2
* x))
<= (1
- (2
*
0 )) by
XREAL_1: 13;
hence thesis by
A1,
Def9;
end;
theorem ::
BORSUK_6:66
Th66:
[(1
/ 2),
0 ]
in
ICC &
[1, 1]
in
ICC
proof
A1:
0
<= ((2
* (1
/ 2))
- 1);
(1
/ 2) is
Point of
I[01] &
0 is
Point of
I[01] by
BORSUK_1: 43;
hence
[(1
/ 2),
0 ]
in
ICC by
A1,
Def10;
1 is
Point of
I[01] & 1
<= ((2
* 1)
- 1) by
BORSUK_1: 43;
hence thesis by
Def10;
end;
theorem ::
BORSUK_6:67
Th67:
[(1
/ 2),
0 ]
in
IBB
proof
A1:
0
<= (1
- (2
* (1
/ 2)));
(1
/ 2) is
Point of
I[01] &
0 is
Point of
I[01] by
BORSUK_1: 43;
hence thesis by
A1,
Def9;
end;
theorem ::
BORSUK_6:68
Th68: for x be
Point of
I[01] holds
[1, x]
in
ICC
proof
let x be
Point of
I[01] ;
1 is
Point of
I[01] & x
<= ((2
* 1)
- 1) by
BORSUK_1: 43;
hence thesis by
Def10;
end;
theorem ::
BORSUK_6:69
Th69: for x be
Point of
I[01] st x
>= (1
/ 2) holds
[x,
0 ]
in
ICC
proof
let x be
Point of
I[01] ;
assume x
>= (1
/ 2);
then (2
* x)
>= (2
* (1
/ 2)) by
XREAL_1: 64;
then
A1: ((2
* x)
- 1)
>= ((2
* (1
/ 2))
- 1) by
XREAL_1: 13;
0 is
Point of
I[01] by
BORSUK_1: 43;
hence thesis by
A1,
Def10;
end;
theorem ::
BORSUK_6:70
Th70: for x be
Point of
I[01] st x
<= (1
/ 2) holds
[x,
0 ]
in
IAA
proof
let x be
Point of
I[01] ;
assume x
<= (1
/ 2);
then (2
* x)
<= (2
* (1
/ 2)) by
XREAL_1: 64;
then
A1: (1
- (2
* x))
>= (1
- (2
* (1
/ 2))) by
XREAL_1: 13;
0 is
Point of
I[01] by
BORSUK_1: 43;
hence thesis by
A1,
Def8;
end;
theorem ::
BORSUK_6:71
Th71: for x be
Point of
I[01] st x
< (1
/ 2) holds not
[x,
0 ]
in
IBB & not
[x,
0 ]
in
ICC
proof
let x be
Point of
I[01] ;
assume
A1: x
< (1
/ 2);
thus not
[x,
0 ]
in
IBB
proof
assume
[x,
0 ]
in
IBB ;
then
consider a,b be
Point of
I[01] such that
A2:
[x,
0 ]
=
[a, b] and
A3: b
>= (1
- (2
* a)) and b
>= ((2
* a)
- 1) by
Def9;
x
= a & b
=
0 by
A2,
XTUPLE_0: 1;
then (
0
+ (2
* x))
>= 1 by
A3,
XREAL_1: 20;
then ((2
* x)
/ 2)
>= (1
/ 2) by
XREAL_1: 72;
hence thesis by
A1;
end;
not
[x,
0 ]
in
ICC
proof
assume
[x,
0 ]
in
ICC ;
then
consider a,b be
Point of
I[01] such that
A4:
[x,
0 ]
=
[a, b] and
A5: b
<= ((2
* a)
- 1) by
Def10;
x
= a & b
=
0 by
A4,
XTUPLE_0: 1;
then (
0
+ 1)
<= (2
* x) by
A5,
XREAL_1: 19;
then (1
/ 2)
<= ((2
* x)
/ 2) by
XREAL_1: 72;
hence thesis by
A1;
end;
hence thesis;
end;
theorem ::
BORSUK_6:72
Th72: (
IAA
/\
ICC )
=
{
[(1
/ 2),
0 ]}
proof
thus (
IAA
/\
ICC )
c=
{
[(1
/ 2),
0 ]}
proof
let x be
object;
assume
A1: x
in (
IAA
/\
ICC );
then
reconsider y = x as
Point of
[:
I[01] ,
I[01] :];
x
in
IAA by
A1,
XBOOLE_0:def 4;
then
A2: (y
`1 )
<= (1
/ 2) by
Th59;
A3: x
in
ICC by
A1,
XBOOLE_0:def 4;
then (y
`1 )
>= (1
/ 2) by
Th60;
then
A4: (y
`1 )
= (1
/ 2) by
A2,
XXREAL_0: 1;
y
in the
carrier of
[:
I[01] ,
I[01] :];
then
A5: y
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
A6: (y
`2 ) is
Point of
I[01] by
Th27;
ex q be
Point of
[:
I[01] ,
I[01] :] st q
= y & (q
`2 )
<= ((2
* (q
`1 ))
- 1) by
A3,
Th55;
then (y
`2 )
=
0 by
A4,
A6,
BORSUK_1: 43;
then y
=
[(1
/ 2),
0 ] by
A5,
A4,
MCART_1: 21;
hence thesis by
TARSKI:def 1;
end;
(1
/ 2) is
Point of
I[01] by
BORSUK_1: 43;
then
[(1
/ 2),
0 ]
in
IAA &
[(1
/ 2),
0 ]
in
ICC by
Th69,
Th70;
then
[(1
/ 2),
0 ]
in (
IAA
/\
ICC ) by
XBOOLE_0:def 4;
hence thesis by
ZFMISC_1: 31;
end;
Lm1: for x,y be
Point of
I[01] holds
[x, y]
in the
carrier of
[:
I[01] ,
I[01] :];
begin
reserve X for non
empty
pathwise_connected
TopSpace,
a1,b1,c1,d1 for
Point of X;
theorem ::
BORSUK_6:73
Th73: for P be
Path of a, b, Q be
Path of b, c, R be
Path of c, d st (a,b)
are_connected & (b,c)
are_connected & (c,d)
are_connected holds (((P
+ Q)
+ R),(P
+ (Q
+ R)))
are_homotopic
proof
let P be
Path of a, b, Q be
Path of b, c, R be
Path of c, d such that
A1: (a,b)
are_connected & (b,c)
are_connected and
A2: (c,d)
are_connected ;
(a,c)
are_connected & (
RePar (((P
+ Q)
+ R),
3RP ))
= (P
+ (Q
+ R)) by
A1,
A2,
Th42,
Th52;
hence thesis by
A2,
Th42,
Th45,
Th49;
end;
theorem ::
BORSUK_6:74
for P be
Path of a1, b1, Q be
Path of b1, c1, R be
Path of c1, d1 holds (((P
+ Q)
+ R),(P
+ (Q
+ R)))
are_homotopic
proof
let P be
Path of a1, b1, Q be
Path of b1, c1, R be
Path of c1, d1;
A1: (c1,d1)
are_connected by
BORSUK_2:def 3;
(a1,b1)
are_connected & (b1,c1)
are_connected by
BORSUK_2:def 3;
hence thesis by
A1,
Th73;
end;
theorem ::
BORSUK_6:75
Th75: for P1,P2 be
Path of a, b, Q1,Q2 be
Path of b, c st (a,b)
are_connected & (b,c)
are_connected & (P1,P2)
are_homotopic & (Q1,Q2)
are_homotopic holds ((P1
+ Q1),(P2
+ Q2))
are_homotopic
proof
set BB =
[:
I[01] ,
I[01] :];
reconsider R1 = (
L[01] (
0 ,(1
/ 2),
0 ,1)) as
continuous
Function of (
Closed-Interval-TSpace (
0 ,(1
/ 2))),
I[01] by
Th34,
TOPMETR: 20;
let P1,P2 be
Path of a, b, Q1,Q2 be
Path of b, c;
assume that
A1: (a,b)
are_connected & (b,c)
are_connected and
A2: (P1,P2)
are_homotopic and
A3: (Q1,Q2)
are_homotopic ;
reconsider R2 = (
L[01] ((1
/ 2),1,
0 ,1)) as
continuous
Function of (
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] by
Th34,
TOPMETR: 20;
A4: 1 is
Point of
I[01] by
BORSUK_1: 43;
A5:
0 is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider A01 =
[.
0 , 1.] as non
empty
Subset of
I[01] by
A4,
BORSUK_4: 24;
A6: (1
/ 2) is
Point of
I[01] by
BORSUK_1: 43;
then
reconsider B01 =
[.
0 , (1
/ 2).] as non
empty
Subset of
I[01] by
A5,
BORSUK_4: 24;
reconsider N2 =
[:
[.(1
/ 2), 1.],
[.
0 , 1.]:] as
compact non
empty
Subset of BB by
A5,
A4,
A6,
Th9;
reconsider N1 =
[:
[.
0 , (1
/ 2).],
[.
0 , 1.]:] as
compact non
empty
Subset of BB by
A5,
A4,
A6,
Th9;
set T1 = (BB
| N1);
set T2 = (BB
| N2);
A01
= (
[#]
I[01] ) by
BORSUK_1: 40;
then
A7:
I[01]
= (
I[01]
| A01) by
TSEP_1: 93;
set f1 =
[:R1, (
id
I[01] ):], g1 =
[:R2, (
id
I[01] ):];
reconsider f1 as
continuous
Function of
[:(
Closed-Interval-TSpace (
0 ,(1
/ 2))),
I[01] :],
[:
I[01] ,
I[01] :];
reconsider g1 as
continuous
Function of
[:(
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] :],
[:
I[01] ,
I[01] :];
A8: (
dom g1)
= the
carrier of
[:(
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] :] by
FUNCT_2:def 1
.=
[:the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)), the
carrier of
I[01] :] by
BORSUK_1:def 2;
reconsider B02 =
[.(1
/ 2), 1.] as non
empty
Subset of
I[01] by
A4,
A6,
BORSUK_4: 24;
consider f be
Function of
[:
I[01] ,
I[01] :], T such that
A9: f is
continuous and
A10: for s be
Point of
I[01] holds (f
. (s,
0 ))
= (P1
. s) & (f
. (s,1))
= (P2
. s) & for t be
Point of
I[01] holds (f
. (
0 ,t))
= a & (f
. (1,t))
= b by
A2;
(
Closed-Interval-TSpace (
0 ,(1
/ 2)))
= (
I[01]
| B01) by
TOPMETR: 24;
then T1
=
[:(
Closed-Interval-TSpace (
0 ,(1
/ 2))),
I[01] :] by
A7,
BORSUK_3: 22;
then
reconsider K1 = (f
* f1) as
continuous
Function of T1, T by
A9;
consider g be
Function of
[:
I[01] ,
I[01] :], T such that
A11: g is
continuous and
A12: for s be
Point of
I[01] holds (g
. (s,
0 ))
= (Q1
. s) & (g
. (s,1))
= (Q2
. s) & for t be
Point of
I[01] holds (g
. (
0 ,t))
= b & (g
. (1,t))
= c by
A3;
(
Closed-Interval-TSpace ((1
/ 2),1))
= (
I[01]
| B02) by
TOPMETR: 24;
then T2
=
[:(
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] :] by
A7,
BORSUK_3: 22;
then
reconsider K2 = (g
* g1) as
continuous
Function of T2, T by
A11;
A13: (
dom K2)
= the
carrier of
[:(
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] :] by
FUNCT_2:def 1
.=
[:the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)), the
carrier of
I[01] :] by
BORSUK_1:def 2;
A14: for p be
set st p
in ((
[#] T1)
/\ (
[#] T2)) holds (K1
. p)
= (K2
. p)
proof
A15: (R2
. (1
/ 2))
=
0 by
Th33;
let p be
set;
A16: (R1
. (1
/ 2))
= 1 by
Th33;
assume p
in ((
[#] T1)
/\ (
[#] T2));
then p
in
[:
{(1
/ 2)},
[.
0 , 1.]:] by
Th29;
then
consider x,y be
object such that
A17: x
in
{(1
/ 2)} and
A18: y
in
[.
0 , 1.] and
A19: p
=
[x, y] by
ZFMISC_1:def 2;
A20: y
in the
carrier of
I[01] by
A18,
TOPMETR: 18,
TOPMETR: 20;
reconsider y as
Point of
I[01] by
A18,
TOPMETR: 18,
TOPMETR: 20;
A21: x
= (1
/ 2) by
A17,
TARSKI:def 1;
then x
in
[.(1
/ 2), 1.] by
XXREAL_1: 1;
then
A22: x
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then p
in
[:the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)), the
carrier of
I[01] :] by
A19,
A20,
ZFMISC_1: 87;
then p
in the
carrier of
[:(
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] :] by
BORSUK_1:def 2;
then
A23: p
in (
dom g1) by
FUNCT_2:def 1;
x
in
[.
0 , (1
/ 2).] by
A21,
XXREAL_1: 1;
then
A24: x
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
TOPMETR: 18;
then x
in (
dom R1) by
FUNCT_2:def 1;
then
A25:
[x, y]
in
[:(
dom R1), (
dom (
id
I[01] )):] by
ZFMISC_1: 87;
x
in (
dom R2) by
A22,
FUNCT_2:def 1;
then
A26:
[x, y]
in
[:(
dom R2), (
dom (
id
I[01] )):] by
ZFMISC_1: 87;
p
in
[:the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))), the
carrier of
I[01] :] by
A19,
A20,
A24,
ZFMISC_1: 87;
then p
in the
carrier of
[:(
Closed-Interval-TSpace (
0 ,(1
/ 2))),
I[01] :] by
BORSUK_1:def 2;
then p
in (
dom f1) by
FUNCT_2:def 1;
then (K1
. p)
= (f
. (f1
. (x,y))) by
A19,
FUNCT_1: 13
.= (f
. ((R1
. x),((
id
I[01] )
. y))) by
A25,
FUNCT_3: 65
.= b by
A10,
A21,
A16
.= (g
. ((R2
. x),((
id
I[01] )
. y))) by
A12,
A21,
A15
.= (g
. (g1
. (x,y))) by
A26,
FUNCT_3: 65
.= (K2
. p) by
A19,
A23,
FUNCT_1: 13;
hence thesis;
end;
((
[#] T1)
\/ (
[#] T2))
= (
[#] BB) by
Th28;
then
consider h be
Function of
[:
I[01] ,
I[01] :], T such that
A27: h
= (K1
+* K2) and
A28: h is
continuous by
A14,
BORSUK_2: 1;
A29: (
dom f1)
= the
carrier of
[:(
Closed-Interval-TSpace (
0 ,(1
/ 2))),
I[01] :] by
FUNCT_2:def 1
.=
[:the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))), the
carrier of
I[01] :] by
BORSUK_1:def 2;
A30: for s be
Point of
I[01] holds (h
. (s,
0 ))
= ((P1
+ Q1)
. s) & (h
. (s,1))
= ((P2
+ Q2)
. s)
proof
let s be
Point of
I[01] ;
A31: (h
. (s,1))
= ((P2
+ Q2)
. s)
proof
per cases ;
suppose
A32: s
< (1
/ 2);
then
A33: (2
* s) is
Point of
I[01] by
Th3;
A34: 1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A35: 1
in (
dom (
id
I[01] ));
A36: s
>=
0 by
BORSUK_1: 43;
then
A37: (R1
. s)
= ((((1
-
0 )
/ ((1
/ 2)
-
0 ))
* (s
-
0 ))
+
0 ) by
A32,
Th35
.= (2
* s);
s
in
[.
0 , (1
/ 2).] by
A32,
A36,
XXREAL_1: 1;
then
A38: s
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
TOPMETR: 18;
then
A39:
[s, 1]
in (
dom f1) by
A29,
A34,
ZFMISC_1: 87;
s
in (
dom R1) by
A38,
FUNCT_2:def 1;
then
A40:
[s, 1]
in
[:(
dom R1), (
dom (
id
I[01] )):] by
A35,
ZFMISC_1: 87;
not s
in
[.(1
/ 2), 1.] by
A32,
XXREAL_1: 1;
then not s
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then not
[s, 1]
in (
dom K2) by
A13,
ZFMISC_1: 87;
then (h
. (s,1))
= (K1
. (s,1)) by
A27,
FUNCT_4: 11
.= (f
. (f1
. (s,1))) by
A39,
FUNCT_1: 13
.= (f
. ((R1
. s),((
id
I[01] )
. 1))) by
A40,
FUNCT_3: 65
.= (f
. ((2
* s),1)) by
A4,
A37,
FUNCT_1: 18
.= (P2
. (2
* s)) by
A10,
A33;
hence thesis by
A1,
A32,
BORSUK_2:def 5;
end;
suppose
A41: s
>= (1
/ 2);
A42: s
<= 1 by
BORSUK_1: 43;
then
A43: (R2
. s)
= ((((1
-
0 )
/ (1
- (1
/ 2)))
* (s
- (1
/ 2)))
+
0 ) by
A41,
Th35
.= ((2
* s)
- 1);
A44: ((2
* s)
- 1) is
Point of
I[01] by
A41,
Th4;
A45: 1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A46: 1
in (
dom (
id
I[01] ));
s
in
[.(1
/ 2), 1.] by
A41,
A42,
XXREAL_1: 1;
then
A47: s
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then
A48:
[s, 1]
in (
dom g1) by
A8,
A45,
ZFMISC_1: 87;
s
in (
dom R2) by
A47,
FUNCT_2:def 1;
then
A49:
[s, 1]
in
[:(
dom R2), (
dom (
id
I[01] )):] by
A46,
ZFMISC_1: 87;
[s, 1]
in (
dom K2) by
A13,
A47,
A45,
ZFMISC_1: 87;
then (h
. (s,1))
= (K2
. (s,1)) by
A27,
FUNCT_4: 13
.= (g
. (g1
. (s,1))) by
A48,
FUNCT_1: 13
.= (g
. ((R2
. s),((
id
I[01] )
. 1))) by
A49,
FUNCT_3: 65
.= (g
. (((2
* s)
- 1),1)) by
A4,
A43,
FUNCT_1: 18
.= (Q2
. ((2
* s)
- 1)) by
A12,
A44;
hence thesis by
A1,
A41,
BORSUK_2:def 5;
end;
end;
(h
. (s,
0 ))
= ((P1
+ Q1)
. s)
proof
per cases ;
suppose
A50: s
< (1
/ 2);
then
A51: (2
* s) is
Point of
I[01] by
Th3;
A52:
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A53:
0
in (
dom (
id
I[01] ));
A54: s
>=
0 by
BORSUK_1: 43;
then
A55: (R1
. s)
= ((((1
-
0 )
/ ((1
/ 2)
-
0 ))
* (s
-
0 ))
+
0 ) by
A50,
Th35
.= (2
* s);
s
in
[.
0 , (1
/ 2).] by
A50,
A54,
XXREAL_1: 1;
then
A56: s
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
TOPMETR: 18;
then
A57:
[s,
0 ]
in (
dom f1) by
A29,
A52,
ZFMISC_1: 87;
s
in (
dom R1) by
A56,
FUNCT_2:def 1;
then
A58:
[s,
0 ]
in
[:(
dom R1), (
dom (
id
I[01] )):] by
A53,
ZFMISC_1: 87;
not s
in
[.(1
/ 2), 1.] by
A50,
XXREAL_1: 1;
then not s
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then not
[s,
0 ]
in (
dom K2) by
A13,
ZFMISC_1: 87;
then (h
. (s,
0 ))
= (K1
. (s,
0 )) by
A27,
FUNCT_4: 11
.= (f
. (f1
. (s,
0 ))) by
A57,
FUNCT_1: 13
.= (f
. ((R1
. s),((
id
I[01] )
.
0 ))) by
A58,
FUNCT_3: 65
.= (f
. ((2
* s),
0 )) by
A5,
A55,
FUNCT_1: 18
.= (P1
. (2
* s)) by
A10,
A51;
hence thesis by
A1,
A50,
BORSUK_2:def 5;
end;
suppose
A59: s
>= (1
/ 2);
A60: s
<= 1 by
BORSUK_1: 43;
then
A61: (R2
. s)
= ((((1
-
0 )
/ (1
- (1
/ 2)))
* (s
- (1
/ 2)))
+
0 ) by
A59,
Th35
.= ((2
* s)
- 1);
A62: ((2
* s)
- 1) is
Point of
I[01] by
A59,
Th4;
A63:
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A64:
0
in (
dom (
id
I[01] ));
s
in
[.(1
/ 2), 1.] by
A59,
A60,
XXREAL_1: 1;
then
A65: s
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then
A66:
[s,
0 ]
in (
dom g1) by
A8,
A63,
ZFMISC_1: 87;
s
in (
dom R2) by
A65,
FUNCT_2:def 1;
then
A67:
[s,
0 ]
in
[:(
dom R2), (
dom (
id
I[01] )):] by
A64,
ZFMISC_1: 87;
[s,
0 ]
in (
dom K2) by
A13,
A65,
A63,
ZFMISC_1: 87;
then (h
. (s,
0 ))
= (K2
. (s,
0 )) by
A27,
FUNCT_4: 13
.= (g
. (g1
. (s,
0 ))) by
A66,
FUNCT_1: 13
.= (g
. ((R2
. s),((
id
I[01] )
.
0 ))) by
A67,
FUNCT_3: 65
.= (g
. (((2
* s)
- 1),
0 )) by
A5,
A61,
FUNCT_1: 18
.= (Q1
. ((2
* s)
- 1)) by
A12,
A62;
hence thesis by
A1,
A59,
BORSUK_2:def 5;
end;
end;
hence thesis by
A31;
end;
take h;
for t be
Point of
I[01] holds (h
. (
0 ,t))
= a & (h
. (1,t))
= c
proof
let t be
Point of
I[01] ;
A68: (
dom K2)
= the
carrier of
[:(
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] :] by
FUNCT_2:def 1
.=
[:the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)), the
carrier of
I[01] :] by
BORSUK_1:def 2;
0
in
[.
0 , (1
/ 2).] by
XXREAL_1: 1;
then
A69:
0
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
TOPMETR: 18;
then
A70:
[
0 , t]
in (
dom f1) by
A29,
ZFMISC_1: 87;
0
in (
dom R1) by
A69,
FUNCT_2:def 1;
then
A71:
[
0 , t]
in
[:(
dom R1), (
dom (
id
I[01] )):] by
ZFMISC_1: 87;
not
0
in
[.(1
/ 2), 1.] by
XXREAL_1: 1;
then not
0
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then not
[
0 , t]
in (
dom K2) by
A68,
ZFMISC_1: 87;
hence (h
. (
0 ,t))
= (K1
. (
0 ,t)) by
A27,
FUNCT_4: 11
.= (f
. (f1
. (
0 ,t))) by
A70,
FUNCT_1: 13
.= (f
. ((R1
.
0 ),((
id
I[01] )
. t))) by
A71,
FUNCT_3: 65
.= (f
. ((R1
.
0 ),t)) by
FUNCT_1: 18
.= (f
. (
0 ,t)) by
Th33
.= a by
A10;
1
in
[.(1
/ 2), 1.] by
XXREAL_1: 1;
then
A72: 1
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then 1
in (
dom R2) by
FUNCT_2:def 1;
then
A73:
[1, t]
in
[:(
dom R2), (
dom (
id
I[01] )):] by
ZFMISC_1: 87;
1
in
[.(1
/ 2), 1.] by
XXREAL_1: 1;
then 1
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
then
A74:
[1, t]
in (
dom g1) by
A8,
ZFMISC_1: 87;
[1, t]
in (
dom K2) by
A68,
A72,
ZFMISC_1: 87;
then (h
. (1,t))
= (K2
. (1,t)) by
A27,
FUNCT_4: 13
.= (g
. (g1
. (1,t))) by
A74,
FUNCT_1: 13
.= (g
. ((R2
. 1),((
id
I[01] )
. t))) by
A73,
FUNCT_3: 65
.= (g
. ((R2
. 1),t)) by
FUNCT_1: 18
.= (g
. (1,t)) by
Th33
.= c by
A12;
hence thesis;
end;
hence thesis by
A28,
A30;
end;
theorem ::
BORSUK_6:76
for P1,P2 be
Path of a1, b1, Q1,Q2 be
Path of b1, c1 st (P1,P2)
are_homotopic & (Q1,Q2)
are_homotopic holds ((P1
+ Q1),(P2
+ Q2))
are_homotopic
proof
let P1,P2 be
Path of a1, b1, Q1,Q2 be
Path of b1, c1;
(a1,b1)
are_connected & (b1,c1)
are_connected by
BORSUK_2:def 3;
hence thesis by
Th75;
end;
theorem ::
BORSUK_6:77
Th77: for P,Q be
Path of a, b st (a,b)
are_connected & (P,Q)
are_homotopic holds ((
- P),(
- Q))
are_homotopic
proof
reconsider fF = (
id
I[01] ) as
continuous
Function of
I[01] ,
I[01] ;
reconsider fB = (
L[01] (((
0 ,1)
(#) ),(
(#) (
0 ,1)))) as
continuous
Function of
I[01] ,
I[01] by
TOPMETR: 20,
TREAL_1: 8;
let P,Q be
Path of a, b;
assume
A1: (a,b)
are_connected ;
set F =
[:fB, fF:];
A2: (
dom fB)
= the
carrier of
I[01] by
FUNCT_2:def 1;
assume (P,Q)
are_homotopic ;
then
consider f be
Function of
[:
I[01] ,
I[01] :], T such that
A3: f is
continuous and
A4: for s be
Point of
I[01] holds (f
. (s,
0 ))
= (P
. s) & (f
. (s,1))
= (Q
. s) & for t be
Point of
I[01] holds (f
. (
0 ,t))
= a & (f
. (1,t))
= b;
reconsider ff = (f
* F) as
Function of
[:
I[01] ,
I[01] :], T;
take ff;
thus ff is
continuous by
A3;
A5:
0 is
Point of
I[01] by
BORSUK_1: 43;
A6: for t be
Point of
I[01] holds (ff
. (
0 ,t))
= b & (ff
. (1,t))
= a
proof
A7: for t be
Point of
I[01] , t9 be
Real st t
= t9 holds (fB
. t)
= (1
- t9)
proof
let t be
Point of
I[01] , t9 be
Real;
assume
A8: t
= t9;
reconsider ee = t as
Point of (
Closed-Interval-TSpace (
0 ,1)) by
TOPMETR: 20;
A9: ((
0 ,1)
(#) )
= 1 & (
(#) (
0 ,1))
=
0 by
TREAL_1:def 1,
TREAL_1:def 2;
(fB
. t)
= (fB
. ee)
.= (((
0
- 1)
* t9)
+ 1) by
A8,
A9,
TREAL_1: 7
.= (1
- (1
* t9));
hence thesis;
end;
then
A10: (fB
.
0 )
= (1
-
0 ) by
A5
.= 1;
1 is
Point of
I[01] by
BORSUK_1: 43;
then
A11: (fB
. 1)
= (1
- 1) by
A7
.=
0 ;
let t be
Point of
I[01] ;
A12: (
dom fF)
= the
carrier of
I[01] ;
reconsider tt = t as
Real;
A13: (
dom fB)
= the
carrier of
I[01] by
FUNCT_2:def 1;
then
A14:
0
in (
dom fB) by
BORSUK_1: 43;
A15: (
dom F)
=
[:(
dom fB), (
dom fF):] by
FUNCT_3:def 8;
then
A16:
[
0 , t]
in (
dom F) by
A14,
ZFMISC_1: 87;
A17: 1
in (
dom fB) by
A13,
BORSUK_1: 43;
then
A18:
[1, t]
in (
dom F) by
A15,
ZFMISC_1: 87;
(F
. (1,t))
=
[(fB
. 1), (fF
. t)] by
A12,
A17,
FUNCT_3:def 8
.=
[
0 , tt] by
A11,
FUNCT_1: 18;
then
A19: (ff
. (1,t))
= (f
. (
0 ,t)) by
A18,
FUNCT_1: 13
.= a by
A4;
(F
. (
0 ,t))
=
[(fB
.
0 ), (fF
. t)] by
A12,
A14,
FUNCT_3:def 8
.=
[1, tt] by
A10,
FUNCT_1: 18;
then (ff
. (
0 ,t))
= (f
. (1,t)) by
A16,
FUNCT_1: 13
.= b by
A4;
hence thesis by
A19;
end;
for s be
Point of
I[01] holds (ff
. (s,
0 ))
= ((
- P)
. s) & (ff
. (s,1))
= ((
- Q)
. s)
proof
let s be
Point of
I[01] ;
A20: for t be
Point of
I[01] , t9 be
Real st t
= t9 holds (fB
. t)
= (1
- t9)
proof
let t be
Point of
I[01] , t9 be
Real;
assume
A21: t
= t9;
reconsider ee = t as
Point of (
Closed-Interval-TSpace (
0 ,1)) by
TOPMETR: 20;
A22: ((
0 ,1)
(#) )
= 1 & (
(#) (
0 ,1))
=
0 by
TREAL_1:def 1,
TREAL_1:def 2;
(fB
. t)
= (fB
. ee)
.= (((
0
- 1)
* t9)
+ 1) by
A21,
A22,
TREAL_1: 7
.= (1
- (1
* t9));
hence thesis;
end;
A23: (fB
. s)
= (1
- s) by
A20;
A24: 1 is
Point of
I[01] by
BORSUK_1: 43;
A25: (
dom F)
=
[:(
dom fB), (
dom fF):] by
FUNCT_3:def 8;
A26: 1
in (
dom fF) by
BORSUK_1: 43;
then
A27:
[s, 1]
in (
dom F) by
A2,
A25,
ZFMISC_1: 87;
A28:
0
in (
dom fF) by
BORSUK_1: 43;
then
A29:
[s,
0 ]
in (
dom F) by
A2,
A25,
ZFMISC_1: 87;
A30: (1
- s) is
Point of
I[01] by
JORDAN5B: 4;
(F
. (s,1))
=
[(fB
. s), (fF
. 1)] by
A2,
A26,
FUNCT_3:def 8
.=
[(1
- s), 1] by
A23,
A24,
FUNCT_1: 18;
then
A31: (ff
. (s,1))
= (f
. ((1
- s),1)) by
A27,
FUNCT_1: 13
.= (Q
. (1
- s)) by
A4,
A30
.= ((
- Q)
. s) by
A1,
BORSUK_2:def 6;
(F
. (s,
0 ))
=
[(fB
. s), (fF
.
0 )] by
A2,
A28,
FUNCT_3:def 8
.=
[(1
- s),
0 ] by
A5,
A23,
FUNCT_1: 18;
then (ff
. (s,
0 ))
= (f
. ((1
- s),
0 )) by
A29,
FUNCT_1: 13
.= (P
. (1
- s)) by
A4,
A30
.= ((
- P)
. s) by
A1,
BORSUK_2:def 6;
hence thesis by
A31;
end;
hence thesis by
A6;
end;
theorem ::
BORSUK_6:78
for P,Q be
Path of a1, b1 st (P,Q)
are_homotopic holds ((
- P),(
- Q))
are_homotopic by
Th77,
BORSUK_2:def 3;
theorem ::
BORSUK_6:79
for P,Q,R be
Path of a, b holds (P,Q)
are_homotopic & (Q,R)
are_homotopic implies (P,R)
are_homotopic
proof
(1
/ 2)
in
[.
0 , (1
/ 2).] by
XXREAL_1: 1;
then
A1: (1
/ 2)
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
TOPMETR: 18;
reconsider B02 =
[.(1
/ 2), 1.] as non
empty
Subset of
I[01] by
BORSUK_1: 40,
XXREAL_1: 1,
XXREAL_1: 34;
A2: 1
in
[.
0 , 1.] by
XXREAL_1: 1;
A3: (1
/ 2)
in
[.(1
/ 2), 1.] by
XXREAL_1: 1;
then
A4: (1
/ 2)
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
TOPMETR: 18;
[.
0 , (1
/ 2).]
c= the
carrier of
I[01] by
BORSUK_1: 40,
XXREAL_1: 34;
then
A5:
[:
[.
0 , 1.],
[.
0 , (1
/ 2).]:]
c=
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1: 40,
ZFMISC_1: 96;
A6: the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2)))
=
[.
0 , (1
/ 2).] by
TOPMETR: 18;
0
in
[.
0 , (1
/ 2).] by
XXREAL_1: 1;
then
reconsider Ewa =
[:
[.
0 , 1.],
[.
0 , (1
/ 2).]:] as non
empty
Subset of
[:
I[01] ,
I[01] :] by
A5,
A2,
BORSUK_1:def 2;
set T1 = (
[:
I[01] ,
I[01] :]
| Ewa);
reconsider P2 = (
P[01] ((1
/ 2),1,(
(#) (
0 ,1)),((
0 ,1)
(#) ))) as
continuous
Function of (
Closed-Interval-TSpace ((1
/ 2),1)),
I[01] by
TOPMETR: 20,
TREAL_1: 12;
reconsider P1 = (
P[01] (
0 ,(1
/ 2),(
(#) (
0 ,1)),((
0 ,1)
(#) ))) as
continuous
Function of (
Closed-Interval-TSpace (
0 ,(1
/ 2))),
I[01] by
TOPMETR: 20,
TREAL_1: 12;
let P,Q,R be
Path of a, b;
assume that
A7: (P,Q)
are_homotopic and
A8: (Q,R)
are_homotopic ;
consider f be
Function of
[:
I[01] ,
I[01] :], T such that
A9: f is
continuous and
A10: for s be
Point of
I[01] holds (f
. (s,
0 ))
= (P
. s) & (f
. (s,1))
= (Q
. s) & for t be
Point of
I[01] holds (f
. (
0 ,t))
= a & (f
. (1,t))
= b by
A7;
A11: the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1))
=
[.(1
/ 2), 1.] by
TOPMETR: 18;
[.
0 , 1.]
c= the
carrier of
I[01] by
BORSUK_1: 40;
then
reconsider A01 =
[.
0 , 1.] as non
empty
Subset of
I[01] by
XXREAL_1: 1;
reconsider B01 =
[.
0 , (1
/ 2).] as non
empty
Subset of
I[01] by
BORSUK_1: 40,
XXREAL_1: 1,
XXREAL_1: 34;
A12: the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1))
=
[.(1
/ 2), 1.] by
TOPMETR: 18;
A01
= (
[#]
I[01] ) by
BORSUK_1: 40;
then
A13:
I[01]
= (
I[01]
| A01) by
TSEP_1: 93;
[.(1
/ 2), 1.]
c= the
carrier of
I[01] by
BORSUK_1: 40,
XXREAL_1: 34;
then
A14:
[:
[.
0 , 1.],
[.(1
/ 2), 1.]:]
c=
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1: 40,
ZFMISC_1: 96;
A15: 1
in the
carrier of
I[01] by
BORSUK_1: 43;
1
in
[.(1
/ 2), 1.] by
XXREAL_1: 1;
then
reconsider Ewa1 =
[:
[.
0 , 1.],
[.(1
/ 2), 1.]:] as non
empty
Subset of
[:
I[01] ,
I[01] :] by
A2,
A14,
BORSUK_1:def 2;
set T2 = (
[:
I[01] ,
I[01] :]
| Ewa1);
set e1 =
[:(
id
I[01] ), P1:], e2 =
[:(
id
I[01] ), P2:];
A16: (
dom (
id
I[01] ))
= the
carrier of
I[01] & (
dom (
P[01] ((1
/ 2),1,(
(#) (
0 ,1)),((
0 ,1)
(#) ))))
= the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
FUNCT_2:def 1;
A17: (
rng e2)
=
[:(
rng (
id
I[01] )), (
rng (
P[01] ((1
/ 2),1,(
(#) (
0 ,1)),((
0 ,1)
(#) )))):] by
FUNCT_3: 67;
consider g be
Function of
[:
I[01] ,
I[01] :], T such that
A18: g is
continuous and
A19: for s be
Point of
I[01] holds (g
. (s,
0 ))
= (Q
. s) & (g
. (s,1))
= (R
. s) & for t be
Point of
I[01] holds (g
. (
0 ,t))
= a & (g
. (1,t))
= b by
A8;
set f1 = (f
* e1), g1 = (g
* e2);
(
dom g)
= the
carrier of
[:
I[01] ,
I[01] :] by
FUNCT_2:def 1
.=
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A20: (
dom g1)
= (
dom e2) by
A17,
RELAT_1: 27,
TOPMETR: 20,
ZFMISC_1: 96
.=
[:the
carrier of
I[01] , the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)):] by
A16,
FUNCT_3:def 8;
(
Closed-Interval-TSpace ((1
/ 2),1))
= (
I[01]
| B02) by
TOPMETR: 24;
then e2 is
continuous
Function of
[:
I[01] , (
Closed-Interval-TSpace ((1
/ 2),1)):],
[:
I[01] ,
I[01] :] & T2
=
[:
I[01] , (
Closed-Interval-TSpace ((1
/ 2),1)):] by
A13,
BORSUK_3: 22;
then
reconsider g1 as
continuous
Function of T2, T by
A18;
(
Closed-Interval-TSpace (
0 ,(1
/ 2)))
= (
I[01]
| B01) by
TOPMETR: 24;
then e1 is
continuous
Function of
[:
I[01] , (
Closed-Interval-TSpace (
0 ,(1
/ 2))):],
[:
I[01] ,
I[01] :] & T1
=
[:
I[01] , (
Closed-Interval-TSpace (
0 ,(1
/ 2))):] by
A13,
BORSUK_3: 22;
then
reconsider f1 as
continuous
Function of T1, T by
A9;
A21: 1 is
Point of
I[01] by
BORSUK_1: 43;
A22:
0 is
Point of
I[01] by
BORSUK_1: 43;
then
A23:
[.
0 , 1.] is
compact
Subset of
I[01] by
A21,
BORSUK_4: 24;
A24: (1
/ 2) is
Point of
I[01] by
BORSUK_1: 43;
then
[.
0 , (1
/ 2).] is
compact
Subset of
I[01] by
A22,
BORSUK_4: 24;
then
A25: Ewa is
compact
Subset of
[:
I[01] ,
I[01] :] by
A23,
BORSUK_3: 23;
[.(1
/ 2), 1.] is
compact
Subset of
I[01] by
A21,
A24,
BORSUK_4: 24;
then
A26: Ewa1 is
compact
Subset of
[:
I[01] ,
I[01] :] by
A23,
BORSUK_3: 23;
A27: (
dom e1)
= the
carrier of
[:
I[01] , (
Closed-Interval-TSpace (
0 ,(1
/ 2))):] by
FUNCT_2:def 1
.=
[:the
carrier of
I[01] , the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))):] by
BORSUK_1:def 2;
A28: (
dom e2)
=
[:(
dom (
id
I[01] )), (
dom P2):] by
FUNCT_3:def 8;
A29: (
dom e1)
=
[:(
dom (
id
I[01] )), (
dom P1):] by
FUNCT_3:def 8;
A30: (
dom e2)
= the
carrier of
[:
I[01] , (
Closed-Interval-TSpace ((1
/ 2),1)):] by
FUNCT_2:def 1
.=
[:the
carrier of
I[01] , the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)):] by
BORSUK_1:def 2;
A31: (
[#] T1)
= Ewa & (
[#] T2)
= Ewa1 by
PRE_TOPC:def 5;
then
A32: ((
[#] T1)
/\ (
[#] T2))
=
[:
[.
0 , 1.], (
[.
0 , (1
/ 2).]
/\
[.(1
/ 2), 1.]):] by
ZFMISC_1: 99
.=
[:
[.
0 , 1.],
{(1
/ 2)}:] by
XXREAL_1: 418;
A33: for p be
set st p
in ((
[#] T1)
/\ (
[#] T2)) holds (f1
. p)
= (g1
. p)
proof
let p be
set;
assume p
in ((
[#] T1)
/\ (
[#] T2));
then
consider x,y be
object such that
A34: x
in
[.
0 , 1.] and
A35: y
in
{(1
/ 2)} and
A36: p
=
[x, y] by
A32,
ZFMISC_1:def 2;
x
in { r where r be
Real :
0
<= r & r
<= 1 } by
A34,
RCOMP_1:def 1;
then
A37: ex r1 be
Real st r1
= x &
0
<= r1 & r1
<= 1;
then
reconsider x9 = x as
Point of
I[01] by
BORSUK_1: 43;
A38: y
= (1
/ 2) by
A35,
TARSKI:def 1;
(f1
. p)
= (g1
. p)
proof
(1
/ 2)
in
[.
0 , (1
/ 2).] by
XXREAL_1: 1;
then
reconsider y9 = (1
/ 2) as
Point of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
TOPMETR: 18;
set t9 = (1
/ 2);
reconsider r1 = (
(#) (
0 ,1)), r2 = ((
0 ,1)
(#) ) as
Real;
A39: (P1
. y9)
= ((((r2
- r1)
/ ((1
/ 2)
-
0 ))
* t9)
+ ((((1
/ 2)
* r1)
- (
0
* r2))
/ ((1
/ 2)
-
0 ))) by
TREAL_1: 11
.= ((((1
- r1)
/ ((1
/ 2)
-
0 ))
* t9)
+ ((((1
/ 2)
* r1)
- (
0
* r2))
/ ((1
/ 2)
-
0 ))) by
TREAL_1:def 2
.= ((((1
-
0 )
/ ((1
/ 2)
-
0 ))
* t9)
+ ((((1
/ 2)
* r1)
- (
0
* r2))
/ ((1
/ 2)
-
0 ))) by
TREAL_1:def 1
.= ((((1
-
0 )
/ ((1
/ 2)
-
0 ))
* t9)
+ ((((1
/ 2)
*
0 )
- (
0
* 1))
/ ((1
/ 2)
-
0 ))) by
TREAL_1:def 1
.= 1;
reconsider y9 = (1
/ 2) as
Point of (
Closed-Interval-TSpace ((1
/ 2),1)) by
A3,
TOPMETR: 18;
A40: (P2
. y9)
= ((((r2
- r1)
/ (1
- (1
/ 2)))
* t9)
+ (((1
* r1)
- ((1
/ 2)
* r2))
/ (1
- (1
/ 2)))) by
TREAL_1: 11
.=
0 by
BORSUK_1:def 14,
TREAL_1: 5;
A41: x
in the
carrier of
I[01] by
A37,
BORSUK_1: 43;
then
A42:
[x, y]
in (
dom e2) by
A30,
A4,
A38,
ZFMISC_1: 87;
A43:
[x, y]
in (
dom e1) by
A1,
A27,
A38,
A41,
ZFMISC_1: 87;
then (f1
. p)
= (f
. (e1
. (x,y))) by
A36,
FUNCT_1: 13
.= (f
. (((
id
I[01] )
. x),(P1
. y))) by
A29,
A43,
FUNCT_3: 65
.= (f
. (x9,1)) by
A38,
A39,
FUNCT_1: 18
.= (Q
. x9) by
A10
.= (g
. (x9,
0 )) by
A19
.= (g
. (((
id
I[01] )
. x9),(P2
. y))) by
A38,
A40,
FUNCT_1: 18
.= (g
. (e2
. (x,y))) by
A28,
A42,
FUNCT_3: 65
.= (g1
. p) by
A36,
A42,
FUNCT_1: 13;
hence thesis;
end;
hence thesis;
end;
((
[#] T1)
\/ (
[#] T2))
=
[:
[.
0 , 1.], (
[.
0 , (1
/ 2).]
\/
[.(1
/ 2), 1.]):] by
A31,
ZFMISC_1: 97
.=
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1: 40,
XXREAL_1: 174
.= (
[#]
[:
I[01] ,
I[01] :]) by
BORSUK_1:def 2;
then
consider h be
Function of
[:
I[01] ,
I[01] :], T such that
A44: h
= (f1
+* g1) and
A45: h is
continuous by
A25,
A26,
A33,
BORSUK_2: 1;
A46: the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2)))
=
[.
0 , (1
/ 2).] by
TOPMETR: 18;
A47: for t be
Point of
I[01] holds (h
. (
0 ,t))
= a & (h
. (1,t))
= b
proof
let t be
Point of
I[01] ;
per cases ;
suppose
A48: t
< (1
/ 2);
reconsider r1 = (
(#) (
0 ,1)), r2 = ((
0 ,1)
(#) ) as
Real;
A49:
0
<= t by
BORSUK_1: 43;
then
A50: t
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
A6,
A48,
XXREAL_1: 1;
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A51:
[
0 , t]
in (
dom e1) by
A27,
A50,
ZFMISC_1: 87;
(P1
. t)
= ((((r2
- r1)
/ ((1
/ 2)
-
0 ))
* t)
+ ((((1
/ 2)
* r1)
- (
0
* r2))
/ ((1
/ 2)
-
0 ))) by
A50,
TREAL_1: 11
.= ((((1
- r1)
/ (1
/ 2))
* t)
+ (((1
/ 2)
* r1)
/ (1
/ 2))) by
TREAL_1:def 2
.= ((((1
-
0 )
/ (1
/ 2))
* t)
+ (((1
/ 2)
* r1)
/ (1
/ 2))) by
TREAL_1:def 1
.= (((1
/ (1
/ 2))
* t)
+ (((1
/ 2)
*
0 )
/ (1
/ 2))) by
TREAL_1:def 1
.= (2
* t);
then
A52: (P1
. t) is
Point of
I[01] by
A48,
Th3;
not t
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
A11,
A48,
XXREAL_1: 1;
then not
[
0 , t]
in (
dom g1) by
A20,
ZFMISC_1: 87;
hence (h
. (
0 ,t))
= (f1
. (
0 ,t)) by
A44,
FUNCT_4: 11
.= (f
. (e1
. (
0 ,t))) by
A51,
FUNCT_1: 13
.= (f
. (((
id
I[01] )
.
0 ),(P1
. t))) by
A29,
A51,
FUNCT_3: 65
.= (f
. (
0 ,(P1
. t))) by
A22,
FUNCT_1: 18
.= a by
A10,
A52;
t
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
A46,
A48,
A49,
XXREAL_1: 1;
then
A53:
[1, t]
in (
dom e1) by
A27,
A15,
ZFMISC_1: 87;
(P1
. t)
= ((((r2
- r1)
/ ((1
/ 2)
-
0 ))
* t)
+ ((((1
/ 2)
* r1)
- (
0
* r2))
/ ((1
/ 2)
-
0 ))) by
A50,
TREAL_1: 11
.= ((((1
- r1)
/ (1
/ 2))
* t)
+ (((1
/ 2)
* r1)
/ (1
/ 2))) by
TREAL_1:def 2
.= ((((1
-
0 )
/ (1
/ 2))
* t)
+ (((1
/ 2)
* r1)
/ (1
/ 2))) by
TREAL_1:def 1
.= (((1
/ (1
/ 2))
* t)
+ (((1
/ 2)
*
0 )
/ (1
/ 2))) by
TREAL_1:def 1
.= (2
* t);
then
A54: (P1
. t) is
Point of
I[01] by
A48,
Th3;
not t
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
A12,
A48,
XXREAL_1: 1;
then not
[1, t]
in (
dom g1) by
A20,
ZFMISC_1: 87;
hence (h
. (1,t))
= (f1
. (1,t)) by
A44,
FUNCT_4: 11
.= (f
. (e1
. (1,t))) by
A53,
FUNCT_1: 13
.= (f
. (((
id
I[01] )
. 1),(P1
. t))) by
A29,
A53,
FUNCT_3: 65
.= (f
. (1,(P1
. t))) by
A21,
FUNCT_1: 18
.= b by
A10,
A54;
end;
suppose
A55: t
>= (1
/ 2);
reconsider r1 = (
(#) (
0 ,1)), r2 = ((
0 ,1)
(#) ) as
Real;
t
<= 1 by
BORSUK_1: 43;
then
A56: t
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
A11,
A55,
XXREAL_1: 1;
then
A57:
[1, t]
in (
dom e2) by
A30,
A15,
ZFMISC_1: 87;
(P2
. t)
= ((((r2
- r1)
/ (1
- (1
/ 2)))
* t)
+ (((1
* r1)
- ((1
/ 2)
* r2))
/ (1
- (1
/ 2)))) by
A56,
TREAL_1: 11
.= ((((1
- r1)
/ (1
/ 2))
* t)
+ (((1
* r1)
- ((1
/ 2)
* r2))
/ (1
/ 2))) by
TREAL_1:def 2
.= ((((1
-
0 )
/ (1
/ 2))
* t)
+ (((1
* r1)
- ((1
/ 2)
* r2))
/ (1
/ 2))) by
TREAL_1:def 1
.= ((2
* t)
+ (((1
*
0 )
- ((1
/ 2)
* r2))
/ (1
/ 2))) by
TREAL_1:def 1
.= ((2
* t)
+ ((
- ((1
/ 2)
* r2))
/ (1
/ 2)))
.= ((2
* t)
+ ((
- ((1
/ 2)
* 1))
/ (1
/ 2))) by
TREAL_1:def 2
.= ((2
* t)
- 1);
then
A58: (P2
. t) is
Point of
I[01] by
A55,
Th4;
(P2
. t)
= ((((r2
- r1)
/ (1
- (1
/ 2)))
* t)
+ (((1
* r1)
- ((1
/ 2)
* r2))
/ (1
- (1
/ 2)))) by
A56,
TREAL_1: 11
.= ((((1
- r1)
/ (1
/ 2))
* t)
+ (((1
* r1)
- ((1
/ 2)
* r2))
/ (1
/ 2))) by
TREAL_1:def 2
.= ((((1
-
0 )
/ (1
/ 2))
* t)
+ (((1
* r1)
- ((1
/ 2)
* r2))
/ (1
/ 2))) by
TREAL_1:def 1
.= (((1
/ (1
/ 2))
* t)
+ (((1
*
0 )
- ((1
/ 2)
* r2))
/ (1
/ 2))) by
TREAL_1:def 1
.= (((1
/ (1
/ 2))
* t)
+ (((1
*
0 )
- ((1
/ 2)
* 1))
/ (1
/ 2))) by
TREAL_1:def 2
.= ((2
* t)
- 1);
then
A59: (P2
. t) is
Point of
I[01] by
A55,
Th4;
A60:
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
A61:
[
0 , t]
in (
dom e2) by
A30,
A56,
ZFMISC_1: 87;
[
0 , t]
in (
dom g1) by
A20,
A60,
A56,
ZFMISC_1: 87;
hence (h
. (
0 ,t))
= (g1
. (
0 ,t)) by
A44,
FUNCT_4: 13
.= (g
. (e2
. (
0 ,t))) by
A61,
FUNCT_1: 13
.= (g
. (((
id
I[01] )
.
0 ),(P2
. t))) by
A28,
A61,
FUNCT_3: 65
.= (g
. (
0 ,(P2
. t))) by
A22,
FUNCT_1: 18
.= a by
A19,
A59;
[1, t]
in (
dom g1) by
A20,
A15,
A56,
ZFMISC_1: 87;
hence (h
. (1,t))
= (g1
. (1,t)) by
A44,
FUNCT_4: 13
.= (g
. (e2
. (1,t))) by
A57,
FUNCT_1: 13
.= (g
. (((
id
I[01] )
. 1),(P2
. t))) by
A28,
A57,
FUNCT_3: 65
.= (g
. (1,(P2
. t))) by
A21,
FUNCT_1: 18
.= b by
A19,
A58;
end;
end;
for s be
Point of
I[01] holds (h
. (s,
0 ))
= (P
. s) & (h
. (s,1))
= (R
. s)
proof
reconsider r1 = (
(#) (
0 ,1)), r2 = ((
0 ,1)
(#) ) as
Real;
let s be
Point of
I[01] ;
1
= ((
0 ,1)
(#) ) & 1
= (((1
/ 2),1)
(#) ) by
TREAL_1:def 2;
then
A62: (P2
. 1)
= 1 by
TREAL_1: 13;
A63: the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1))
=
[.(1
/ 2), 1.] by
TOPMETR: 18;
then
A64: 1
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
XXREAL_1: 1;
then
A65:
[s, 1]
in (
dom e2) by
A30,
ZFMISC_1: 87;
[s, 1]
in (
dom g1) by
A20,
A64,
ZFMISC_1: 87;
then
A66: (h
. (s,1))
= (g1
. (s,1)) by
A44,
FUNCT_4: 13
.= (g
. (e2
. (s,1))) by
A65,
FUNCT_1: 13
.= (g
. (((
id
I[01] )
. s),(P2
. 1))) by
A28,
A65,
FUNCT_3: 65
.= (g
. (s,1)) by
A62,
FUNCT_1: 18
.= (R
. s) by
A19;
A67:
0
in the
carrier of (
Closed-Interval-TSpace (
0 ,(1
/ 2))) by
A6,
XXREAL_1: 1;
then
A68: (P1
.
0 )
= ((((r2
- r1)
/ ((1
/ 2)
-
0 ))
*
0 )
+ ((((1
/ 2)
* r1)
- (
0
* r2))
/ ((1
/ 2)
-
0 ))) by
TREAL_1: 11
.= ((((1
/ 2)
*
0 )
- (
0
* r2))
/ ((1
/ 2)
-
0 )) by
TREAL_1:def 1;
A69:
[s,
0 ]
in (
dom e1) by
A27,
A67,
ZFMISC_1: 87;
not
0
in the
carrier of (
Closed-Interval-TSpace ((1
/ 2),1)) by
A63,
XXREAL_1: 1;
then not
[s,
0 ]
in (
dom g1) by
A20,
ZFMISC_1: 87;
then (h
. (s,
0 ))
= (f1
. (s,
0 )) by
A44,
FUNCT_4: 11
.= (f
. (e1
. (s,
0 ))) by
A69,
FUNCT_1: 13
.= (f
. (((
id
I[01] )
. s),(P1
.
0 ))) by
A29,
A69,
FUNCT_3: 65
.= (f
. (s,
0 )) by
A68,
FUNCT_1: 18
.= (P
. s) by
A10;
hence thesis by
A66;
end;
hence thesis by
A45,
A47;
end;
theorem ::
BORSUK_6:80
Th80: for P be
Path of a, b, Q be
constant
Path of b, b st (a,b)
are_connected holds ((P
+ Q),P)
are_homotopic
proof
let P be
Path of a, b, Q be
constant
Path of b, b such that
A1: (a,b)
are_connected ;
(
RePar (P,
1RP ))
= (P
+ Q) by
A1,
Th50;
hence thesis by
A1,
Th45,
Th47;
end;
theorem ::
BORSUK_6:81
for P be
Path of a1, b1, Q be
constant
Path of b1, b1 holds ((P
+ Q),P)
are_homotopic by
Th80,
BORSUK_2:def 3;
theorem ::
BORSUK_6:82
Th82: for P be
Path of a, b, Q be
constant
Path of a, a st (a,b)
are_connected holds ((Q
+ P),P)
are_homotopic
proof
let P be
Path of a, b, Q be
constant
Path of a, a such that
A1: (a,b)
are_connected ;
(
RePar (P,
2RP ))
= (Q
+ P) by
A1,
Th51;
hence thesis by
A1,
Th45,
Th48;
end;
theorem ::
BORSUK_6:83
for P be
Path of a1, b1, Q be
constant
Path of a1, a1 holds ((Q
+ P),P)
are_homotopic by
Th82,
BORSUK_2:def 3;
theorem ::
BORSUK_6:84
Th84: for P be
Path of a, b, Q be
constant
Path of a, a st (a,b)
are_connected holds ((P
+ (
- P)),Q)
are_homotopic
proof
set S =
[:
I[01] ,
I[01] :];
let P be
Path of a, b, Q be
constant
Path of a, a such that
A1: (a,b)
are_connected ;
reconsider e2 = (
pr2 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of S,
I[01] by
YELLOW12: 40;
set gg = ((
- P)
* e2);
(
- P) is
continuous by
A1,
BORSUK_2:def 2;
then
reconsider gg as
continuous
Function of S, T;
set S2 = (S
|
IBB );
reconsider g = (gg
|
IBB ) as
Function of S2, T by
PRE_TOPC: 9;
reconsider g as
continuous
Function of S2, T by
TOPMETR: 7;
A2: for x be
Point of S2 holds (g
. x)
= (P
. (1
- (x
`2 )))
proof
let x be
Point of S2;
x
in the
carrier of S2;
then
A3: x
in
IBB by
PRE_TOPC: 8;
then
A4: x
in the
carrier of S;
then
A5: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A6: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
then
A7: (x
`2 )
in the
carrier of
I[01] by
A5,
ZFMISC_1: 87;
(x
`1 )
in the
carrier of
I[01] by
A5,
A6,
ZFMISC_1: 87;
then
A8: (e2
. ((x
`1 ),(x
`2 )))
= (x
`2 ) by
A7,
FUNCT_3:def 5;
A9: x
in (
dom e2) by
A4,
FUNCT_2:def 1;
(g
. x)
= (gg
. x) by
A3,
FUNCT_1: 49
.= ((
- P)
. (e2
. x)) by
A9,
FUNCT_1: 13
.= (P
. (1
- (x
`2 ))) by
A1,
A6,
A7,
A8,
BORSUK_2:def 6;
hence thesis;
end;
set S3 = (S
|
ICC );
set S1 = (S
|
IAA );
reconsider e1 = (
pr1 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of S,
I[01] by
YELLOW12: 39;
A10: (a,a)
are_connected ;
then
reconsider PP = (P
+ (
- P)) as
continuous
Path of a, a by
BORSUK_2:def 2;
set ff = (PP
* e1);
reconsider f = (ff
|
IAA ) as
Function of S1, T by
PRE_TOPC: 9;
reconsider f as
continuous
Function of S1, T by
TOPMETR: 7;
set S12 = (S
| (
IAA
\/
IBB ));
reconsider S12 as non
empty
SubSpace of S;
A11: the
carrier of S12
= (
IAA
\/
IBB ) by
PRE_TOPC: 8;
set hh = (PP
* e1);
reconsider h = (hh
|
ICC ) as
Function of S3, T by
PRE_TOPC: 9;
reconsider h as
continuous
Function of S3, T by
TOPMETR: 7;
A12: for x be
Point of S3 holds (h
. x)
= ((
- P)
. ((2
* (x
`1 ))
- 1))
proof
let x be
Point of S3;
x
in the
carrier of S3;
then
A13: x
in
ICC by
PRE_TOPC: 8;
then
A14: (x
`1 )
>= (1
/ 2) by
Th60;
A15: x
in the
carrier of S by
A13;
then
A16: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A17: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
then
A18: (x
`1 )
in the
carrier of
I[01] by
A16,
ZFMISC_1: 87;
(x
`2 )
in the
carrier of
I[01] by
A16,
A17,
ZFMISC_1: 87;
then
A19: (e1
. ((x
`1 ),(x
`2 )))
= (x
`1 ) by
A18,
FUNCT_3:def 4;
A20: x
in (
dom e1) by
A15,
FUNCT_2:def 1;
(h
. x)
= (hh
. x) by
A13,
FUNCT_1: 49
.= ((P
+ (
- P))
. (e1
. x)) by
A20,
FUNCT_1: 13
.= ((
- P)
. ((2
* (x
`1 ))
- 1)) by
A1,
A17,
A18,
A19,
A14,
BORSUK_2:def 5;
hence thesis;
end;
A21: for x be
Point of S1 holds (f
. x)
= (P
. (2
* (x
`1 )))
proof
let x be
Point of S1;
x
in the
carrier of S1;
then
A22: x
in
IAA by
PRE_TOPC: 8;
then
A23: (x
`1 )
<= (1
/ 2) by
Th59;
A24: x
in the
carrier of S by
A22;
then
A25: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A26: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
then
A27: (x
`1 )
in the
carrier of
I[01] by
A25,
ZFMISC_1: 87;
(x
`2 )
in the
carrier of
I[01] by
A25,
A26,
ZFMISC_1: 87;
then
A28: (e1
. ((x
`1 ),(x
`2 )))
= (x
`1 ) by
A27,
FUNCT_3:def 4;
A29: x
in (
dom e1) by
A24,
FUNCT_2:def 1;
(f
. x)
= (ff
. x) by
A22,
FUNCT_1: 49
.= ((P
+ (
- P))
. (e1
. x)) by
A29,
FUNCT_1: 13
.= (P
. (2
* (x
`1 ))) by
A1,
A26,
A27,
A28,
A23,
BORSUK_2:def 5;
hence thesis;
end;
A30: for p be
object st p
in ((
[#] S1)
/\ (
[#] S2)) holds (f
. p)
= (g
. p)
proof
let p be
object;
assume p
in ((
[#] S1)
/\ (
[#] S2));
then
A31: p
in ((
[#] S1)
/\
IBB ) by
PRE_TOPC:def 5;
then
A32: p
in (
IAA
/\
IBB ) by
PRE_TOPC:def 5;
then
consider r be
Point of S such that
A33: r
= p and
A34: (r
`2 )
= (1
- (2
* (r
`1 ))) by
Th57;
A35: (2
* (r
`1 ))
= (1
- (r
`2 )) by
A34;
p
in
IAA by
A32,
XBOOLE_0:def 4;
then
reconsider pp = p as
Point of S1 by
PRE_TOPC: 8;
p
in
IBB by
A31,
XBOOLE_0:def 4;
then
A36: pp is
Point of S2 by
PRE_TOPC: 8;
(f
. p)
= (P
. (2
* (pp
`1 ))) by
A21
.= (g
. p) by
A2,
A33,
A35,
A36;
hence thesis;
end;
reconsider s3 = (
[#] S3) as
Subset of S by
PRE_TOPC:def 5;
A37: s3
=
ICC by
PRE_TOPC:def 5;
A38: S1 is
SubSpace of S12 & S2 is
SubSpace of S12 by
TOPMETR: 22,
XBOOLE_1: 7;
A39: (
[#] S2)
=
IBB by
PRE_TOPC:def 5;
A40: (
[#] S1)
=
IAA by
PRE_TOPC:def 5;
then
reconsider s1 = (
[#] S1), s2 = (
[#] S2) as
Subset of S12 by
A11,
A39,
XBOOLE_1: 7;
A41: s1 is
closed by
A40,
TOPS_2: 26;
A42: s2 is
closed by
A39,
TOPS_2: 26;
((
[#] S1)
\/ (
[#] S2))
= (
[#] S12) by
A11,
A39,
PRE_TOPC:def 5;
then
consider fg be
Function of S12, T such that
A43: fg
= (f
+* g) and
A44: fg is
continuous by
A30,
A38,
A41,
A42,
JGRAPH_2: 1;
A45: (
[#] S3)
=
ICC by
PRE_TOPC:def 5;
A46: for p be
object st p
in ((
[#] S12)
/\ (
[#] S3)) holds (fg
. p)
= (h
. p)
proof
let p be
object;
[(1
/ 2),
0 ]
in (
IBB
/\
ICC ) by
Th66,
Th67,
XBOOLE_0:def 4;
then
A47:
{
[(1
/ 2),
0 ]}
c= (
IBB
/\
ICC ) by
ZFMISC_1: 31;
assume p
in ((
[#] S12)
/\ (
[#] S3));
then p
in (
{
[(1
/ 2),
0 ]}
\/ (
IBB
/\
ICC )) by
A11,
A45,
Th72,
XBOOLE_1: 23;
then
A48: p
in (
IBB
/\
ICC ) by
A47,
XBOOLE_1: 12;
then p
in
ICC by
XBOOLE_0:def 4;
then
reconsider pp = p as
Point of S3 by
PRE_TOPC: 8;
A49: p
in
IBB by
A48,
XBOOLE_0:def 4;
then
A50: pp is
Point of S2 by
PRE_TOPC: 8;
A51: ex q be
Point of S st q
= p & (q
`2 )
= ((2
* (q
`1 ))
- 1) by
A48,
Th58;
then
A52: ((2
* (pp
`1 ))
- 1) is
Point of
I[01] by
Th27;
p
in the
carrier of S2 by
A49,
PRE_TOPC: 8;
then p
in (
dom g) by
FUNCT_2:def 1;
then (fg
. p)
= (g
. p) by
A43,
FUNCT_4: 13
.= (P
. (1
- (pp
`2 ))) by
A2,
A50
.= ((
- P)
. ((2
* (pp
`1 ))
- 1)) by
A1,
A51,
A52,
BORSUK_2:def 6
.= (h
. p) by
A12;
hence thesis;
end;
((
[#] S12)
\/ (
[#] S3))
= ((
IAA
\/
IBB )
\/
ICC ) by
A11,
PRE_TOPC:def 5
.= (
[#] S) by
Th56,
BORSUK_1: 40,
BORSUK_1:def 2;
then
consider H be
Function of S, T such that
A53: H
= (fg
+* h) and
A54: H is
continuous by
A11,
A44,
A46,
A37,
JGRAPH_2: 1;
A55: for s be
Point of
I[01] holds (H
. (s,
0 ))
= ((P
+ (
- P))
. s) & (H
. (s,1))
= (Q
. s)
proof
let s be
Point of
I[01] ;
thus (H
. (s,
0 ))
= ((P
+ (
- P))
. s)
proof
A56: (
[s,
0 ]
`1 )
= s;
per cases by
XXREAL_0: 1;
suppose
A57: s
< (1
/ 2);
then not
[s,
0 ]
in
IBB by
Th71;
then not
[s,
0 ]
in the
carrier of S2 by
PRE_TOPC: 8;
then
A58: not
[s,
0 ]
in (
dom g);
[s,
0 ]
in
IAA by
A57,
Th70;
then
A59:
[s,
0 ]
in the
carrier of S1 by
PRE_TOPC: 8;
not
[s,
0 ]
in
ICC by
A57,
Th71;
then not
[s,
0 ]
in the
carrier of S3 by
PRE_TOPC: 8;
then not
[s,
0 ]
in (
dom h);
then (H
.
[s,
0 ])
= (fg
.
[s,
0 ]) by
A53,
FUNCT_4: 11
.= (f
.
[s,
0 ]) by
A43,
A58,
FUNCT_4: 11
.= (P
. (2
* s)) by
A21,
A56,
A59
.= ((P
+ (
- P))
. s) by
A1,
A57,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A60: s
= (1
/ 2);
then
A61:
[s,
0 ]
in the
carrier of S3 by
Th66,
PRE_TOPC: 8;
then
[s,
0 ]
in (
dom h) by
FUNCT_2:def 1;
then (H
.
[s,
0 ])
= (h
.
[s,
0 ]) by
A53,
FUNCT_4: 13
.= ((
- P)
. ((2
* s)
- 1)) by
A12,
A56,
A61
.= b by
A1,
A60,
BORSUK_2:def 2
.= (P
. (2
* (1
/ 2))) by
A1,
BORSUK_2:def 2
.= ((P
+ (
- P))
. s) by
A1,
A60,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A62: s
> (1
/ 2);
then
[s,
0 ]
in
ICC by
Th69;
then
A63:
[s,
0 ]
in the
carrier of S3 by
PRE_TOPC: 8;
then
[s,
0 ]
in (
dom h) by
FUNCT_2:def 1;
then (H
.
[s,
0 ])
= (h
.
[s,
0 ]) by
A53,
FUNCT_4: 13
.= ((
- P)
. ((2
* s)
- 1)) by
A12,
A56,
A63
.= ((P
+ (
- P))
. s) by
A1,
A62,
BORSUK_2:def 5;
hence thesis;
end;
end;
thus (H
. (s,1))
= (Q
. s)
proof
A64: (
[s, 1]
`2 )
= 1;
A65: (
[s, 1]
`1 )
= s;
A66: (
dom Q)
= the
carrier of
I[01] by
FUNCT_2:def 1;
then
A67:
0
in (
dom Q) by
BORSUK_1: 43;
per cases ;
suppose
A68: s
<> 1;
[s, 1]
in
IBB by
Th65;
then
A69:
[s, 1]
in the
carrier of S2 by
PRE_TOPC: 8;
then
A70:
[s, 1]
in (
dom g) by
FUNCT_2:def 1;
not
[s, 1]
in
ICC by
A68,
Th63;
then not
[s, 1]
in the
carrier of S3 by
PRE_TOPC: 8;
then not
[s, 1]
in (
dom h);
then (H
.
[s, 1])
= (fg
.
[s, 1]) by
A53,
FUNCT_4: 11
.= (g
.
[s, 1]) by
A43,
A70,
FUNCT_4: 13
.= (P
. (1
- 1)) by
A2,
A64,
A69
.= a by
A1,
BORSUK_2:def 2
.= (Q
.
0 ) by
A10,
BORSUK_2:def 2
.= (Q
. s) by
A66,
A67,
FUNCT_1:def 10;
hence thesis;
end;
suppose
A71: s
= 1;
then
A72:
[s, 1]
in the
carrier of S3 by
Th66,
PRE_TOPC: 8;
then
[s, 1]
in (
dom h) by
FUNCT_2:def 1;
then (H
.
[s, 1])
= (h
.
[s, 1]) by
A53,
FUNCT_4: 13
.= ((
- P)
. ((2
* s)
- 1)) by
A12,
A65,
A72
.= a by
A1,
A71,
BORSUK_2:def 2
.= (Q
.
0 ) by
A10,
BORSUK_2:def 2
.= (Q
. s) by
A66,
A67,
FUNCT_1:def 10;
hence thesis;
end;
end;
end;
for t be
Point of
I[01] holds (H
. (
0 ,t))
= a & (H
. (1,t))
= a
proof
let t be
Point of
I[01] ;
thus (H
. (
0 ,t))
= a
proof
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
reconsider x =
[
0 , t] as
Point of S by
Lm1;
x
in
IAA by
Th61;
then
A73: x is
Point of S1 by
PRE_TOPC: 8;
(x
`1 )
=
0 ;
then not x
in
ICC by
Th60;
then not x
in the
carrier of S3 by
PRE_TOPC: 8;
then
A74: not
[
0 , t]
in (
dom h);
per cases ;
suppose t
<> 1;
then not x
in
IBB by
Th62;
then not x
in the
carrier of S2 by
PRE_TOPC: 8;
then not x
in (
dom g);
then (fg
.
[
0 , t])
= (f
.
[
0 , t]) by
A43,
FUNCT_4: 11
.= (P
. (2
* (x
`1 ))) by
A21,
A73
.= a by
A1,
BORSUK_2:def 2;
hence thesis by
A53,
A74,
FUNCT_4: 11;
end;
suppose
A75: t
= 1;
then
A76: x
in the
carrier of S2 by
Th64,
PRE_TOPC: 8;
then x
in (
dom g) by
FUNCT_2:def 1;
then (fg
.
[
0 , t])
= (g
.
[
0 , 1]) by
A43,
A75,
FUNCT_4: 13
.= (P
. (1
- (x
`2 ))) by
A2,
A75,
A76
.= a by
A1,
A75,
BORSUK_2:def 2;
hence thesis by
A53,
A74,
FUNCT_4: 11;
end;
end;
thus (H
. (1,t))
= a
proof
1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
reconsider x =
[1, t] as
Point of S by
Lm1;
x
in
ICC by
Th68;
then
A77: x
in the
carrier of S3 by
PRE_TOPC: 8;
then
A78:
[1, t]
in (
dom h) by
FUNCT_2:def 1;
(h
.
[1, t])
= ((
- P)
. ((2
* (x
`1 ))
- 1)) by
A12,
A77
.= a by
A1,
BORSUK_2:def 2;
hence thesis by
A53,
A78,
FUNCT_4: 13;
end;
end;
hence thesis by
A54,
A55;
end;
theorem ::
BORSUK_6:85
for P be
Path of a1, b1, Q be
constant
Path of a1, a1 holds ((P
+ (
- P)),Q)
are_homotopic by
Th84,
BORSUK_2:def 3;
theorem ::
BORSUK_6:86
Th86: for P be
Path of b, a, Q be
constant
Path of a, a st (b,a)
are_connected holds (((
- P)
+ P),Q)
are_homotopic
proof
set S =
[:
I[01] ,
I[01] :];
let P be
Path of b, a, Q be
constant
Path of a, a such that
A1: (b,a)
are_connected ;
reconsider e2 = (
pr2 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of S,
I[01] by
YELLOW12: 40;
set gg = (P
* e2);
P is
continuous by
A1,
BORSUK_2:def 2;
then
reconsider gg as
continuous
Function of S, T;
set S2 = (S
|
IBB );
reconsider g = (gg
|
IBB ) as
Function of S2, T by
PRE_TOPC: 9;
reconsider g as
continuous
Function of S2, T by
TOPMETR: 7;
A2: for x be
Point of S2 holds (g
. x)
= ((
- P)
. (1
- (x
`2 )))
proof
let x be
Point of S2;
x
in the
carrier of S2;
then
A3: x
in
IBB by
PRE_TOPC: 8;
then
A4: x
in the
carrier of S;
then
A5: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A6: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
then
A7: (x
`2 )
in the
carrier of
I[01] by
A5,
ZFMISC_1: 87;
then
A8: (1
- (x
`2 ))
in the
carrier of
I[01] by
JORDAN5B: 4;
(x
`1 )
in the
carrier of
I[01] by
A5,
A6,
ZFMISC_1: 87;
then
A9: (e2
. ((x
`1 ),(x
`2 )))
= (x
`2 ) by
A7,
FUNCT_3:def 5;
A10: x
in (
dom e2) by
A4,
FUNCT_2:def 1;
(g
. x)
= (gg
. ((x
`1 ),(x
`2 ))) by
A3,
A6,
FUNCT_1: 49
.= (P
. (1
- (1
- (x
`2 )))) by
A6,
A9,
A10,
FUNCT_1: 13
.= ((
- P)
. (1
- (x
`2 ))) by
A1,
A8,
BORSUK_2:def 6;
hence thesis;
end;
set S3 = (S
|
ICC );
set S1 = (S
|
IAA );
reconsider e1 = (
pr1 (the
carrier of
I[01] ,the
carrier of
I[01] )) as
continuous
Function of S,
I[01] by
YELLOW12: 39;
A11: (a,a)
are_connected ;
then
reconsider PP = ((
- P)
+ P) as
continuous
Path of a, a by
BORSUK_2:def 2;
set ff = (PP
* e1);
reconsider f = (ff
|
IAA ) as
Function of S1, T by
PRE_TOPC: 9;
reconsider f as
continuous
Function of S1, T by
TOPMETR: 7;
set S12 = (S
| (
IAA
\/
IBB ));
reconsider S12 as non
empty
SubSpace of S;
A12: the
carrier of S12
= (
IAA
\/
IBB ) by
PRE_TOPC: 8;
set hh = (PP
* e1);
reconsider h = (hh
|
ICC ) as
Function of S3, T by
PRE_TOPC: 9;
reconsider h as
continuous
Function of S3, T by
TOPMETR: 7;
A13: for x be
Point of S3 holds (h
. x)
= (P
. ((2
* (x
`1 ))
- 1))
proof
let x be
Point of S3;
x
in the
carrier of S3;
then
A14: x
in
ICC by
PRE_TOPC: 8;
then
A15: (x
`1 )
>= (1
/ 2) by
Th60;
A16: x
in the
carrier of S by
A14;
then
A17: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A18: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
then
A19: (x
`1 )
in the
carrier of
I[01] by
A17,
ZFMISC_1: 87;
(x
`2 )
in the
carrier of
I[01] by
A17,
A18,
ZFMISC_1: 87;
then
A20: (e1
. ((x
`1 ),(x
`2 )))
= (x
`1 ) by
A19,
FUNCT_3:def 4;
A21: x
in (
dom e1) by
A16,
FUNCT_2:def 1;
(h
. x)
= (hh
. x) by
A14,
FUNCT_1: 49
.= (((
- P)
+ P)
. (e1
. ((x
`1 ),(x
`2 )))) by
A18,
A21,
FUNCT_1: 13
.= (P
. ((2
* (x
`1 ))
- 1)) by
A1,
A19,
A20,
A15,
BORSUK_2:def 5;
hence thesis;
end;
A22: for x be
Point of S1 holds (f
. x)
= ((
- P)
. (2
* (x
`1 )))
proof
let x be
Point of S1;
x
in the
carrier of S1;
then
A23: x
in
IAA by
PRE_TOPC: 8;
then
A24: (x
`1 )
<= (1
/ 2) by
Th59;
A25: x
in the
carrier of S by
A23;
then
A26: x
in
[:the
carrier of
I[01] , the
carrier of
I[01] :] by
BORSUK_1:def 2;
then
A27: x
=
[(x
`1 ), (x
`2 )] by
MCART_1: 21;
then
A28: (x
`1 )
in the
carrier of
I[01] by
A26,
ZFMISC_1: 87;
(x
`2 )
in the
carrier of
I[01] by
A26,
A27,
ZFMISC_1: 87;
then
A29: (e1
. ((x
`1 ),(x
`2 )))
= (x
`1 ) by
A28,
FUNCT_3:def 4;
A30: x
in (
dom e1) by
A25,
FUNCT_2:def 1;
(f
. x)
= (ff
. x) by
A23,
FUNCT_1: 49
.= (((
- P)
+ P)
. (e1
. x)) by
A30,
FUNCT_1: 13
.= ((
- P)
. (2
* (x
`1 ))) by
A1,
A27,
A28,
A29,
A24,
BORSUK_2:def 5;
hence thesis;
end;
A31: for p be
object st p
in ((
[#] S1)
/\ (
[#] S2)) holds (f
. p)
= (g
. p)
proof
let p be
object;
assume p
in ((
[#] S1)
/\ (
[#] S2));
then
A32: p
in ((
[#] S1)
/\
IBB ) by
PRE_TOPC:def 5;
then
A33: p
in (
IAA
/\
IBB ) by
PRE_TOPC:def 5;
then
consider r be
Point of S such that
A34: r
= p and
A35: (r
`2 )
= (1
- (2
* (r
`1 ))) by
Th57;
A36: (2
* (r
`1 ))
= (1
- (r
`2 )) by
A35;
p
in
IAA by
A33,
XBOOLE_0:def 4;
then
reconsider pp = p as
Point of S1 by
PRE_TOPC: 8;
p
in
IBB by
A32,
XBOOLE_0:def 4;
then
A37: pp is
Point of S2 by
PRE_TOPC: 8;
(f
. p)
= ((
- P)
. (2
* (pp
`1 ))) by
A22
.= (g
. p) by
A2,
A34,
A36,
A37;
hence thesis;
end;
reconsider s3 = (
[#] S3) as
Subset of S by
PRE_TOPC:def 5;
A38: s3
=
ICC by
PRE_TOPC:def 5;
A39: S1 is
SubSpace of S12 & S2 is
SubSpace of S12 by
TOPMETR: 22,
XBOOLE_1: 7;
A40: (
[#] S2)
=
IBB by
PRE_TOPC:def 5;
A41: (
[#] S1)
=
IAA by
PRE_TOPC:def 5;
then
reconsider s1 = (
[#] S1), s2 = (
[#] S2) as
Subset of S12 by
A12,
A40,
XBOOLE_1: 7;
A42: s1 is
closed by
A41,
TOPS_2: 26;
A43: s2 is
closed by
A40,
TOPS_2: 26;
((
[#] S1)
\/ (
[#] S2))
= (
[#] S12) by
A12,
A40,
PRE_TOPC:def 5;
then
consider fg be
Function of S12, T such that
A44: fg
= (f
+* g) and
A45: fg is
continuous by
A31,
A39,
A42,
A43,
JGRAPH_2: 1;
A46: (
[#] S3)
=
ICC by
PRE_TOPC:def 5;
A47: for p be
object st p
in ((
[#] S12)
/\ (
[#] S3)) holds (fg
. p)
= (h
. p)
proof
let p be
object;
[(1
/ 2),
0 ]
in (
IBB
/\
ICC ) by
Th66,
Th67,
XBOOLE_0:def 4;
then
A48:
{
[(1
/ 2),
0 ]}
c= (
IBB
/\
ICC ) by
ZFMISC_1: 31;
assume p
in ((
[#] S12)
/\ (
[#] S3));
then p
in (
{
[(1
/ 2),
0 ]}
\/ (
IBB
/\
ICC )) by
A12,
A46,
Th72,
XBOOLE_1: 23;
then
A49: p
in (
IBB
/\
ICC ) by
A48,
XBOOLE_1: 12;
then p
in
ICC by
XBOOLE_0:def 4;
then
reconsider pp = p as
Point of S3 by
PRE_TOPC: 8;
A50: ex q be
Point of S st q
= p & (q
`2 )
= ((2
* (q
`1 ))
- 1) by
A49,
Th58;
(pp
`2 ) is
Point of
I[01] by
A49,
Th27;
then
A51: (1
- (pp
`2 ))
in the
carrier of
I[01] by
JORDAN5B: 4;
A52: p
in
IBB by
A49,
XBOOLE_0:def 4;
then
A53: pp is
Point of S2 by
PRE_TOPC: 8;
p
in the
carrier of S2 by
A52,
PRE_TOPC: 8;
then p
in (
dom g) by
FUNCT_2:def 1;
then (fg
. p)
= (g
. p) by
A44,
FUNCT_4: 13
.= ((
- P)
. (1
- (pp
`2 ))) by
A2,
A53
.= (P
. (1
- (1
- (pp
`2 )))) by
A1,
A51,
BORSUK_2:def 6
.= (h
. p) by
A13,
A50;
hence thesis;
end;
((
[#] S12)
\/ (
[#] S3))
= (
[#] S) by
A12,
A46,
Th56,
BORSUK_1: 40,
BORSUK_1:def 2;
then
consider H be
Function of S, T such that
A54: H
= (fg
+* h) and
A55: H is
continuous by
A12,
A45,
A47,
A38,
JGRAPH_2: 1;
A56: for s be
Point of
I[01] holds (H
. (s,
0 ))
= (((
- P)
+ P)
. s) & (H
. (s,1))
= (Q
. s)
proof
let s be
Point of
I[01] ;
thus (H
. (s,
0 ))
= (((
- P)
+ P)
. s)
proof
A57: (
[s,
0 ]
`1 )
= s;
per cases by
XXREAL_0: 1;
suppose
A58: s
< (1
/ 2);
then not
[s,
0 ]
in
IBB by
Th71;
then not
[s,
0 ]
in the
carrier of S2 by
PRE_TOPC: 8;
then
A59: not
[s,
0 ]
in (
dom g);
[s,
0 ]
in
IAA by
A58,
Th70;
then
A60:
[s,
0 ]
in the
carrier of S1 by
PRE_TOPC: 8;
not
[s,
0 ]
in
ICC by
A58,
Th71;
then not
[s,
0 ]
in the
carrier of S3 by
PRE_TOPC: 8;
then not
[s,
0 ]
in (
dom h);
then (H
.
[s,
0 ])
= (fg
.
[s,
0 ]) by
A54,
FUNCT_4: 11
.= (f
.
[s,
0 ]) by
A44,
A59,
FUNCT_4: 11
.= ((
- P)
. (2
* s)) by
A22,
A57,
A60
.= (((
- P)
+ P)
. s) by
A1,
A58,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A61: s
= (1
/ 2);
then
A62:
[s,
0 ]
in the
carrier of S3 by
Th66,
PRE_TOPC: 8;
then
[s,
0 ]
in (
dom h) by
FUNCT_2:def 1;
then (H
.
[s,
0 ])
= (h
.
[s,
0 ]) by
A54,
FUNCT_4: 13
.= (P
. ((2
* s)
- 1)) by
A13,
A57,
A62
.= b by
A1,
A61,
BORSUK_2:def 2
.= ((
- P)
. (2
* (1
/ 2))) by
A1,
BORSUK_2:def 2
.= (((
- P)
+ P)
. s) by
A1,
A61,
BORSUK_2:def 5;
hence thesis;
end;
suppose
A63: s
> (1
/ 2);
then
[s,
0 ]
in
ICC by
Th69;
then
A64:
[s,
0 ]
in the
carrier of S3 by
PRE_TOPC: 8;
then
[s,
0 ]
in (
dom h) by
FUNCT_2:def 1;
then (H
.
[s,
0 ])
= (h
.
[s,
0 ]) by
A54,
FUNCT_4: 13
.= (P
. ((2
* s)
- 1)) by
A13,
A57,
A64
.= (((
- P)
+ P)
. s) by
A1,
A63,
BORSUK_2:def 5;
hence thesis;
end;
end;
thus (H
. (s,1))
= (Q
. s)
proof
A65: (
[s, 1]
`2 )
= 1;
A66: (
[s, 1]
`1 )
= s;
A67: (
dom Q)
= the
carrier of
I[01] by
FUNCT_2:def 1;
then
A68:
0
in (
dom Q) by
BORSUK_1: 43;
per cases ;
suppose
A69: s
<> 1;
[s, 1]
in
IBB by
Th65;
then
A70:
[s, 1]
in the
carrier of S2 by
PRE_TOPC: 8;
then
A71:
[s, 1]
in (
dom g) by
FUNCT_2:def 1;
not
[s, 1]
in
ICC by
A69,
Th63;
then not
[s, 1]
in the
carrier of S3 by
PRE_TOPC: 8;
then not
[s, 1]
in (
dom h);
then (H
.
[s, 1])
= (fg
.
[s, 1]) by
A54,
FUNCT_4: 11
.= (g
.
[s, 1]) by
A44,
A71,
FUNCT_4: 13
.= ((
- P)
. (1
- 1)) by
A2,
A65,
A70
.= a by
A1,
BORSUK_2:def 2
.= (Q
.
0 ) by
A11,
BORSUK_2:def 2
.= (Q
. s) by
A67,
A68,
FUNCT_1:def 10;
hence thesis;
end;
suppose
A72: s
= 1;
then
A73:
[s, 1]
in the
carrier of S3 by
Th66,
PRE_TOPC: 8;
then
[s, 1]
in (
dom h) by
FUNCT_2:def 1;
then (H
.
[s, 1])
= (h
.
[s, 1]) by
A54,
FUNCT_4: 13
.= (P
. ((2
* s)
- 1)) by
A13,
A66,
A73
.= a by
A1,
A72,
BORSUK_2:def 2
.= (Q
.
0 ) by
A11,
BORSUK_2:def 2
.= (Q
. s) by
A67,
A68,
FUNCT_1:def 10;
hence thesis;
end;
end;
end;
for t be
Point of
I[01] holds (H
. (
0 ,t))
= a & (H
. (1,t))
= a
proof
let t be
Point of
I[01] ;
thus (H
. (
0 ,t))
= a
proof
0
in the
carrier of
I[01] by
BORSUK_1: 43;
then
reconsider x =
[
0 , t] as
Point of S by
Lm1;
x
in
IAA by
Th61;
then
A74: x is
Point of S1 by
PRE_TOPC: 8;
(x
`1 )
=
0 ;
then not x
in
ICC by
Th60;
then not x
in the
carrier of S3 by
PRE_TOPC: 8;
then
A75: not
[
0 , t]
in (
dom h);
per cases ;
suppose t
<> 1;
then not x
in
IBB by
Th62;
then not x
in the
carrier of S2 by
PRE_TOPC: 8;
then not x
in (
dom g);
then (fg
.
[
0 , t])
= (f
.
[
0 , t]) by
A44,
FUNCT_4: 11
.= ((
- P)
. (2
* (x
`1 ))) by
A22,
A74
.= a by
A1,
BORSUK_2:def 2;
hence thesis by
A54,
A75,
FUNCT_4: 11;
end;
suppose
A76: t
= 1;
then
A77: x
in the
carrier of S2 by
Th64,
PRE_TOPC: 8;
then x
in (
dom g) by
FUNCT_2:def 1;
then (fg
.
[
0 , t])
= (g
.
[
0 , 1]) by
A44,
A76,
FUNCT_4: 13
.= ((
- P)
. (1
- (x
`2 ))) by
A2,
A76,
A77
.= a by
A1,
A76,
BORSUK_2:def 2;
hence thesis by
A54,
A75,
FUNCT_4: 11;
end;
end;
thus (H
. (1,t))
= a
proof
1
in the
carrier of
I[01] by
BORSUK_1: 43;
then
reconsider x =
[1, t] as
Point of S by
Lm1;
x
in
ICC by
Th68;
then
A78: x
in the
carrier of S3 by
PRE_TOPC: 8;
then
A79:
[1, t]
in (
dom h) by
FUNCT_2:def 1;
(h
.
[1, t])
= (P
. ((2
* (x
`1 ))
- 1)) by
A13,
A78
.= a by
A1,
BORSUK_2:def 2;
hence thesis by
A54,
A79,
FUNCT_4: 13;
end;
end;
hence thesis by
A55,
A56;
end;
theorem ::
BORSUK_6:87
for P be
Path of b1, a1, Q be
constant
Path of a1, a1 holds (((
- P)
+ P),Q)
are_homotopic by
Th86,
BORSUK_2:def 3;
theorem ::
BORSUK_6:88
for P,Q be
constant
Path of a, a holds (P,Q)
are_homotopic
proof
let P,Q be
constant
Path of a, a;
P
= (
I[01]
--> a) & Q
= (
I[01]
--> a) by
BORSUK_2: 5;
hence thesis by
BORSUK_2: 12;
end;
definition
let T be non
empty
TopSpace;
let a,b be
Point of T;
let P,Q be
Path of a, b;
assume
A1: (P,Q)
are_homotopic ;
::
BORSUK_6:def11
mode
Homotopy of P,Q ->
Function of
[:
I[01] ,
I[01] :], T means it is
continuous & for t be
Point of
I[01] holds (it
. (t,
0 ))
= (P
. t) & (it
. (t,1))
= (Q
. t) & (it
. (
0 ,t))
= a & (it
. (1,t))
= b;
existence by
A1;
end