:: BORSUK_5 semantic presentation
theorem Th1: :: BORSUK_5:1
canceled;
theorem Th2: :: 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 Th3: :: 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}
:: according to XBOOLE_0:def 10
proof
let c
7 be
set ;
:: according to 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 ;
:: according to 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 c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different means :
Def1:
:: 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 Def1 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 c
1,c
2,c
3,c
4,c
5,c
6,c
7 are_mutually_different means :
Def2:
:: 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 Def2 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 Th4: :: 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 Def1;
then
c
1,c
2,c
3,c
4,c
5 are_mutually_different
by CARD_2:def 4;
then E6:
card {c1,c2,c3,c4,c5} = 5
by CARD_2:82;
( 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 Th5: :: 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 Def2;
then
c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
by Def1;
then E6:
card {c1,c2,c3,c4,c5,c6} = 6
by Th4;
( 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 Th6: :: 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 Th7: :: 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, Th6;
hence
c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
by E9, E10, Def1;
end;
theorem Th8: :: 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, Def1;
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, Def2;
end;
theorem Th9: :: 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 Def2;
hence
c
7,c
1,c
2,c
3,c
4,c
5,c
6 are_mutually_different
by Def2;
end;
theorem Th10: :: 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 Def2;
hence
c
1,c
2,c
5,c
3,c
6,c
7,c
4 are_mutually_different
by Def2;
end;
theorem Th11: :: BORSUK_5:11
Lemma7:
R^1 is arcwise_connected
proof
let c
1, c
2 be
Point of
R^1 ;
:: according to BORSUK_2:def 3
per cases
( c1 <= c2 or c2 <= c1 )
;
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
;
:: according to 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;
:: according to 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, Th11;
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 Th12: :: BORSUK_5:12
canceled;
theorem Th13: :: BORSUK_5:13
theorem Th14: :: BORSUK_5:14
theorem Th15: :: BORSUK_5:15
theorem Th16: :: BORSUK_5:16
theorem Th17: :: BORSUK_5:17
theorem Th18: :: BORSUK_5:18
theorem Th19: :: 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, XXREAL_0:2;
end;
theorem Th20: :: 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, XXREAL_0:2;
end;
theorem Th21: :: 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, Th19;
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, Th20;
hence
c
1,c
2 are_separated
by E19, CONNSP_1:def 1;
end;
Lemma16:
for b1 being real number holds REAL \ ].-infty,b1.[ = [.b1,+infty.[
by LIMFUNC1:24;
Lemma17:
for b1 being real number holds REAL \ ].-infty,b1.] = ].b1,+infty.[
by LIMFUNC1:24;
Lemma18:
for b1 being real number holds REAL \ [.b1,+infty.[ = ].-infty,b1.[
by LIMFUNC1:24;
theorem Th22: :: BORSUK_5:22
canceled;
theorem Th23: :: BORSUK_5:23
canceled;
theorem Th24: :: BORSUK_5:24
canceled;
theorem Th25: :: BORSUK_5:25
canceled;
theorem Th26: :: BORSUK_5:26
theorem Th27: :: BORSUK_5:27
theorem Th28: :: 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 Th29: :: BORSUK_5:29
theorem Th30: :: BORSUK_5:30
canceled;
theorem Th31: :: BORSUK_5:31
canceled;
theorem Th32: :: BORSUK_5:32
canceled;
theorem Th33: :: BORSUK_5:33
theorem Th34: :: BORSUK_5:34
theorem Th35: :: 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
;
:: according to XBOOLE_0:def 10
thus
the
carrier of
R^1 c= Cl c
1
proof
let c
2 be
set ;
:: according to 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, Th34;
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 GOBOARD6:95, TOPMETR:def 7;
end;
end;
hence
Cl c
1 = the
carrier of
R^1
;
end;
theorem Th36: :: BORSUK_5:36