:: BORSUK_5 semantic presentation
theorem :: BORSUK_5:1
canceled;
theorem E1: :: BORSUK_5:2
for b
1, b
2, b
3 being
set holds
not ( b
1 c= b
2 & b
2 c= b
1 \/ {b3} & not b
1 \/ {b3} = b
2 & not b
1 = b
2 )
theorem :: BORSUK_5:3
for b
1, b
2, b
3, b
4, b
5, b
6 being
set holds
{b1,b2,b3,b4,b5,b6} = {b1,b3,b6} \/ {b2,b4,b5}
proof
let c
1, c
2, c
3, c
4, c
5, c
6 be
set ;
thus
{c1,c2,c3,c4,c5,c6} c= {c1,c3,c6} \/ {c2,c4,c5}
:: uses XBOOLE_0:def 10
proof
let c
7 be
set ;
:: uses TARSKI:def 3
assume
c
7 in {c1,c2,c3,c4,c5,c6}
;
then
not ( not c
7 = c
1 & not c
7 = c
2 & not c
7 = c
3 & not c
7 = c
4 & not c
7 = c
5 & not c
7 = c
6 )
by ENUMSET1:def 4;
then
( c
7 in {c1,c3,c6} or c
7 in {c2,c4,c5} )
by ENUMSET1:def 1;
hence
c
7 in {c1,c3,c6} \/ {c2,c4,c5}
by XBOOLE_0:def 2;
end;
let c
7 be
set ;
:: uses TARSKI:def 3
assume
c
7 in {c1,c3,c6} \/ {c2,c4,c5}
;
then
( c
7 in {c1,c3,c6} or c
7 in {c2,c4,c5} )
by XBOOLE_0:def 2;
then
not ( not c
7 = c
1 & not c
7 = c
3 & not c
7 = c
6 & not c
7 = c
2 & not c
7 = c
4 & not c
7 = c
5 )
by ENUMSET1:def 1;
hence
c
7 in {c1,c2,c3,c4,c5,c6}
by ENUMSET1:def 4;
end;
definition
let c
1, c
2, c
3, c
4, c
5, c
6 be
set ;
pred a
1,a
2,a
3,a
4,a
5,a
6 are_mutually_different means :
E2:
:: BORSUK_5:def 1
( a
1 <> a
2 & a
1 <> a
3 & a
1 <> a
4 & a
1 <> a
5 & a
1 <> a
6 & a
2 <> a
3 & a
2 <> a
4 & a
2 <> a
5 & a
2 <> a
6 & a
3 <> a
4 & a
3 <> a
5 & a
3 <> a
6 & a
4 <> a
5 & a
4 <> a
6 & a
5 <> a
6 );
end;
:: deftheorem E2 defines are_mutually_different BORSUK_5:def 1 :
for b
1, b
2, b
3, b
4, b
5, b
6 being
set holds
( b
1,b
2,b
3,b
4,b
5,b
6 are_mutually_different iff ( b
1 <> b
2 & b
1 <> b
3 & b
1 <> b
4 & b
1 <> b
5 & b
1 <> b
6 & b
2 <> b
3 & b
2 <> b
4 & b
2 <> b
5 & b
2 <> b
6 & b
3 <> b
4 & b
3 <> b
5 & b
3 <> b
6 & b
4 <> b
5 & b
4 <> b
6 & b
5 <> b
6 ) );
definition
let c
1, c
2, c
3, c
4, c
5, c
6, c
7 be
set ;
pred a
1,a
2,a
3,a
4,a
5,a
6,a
7 are_mutually_different means :
E3:
:: BORSUK_5:def 2
( a
1 <> a
2 & a
1 <> a
3 & a
1 <> a
4 & a
1 <> a
5 & a
1 <> a
6 & a
1 <> a
7 & a
2 <> a
3 & a
2 <> a
4 & a
2 <> a
5 & a
2 <> a
6 & a
2 <> a
7 & a
3 <> a
4 & a
3 <> a
5 & a
3 <> a
6 & a
3 <> a
7 & a
4 <> a
5 & a
4 <> a
6 & a
4 <> a
7 & a
5 <> a
6 & a
5 <> a
7 & a
6 <> a
7 );
end;
:: deftheorem E3 defines are_mutually_different BORSUK_5:def 2 :
for b
1, b
2, b
3, b
4, b
5, b
6, b
7 being
set holds
( b
1,b
2,b
3,b
4,b
5,b
6,b
7 are_mutually_different iff ( b
1 <> b
2 & b
1 <> b
3 & b
1 <> b
4 & b
1 <> b
5 & b
1 <> b
6 & b
1 <> b
7 & b
2 <> b
3 & b
2 <> b
4 & b
2 <> b
5 & b
2 <> b
6 & b
2 <> b
7 & b
3 <> b
4 & b
3 <> b
5 & b
3 <> b
6 & b
3 <> b
7 & b
4 <> b
5 & b
4 <> b
6 & b
4 <> b
7 & b
5 <> b
6 & b
5 <> b
7 & b
6 <> b
7 ) );
theorem E4: :: BORSUK_5:4
for b
1, b
2, b
3, b
4, b
5, b
6 being
set holds
( b
1,b
2,b
3,b
4,b
5,b
6 are_mutually_different implies
card {b1,b2,b3,b4,b5,b6} = 6 )
proof
let c
1, c
2, c
3, c
4, c
5, c
6 be
set ;
assume
c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
;
then E5:
( c
1 <> c
2 & c
1 <> c
3 & c
1 <> c
4 & c
1 <> c
5 & c
1 <> c
6 & c
2 <> c
3 & c
2 <> c
4 & c
2 <> c
5 & c
2 <> c
6 & c
3 <> c
4 & c
3 <> c
5 & c
3 <> c
6 & c
4 <> c
5 & c
4 <> c
6 & c
5 <> c
6 )
by E2;
then
c
1,c
2,c
3,c
4,c
5 are_mutually_different
by NECKLACE:def 1;
then E6:
card {c1,c2,c3,c4,c5} = 5
by NECKLACE:1;
( not c
6 in {c1,c2,c3,c4,c5} &
{c1,c2,c3,c4,c5} is
finite &
{c1,c2,c3,c4,c5,c6} = {c1,c2,c3,c4,c5} \/ {c6} )
by E5, ENUMSET1:def 3, ENUMSET1:55;
hence card {c1,c2,c3,c4,c5,c6} =
5
+ 1
by E6, CARD_2:54
.=
6
;
end;
theorem :: BORSUK_5:5
for b
1, b
2, b
3, b
4, b
5, b
6, b
7 being
set holds
( b
1,b
2,b
3,b
4,b
5,b
6,b
7 are_mutually_different implies
card {b1,b2,b3,b4,b5,b6,b7} = 7 )
proof
let c
1, c
2, c
3, c
4, c
5, c
6, c
7 be
set ;
assume
c
1,c
2,c
3,c
4,c
5,c
6,c
7 are_mutually_different
;
then E5:
( c
1 <> c
2 & c
1 <> c
3 & c
1 <> c
4 & c
1 <> c
5 & c
1 <> c
6 & c
1 <> c
7 & c
2 <> c
3 & c
2 <> c
4 & c
2 <> c
5 & c
2 <> c
6 & c
2 <> c
7 & c
3 <> c
4 & c
3 <> c
5 & c
3 <> c
6 & c
3 <> c
7 & c
4 <> c
5 & c
4 <> c
6 & c
4 <> c
7 & c
5 <> c
6 & c
5 <> c
7 & c
6 <> c
7 )
by E3;
then
c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
by E2;
then E6:
card {c1,c2,c3,c4,c5,c6} = 6
by E4;
( not c
7 in {c1,c2,c3,c4,c5,c6} &
{c1,c2,c3,c4,c5,c6} is
finite &
{c1,c2,c3,c4,c5,c6,c7} = {c1,c2,c3,c4,c5,c6} \/ {c7} )
by E5, ENUMSET1:def 4, ENUMSET1:61;
hence card {c1,c2,c3,c4,c5,c6,c7} =
6
+ 1
by E6, CARD_2:54
.=
7
;
end;
theorem E5: :: BORSUK_5:6
for b
1, b
2, b
3, b
4, b
5, b
6 being
set holds
(
{b1,b2,b3} misses {b4,b5,b6} implies ( b
1 <> b
4 & b
1 <> b
5 & b
1 <> b
6 & b
2 <> b
4 & b
2 <> b
5 & b
2 <> b
6 & b
3 <> b
4 & b
3 <> b
5 & b
3 <> b
6 ) )
proof
let c
1, c
2, c
3, c
4, c
5, c
6 be
set ;
assume E6:
{c1,c2,c3} misses {c4,c5,c6}
;
assume
not ( not c
1 = c
4 & not c
1 = c
5 & not c
1 = c
6 & not c
2 = c
4 & not c
2 = c
5 & not c
2 = c
6 & not c
3 = c
4 & not c
3 = c
5 & not c
3 = c
6 )
;
then E7:
not ( not c
4 in {c1,c2,c3} & not c
5 in {c1,c2,c3} & not c
6 in {c1,c2,c3} )
by ENUMSET1:def 1;
( c
4 in {c4,c5,c6} & c
5 in {c4,c5,c6} & c
6 in {c4,c5,c6} )
by ENUMSET1:def 1;
hence
not verum
by E6, E7, XBOOLE_0:3;
end;
theorem :: BORSUK_5:7
for b
1, b
2, b
3, b
4, b
5, b
6 being
set holds
( ( b
1,b
2,b
3 are_mutually_different & b
4,b
5,b
6 are_mutually_different &
{b1,b2,b3} misses {b4,b5,b6} ) implies ( b
1,b
2,b
3,b
4,b
5,b
6 are_mutually_different ) )
proof
let c
1, c
2, c
3, c
4, c
5, c
6 be
set ;
assume that
E6:
c
1,c
2,c
3 are_mutually_different
and
E7:
c
4,c
5,c
6 are_mutually_different
and
E8:
{c1,c2,c3} misses {c4,c5,c6}
;
E9:
( c
1 <> c
2 & c
2 <> c
3 & c
1 <> c
3 )
by E6, INCPROJ:def 5;
E10:
( c
4 <> c
5 & c
5 <> c
6 & c
4 <> c
6 )
by E7, INCPROJ:def 5;
( c
1 <> c
4 & c
1 <> c
5 & c
1 <> c
6 & c
2 <> c
4 & c
2 <> c
5 & c
2 <> c
6 & c
3 <> c
4 & c
3 <> c
5 & c
3 <> c
6 )
by E8, E5;
hence
c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
by E9, E10, E2;
end;
theorem :: BORSUK_5:8
for b
1, b
2, b
3, b
4, b
5, b
6, b
7 being
set holds
( ( b
1,b
2,b
3,b
4,b
5,b
6 are_mutually_different &
{b1,b2,b3,b4,b5,b6} misses {b7} ) implies ( b
1,b
2,b
3,b
4,b
5,b
6,b
7 are_mutually_different ) )
proof
let c
1, c
2, c
3, c
4, c
5, c
6, c
7 be
set ;
assume that
E6:
c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
and
E7:
{c1,c2,c3,c4,c5,c6} misses {c7}
;
E8:
( c
1 <> c
2 & c
1 <> c
3 & c
1 <> c
4 & c
1 <> c
5 & c
1 <> c
6 & c
2 <> c
3 & c
2 <> c
4 & c
2 <> c
5 & c
2 <> c
6 & c
3 <> c
4 & c
3 <> c
5 & c
3 <> c
6 & c
4 <> c
5 & c
4 <> c
6 & c
5 <> c
6 )
by E6, E2;
not c
7 in {c1,c2,c3,c4,c5,c6}
by E7, ZFMISC_1:54;
then
( c
7 <> c
1 & c
7 <> c
2 & c
7 <> c
3 & c
7 <> c
4 & c
7 <> c
5 & c
7 <> c
6 )
by ENUMSET1:def 4;
hence
c
1,c
2,c
3,c
4,c
5,c
6,c
7 are_mutually_different
by E8, E3;
end;
theorem :: BORSUK_5:9
for b
1, b
2, b
3, b
4, b
5, b
6, b
7 being
set holds
( b
1,b
2,b
3,b
4,b
5,b
6,b
7 are_mutually_different implies b
7,b
1,b
2,b
3,b
4,b
5,b
6 are_mutually_different )
proof
let c
1, c
2, c
3, c
4, c
5, c
6, c
7 be
set ;
assume
c
1,c
2,c
3,c
4,c
5,c
6,c
7 are_mutually_different
;
then
( c
1 <> c
2 & c
1 <> c
3 & c
1 <> c
4 & c
1 <> c
5 & c
1 <> c
6 & c
1 <> c
7 & c
2 <> c
3 & c
2 <> c
4 & c
2 <> c
5 & c
2 <> c
6 & c
2 <> c
7 & c
3 <> c
4 & c
3 <> c
5 & c
3 <> c
6 & c
3 <> c
7 & c
4 <> c
5 & c
4 <> c
6 & c
4 <> c
7 & c
5 <> c
6 & c
5 <> c
7 & c
6 <> c
7 )
by E3;
hence
c
7,c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
by E3;
end;
theorem :: BORSUK_5:10
for b
1, b
2, b
3, b
4, b
5, b
6, b
7 being
set holds
( b
1,b
2,b
3,b
4,b
5,b
6,b
7 are_mutually_different implies b
1,b
2,b
5,b
3,b
6,b
7,b
4 are_mutually_different )
proof
let c
1, c
2, c
3, c
4, c
5, c
6, c
7 be
set ;
assume
c
1,c
2,c
3,c
4,c
5,c
6,c
7 are_mutually_different
;
then
( c
1 <> c
2 & c
1 <> c
3 & c
1 <> c
4 & c
1 <> c
5 & c
1 <> c
6 & c
1 <> c
7 & c
2 <> c
3 & c
2 <> c
4 & c
2 <> c
5 & c
2 <> c
6 & c
2 <> c
7 & c
3 <> c
4 & c
3 <> c
5 & c
3 <> c
6 & c
3 <> c
7 & c
4 <> c
5 & c
4 <> c
6 & c
4 <> c
7 & c
5 <> c
6 & c
5 <> c
7 & c
6 <> c
7 )
by E3;
hence
c
1,c
2,c
5,c
3,c
6,c
7,c
4 are_mutually_different
by E3;
end;
theorem E6: :: BORSUK_5:11
proof
let c
1 be non
empty TopSpace;
let c
2, c
3 be
Point of c
1;
given c
4 being
Function of
I[01] ,c
1 such that
E7:
( c
4 is
continuous & c
4 . 0
= c
2 & c
4 . 1
= c
3 )
;
set c
5 =
L[01] (0,1 (#) ),
((#) 0,1);
E8:
(L[01] (0,1 (#) ),((#) 0,1)) . 0 =
(L[01] (0,1 (#) ),((#) 0,1)) . ((#) 0,1)
by TREAL_1:def 1
.=
0,1
(#)
by TREAL_1:12
.=
1
by TREAL_1:def 2
;
E9:
(L[01] (0,1 (#) ),((#) 0,1)) . 1 =
(L[01] (0,1 (#) ),((#) 0,1)) . (0,1 (#) )
by TREAL_1:def 2
.=
(#) 0,1
by TREAL_1:12
.=
0
by TREAL_1:def 1
;
set c
6 =
(L[01] (0,1 (#) ),((#) 0,1)) * c
4;
reconsider c
7 =
(L[01] (0,1 (#) ),((#) 0,1)) * c
4 as
Function of
I[01] ,c
1 by FUNCT_2:19, TOPMETR:27;
0
in [.0,1.]
by RCOMP_1:48;
then
0
in the
carrier of
(Closed-Interval-TSpace 0,1)
by TOPMETR:25;
then E10:
0
in dom (L[01] (0,1 (#) ),((#) 0,1))
by FUNCT_2:def 1;
1
in [.0,1.]
by RCOMP_1:48;
then
1
in the
carrier of
(Closed-Interval-TSpace 0,1)
by TOPMETR:25;
then E11:
1
in dom (L[01] (0,1 (#) ),((#) 0,1))
by FUNCT_2:def 1;
take
c
7
;
L[01] (0,1 (#) ),
((#) 0,1) is
continuous Function of
(Closed-Interval-TSpace 0,1),
(Closed-Interval-TSpace 0,1)
by TREAL_1:11;
hence
c
7 is
continuous
by E7, TOPMETR:27, TOPS_2:58;
thus
( c
7 . 0
= c
3 & c
7 . 1
= c
2 )
by E7, E8, E9, E10, E11, FUNCT_1:23;
end;
E7:
R^1 is arcwise_connected
proof
let c
1, c
2 be
Point of
R^1 ;
:: uses BORSUK_2:def 3
per cases
( c
1 <= c
2 or c
2 <= c
1 )
;
suppose E8:
c
1 <= c
2
;
reconsider c
3 =
[.c1,c2.] as
Subset of
R^1 by TOPMETR:24;
reconsider c
4 = c
3 as non
empty Subset of
R^1 by E8, RCOMP_1:48;
E9:
Closed-Interval-TSpace c
1,c
2 = R^1 | c
4
by E8, TOPMETR:26;
then E10:
L[01] ((#) c1,c2),
(c1,c2 (#) ) is
continuous Function of
I[01] ,
(R^1 | c4)
by E8, TOPMETR:27, TREAL_1:11;
the
carrier of
(R^1 | c4) c= the
carrier of
R^1
by BORSUK_1:35;
then reconsider c
5 =
L[01] ((#) c1,c2),
(c1,c2 (#) ) as
Function of the
carrier of
I[01] ,the
carrier of
R^1 by E9, FUNCT_2:9, TOPMETR:27;
reconsider c
6 = c
5 as
Function of
I[01] ,
R^1 ;
take
c
6
;
:: uses BORSUK_2:def 1thus
c
6 is
continuous
by E10, TOPMETR:7;
0
= (#) 0,1
by TREAL_1:def 1;
hence c
6 . 0 =
(#) c
1,c
2
by E8, TREAL_1:12
.=
c
1
by E8, TREAL_1:def 1
;
1
= 0,1
(#)
by TREAL_1:def 2;
hence c
6 . 1 =
c
1,c
2 (#)
by E8, TREAL_1:12
.=
c
2
by E8, TREAL_1:def 2
;
end;
suppose E8:
c
2 <= c
1
;
reconsider c
3 =
[.c2,c1.] as
Subset of
R^1 by TOPMETR:24;
c
2 in c
3
by E8, RCOMP_1:48;
then reconsider c
4 =
[.c2,c1.] as non
empty Subset of
R^1 ;
E9:
Closed-Interval-TSpace c
2,c
1 = R^1 | c
4
by E8, TOPMETR:26;
then E10:
L[01] ((#) c2,c1),
(c2,c1 (#) ) is
continuous Function of
I[01] ,
(R^1 | c4)
by E8, TOPMETR:27, TREAL_1:11;
the
carrier of
(R^1 | c4) c= the
carrier of
R^1
by BORSUK_1:35;
then reconsider c
5 =
L[01] ((#) c2,c1),
(c2,c1 (#) ) as
Function of the
carrier of
I[01] ,the
carrier of
R^1 by E9, FUNCT_2:9, TOPMETR:27;
reconsider c
6 = c
5 as
Function of
I[01] ,
R^1 ;
E11:
c
6 is
continuous
by E10, TOPMETR:7;
0
= (#) 0,1
by TREAL_1:def 1;
then E12: c
6 . 0 =
(#) c
2,c
1
by E8, TREAL_1:12
.=
c
2
by E8, TREAL_1:def 1
;
1
= 0,1
(#)
by TREAL_1:def 2;
then E13: c
6 . 1 =
c
2,c
1 (#)
by E8, TREAL_1:12
.=
c
1
by E8, TREAL_1:def 2
;
then
c
2,c
1 are_connected
by E11, E12, BORSUK_2:def 1;
then reconsider c
7 = c
6 as
Path of c
2,c
1 by E11, E12, E13, BORSUK_2:def 2;
take c
8 =
- c
7;
:: uses BORSUK_2:def 1
ex b
1 being
Function of
I[01] ,
R^1 st
( b
1 is
continuous & b
1 . 0
= c
1 & b
1 . 1
= c
2 )
by E11, E12, E13, E6;
then
c
1,c
2 are_connected
by BORSUK_2:def 1;
hence
( c
8 is
continuous & c
8 . 0
= c
1 & c
8 . 1
= c
2 )
by BORSUK_2:def 2;
end;
end;
end;
theorem :: BORSUK_5:12
canceled;
theorem E8: :: BORSUK_5:13
theorem E9: :: BORSUK_5:14
theorem E10: :: BORSUK_5:15
theorem E11: :: BORSUK_5:16
theorem E12: :: BORSUK_5:17
theorem E13: :: BORSUK_5:18
theorem E14: :: BORSUK_5:19
proof
let c
1, c
2, c
3, c
4 be
real number ;
assume E15:
( c
1 < c
2 & c
2 <= c
3 )
;
assume
[.c1,c2.] meets ].c3,c4.]
;
then consider c
5 being
set such that
E16:
( c
5 in [.c1,c2.] & c
5 in ].c3,c4.] )
by XBOOLE_0:3;
reconsider c
6 = c
5 as
real number by E16, XREAL_0:def 1;
( c
6 <= c
2 & c
6 > c
3 )
by E16, RCOMP_2:4, RCOMP_1:48;
hence
not verum
by E15, XREAL_1:2;
end;
theorem E15: :: BORSUK_5:20
proof
let c
1, c
2, c
3, c
4 be
real number ;
assume E16:
( c
1 < c
2 & c
2 <= c
3 )
;
assume
[.c1,c2.[ meets [.c3,c4.]
;
then consider c
5 being
set such that
E17:
( c
5 in [.c1,c2.[ & c
5 in [.c3,c4.] )
by XBOOLE_0:3;
reconsider c
6 = c
5 as
real number by E17, XREAL_0:def 1;
( c
6 < c
2 & c
6 >= c
3 )
by E17, RCOMP_2:3, RCOMP_1:48;
hence
not verum
by E16, XREAL_1:2;
end;
theorem :: BORSUK_5:21
proof
let c
1, c
2 be
Subset of
R^1 ;
let c
3, c
4, c
5, c
6 be
real number ;
assume that
E16:
( c
3 < c
4 & c
4 <= c
5 & c
5 < c
6 )
and
E17:
c
1 = [.c3,c4.[
and
E18:
c
2 = ].c5,c6.]
;
Cl [.c3,c4.[ = [.c3,c4.]
by E16, BORSUK_4:21;
then
Cl c
1 = [.c3,c4.]
by E17, TOPREAL6:80;
then E19:
Cl c
1 misses c
2
by E16, E18, E14;
Cl ].c5,c6.] = [.c5,c6.]
by E16, BORSUK_4:20;
then
Cl c
2 = [.c5,c6.]
by E18, TOPREAL6:80;
then
Cl c
2 misses c
1
by E16, E17, E15;
hence
c
1,c
2 are_separated
by E19, CONNSP_1:def 1;
end;
E16:
for b1 being real number holds REAL \ ].-infty,b1.[ = [.b1,+infty.[
by LIMFUNC1:24;
E17:
for b1 being real number holds REAL \ ].-infty,b1.] = ].b1,+infty.[
by LIMFUNC1:24;
E18:
for b1 being real number holds REAL \ [.b1,+infty.[ = ].-infty,b1.[
by LIMFUNC1:24;
theorem :: BORSUK_5:22
canceled;
theorem :: BORSUK_5:23
canceled;
theorem :: BORSUK_5:24
canceled;
theorem :: BORSUK_5:25
canceled;
theorem E19: :: BORSUK_5:26
theorem E20: :: BORSUK_5:27
theorem E21: :: BORSUK_5:28
proof
let c
1, c
2, c
3 be
real number ;
assume E22:
( c
1 <= c
3 & c
3 <= c
2 )
;
E23:
[.c1,+infty.[ c= [.c1,c2.] \/ [.c3,+infty.[
[.c1,c2.] \/ [.c3,+infty.[ c= [.c1,+infty.[
hence
[.c1,c2.] \/ [.c3,+infty.[ = [.c1,+infty.[
by E23, XBOOLE_0:def 10;
end;
theorem E22: :: BORSUK_5:29
theorem :: BORSUK_5:30
canceled;
theorem :: BORSUK_5:31
canceled;
theorem :: BORSUK_5:32
canceled;
theorem :: BORSUK_5:33
theorem E23: :: BORSUK_5:34
theorem E24: :: BORSUK_5:35
proof
let c
1 be
Subset of
R^1 ;
assume E25:
c
1 = RAT
;
Cl c
1 = the
carrier of
R^1
proof
thus
Cl c
1 c= the
carrier of
R^1
;
:: uses XBOOLE_0:def 10
thus
the
carrier of
R^1 c= Cl c
1
proof
let c
2 be
set ;
:: uses TARSKI:def 3
assume
c
2 in the
carrier of
R^1
;
then reconsider c
3 = c
2 as
Element of
RealSpace by METRIC_1:def 14, TOPMETR:24;
now
let c
4 be
real number ;
assume E26:
c
4 > 0
;
reconsider c
5 = c
3 + c
4 as
Element of
RealSpace by METRIC_1:def 14, XREAL_0:def 1;
c
3 < c
5
by E26, XREAL_1:31;
then consider c
6 being
rational number such that
E27:
( c
3 < c
6 & c
6 < c
5 )
by RAT_1:22;
E28:
c
6 in c
1
by E25, RAT_1:def 2;
reconsider c
7 = c
6 as
Element of
RealSpace by METRIC_1:def 14, XREAL_0:def 1;
c
7 - c
3 < c
5 - c
3
by E27, XREAL_1:11;
then
dist c
3,c
7 < c
4
by E27, E23;
then
c
7 in Ball c
3,c
4
by METRIC_1:12;
hence
Ball c
3,c
4 meets c
1
by E28, XBOOLE_0:3;
end;
hence
c
2 in Cl c
1
by HAUSDORF:7, TOPMETR:def 7;
end;
end;
hence
Cl c
1 = the
carrier of
R^1
;
end;
theorem E25: :: BORSUK_5:36
:: deftheorem defines IRRAT BORSUK_5:def 3 :
:: deftheorem defines RAT BORSUK_5:def 4 :
:: deftheorem defines IRRAT BORSUK_5:def 5 :
theorem E26: :: BORSUK_5:37
theorem E27: :: BORSUK_5:38
theorem E28: :: BORSUK_5:39