:: BORSUK_5 semantic presentation
begin
theorem :: BORSUK_5:1
canceled;
theorem :: BORSUK_5:2
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}
thus {x1,x2,x3,x4,x5,x6} c= {x1,x3,x6} \/ {x2,x4,x5} :: according to XBOOLE_0:def_10 ::_thesis: {x1,x3,x6} \/ {x2,x4,x5} c= {x1,x2,x3,x4,x5,x6}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6} or x in {x1,x3,x6} \/ {x2,x4,x5} )
assume x in {x1,x2,x3,x4,x5,x6} ; ::_thesis: x in {x1,x3,x6} \/ {x2,x4,x5}
then ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) by ENUMSET1:def_4;
then ( x in {x1,x3,x6} or x in {x2,x4,x5} ) by ENUMSET1:def_1;
hence x in {x1,x3,x6} \/ {x2,x4,x5} by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x3,x6} \/ {x2,x4,x5} or x in {x1,x2,x3,x4,x5,x6} )
assume x in {x1,x3,x6} \/ {x2,x4,x5} ; ::_thesis: x in {x1,x2,x3,x4,x5,x6}
then ( x in {x1,x3,x6} or x in {x2,x4,x5} ) by XBOOLE_0:def_3;
then ( x = x1 or x = x3 or x = x6 or x = x2 or x = x4 or x = x5 ) by ENUMSET1:def_1;
hence x in {x1,x2,x3,x4,x5,x6} by ENUMSET1:def_4; ::_thesis: verum
end;
theorem Th3: :: BORSUK_5:3
for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3,x4,x5,x6 are_mutually_different holds
card {x1,x2,x3,x4,x5,x6} = 6
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6 are_mutually_different implies card {x1,x2,x3,x4,x5,x6} = 6 )
A1: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6} by ENUMSET1:15;
assume A2: x1,x2,x3,x4,x5,x6 are_mutually_different ; ::_thesis: card {x1,x2,x3,x4,x5,x6} = 6
then A3: x1 <> x3 by ZFMISC_1:def_8;
A4: x4 <> x5 by A2, ZFMISC_1:def_8;
A5: x3 <> x5 by A2, ZFMISC_1:def_8;
A6: x3 <> x4 by A2, ZFMISC_1:def_8;
A7: x2 <> x5 by A2, ZFMISC_1:def_8;
A8: x2 <> x4 by A2, ZFMISC_1:def_8;
A9: x2 <> x3 by A2, ZFMISC_1:def_8;
A10: x1 <> x5 by A2, ZFMISC_1:def_8;
A11: x1 <> x4 by A2, ZFMISC_1:def_8;
x1 <> x2 by A2, ZFMISC_1:def_8;
then x1,x2,x3,x4,x5 are_mutually_different by A3, A11, A10, A9, A8, A7, A6, A5, A4, ZFMISC_1:def_7;
then A12: card {x1,x2,x3,x4,x5} = 5 by CARD_2:63;
A13: x3 <> x6 by A2, ZFMISC_1:def_8;
A14: x2 <> x6 by A2, ZFMISC_1:def_8;
A15: x5 <> x6 by A2, ZFMISC_1:def_8;
A16: x4 <> x6 by A2, ZFMISC_1:def_8;
x1 <> x6 by A2, ZFMISC_1:def_8;
then not x6 in {x1,x2,x3,x4,x5} by A14, A13, A16, A15, ENUMSET1:def_3;
hence card {x1,x2,x3,x4,x5,x6} = 5 + 1 by A12, A1, CARD_2:41
.= 6 ;
::_thesis: verum
end;
theorem :: BORSUK_5:4
for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds
card {x1,x2,x3,x4,x5,x6,x7} = 7
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6,x7 are_mutually_different implies card {x1,x2,x3,x4,x5,x6,x7} = 7 )
A1: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7} by ENUMSET1:21;
assume A2: x1,x2,x3,x4,x5,x6,x7 are_mutually_different ; ::_thesis: card {x1,x2,x3,x4,x5,x6,x7} = 7
then A3: x1 <> x3 by ZFMISC_1:def_9;
A4: x5 <> x7 by A2, ZFMISC_1:def_9;
A5: x4 <> x7 by A2, ZFMISC_1:def_9;
A6: x3 <> x7 by A2, ZFMISC_1:def_9;
A7: x2 <> x7 by A2, ZFMISC_1:def_9;
A8: x4 <> x6 by A2, ZFMISC_1:def_9;
A9: x4 <> x5 by A2, ZFMISC_1:def_9;
A10: x5 <> x6 by A2, ZFMISC_1:def_9;
A11: x1 <> x5 by A2, ZFMISC_1:def_9;
A12: x1 <> x4 by A2, ZFMISC_1:def_9;
A13: x3 <> x6 by A2, ZFMISC_1:def_9;
A14: x3 <> x5 by A2, ZFMISC_1:def_9;
A15: x3 <> x4 by A2, ZFMISC_1:def_9;
A16: x2 <> x6 by A2, ZFMISC_1:def_9;
A17: x2 <> x5 by A2, ZFMISC_1:def_9;
A18: x2 <> x4 by A2, ZFMISC_1:def_9;
A19: x2 <> x3 by A2, ZFMISC_1:def_9;
A20: x1 <> x6 by A2, ZFMISC_1:def_9;
x1 <> x2 by A2, ZFMISC_1:def_9;
then x1,x2,x3,x4,x5,x6 are_mutually_different by A3, A12, A11, A20, A19, A18, A17, A16, A15, A14, A13, A9, A8, A10, ZFMISC_1:def_8;
then A21: card {x1,x2,x3,x4,x5,x6} = 6 by Th3;
A22: x6 <> x7 by A2, ZFMISC_1:def_9;
x1 <> x7 by A2, ZFMISC_1:def_9;
then not x7 in {x1,x2,x3,x4,x5,x6} by A7, A6, A5, A4, A22, ENUMSET1:def_4;
hence card {x1,x2,x3,x4,x5,x6,x7} = 6 + 1 by A21, A1, CARD_2:41
.= 7 ;
::_thesis: verum
end;
theorem Th5: :: BORSUK_5:5
for x1, x2, x3, x4, x5, x6 being set st {x1,x2,x3} misses {x4,x5,x6} holds
( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 )
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: ( {x1,x2,x3} misses {x4,x5,x6} implies ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 ) )
assume A1: {x1,x2,x3} misses {x4,x5,x6} ; ::_thesis: ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 )
A2: x5 in {x4,x5,x6} by ENUMSET1:def_1;
assume ( x1 = x4 or x1 = x5 or x1 = x6 or x2 = x4 or x2 = x5 or x2 = x6 or x3 = x4 or x3 = x5 or x3 = x6 ) ; ::_thesis: contradiction
then A3: ( x4 in {x1,x2,x3} or x5 in {x1,x2,x3} or x6 in {x1,x2,x3} ) by ENUMSET1:def_1;
A4: x6 in {x4,x5,x6} by ENUMSET1:def_1;
x4 in {x4,x5,x6} by ENUMSET1:def_1;
hence contradiction by A1, A3, A2, A4, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: BORSUK_5:6
for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3 are_mutually_different & x4,x5,x6 are_mutually_different & {x1,x2,x3} misses {x4,x5,x6} holds
x1,x2,x3,x4,x5,x6 are_mutually_different
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: ( x1,x2,x3 are_mutually_different & x4,x5,x6 are_mutually_different & {x1,x2,x3} misses {x4,x5,x6} implies x1,x2,x3,x4,x5,x6 are_mutually_different )
assume that
A1: x1,x2,x3 are_mutually_different and
A2: x4,x5,x6 are_mutually_different and
A3: {x1,x2,x3} misses {x4,x5,x6} ; ::_thesis: x1,x2,x3,x4,x5,x6 are_mutually_different
A4: x1 <> x2 by A1, ZFMISC_1:def_5;
A5: x3 <> x5 by A3, Th5;
A6: x3 <> x4 by A3, Th5;
A7: x1 <> x6 by A3, Th5;
A8: x1 <> x3 by A1, ZFMISC_1:def_5;
A9: x2 <> x5 by A3, Th5;
A10: x5 <> x6 by A2, ZFMISC_1:def_5;
A11: x2 <> x4 by A3, Th5;
A12: x4 <> x5 by A2, ZFMISC_1:def_5;
A13: x2 <> x6 by A3, Th5;
A14: x4 <> x6 by A2, ZFMISC_1:def_5;
A15: x3 <> x6 by A3, Th5;
A16: x1 <> x5 by A3, Th5;
A17: x2 <> x3 by A1, ZFMISC_1:def_5;
x1 <> x4 by A3, Th5;
hence x1,x2,x3,x4,x5,x6 are_mutually_different by A4, A17, A8, A12, A10, A14, A16, A7, A11, A9, A13, A6, A5, A15, ZFMISC_1:def_8; ::_thesis: verum
end;
theorem :: BORSUK_5:7
for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6 are_mutually_different & {x1,x2,x3,x4,x5,x6} misses {x7} holds
x1,x2,x3,x4,x5,x6,x7 are_mutually_different
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6 are_mutually_different & {x1,x2,x3,x4,x5,x6} misses {x7} implies x1,x2,x3,x4,x5,x6,x7 are_mutually_different )
assume that
A1: x1,x2,x3,x4,x5,x6 are_mutually_different and
A2: {x1,x2,x3,x4,x5,x6} misses {x7} ; ::_thesis: x1,x2,x3,x4,x5,x6,x7 are_mutually_different
A3: x1 <> x3 by A1, ZFMISC_1:def_8;
A4: x2 <> x3 by A1, ZFMISC_1:def_8;
A5: x1 <> x6 by A1, ZFMISC_1:def_8;
A6: x1 <> x5 by A1, ZFMISC_1:def_8;
A7: x1 <> x4 by A1, ZFMISC_1:def_8;
A8: not x7 in {x1,x2,x3,x4,x5,x6} by A2, ZFMISC_1:48;
then A9: x7 <> x1 by ENUMSET1:def_4;
A10: x4 <> x6 by A1, ZFMISC_1:def_8;
A11: x4 <> x5 by A1, ZFMISC_1:def_8;
A12: x3 <> x6 by A1, ZFMISC_1:def_8;
A13: x3 <> x5 by A1, ZFMISC_1:def_8;
A14: x3 <> x4 by A1, ZFMISC_1:def_8;
A15: x2 <> x6 by A1, ZFMISC_1:def_8;
A16: x2 <> x5 by A1, ZFMISC_1:def_8;
A17: x2 <> x4 by A1, ZFMISC_1:def_8;
A18: x7 <> x6 by A8, ENUMSET1:def_4;
A19: x5 <> x6 by A1, ZFMISC_1:def_8;
A20: x7 <> x5 by A8, ENUMSET1:def_4;
A21: x7 <> x4 by A8, ENUMSET1:def_4;
A22: x7 <> x3 by A8, ENUMSET1:def_4;
A23: x7 <> x2 by A8, ENUMSET1:def_4;
x1 <> x2 by A1, ZFMISC_1:def_8;
hence x1,x2,x3,x4,x5,x6,x7 are_mutually_different by A3, A7, A6, A5, A4, A17, A16, A15, A14, A13, A12, A11, A10, A19, A9, A23, A22, A21, A20, A18, ZFMISC_1:def_9; ::_thesis: verum
end;
theorem :: BORSUK_5:8
for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds
x7,x1,x2,x3,x4,x5,x6 are_mutually_different
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6,x7 are_mutually_different implies x7,x1,x2,x3,x4,x5,x6 are_mutually_different )
assume A1: x1,x2,x3,x4,x5,x6,x7 are_mutually_different ; ::_thesis: x7,x1,x2,x3,x4,x5,x6 are_mutually_different
then A2: x1 <> x3 by ZFMISC_1:def_9;
A3: x5 <> x7 by A1, ZFMISC_1:def_9;
A4: x5 <> x6 by A1, ZFMISC_1:def_9;
A5: x4 <> x7 by A1, ZFMISC_1:def_9;
A6: x4 <> x6 by A1, ZFMISC_1:def_9;
A7: x6 <> x7 by A1, ZFMISC_1:def_9;
A8: x1 <> x5 by A1, ZFMISC_1:def_9;
A9: x1 <> x4 by A1, ZFMISC_1:def_9;
A10: x2 <> x4 by A1, ZFMISC_1:def_9;
A11: x2 <> x3 by A1, ZFMISC_1:def_9;
A12: x1 <> x7 by A1, ZFMISC_1:def_9;
A13: x1 <> x6 by A1, ZFMISC_1:def_9;
A14: x4 <> x5 by A1, ZFMISC_1:def_9;
A15: x3 <> x7 by A1, ZFMISC_1:def_9;
A16: x3 <> x6 by A1, ZFMISC_1:def_9;
A17: x3 <> x5 by A1, ZFMISC_1:def_9;
A18: x3 <> x4 by A1, ZFMISC_1:def_9;
A19: x2 <> x7 by A1, ZFMISC_1:def_9;
A20: x2 <> x6 by A1, ZFMISC_1:def_9;
A21: x2 <> x5 by A1, ZFMISC_1:def_9;
x1 <> x2 by A1, ZFMISC_1:def_9;
hence x7,x1,x2,x3,x4,x5,x6 are_mutually_different by A2, A9, A8, A13, A12, A11, A10, A21, A20, A19, A18, A17, A16, A15, A14, A6, A5, A4, A3, A7, ZFMISC_1:def_9; ::_thesis: verum
end;
theorem :: BORSUK_5:9
for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds
x1,x2,x5,x3,x6,x7,x4 are_mutually_different
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6,x7 are_mutually_different implies x1,x2,x5,x3,x6,x7,x4 are_mutually_different )
assume A1: x1,x2,x3,x4,x5,x6,x7 are_mutually_different ; ::_thesis: x1,x2,x5,x3,x6,x7,x4 are_mutually_different
then A2: x1 <> x3 by ZFMISC_1:def_9;
A3: x5 <> x7 by A1, ZFMISC_1:def_9;
A4: x5 <> x6 by A1, ZFMISC_1:def_9;
A5: x4 <> x7 by A1, ZFMISC_1:def_9;
A6: x4 <> x6 by A1, ZFMISC_1:def_9;
A7: x6 <> x7 by A1, ZFMISC_1:def_9;
A8: x1 <> x5 by A1, ZFMISC_1:def_9;
A9: x1 <> x4 by A1, ZFMISC_1:def_9;
A10: x2 <> x4 by A1, ZFMISC_1:def_9;
A11: x2 <> x3 by A1, ZFMISC_1:def_9;
A12: x1 <> x7 by A1, ZFMISC_1:def_9;
A13: x1 <> x6 by A1, ZFMISC_1:def_9;
A14: x4 <> x5 by A1, ZFMISC_1:def_9;
A15: x3 <> x7 by A1, ZFMISC_1:def_9;
A16: x3 <> x6 by A1, ZFMISC_1:def_9;
A17: x3 <> x5 by A1, ZFMISC_1:def_9;
A18: x3 <> x4 by A1, ZFMISC_1:def_9;
A19: x2 <> x7 by A1, ZFMISC_1:def_9;
A20: x2 <> x6 by A1, ZFMISC_1:def_9;
A21: x2 <> x5 by A1, ZFMISC_1:def_9;
x1 <> x2 by A1, ZFMISC_1:def_9;
hence x1,x2,x5,x3,x6,x7,x4 are_mutually_different by A2, A9, A8, A13, A12, A11, A10, A21, A20, A19, A18, A17, A16, A15, A14, A6, A5, A4, A3, A7, ZFMISC_1:def_9; ::_thesis: verum
end;
Lm1: R^1 is pathwise_connected
proof
let a, b be Point of R^1; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
percases ( a <= b or b <= a ) ;
supposeA1: a <= b ; ::_thesis: a,b are_connected
reconsider B = [.a,b.] as Subset of R^1 by TOPMETR:17;
reconsider B = B as non empty Subset of R^1 by A1, XXREAL_1:1;
A2: Closed-Interval-TSpace (a,b) = R^1 | B by A1, TOPMETR:19;
the carrier of (R^1 | B) c= the carrier of R^1 by BORSUK_1:1;
then reconsider g = L[01] (((#) (a,b)),((a,b) (#))) as Function of the carrier of I[01], the carrier of R^1 by A2, FUNCT_2:7, TOPMETR:20;
reconsider g = g as Function of I[01],R^1 ;
take g ; :: according to BORSUK_2:def_1 ::_thesis: ( g is continuous & g . 0 = a & g . 1 = b )
L[01] (((#) (a,b)),((a,b) (#))) is continuous Function of I[01],(R^1 | B) by A1, A2, TOPMETR:20, TREAL_1:8;
hence g is continuous by PRE_TOPC:26; ::_thesis: ( g . 0 = a & g . 1 = b )
0 = (#) (0,1) by TREAL_1:def_1;
hence g . 0 = (#) (a,b) by A1, TREAL_1:9
.= a by A1, TREAL_1:def_1 ;
::_thesis: g . 1 = b
1 = (0,1) (#) by TREAL_1:def_2;
hence g . 1 = (a,b) (#) by A1, TREAL_1:9
.= b by A1, TREAL_1:def_2 ;
::_thesis: verum
end;
supposeA3: b <= a ; ::_thesis: a,b are_connected
reconsider B = [.b,a.] as Subset of R^1 by TOPMETR:17;
b in B by A3, XXREAL_1:1;
then reconsider B = [.b,a.] as non empty Subset of R^1 ;
A4: Closed-Interval-TSpace (b,a) = R^1 | B by A3, TOPMETR:19;
the carrier of (R^1 | B) c= the carrier of R^1 by BORSUK_1:1;
then reconsider g = L[01] (((#) (b,a)),((b,a) (#))) as Function of the carrier of I[01], the carrier of R^1 by A4, FUNCT_2:7, TOPMETR:20;
reconsider g = g as Function of I[01],R^1 ;
0 = (#) (0,1) by TREAL_1:def_1;
then A5: g . 0 = (#) (b,a) by A3, TREAL_1:9
.= b by A3, TREAL_1:def_1 ;
1 = (0,1) (#) by TREAL_1:def_2;
then A6: g . 1 = (b,a) (#) by A3, TREAL_1:9
.= a by A3, TREAL_1:def_2 ;
L[01] (((#) (b,a)),((b,a) (#))) is continuous Function of I[01],(R^1 | B) by A3, A4, TOPMETR:20, TREAL_1:8;
then A7: g is continuous by PRE_TOPC:26;
then b,a are_connected by A5, A6, BORSUK_2:def_1;
then reconsider P = g as Path of b,a by A7, A5, A6, BORSUK_2:def_2;
take - P ; :: according to BORSUK_2:def_1 ::_thesis: ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b )
ex t being Function of I[01],R^1 st
( t is continuous & t . 0 = a & t . 1 = b ) by A7, A5, A6, BORSUK_2:15;
then a,b are_connected by BORSUK_2:def_1;
hence ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b ) by BORSUK_2:def_2; ::_thesis: verum
end;
end;
end;
registration
cluster R^1 -> pathwise_connected ;
coherence
R^1 is pathwise_connected by Lm1;
end;
registration
cluster non empty TopSpace-like connected for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is connected & not b1 is empty )
proof
take R^1 ; ::_thesis: ( R^1 is connected & not R^1 is empty )
thus ( R^1 is connected & not R^1 is empty ) ; ::_thesis: verum
end;
end;
begin
theorem :: BORSUK_5:10
for A, B being Subset of R^1
for a, b, c, d being real number st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds
A,B are_separated
proof
let A, B be Subset of R^1; ::_thesis: for a, b, c, d being real number st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds
A,B are_separated
let a, b, c, d be real number ; ::_thesis: ( a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] implies A,B are_separated )
assume that
A1: a < b and
A2: b <= c and
A3: c < d and
A4: A = [.a,b.[ and
A5: B = ].c,d.] ; ::_thesis: A,B are_separated
Cl ].c,d.] = [.c,d.] by A3, BORSUK_4:11;
then Cl B = [.c,d.] by A5, JORDAN5A:24;
then A6: Cl B misses A by A2, A4, XXREAL_1:95;
Cl [.a,b.[ = [.a,b.] by A1, BORSUK_4:12;
then Cl A = [.a,b.] by A4, JORDAN5A:24;
then Cl A misses B by A2, A5, XXREAL_1:90;
hence A,B are_separated by A6, CONNSP_1:def_1; ::_thesis: verum
end;
theorem Th11: :: BORSUK_5:11
for a, b, c being real number st a <= c & c <= b holds
[.a,b.] \/ [.c,+infty.[ = [.a,+infty.[
proof
let a, b, c be real number ; ::_thesis: ( a <= c & c <= b implies [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ )
assume that
A1: a <= c and
A2: c <= b ; ::_thesis: [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[
A3: [.a,+infty.[ c= [.a,b.] \/ [.c,+infty.[
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in [.a,+infty.[ or r in [.a,b.] \/ [.c,+infty.[ )
assume A4: r in [.a,+infty.[ ; ::_thesis: r in [.a,b.] \/ [.c,+infty.[
then reconsider s = r as Real ;
A5: a <= s by A4, XXREAL_1:236;
percases ( s <= b or not s <= b ) ;
suppose s <= b ; ::_thesis: r in [.a,b.] \/ [.c,+infty.[
then s in [.a,b.] by A5, XXREAL_1:1;
hence r in [.a,b.] \/ [.c,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not s <= b ; ::_thesis: r in [.a,b.] \/ [.c,+infty.[
then c <= s by A2, XXREAL_0:2;
then s in [.c,+infty.[ by XXREAL_1:236;
hence r in [.a,b.] \/ [.c,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
A6: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
[.c,+infty.[ c= [.a,+infty.[ by A1, XXREAL_1:38;
then [.a,b.] \/ [.c,+infty.[ c= [.a,+infty.[ by A6, XBOOLE_1:8;
hence [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th12: :: BORSUK_5:12
for a, b, c being real number st a <= c & c <= b holds
].-infty,c.] \/ [.a,b.] = ].-infty,b.]
proof
let a, b, c be real number ; ::_thesis: ( a <= c & c <= b implies ].-infty,c.] \/ [.a,b.] = ].-infty,b.] )
assume that
A1: a <= c and
A2: c <= b ; ::_thesis: ].-infty,c.] \/ [.a,b.] = ].-infty,b.]
thus ].-infty,c.] \/ [.a,b.] c= ].-infty,b.] :: according to XBOOLE_0:def_10 ::_thesis: ].-infty,b.] c= ].-infty,c.] \/ [.a,b.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,c.] \/ [.a,b.] or x in ].-infty,b.] )
assume A3: x in ].-infty,c.] \/ [.a,b.] ; ::_thesis: x in ].-infty,b.]
then reconsider x = x as real number ;
percases ( x in ].-infty,c.] or x in [.a,b.] ) by A3, XBOOLE_0:def_3;
suppose x in ].-infty,c.] ; ::_thesis: x in ].-infty,b.]
then x <= c by XXREAL_1:234;
then x <= b by A2, XXREAL_0:2;
hence x in ].-infty,b.] by XXREAL_1:234; ::_thesis: verum
end;
suppose x in [.a,b.] ; ::_thesis: x in ].-infty,b.]
then x <= b by XXREAL_1:1;
hence x in ].-infty,b.] by XXREAL_1:234; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,b.] or x in ].-infty,c.] \/ [.a,b.] )
assume A4: x in ].-infty,b.] ; ::_thesis: x in ].-infty,c.] \/ [.a,b.]
then reconsider x = x as real number ;
percases ( x <= c or x > c ) ;
suppose x <= c ; ::_thesis: x in ].-infty,c.] \/ [.a,b.]
then x in ].-infty,c.] by XXREAL_1:234;
hence x in ].-infty,c.] \/ [.a,b.] by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA5: x > c ; ::_thesis: x in ].-infty,c.] \/ [.a,b.]
A6: x <= b by A4, XXREAL_1:234;
x > a by A1, A5, XXREAL_0:2;
then x in [.a,b.] by A6, XXREAL_1:1;
hence x in ].-infty,c.] \/ [.a,b.] by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
registration
cluster -> real for Element of RAT ;
coherence
for b1 being Element of RAT holds b1 is real ;
end;
theorem :: BORSUK_5:13
for A being Subset of R^1
for p being Point of RealSpace holds
( p in Cl A iff for r being real number st r > 0 holds
Ball (p,r) meets A ) by GOBOARD6:92, TOPMETR:def_6;
theorem Th14: :: BORSUK_5:14
for p, q being Element of RealSpace st q >= p holds
dist (p,q) = q - p
proof
let p, q be Element of RealSpace; ::_thesis: ( q >= p implies dist (p,q) = q - p )
assume p <= q ; ::_thesis: dist (p,q) = q - p
then A1: q - p >= 0 by XREAL_1:48;
dist (p,q) = abs (q - p) by TOPMETR:11
.= q - p by A1, ABSVALUE:def_1 ;
hence dist (p,q) = q - p ; ::_thesis: verum
end;
theorem Th15: :: BORSUK_5:15
for A being Subset of R^1 st A = RAT holds
Cl A = the carrier of R^1
proof
let A be Subset of R^1; ::_thesis: ( A = RAT implies Cl A = the carrier of R^1 )
assume A1: A = RAT ; ::_thesis: Cl A = the carrier of R^1
the carrier of R^1 c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R^1 or x in Cl A )
assume x in the carrier of R^1 ; ::_thesis: x in Cl A
then reconsider p = x as Element of RealSpace by METRIC_1:def_13, TOPMETR:17;
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
Ball_(p,r)_meets_A
let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A )
reconsider pr = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
assume r > 0 ; ::_thesis: Ball (p,r) meets A
then consider Q being rational number such that
A2: p < Q and
A3: Q < pr by RAT_1:7, XREAL_1:29;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
P - p < pr - p by A3, XREAL_1:9;
then dist (p,P) < r by A2, Th14;
then A4: P in Ball (p,r) by METRIC_1:11;
Q in A by A1, RAT_1:def_2;
hence Ball (p,r) meets A by A4, XBOOLE_0:3; ::_thesis: verum
end;
hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
hence Cl A = the carrier of R^1 by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th16: :: BORSUK_5:16
for A being Subset of R^1
for a, b being real number st A = ].a,b.[ & a <> b holds
Cl A = [.a,b.]
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st A = ].a,b.[ & a <> b holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( A = ].a,b.[ & a <> b implies Cl A = [.a,b.] )
assume that
A1: A = ].a,b.[ and
A2: a <> b ; ::_thesis: Cl A = [.a,b.]
Cl ].a,b.[ = [.a,b.] by A2, JORDAN5A:26;
hence Cl A = [.a,b.] by A1, JORDAN5A:24; ::_thesis: verum
end;
begin
registration
cluster number_e -> irrational ;
coherence
number_e is irrational by IRRAT_1:41;
end;
definition
func IRRAT -> Subset of REAL equals :: BORSUK_5:def 1
REAL \ RAT;
coherence
REAL \ RAT is Subset of REAL ;
end;
:: deftheorem defines IRRAT BORSUK_5:def_1_:_
IRRAT = REAL \ RAT;
definition
let a, b be real number ;
func RAT (a,b) -> Subset of REAL equals :: BORSUK_5:def 2
RAT /\ ].a,b.[;
coherence
RAT /\ ].a,b.[ is Subset of REAL ;
func IRRAT (a,b) -> Subset of REAL equals :: BORSUK_5:def 3
IRRAT /\ ].a,b.[;
coherence
IRRAT /\ ].a,b.[ is Subset of REAL ;
end;
:: deftheorem defines RAT BORSUK_5:def_2_:_
for a, b being real number holds RAT (a,b) = RAT /\ ].a,b.[;
:: deftheorem defines IRRAT BORSUK_5:def_3_:_
for a, b being real number holds IRRAT (a,b) = IRRAT /\ ].a,b.[;
theorem Th17: :: BORSUK_5:17
for x being real number holds
( x is irrational iff x in IRRAT )
proof
let x be real number ; ::_thesis: ( x is irrational iff x in IRRAT )
A1: x in REAL by XREAL_0:def_1;
hereby ::_thesis: ( x in IRRAT implies x is irrational )
assume x is irrational ; ::_thesis: x in IRRAT
then not x in RAT ;
hence x in IRRAT by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
assume x in IRRAT ; ::_thesis: x is irrational
then not x in RAT by XBOOLE_0:def_5;
hence x is irrational by RAT_1:def_2; ::_thesis: verum
end;
registration
cluster complex real ext-real irrational for set ;
existence
ex b1 being real number st b1 is irrational by IRRAT_1:41;
end;
registration
cluster IRRAT -> non empty ;
coherence
not IRRAT is empty by Th17, IRRAT_1:41;
end;
registration
let a be rational number ;
let b be real irrational number ;
clustera + b -> irrational ;
coherence
a + b is irrational
proof
set m1 = the Integer;
assume a + b is rational ; ::_thesis: contradiction
then consider m, n being Integer such that
n <> 0 and
A1: a + b = m / n by RAT_1:2;
(a + b) - a = ((m * the Integer) - ( the Integer * n)) / ( the Integer * n) by A1;
hence contradiction ; ::_thesis: verum
end;
clusterb + a -> irrational ;
coherence
b + a is irrational ;
end;
theorem :: BORSUK_5:18
for a being rational number
for b being real irrational number holds a + b is irrational ;
registration
let a be real irrational number ;
cluster - a -> irrational ;
coherence
- a is irrational
proof
assume - a is rational ; ::_thesis: contradiction
then reconsider b = - a as rational number ;
- b is rational ;
hence contradiction ; ::_thesis: verum
end;
end;
theorem :: BORSUK_5:19
for a being real irrational number holds - a is irrational ;
registration
let a be rational number ;
let b be real irrational number ;
clustera - b -> irrational ;
coherence
a - b is irrational
proof
a + (- b) is irrational ;
hence a - b is irrational ; ::_thesis: verum
end;
clusterb - a -> irrational ;
coherence
b - a is irrational
proof
b + (- a) is irrational ;
hence b - a is irrational ; ::_thesis: verum
end;
end;
theorem :: BORSUK_5:20
for a being rational number
for b being real irrational number holds a - b is irrational ;
theorem :: BORSUK_5:21
for a being rational number
for b being real irrational number holds b - a is irrational ;
theorem Th22: :: BORSUK_5:22
for a being rational number
for b being real irrational number st a <> 0 holds
a * b is irrational
proof
let a be rational number ; ::_thesis: for b being real irrational number st a <> 0 holds
a * b is irrational
let b be real irrational number ; ::_thesis: ( a <> 0 implies a * b is irrational )
assume A1: a <> 0 ; ::_thesis: a * b is irrational
assume a * b is rational ; ::_thesis: contradiction
then consider m, n being Integer such that
n <> 0 and
A2: a * b = m / n by RAT_1:2;
consider m1, n1 being Integer such that
n1 <> 0 and
A3: a = m1 / n1 by RAT_1:2;
(a * b) / a = (m * n1) / (n * m1) by A2, A3, XCMPLX_1:84;
hence contradiction by A1, XCMPLX_1:89; ::_thesis: verum
end;
theorem Th23: :: BORSUK_5:23
for a being rational number
for b being real irrational number st a <> 0 holds
b / a is irrational
proof
let a be rational number ; ::_thesis: for b being real irrational number st a <> 0 holds
b / a is irrational
let b be real irrational number ; ::_thesis: ( a <> 0 implies b / a is irrational )
assume A1: a <> 0 ; ::_thesis: b / a is irrational
assume b / a is rational ; ::_thesis: contradiction
then reconsider c = b / a as rational number ;
c * a is rational ;
hence contradiction by A1, XCMPLX_1:87; ::_thesis: verum
end;
registration
cluster real irrational -> non zero real for set ;
coherence
for b1 being real number st b1 is irrational holds
not b1 is zero
proof
let a be real number ; ::_thesis: ( a is irrational implies not a is zero )
assume A1: a is irrational ; ::_thesis: not a is zero
assume a is zero ; ::_thesis: contradiction
then a = 0 / 1 ;
hence contradiction by A1; ::_thesis: verum
end;
end;
theorem Th24: :: BORSUK_5:24
for a being rational number
for b being real irrational number st a <> 0 holds
a / b is irrational
proof
let a be rational number ; ::_thesis: for b being real irrational number st a <> 0 holds
a / b is irrational
let b be real irrational number ; ::_thesis: ( a <> 0 implies a / b is irrational )
assume A1: a <> 0 ; ::_thesis: a / b is irrational
assume a / b is rational ; ::_thesis: contradiction
then reconsider c = a / b as rational number ;
c * b is irrational by A1, Th22, XCMPLX_1:50;
hence contradiction by XCMPLX_1:87; ::_thesis: verum
end;
registration
let r be real irrational number ;
cluster frac r -> irrational ;
coherence
frac r is irrational
proof
frac r = r - [\r/] by INT_1:def_8;
hence frac r is irrational ; ::_thesis: verum
end;
end;
theorem :: BORSUK_5:25
for r being real irrational number holds frac r is irrational ;
registration
cluster non zero complex real ext-real rational for set ;
existence
not for b1 being rational number holds b1 is zero
proof
1 <> 0 ;
hence not for b1 being rational number holds b1 is zero ; ::_thesis: verum
end;
end;
registration
let a be non zero rational number ;
let b be real irrational number ;
clustera * b -> irrational ;
coherence
a * b is irrational by Th22;
clusterb * a -> irrational ;
coherence
b * a is irrational ;
clustera / b -> irrational ;
coherence
a / b is irrational by Th24;
clusterb / a -> irrational ;
coherence
b / a is irrational by Th23;
end;
theorem Th26: :: BORSUK_5:26
for a, b being real number st a < b holds
ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b )
proof
let a, b be real number ; ::_thesis: ( a < b implies ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b ) )
assume a < b ; ::_thesis: ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b )
then consider p1 being rational number such that
A1: a < p1 and
A2: p1 < b by RAT_1:7;
ex p2 being rational number st
( p1 < p2 & p2 < b ) by A2, RAT_1:7;
hence ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b ) by A1; ::_thesis: verum
end;
theorem Th27: :: BORSUK_5:27
for a, b being real number st a < b holds
ex p being real irrational number st
( a < p & p < b )
proof
set x = frac number_e;
let a, b be real number ; ::_thesis: ( a < b implies ex p being real irrational number st
( a < p & p < b ) )
A1: frac number_e < 1 by INT_1:43;
assume a < b ; ::_thesis: ex p being real irrational number st
( a < p & p < b )
then consider p1, p2 being rational number such that
A2: a < p1 and
A3: p1 < p2 and
A4: p2 < b by Th26;
set y = ((1 - (frac number_e)) * p1) + ((frac number_e) * p2);
A5: 0 < frac number_e by INT_1:43;
then ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) < p2 by A3, A1, XREAL_1:178;
then A6: ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) < b by A4, XXREAL_0:2;
((1 - (frac number_e)) * p1) + ((frac number_e) * p2) > p1 by A3, A5, A1, XREAL_1:177;
then A7: ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) > a by A2, XXREAL_0:2;
A8: ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) = p1 + ((frac number_e) * (p2 - p1)) ;
p2 - p1 <> 0 by A3;
hence ex p being real irrational number st
( a < p & p < b ) by A8, A6, A7; ::_thesis: verum
end;
theorem Th28: :: BORSUK_5:28
for A being Subset of R^1 st A = IRRAT holds
Cl A = the carrier of R^1
proof
let A be Subset of R^1; ::_thesis: ( A = IRRAT implies Cl A = the carrier of R^1 )
assume A1: A = IRRAT ; ::_thesis: Cl A = the carrier of R^1
the carrier of R^1 c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R^1 or x in Cl A )
assume x in the carrier of R^1 ; ::_thesis: x in Cl A
then reconsider p = x as Element of RealSpace by METRIC_1:def_13, TOPMETR:17;
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
Ball_(p,r)_meets_A
let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A )
reconsider pr = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
assume r > 0 ; ::_thesis: Ball (p,r) meets A
then consider Q being real irrational number such that
A2: p < Q and
A3: Q < pr by Th27, XREAL_1:29;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
P - p < pr - p by A3, XREAL_1:9;
then dist (p,P) < r by A2, Th14;
then A4: P in Ball (p,r) by METRIC_1:11;
Q in A by A1, Th17;
hence Ball (p,r) meets A by A4, XBOOLE_0:3; ::_thesis: verum
end;
hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
hence Cl A = the carrier of R^1 by XBOOLE_0:def_10; ::_thesis: verum
end;
Lm2: for A being Subset of R^1
for a, b being real number st a < b & A = RAT (a,b) holds
( a in Cl A & b in Cl A )
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = RAT (a,b) holds
( a in Cl A & b in Cl A )
let a, b be real number ; ::_thesis: ( a < b & A = RAT (a,b) implies ( a in Cl A & b in Cl A ) )
assume that
A1: a < b and
A2: A = RAT (a,b) ; ::_thesis: ( a in Cl A & b in Cl A )
thus a in Cl A ::_thesis: b in Cl A
proof
reconsider a9 = a as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
for r being real number st r > 0 holds
Ball (a9,r) meets A
proof
set p = a;
let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A )
reconsider pp = a + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
set pr = min (pp,((a + b) / 2));
A3: min (pp,((a + b) / 2)) <= (a + b) / 2 by XXREAL_0:17;
assume A4: r > 0 ; ::_thesis: Ball (a9,r) meets A
a < min (pp,((a + b) / 2))
proof
percases ( min (pp,((a + b) / 2)) = pp or min (pp,((a + b) / 2)) = (a + b) / 2 ) by XXREAL_0:15;
suppose min (pp,((a + b) / 2)) = pp ; ::_thesis: a < min (pp,((a + b) / 2))
hence a < min (pp,((a + b) / 2)) by A4, XREAL_1:29; ::_thesis: verum
end;
suppose min (pp,((a + b) / 2)) = (a + b) / 2 ; ::_thesis: a < min (pp,((a + b) / 2))
hence a < min (pp,((a + b) / 2)) by A1, XREAL_1:226; ::_thesis: verum
end;
end;
end;
then consider Q being rational number such that
A5: a < Q and
A6: Q < min (pp,((a + b) / 2)) by RAT_1:7;
(a + b) / 2 < b by A1, XREAL_1:226;
then min (pp,((a + b) / 2)) < b by A3, XXREAL_0:2;
then Q < b by A6, XXREAL_0:2;
then A7: Q in ].a,b.[ by A5, XXREAL_1:4;
min (pp,((a + b) / 2)) <= pp by XXREAL_0:17;
then A8: (min (pp,((a + b) / 2))) - a <= pp - a by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
P - a < (min (pp,((a + b) / 2))) - a by A6, XREAL_1:9;
then P - a < r by A8, XXREAL_0:2;
then dist (a9,P) < r by A5, Th14;
then A9: P in Ball (a9,r) by METRIC_1:11;
Q in RAT by RAT_1:def_2;
then Q in A by A2, A7, XBOOLE_0:def_4;
hence Ball (a9,r) meets A by A9, XBOOLE_0:3; ::_thesis: verum
end;
hence a in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
b in Cl A
proof
reconsider a9 = b as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
for r being real number st r > 0 holds
Ball (a9,r) meets A
proof
set p = b;
let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A )
reconsider pp = b - r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
set pr = max (pp,((b + a) / 2));
A10: max (pp,((b + a) / 2)) >= (b + a) / 2 by XXREAL_0:25;
assume r > 0 ; ::_thesis: Ball (a9,r) meets A
then A11: b < b + r by XREAL_1:29;
b > max (pp,((b + a) / 2))
proof
percases ( max (pp,((b + a) / 2)) = pp or max (pp,((b + a) / 2)) = (b + a) / 2 ) by XXREAL_0:16;
suppose max (pp,((b + a) / 2)) = pp ; ::_thesis: b > max (pp,((b + a) / 2))
hence b > max (pp,((b + a) / 2)) by A11, XREAL_1:19; ::_thesis: verum
end;
suppose max (pp,((b + a) / 2)) = (b + a) / 2 ; ::_thesis: b > max (pp,((b + a) / 2))
hence b > max (pp,((b + a) / 2)) by A1, XREAL_1:226; ::_thesis: verum
end;
end;
end;
then consider Q being rational number such that
A12: max (pp,((b + a) / 2)) < Q and
A13: Q < b by RAT_1:7;
(b + a) / 2 > a by A1, XREAL_1:226;
then a < max (pp,((b + a) / 2)) by A10, XXREAL_0:2;
then a < Q by A12, XXREAL_0:2;
then A14: Q in ].a,b.[ by A13, XXREAL_1:4;
max (pp,((b + a) / 2)) >= pp by XXREAL_0:25;
then A15: b - (max (pp,((b + a) / 2))) <= b - pp by XREAL_1:13;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
b - P < b - (max (pp,((b + a) / 2))) by A12, XREAL_1:10;
then b - P < r by A15, XXREAL_0:2;
then dist (a9,P) < r by A13, Th14;
then A16: P in Ball (a9,r) by METRIC_1:11;
Q in RAT by RAT_1:def_2;
then Q in A by A2, A14, XBOOLE_0:def_4;
hence Ball (a9,r) meets A by A16, XBOOLE_0:3; ::_thesis: verum
end;
hence b in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
hence b in Cl A ; ::_thesis: verum
end;
Lm3: for A being Subset of R^1
for a, b being real number st a < b & A = IRRAT (a,b) holds
( a in Cl A & b in Cl A )
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = IRRAT (a,b) holds
( a in Cl A & b in Cl A )
let a, b be real number ; ::_thesis: ( a < b & A = IRRAT (a,b) implies ( a in Cl A & b in Cl A ) )
assume that
A1: a < b and
A2: A = IRRAT (a,b) ; ::_thesis: ( a in Cl A & b in Cl A )
thus a in Cl A ::_thesis: b in Cl A
proof
reconsider a9 = a as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
for r being real number st r > 0 holds
Ball (a9,r) meets A
proof
set p = a;
let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A )
reconsider pp = a + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
set pr = min (pp,((a + b) / 2));
A3: min (pp,((a + b) / 2)) <= (a + b) / 2 by XXREAL_0:17;
assume A4: r > 0 ; ::_thesis: Ball (a9,r) meets A
a < min (pp,((a + b) / 2))
proof
percases ( min (pp,((a + b) / 2)) = pp or min (pp,((a + b) / 2)) = (a + b) / 2 ) by XXREAL_0:15;
suppose min (pp,((a + b) / 2)) = pp ; ::_thesis: a < min (pp,((a + b) / 2))
hence a < min (pp,((a + b) / 2)) by A4, XREAL_1:29; ::_thesis: verum
end;
suppose min (pp,((a + b) / 2)) = (a + b) / 2 ; ::_thesis: a < min (pp,((a + b) / 2))
hence a < min (pp,((a + b) / 2)) by A1, XREAL_1:226; ::_thesis: verum
end;
end;
end;
then consider Q being real irrational number such that
A5: a < Q and
A6: Q < min (pp,((a + b) / 2)) by Th27;
(a + b) / 2 < b by A1, XREAL_1:226;
then min (pp,((a + b) / 2)) < b by A3, XXREAL_0:2;
then Q < b by A6, XXREAL_0:2;
then A7: Q in ].a,b.[ by A5, XXREAL_1:4;
min (pp,((a + b) / 2)) <= pp by XXREAL_0:17;
then A8: (min (pp,((a + b) / 2))) - a <= pp - a by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
P - a < (min (pp,((a + b) / 2))) - a by A6, XREAL_1:9;
then P - a < r by A8, XXREAL_0:2;
then dist (a9,P) < r by A5, Th14;
then A9: P in Ball (a9,r) by METRIC_1:11;
Q in IRRAT by Th17;
then Q in A by A2, A7, XBOOLE_0:def_4;
hence Ball (a9,r) meets A by A9, XBOOLE_0:3; ::_thesis: verum
end;
hence a in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
b in Cl A
proof
reconsider a9 = b as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
for r being real number st r > 0 holds
Ball (a9,r) meets A
proof
set p = b;
let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A )
reconsider pp = b - r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
set pr = max (pp,((b + a) / 2));
A10: max (pp,((b + a) / 2)) >= (b + a) / 2 by XXREAL_0:25;
assume r > 0 ; ::_thesis: Ball (a9,r) meets A
then A11: b < b + r by XREAL_1:29;
b > max (pp,((b + a) / 2))
proof
percases ( max (pp,((b + a) / 2)) = pp or max (pp,((b + a) / 2)) = (b + a) / 2 ) by XXREAL_0:16;
suppose max (pp,((b + a) / 2)) = pp ; ::_thesis: b > max (pp,((b + a) / 2))
hence b > max (pp,((b + a) / 2)) by A11, XREAL_1:19; ::_thesis: verum
end;
suppose max (pp,((b + a) / 2)) = (b + a) / 2 ; ::_thesis: b > max (pp,((b + a) / 2))
hence b > max (pp,((b + a) / 2)) by A1, XREAL_1:226; ::_thesis: verum
end;
end;
end;
then consider Q being real irrational number such that
A12: max (pp,((b + a) / 2)) < Q and
A13: Q < b by Th27;
(b + a) / 2 > a by A1, XREAL_1:226;
then a < max (pp,((b + a) / 2)) by A10, XXREAL_0:2;
then a < Q by A12, XXREAL_0:2;
then A14: Q in ].a,b.[ by A13, XXREAL_1:4;
max (pp,((b + a) / 2)) >= pp by XXREAL_0:25;
then A15: b - (max (pp,((b + a) / 2))) <= b - pp by XREAL_1:13;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
b - P < b - (max (pp,((b + a) / 2))) by A12, XREAL_1:10;
then b - P < r by A15, XXREAL_0:2;
then dist (a9,P) < r by A13, Th14;
then A16: P in Ball (a9,r) by METRIC_1:11;
Q in IRRAT by Th17;
then Q in A by A2, A14, XBOOLE_0:def_4;
hence Ball (a9,r) meets A by A16, XBOOLE_0:3; ::_thesis: verum
end;
hence b in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
hence b in Cl A ; ::_thesis: verum
end;
theorem Th29: :: BORSUK_5:29
for a, b, c being real number holds
( c in RAT (a,b) iff ( c is rational & a < c & c < b ) )
proof
let a, b, c be real number ; ::_thesis: ( c in RAT (a,b) iff ( c is rational & a < c & c < b ) )
hereby ::_thesis: ( c is rational & a < c & c < b implies c in RAT (a,b) )
assume A1: c in RAT (a,b) ; ::_thesis: ( c is rational & a < c & c < b )
then c in ].a,b.[ by XBOOLE_0:def_4;
hence ( c is rational & a < c & c < b ) by A1, XXREAL_1:4; ::_thesis: verum
end;
assume that
A2: c is rational and
A3: a < c and
A4: c < b ; ::_thesis: c in RAT (a,b)
A5: c in RAT by A2, RAT_1:def_2;
c in ].a,b.[ by A3, A4, XXREAL_1:4;
hence c in RAT (a,b) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th30: :: BORSUK_5:30
for a, b, c being real number holds
( c in IRRAT (a,b) iff ( c is irrational & a < c & c < b ) )
proof
let a, b, c be real number ; ::_thesis: ( c in IRRAT (a,b) iff ( c is irrational & a < c & c < b ) )
hereby ::_thesis: ( c is irrational & a < c & c < b implies c in IRRAT (a,b) )
assume A1: c in IRRAT (a,b) ; ::_thesis: ( c is irrational & a < c & c < b )
then A2: c in ].a,b.[ by XBOOLE_0:def_4;
c in IRRAT by A1, XBOOLE_0:def_4;
hence ( c is irrational & a < c & c < b ) by A2, Th17, XXREAL_1:4; ::_thesis: verum
end;
assume that
A3: c is irrational and
A4: a < c and
A5: c < b ; ::_thesis: c in IRRAT (a,b)
A6: c in ].a,b.[ by A4, A5, XXREAL_1:4;
c in IRRAT by A3, Th17;
hence c in IRRAT (a,b) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th31: :: BORSUK_5:31
for A being Subset of R^1
for a, b being real number st a < b & A = RAT (a,b) holds
Cl A = [.a,b.]
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = RAT (a,b) holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( a < b & A = RAT (a,b) implies Cl A = [.a,b.] )
assume that
A1: a < b and
A2: A = RAT (a,b) ; ::_thesis: Cl A = [.a,b.]
reconsider ab = ].a,b.[, RT = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;
reconsider RR = RAT /\ ].a,b.[ as Subset of R^1 by TOPMETR:17;
A3: the carrier of R^1 /\ (Cl ab) = Cl ab by XBOOLE_1:28;
A4: Cl RR c= (Cl RT) /\ (Cl ab) by PRE_TOPC:21;
thus Cl A c= [.a,b.] :: according to XBOOLE_0:def_10 ::_thesis: [.a,b.] c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in [.a,b.] )
assume x in Cl A ; ::_thesis: x in [.a,b.]
then x in (Cl RT) /\ (Cl ab) by A2, A4;
then x in the carrier of R^1 /\ (Cl ab) by Th15;
hence x in [.a,b.] by A1, A3, Th16; ::_thesis: verum
end;
thus [.a,b.] c= Cl A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.] or x in Cl A )
assume A5: x in [.a,b.] ; ::_thesis: x in Cl A
then reconsider p = x as Element of RealSpace by METRIC_1:def_13;
A6: a <= p by A5, XXREAL_1:1;
A7: p <= b by A5, XXREAL_1:1;
percases ( p < b or p = b ) by A7, XXREAL_0:1;
supposeA8: p < b ; ::_thesis: x in Cl A
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
Ball_(p,r)_meets_A
let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A )
reconsider pp = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
set pr = min (pp,((p + b) / 2));
A9: min (pp,((p + b) / 2)) <= (p + b) / 2 by XXREAL_0:17;
assume A10: r > 0 ; ::_thesis: Ball (p,r) meets A
p < min (pp,((p + b) / 2))
proof
percases ( min (pp,((p + b) / 2)) = pp or min (pp,((p + b) / 2)) = (p + b) / 2 ) by XXREAL_0:15;
suppose min (pp,((p + b) / 2)) = pp ; ::_thesis: p < min (pp,((p + b) / 2))
hence p < min (pp,((p + b) / 2)) by A10, XREAL_1:29; ::_thesis: verum
end;
suppose min (pp,((p + b) / 2)) = (p + b) / 2 ; ::_thesis: p < min (pp,((p + b) / 2))
hence p < min (pp,((p + b) / 2)) by A8, XREAL_1:226; ::_thesis: verum
end;
end;
end;
then consider Q being rational number such that
A11: p < Q and
A12: Q < min (pp,((p + b) / 2)) by RAT_1:7;
(p + b) / 2 < b by A8, XREAL_1:226;
then min (pp,((p + b) / 2)) < b by A9, XXREAL_0:2;
then A13: Q < b by A12, XXREAL_0:2;
min (pp,((p + b) / 2)) <= pp by XXREAL_0:17;
then A14: (min (pp,((p + b) / 2))) - p <= pp - p by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
P - p < (min (pp,((p + b) / 2))) - p by A12, XREAL_1:9;
then P - p < r by A14, XXREAL_0:2;
then dist (p,P) < r by A11, Th14;
then A15: P in Ball (p,r) by METRIC_1:11;
a < Q by A6, A11, XXREAL_0:2;
then A16: Q in ].a,b.[ by A13, XXREAL_1:4;
Q in RAT by RAT_1:def_2;
then Q in A by A2, A16, XBOOLE_0:def_4;
hence Ball (p,r) meets A by A15, XBOOLE_0:3; ::_thesis: verum
end;
hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
suppose p = b ; ::_thesis: x in Cl A
hence x in Cl A by A1, A2, Lm2; ::_thesis: verum
end;
end;
end;
end;
theorem Th32: :: BORSUK_5:32
for A being Subset of R^1
for a, b being real number st a < b & A = IRRAT (a,b) holds
Cl A = [.a,b.]
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = IRRAT (a,b) holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( a < b & A = IRRAT (a,b) implies Cl A = [.a,b.] )
assume that
A1: a < b and
A2: A = IRRAT (a,b) ; ::_thesis: Cl A = [.a,b.]
reconsider ab = ].a,b.[, RT = IRRAT as Subset of R^1 by TOPMETR:17;
reconsider RR = IRRAT /\ ].a,b.[ as Subset of R^1 by TOPMETR:17;
A3: the carrier of R^1 /\ (Cl ab) = Cl ab by XBOOLE_1:28;
A4: Cl RR c= (Cl RT) /\ (Cl ab) by PRE_TOPC:21;
thus Cl A c= [.a,b.] :: according to XBOOLE_0:def_10 ::_thesis: [.a,b.] c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in [.a,b.] )
assume x in Cl A ; ::_thesis: x in [.a,b.]
then x in (Cl RT) /\ (Cl ab) by A2, A4;
then x in the carrier of R^1 /\ (Cl ab) by Th28;
hence x in [.a,b.] by A1, A3, Th16; ::_thesis: verum
end;
thus [.a,b.] c= Cl A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.] or x in Cl A )
assume A5: x in [.a,b.] ; ::_thesis: x in Cl A
then reconsider p = x as Element of RealSpace by METRIC_1:def_13;
A6: a <= p by A5, XXREAL_1:1;
A7: p <= b by A5, XXREAL_1:1;
percases ( p < b or p = b ) by A7, XXREAL_0:1;
supposeA8: p < b ; ::_thesis: x in Cl A
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
Ball_(p,r)_meets_A
let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A )
reconsider pp = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
set pr = min (pp,((p + b) / 2));
A9: min (pp,((p + b) / 2)) <= (p + b) / 2 by XXREAL_0:17;
assume A10: r > 0 ; ::_thesis: Ball (p,r) meets A
p < min (pp,((p + b) / 2))
proof
percases ( min (pp,((p + b) / 2)) = pp or min (pp,((p + b) / 2)) = (p + b) / 2 ) by XXREAL_0:15;
suppose min (pp,((p + b) / 2)) = pp ; ::_thesis: p < min (pp,((p + b) / 2))
hence p < min (pp,((p + b) / 2)) by A10, XREAL_1:29; ::_thesis: verum
end;
suppose min (pp,((p + b) / 2)) = (p + b) / 2 ; ::_thesis: p < min (pp,((p + b) / 2))
hence p < min (pp,((p + b) / 2)) by A8, XREAL_1:226; ::_thesis: verum
end;
end;
end;
then consider Q being real irrational number such that
A11: p < Q and
A12: Q < min (pp,((p + b) / 2)) by Th27;
(p + b) / 2 < b by A8, XREAL_1:226;
then min (pp,((p + b) / 2)) < b by A9, XXREAL_0:2;
then A13: Q < b by A12, XXREAL_0:2;
min (pp,((p + b) / 2)) <= pp by XXREAL_0:17;
then A14: (min (pp,((p + b) / 2))) - p <= pp - p by XREAL_1:9;
reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1;
P - p < (min (pp,((p + b) / 2))) - p by A12, XREAL_1:9;
then P - p < r by A14, XXREAL_0:2;
then dist (p,P) < r by A11, Th14;
then A15: P in Ball (p,r) by METRIC_1:11;
a < Q by A6, A11, XXREAL_0:2;
then A16: Q in ].a,b.[ by A13, XXREAL_1:4;
Q in IRRAT by Th17;
then Q in A by A2, A16, XBOOLE_0:def_4;
hence Ball (p,r) meets A by A15, XBOOLE_0:3; ::_thesis: verum
end;
hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum
end;
suppose p = b ; ::_thesis: x in Cl A
hence x in Cl A by A1, A2, Lm3; ::_thesis: verum
end;
end;
end;
end;
theorem Th33: :: BORSUK_5:33
for T being connected TopSpace
for A being open closed Subset of T holds
( A = {} or A = [#] T )
proof
let T be connected TopSpace; ::_thesis: for A being open closed Subset of T holds
( A = {} or A = [#] T )
let A be open closed Subset of T; ::_thesis: ( A = {} or A = [#] T )
assume that
A1: A <> {} and
A2: A <> [#] T ; ::_thesis: contradiction
A3: A ` <> {} by A2, PRE_TOPC:4;
A misses A ` by SUBSET_1:24;
then A4: A,A ` are_separated by CONNSP_1:2;
A5: [#] T = A \/ (A `) by PRE_TOPC:2;
A <> {} T by A1;
then not [#] T is connected by A5, A4, A3, CONNSP_1:15;
hence contradiction by CONNSP_1:27; ::_thesis: verum
end;
theorem Th34: :: BORSUK_5:34
for A being Subset of R^1 st A is closed & A is open & not A = {} holds
A = REAL
proof
let A be Subset of R^1; ::_thesis: ( A is closed & A is open & not A = {} implies A = REAL )
assume ( A is closed & A is open ) ; ::_thesis: ( A = {} or A = REAL )
then reconsider A = A as open closed Subset of R^1 ;
( A = {} or A = [#] R^1 ) by Th33;
hence ( A = {} or A = REAL ) by TOPMETR:17; ::_thesis: verum
end;
begin
theorem Th35: :: BORSUK_5:35
for A being Subset of R^1
for a, b being real number st A = [.a,b.[ & a <> b holds
Cl A = [.a,b.]
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st A = [.a,b.[ & a <> b holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( A = [.a,b.[ & a <> b implies Cl A = [.a,b.] )
assume that
A1: A = [.a,b.[ and
A2: a <> b ; ::_thesis: Cl A = [.a,b.]
Cl [.a,b.[ = [.a,b.] by A2, BORSUK_4:12;
hence Cl A = [.a,b.] by A1, JORDAN5A:24; ::_thesis: verum
end;
theorem Th36: :: BORSUK_5:36
for A being Subset of R^1
for a, b being real number st A = ].a,b.] & a <> b holds
Cl A = [.a,b.]
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st A = ].a,b.] & a <> b holds
Cl A = [.a,b.]
let a, b be real number ; ::_thesis: ( A = ].a,b.] & a <> b implies Cl A = [.a,b.] )
assume that
A1: A = ].a,b.] and
A2: a <> b ; ::_thesis: Cl A = [.a,b.]
Cl ].a,b.] = [.a,b.] by A2, BORSUK_4:11;
hence Cl A = [.a,b.] by A1, JORDAN5A:24; ::_thesis: verum
end;
theorem :: BORSUK_5:37
for A being Subset of R^1
for a, b, c being real number st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds
Cl A = [.a,c.]
proof
let A be Subset of R^1; ::_thesis: for a, b, c being real number st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds
Cl A = [.a,c.]
let a, b, c be real number ; ::_thesis: ( A = [.a,b.[ \/ ].b,c.] & a < b & b < c implies Cl A = [.a,c.] )
assume that
A1: A = [.a,b.[ \/ ].b,c.] and
A2: a < b and
A3: b < c ; ::_thesis: Cl A = [.a,c.]
reconsider B = [.a,b.[, C = ].b,c.] as Subset of R^1 by TOPMETR:17;
Cl A = (Cl B) \/ (Cl C) by A1, PRE_TOPC:20
.= [.a,b.] \/ (Cl C) by A2, Th35
.= [.a,b.] \/ [.b,c.] by A3, Th36
.= [.a,c.] by A2, A3, XXREAL_1:174 ;
hence Cl A = [.a,c.] ; ::_thesis: verum
end;
theorem Th38: :: BORSUK_5:38
for A being Subset of R^1
for a being real number st A = {a} holds
Cl A = {a}
proof
let A be Subset of R^1; ::_thesis: for a being real number st A = {a} holds
Cl A = {a}
let a be real number ; ::_thesis: ( A = {a} implies Cl A = {a} )
A1: a is Point of R^1 by TOPMETR:17, XREAL_0:def_1;
assume A = {a} ; ::_thesis: Cl A = {a}
hence Cl A = {a} by A1, YELLOW_8:26; ::_thesis: verum
end;
theorem Th39: :: BORSUK_5:39
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is open iff B is open )
proof
let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds
( A is open iff B is open )
let B be Subset of R^1; ::_thesis: ( A = B implies ( A is open iff B is open ) )
assume A1: A = B ; ::_thesis: ( A is open iff B is open )
hereby ::_thesis: ( B is open implies A is open )
assume A is open ; ::_thesis: B is open
then A in Family_open_set RealSpace by JORDAN5A:5;
then A in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12;
hence B is open by A1, PRE_TOPC:def_2, TOPMETR:def_6; ::_thesis: verum
end;
assume B is open ; ::_thesis: A is open
then B in the topology of R^1 by PRE_TOPC:def_2;
then A in Family_open_set RealSpace by A1, TOPMETR:12, TOPMETR:def_6;
hence A is open by JORDAN5A:5; ::_thesis: verum
end;
Lm4: for a being real number holds ].-infty,a.] is closed
proof
let a be real number ; ::_thesis: ].-infty,a.] is closed
].-infty,a.] = left_closed_halfline a ;
hence ].-infty,a.] is closed ; ::_thesis: verum
end;
Lm5: for a being real number holds [.a,+infty.[ is closed
proof
let a be real number ; ::_thesis: [.a,+infty.[ is closed
[.a,+infty.[ = right_closed_halfline a ;
hence [.a,+infty.[ is closed ; ::_thesis: verum
end;
registration
let A, B be open Subset of REAL;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17;
clusterA /\ B -> open for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = A /\ B holds
b1 is open
proof
A1: B1 is open by Th39;
A1 is open by Th39;
then A1 /\ B1 is open by A1;
hence for b1 being Subset of REAL st b1 = A /\ B holds
b1 is open by Th39; ::_thesis: verum
end;
clusterA \/ B -> open for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = A \/ B holds
b1 is open
proof
A2: B1 is open by Th39;
A1 is open by Th39;
then A1 \/ B1 is open by A2;
hence for b1 being Subset of REAL st b1 = A \/ B holds
b1 is open by Th39; ::_thesis: verum
end;
end;
Lm6: for a, b being ext-real number holds ].a,b.[ is open
proof
let a, b be ext-real number ; ::_thesis: ].a,b.[ is open
set A = ].a,b.[;
percases ( ( a in REAL & b in REAL ) or a = +infty or ( a = -infty & b in REAL ) or ( a in REAL & b = +infty ) or b = -infty or ( a = -infty & b = +infty ) ) by XXREAL_0:14;
suppose ( a in REAL & b in REAL ) ; ::_thesis: ].a,b.[ is open
then reconsider a = a, b = b as real number ;
].a,b.[ = ].-infty,b.[ /\ ].a,+infty.[ by XXREAL_1:269;
hence ].a,b.[ is open ; ::_thesis: verum
end;
suppose a = +infty ; ::_thesis: ].a,b.[ is open
then ].a,b.[ = {} by XXREAL_1:214;
hence ].a,b.[ is open ; ::_thesis: verum
end;
supposethat A1: a = -infty and
A2: b in REAL ; ::_thesis: ].a,b.[ is open
reconsider b = b as real number by A2;
].a,b.[ = left_open_halfline b by A1;
hence ].a,b.[ is open ; ::_thesis: verum
end;
supposethat A3: a in REAL and
A4: b = +infty ; ::_thesis: ].a,b.[ is open
reconsider a = a as real number by A3;
].a,b.[ = right_open_halfline a by A4;
hence ].a,b.[ is open ; ::_thesis: verum
end;
suppose b = -infty ; ::_thesis: ].a,b.[ is open
then ].a,b.[ = {} by XXREAL_1:210;
hence ].a,b.[ is open ; ::_thesis: verum
end;
suppose ( a = -infty & b = +infty ) ; ::_thesis: ].a,b.[ is open
then ].a,b.[ = [#] REAL by XXREAL_1:224;
hence ].a,b.[ is open ; ::_thesis: verum
end;
end;
end;
theorem Th40: :: BORSUK_5:40
for A being Subset of R^1
for a, b being ext-real number st A = ].a,b.[ holds
A is open
proof
let A be Subset of R^1; ::_thesis: for a, b being ext-real number st A = ].a,b.[ holds
A is open
let a, b be ext-real number ; ::_thesis: ( A = ].a,b.[ implies A is open )
].a,b.[ is open by Lm6;
hence ( A = ].a,b.[ implies A is open ) by Th39; ::_thesis: verum
end;
theorem Th41: :: BORSUK_5:41
for A being Subset of R^1
for a being real number st A = ].-infty,a.] holds
A is closed
proof
let A be Subset of R^1; ::_thesis: for a being real number st A = ].-infty,a.] holds
A is closed
let a be real number ; ::_thesis: ( A = ].-infty,a.] implies A is closed )
assume A1: A = ].-infty,a.] ; ::_thesis: A is closed
].-infty,a.] is closed by Lm4;
hence A is closed by A1, JORDAN5A:23; ::_thesis: verum
end;
theorem Th42: :: BORSUK_5:42
for A being Subset of R^1
for a being real number st A = [.a,+infty.[ holds
A is closed
proof
let A be Subset of R^1; ::_thesis: for a being real number st A = [.a,+infty.[ holds
A is closed
let a be real number ; ::_thesis: ( A = [.a,+infty.[ implies A is closed )
assume A1: A = [.a,+infty.[ ; ::_thesis: A is closed
[.a,+infty.[ is closed by Lm5;
hence A is closed by A1, JORDAN5A:23; ::_thesis: verum
end;
theorem Th43: :: BORSUK_5:43
for a being real number holds [.a,+infty.[ = {a} \/ ].a,+infty.[
proof
let a be real number ; ::_thesis: [.a,+infty.[ = {a} \/ ].a,+infty.[
thus [.a,+infty.[ c= {a} \/ ].a,+infty.[ :: according to XBOOLE_0:def_10 ::_thesis: {a} \/ ].a,+infty.[ c= [.a,+infty.[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,+infty.[ or x in {a} \/ ].a,+infty.[ )
assume A1: x in [.a,+infty.[ ; ::_thesis: x in {a} \/ ].a,+infty.[
then reconsider x = x as real number ;
A2: x >= a by A1, XXREAL_1:236;
percases ( x = a or x > a ) by A2, XXREAL_0:1;
suppose x = a ; ::_thesis: x in {a} \/ ].a,+infty.[
then x in {a} by TARSKI:def_1;
hence x in {a} \/ ].a,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x > a ; ::_thesis: x in {a} \/ ].a,+infty.[
then x in ].a,+infty.[ by XXREAL_1:235;
hence x in {a} \/ ].a,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} \/ ].a,+infty.[ or x in [.a,+infty.[ )
assume A3: x in {a} \/ ].a,+infty.[ ; ::_thesis: x in [.a,+infty.[
then reconsider x = x as real number ;
( x in {a} or x in ].a,+infty.[ ) by A3, XBOOLE_0:def_3;
then ( x = a or x > a ) by TARSKI:def_1, XXREAL_1:235;
hence x in [.a,+infty.[ by XXREAL_1:236; ::_thesis: verum
end;
theorem Th44: :: BORSUK_5:44
for a being real number holds ].-infty,a.] = {a} \/ ].-infty,a.[
proof
let a be real number ; ::_thesis: ].-infty,a.] = {a} \/ ].-infty,a.[
thus ].-infty,a.] c= {a} \/ ].-infty,a.[ :: according to XBOOLE_0:def_10 ::_thesis: {a} \/ ].-infty,a.[ c= ].-infty,a.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,a.] or x in {a} \/ ].-infty,a.[ )
assume A1: x in ].-infty,a.] ; ::_thesis: x in {a} \/ ].-infty,a.[
then reconsider x = x as real number ;
A2: x <= a by A1, XXREAL_1:234;
percases ( x = a or x < a ) by A2, XXREAL_0:1;
suppose x = a ; ::_thesis: x in {a} \/ ].-infty,a.[
then x in {a} by TARSKI:def_1;
hence x in {a} \/ ].-infty,a.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x < a ; ::_thesis: x in {a} \/ ].-infty,a.[
then x in ].-infty,a.[ by XXREAL_1:233;
hence x in {a} \/ ].-infty,a.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} \/ ].-infty,a.[ or x in ].-infty,a.] )
assume A3: x in {a} \/ ].-infty,a.[ ; ::_thesis: x in ].-infty,a.]
then reconsider x = x as real number ;
( x in {a} or x in ].-infty,a.[ ) by A3, XBOOLE_0:def_3;
then ( x = a or x < a ) by TARSKI:def_1, XXREAL_1:233;
hence x in ].-infty,a.] by XXREAL_1:234; ::_thesis: verum
end;
registration
let a be real number ;
clusterK451(a,+infty) -> non empty ;
coherence
not ].a,+infty.[ is empty
proof
a < a + 1 by XREAL_1:29;
hence not ].a,+infty.[ is empty by XXREAL_1:235; ::_thesis: verum
end;
clusterK450(-infty,a) -> non empty ;
coherence
not ].-infty,a.] is empty by XXREAL_1:234;
clusterK451(-infty,a) -> non empty ;
coherence
not ].-infty,a.[ is empty
proof
a - 1 < a by XREAL_1:146;
hence not ].-infty,a.[ is empty by XXREAL_1:233; ::_thesis: verum
end;
clusterK449(a,+infty) -> non empty ;
coherence
not [.a,+infty.[ is empty by XXREAL_1:236;
end;
theorem Th45: :: BORSUK_5:45
for a being real number holds ].a,+infty.[ <> REAL
proof
let a be real number ; ::_thesis: ].a,+infty.[ <> REAL
a in REAL by XREAL_0:def_1;
hence ].a,+infty.[ <> REAL by XXREAL_1:235; ::_thesis: verum
end;
theorem :: BORSUK_5:46
for a being real number holds [.a,+infty.[ <> REAL
proof
let a be real number ; ::_thesis: [.a,+infty.[ <> REAL
A1: a - 1 < a by XREAL_1:146;
a - 1 in REAL by XREAL_0:def_1;
hence [.a,+infty.[ <> REAL by A1, XXREAL_1:236; ::_thesis: verum
end;
theorem :: BORSUK_5:47
for a being real number holds ].-infty,a.] <> REAL
proof
let a be real number ; ::_thesis: ].-infty,a.] <> REAL
A1: a + 1 > a by XREAL_1:29;
a + 1 in REAL by XREAL_0:def_1;
hence ].-infty,a.] <> REAL by A1, XXREAL_1:234; ::_thesis: verum
end;
theorem Th48: :: BORSUK_5:48
for a being real number holds ].-infty,a.[ <> REAL
proof
let a be real number ; ::_thesis: ].-infty,a.[ <> REAL
A1: a + 1 > a by XREAL_1:29;
a + 1 in REAL by XREAL_0:def_1;
hence ].-infty,a.[ <> REAL by A1, XXREAL_1:233; ::_thesis: verum
end;
theorem Th49: :: BORSUK_5:49
for A being Subset of R^1
for a being real number st A = ].a,+infty.[ holds
Cl A = [.a,+infty.[
proof
let A be Subset of R^1; ::_thesis: for a being real number st A = ].a,+infty.[ holds
Cl A = [.a,+infty.[
let a be real number ; ::_thesis: ( A = ].a,+infty.[ implies Cl A = [.a,+infty.[ )
reconsider A9 = A as Subset of R^1 ;
reconsider C = [.a,+infty.[ as Subset of R^1 by TOPMETR:17;
assume A1: A = ].a,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[
then A2: A9 is open by Th40;
C is closed by Th42;
then A3: Cl A9 c= C by A1, TOPS_1:5, XXREAL_1:45;
A4: C = A9 \/ {a} by A1, Th43;
percases ( Cl A9 = C or Cl A9 = A9 ) by A4, A3, ZFMISC_1:138, PRE_TOPC:18;
suppose Cl A9 = C ; ::_thesis: Cl A = [.a,+infty.[
hence Cl A = [.a,+infty.[ ; ::_thesis: verum
end;
suppose Cl A9 = A9 ; ::_thesis: Cl A = [.a,+infty.[
hence Cl A = [.a,+infty.[ by A1, A2, Th34, Th45; ::_thesis: verum
end;
end;
end;
theorem :: BORSUK_5:50
for a being real number holds Cl ].a,+infty.[ = [.a,+infty.[
proof
let a be real number ; ::_thesis: Cl ].a,+infty.[ = [.a,+infty.[
reconsider A = ].a,+infty.[ as Subset of R^1 by TOPMETR:17;
Cl A = [.a,+infty.[ by Th49;
hence Cl ].a,+infty.[ = [.a,+infty.[ by JORDAN5A:24; ::_thesis: verum
end;
theorem Th51: :: BORSUK_5:51
for A being Subset of R^1
for a being real number st A = ].-infty,a.[ holds
Cl A = ].-infty,a.]
proof
let A be Subset of R^1; ::_thesis: for a being real number st A = ].-infty,a.[ holds
Cl A = ].-infty,a.]
let a be real number ; ::_thesis: ( A = ].-infty,a.[ implies Cl A = ].-infty,a.] )
reconsider A9 = A as Subset of R^1 ;
reconsider C = ].-infty,a.] as Subset of R^1 by TOPMETR:17;
assume A1: A = ].-infty,a.[ ; ::_thesis: Cl A = ].-infty,a.]
then A2: A9 is open by Th40;
C is closed by Th41;
then A3: Cl A9 c= C by A1, TOPS_1:5, XXREAL_1:41;
A4: C = A9 \/ {a} by A1, Th44;
percases ( Cl A9 = C or Cl A9 = A9 ) by A4, A3, ZFMISC_1:138, PRE_TOPC:18;
suppose Cl A9 = C ; ::_thesis: Cl A = ].-infty,a.]
hence Cl A = ].-infty,a.] ; ::_thesis: verum
end;
suppose Cl A9 = A9 ; ::_thesis: Cl A = ].-infty,a.]
hence Cl A = ].-infty,a.] by A1, A2, Th34, Th48; ::_thesis: verum
end;
end;
end;
theorem :: BORSUK_5:52
for a being real number holds Cl ].-infty,a.[ = ].-infty,a.]
proof
let a be real number ; ::_thesis: Cl ].-infty,a.[ = ].-infty,a.]
reconsider A = ].-infty,a.[ as Subset of R^1 by TOPMETR:17;
Cl A = ].-infty,a.] by Th51;
hence Cl ].-infty,a.[ = ].-infty,a.] by JORDAN5A:24; ::_thesis: verum
end;
theorem Th53: :: BORSUK_5:53
for A, B being Subset of R^1
for b being real number st A = ].-infty,b.[ & B = ].b,+infty.[ holds
A,B are_separated
proof
let A, B be Subset of R^1; ::_thesis: for b being real number st A = ].-infty,b.[ & B = ].b,+infty.[ holds
A,B are_separated
let b be real number ; ::_thesis: ( A = ].-infty,b.[ & B = ].b,+infty.[ implies A,B are_separated )
assume that
A1: A = ].-infty,b.[ and
A2: B = ].b,+infty.[ ; ::_thesis: A,B are_separated
Cl B = [.b,+infty.[ by A2, Th49;
then A3: Cl B misses A by A1, XXREAL_1:94;
Cl A = ].-infty,b.] by A1, Th51;
then Cl A misses B by A2, XXREAL_1:91;
hence A,B are_separated by A3, CONNSP_1:def_1; ::_thesis: verum
end;
theorem :: BORSUK_5:54
for A being Subset of R^1
for a, b being real number st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[
let a, b be real number ; ::_thesis: ( a < b & A = [.a,b.[ \/ ].b,+infty.[ implies Cl A = [.a,+infty.[ )
assume that
A1: a < b and
A2: A = [.a,b.[ \/ ].b,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[
reconsider B = [.a,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17;
A3: Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20;
A4: Cl C = [.b,+infty.[ by Th49;
Cl B = [.a,b.] by A1, Th35;
hence Cl A = [.a,+infty.[ by A1, A4, A3, Th11; ::_thesis: verum
end;
theorem Th55: :: BORSUK_5:55
for A being Subset of R^1
for a, b being real number st a < b & A = ].a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = ].a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[
let a, b be real number ; ::_thesis: ( a < b & A = ].a,b.[ \/ ].b,+infty.[ implies Cl A = [.a,+infty.[ )
assume that
A1: a < b and
A2: A = ].a,b.[ \/ ].b,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[
reconsider B = ].a,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17;
A3: Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20;
A4: Cl C = [.b,+infty.[ by Th49;
Cl B = [.a,b.] by A1, Th16;
hence Cl A = [.a,+infty.[ by A1, A3, A4, Th11; ::_thesis: verum
end;
theorem :: BORSUK_5:56
for A being Subset of R^1
for a, b, c being real number st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds
Cl A = [.a,+infty.[
proof
let A be Subset of R^1; ::_thesis: for a, b, c being real number st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds
Cl A = [.a,+infty.[
let a, b, c be real number ; ::_thesis: ( a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ implies Cl A = [.a,+infty.[ )
assume that
A1: a < b and
A2: b < c ; ::_thesis: ( not A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ or Cl A = [.a,+infty.[ )
reconsider B = RAT (a,b) as Subset of R^1 by TOPMETR:17;
reconsider C = ].b,c.[ \/ ].c,+infty.[ as Subset of R^1 by TOPMETR:17;
assume A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[
then A = (RAT (a,b)) \/ C by XBOOLE_1:4;
then Cl A = (Cl B) \/ (Cl C) by PRE_TOPC:20;
then Cl A = (Cl B) \/ [.b,+infty.[ by A2, Th55;
then Cl A = [.a,b.] \/ [.b,+infty.[ by A1, Th31;
hence Cl A = [.a,+infty.[ by A1, Th11; ::_thesis: verum
end;
theorem Th57: :: BORSUK_5:57
for a, b being real number holds IRRAT (a,b) misses RAT (a,b)
proof
let a, b be real number ; ::_thesis: IRRAT (a,b) misses RAT (a,b)
assume IRRAT (a,b) meets RAT (a,b) ; ::_thesis: contradiction
then consider x being set such that
A1: x in IRRAT (a,b) and
A2: x in RAT (a,b) by XBOOLE_0:3;
thus contradiction by A1, A2, Th30; ::_thesis: verum
end;
theorem Th58: :: BORSUK_5:58
for a, b being real number holds REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
proof
let a, b be real number ; ::_thesis: REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
thus REAL \ (RAT (a,b)) c= (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ :: according to XBOOLE_0:def_10 ::_thesis: (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ c= REAL \ (RAT (a,b))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL \ (RAT (a,b)) or x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ )
assume A1: x in REAL \ (RAT (a,b)) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
then A2: not x in RAT (a,b) by XBOOLE_0:def_5;
reconsider x = x as real number by A1;
percases ( ( x <= a & x < b ) or ( x <= a & x >= b ) or ( x > a & x < b ) or ( x > a & x >= b ) ) ;
suppose ( x <= a & x < b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
then x in ].-infty,a.] by XXREAL_1:234;
then x in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3;
hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x <= a & x >= b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
then x in ].-infty,a.] by XXREAL_1:234;
then x in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3;
hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA3: ( x > a & x < b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
x in IRRAT (a,b)
proof
percases ( x is rational or x is irrational ) ;
suppose x is rational ; ::_thesis: x in IRRAT (a,b)
hence x in IRRAT (a,b) by A2, A3, Th29; ::_thesis: verum
end;
suppose x is irrational ; ::_thesis: x in IRRAT (a,b)
hence x in IRRAT (a,b) by A3, Th30; ::_thesis: verum
end;
end;
end;
then x in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3;
hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose ( x > a & x >= b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
then x in [.b,+infty.[ by XXREAL_1:236;
hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ or x in REAL \ (RAT (a,b)) )
assume A4: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ ; ::_thesis: x in REAL \ (RAT (a,b))
then reconsider x = x as real number ;
A5: ( x in ].-infty,a.] \/ (IRRAT (a,b)) or x in [.b,+infty.[ ) by A4, XBOOLE_0:def_3;
percases ( x in ].-infty,a.] or x in IRRAT (a,b) or x in [.b,+infty.[ ) by A5, XBOOLE_0:def_3;
suppose x in ].-infty,a.] ; ::_thesis: x in REAL \ (RAT (a,b))
then x <= a by XXREAL_1:234;
then A6: not x in RAT (a,b) by Th29;
x in REAL by XREAL_0:def_1;
hence x in REAL \ (RAT (a,b)) by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA7: x in IRRAT (a,b) ; ::_thesis: x in REAL \ (RAT (a,b))
IRRAT (a,b) misses RAT (a,b) by Th57;
then A8: not x in RAT (a,b) by A7, XBOOLE_0:3;
x in REAL by XREAL_0:def_1;
hence x in REAL \ (RAT (a,b)) by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose x in [.b,+infty.[ ; ::_thesis: x in REAL \ (RAT (a,b))
then x >= b by XXREAL_1:236;
then A9: not x in RAT (a,b) by Th29;
x in REAL by XREAL_0:def_1;
hence x in REAL \ (RAT (a,b)) by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
theorem Th59: :: BORSUK_5:59
for a, b being real number st a < b holds
[.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b}
proof
let a, b be real number ; ::_thesis: ( a < b implies [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b} )
A1: not b in ].a,b.[ \/ ].b,+infty.[ by XXREAL_1:205;
assume A2: a < b ; ::_thesis: [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b}
then A3: not a in ].a,b.[ \/ ].b,+infty.[ by XXREAL_1:223;
[.a,+infty.[ = [.a,b.] \/ [.b,+infty.[ by A2, Th11
.= ({a,b} \/ ].a,b.[) \/ [.b,+infty.[ by A2, XXREAL_1:128
.= ({a,b} \/ ].a,b.[) \/ ({b} \/ ].b,+infty.[) by Th43
.= (({a,b} \/ ].a,b.[) \/ {b}) \/ ].b,+infty.[ by XBOOLE_1:4
.= (({a,b} \/ {b}) \/ ].a,b.[) \/ ].b,+infty.[ by XBOOLE_1:4
.= ({a,b} \/ ].a,b.[) \/ ].b,+infty.[ by ZFMISC_1:9
.= {a,b} \/ (].a,b.[ \/ ].b,+infty.[) by XBOOLE_1:4 ;
then [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a,b} by A3, A1, XBOOLE_1:88, ZFMISC_1:51;
hence [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b} by ENUMSET1:1; ::_thesis: verum
end;
theorem :: BORSUK_5:60
for A being Subset of R^1 st A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ holds
A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}
proof
A1: ].-infty,2.] \/ (IRRAT (2,4)) c= ].-infty,4.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,2.] \/ (IRRAT (2,4)) or x in ].-infty,4.] )
assume A2: x in ].-infty,2.] \/ (IRRAT (2,4)) ; ::_thesis: x in ].-infty,4.]
then reconsider x = x as real number ;
percases ( x in ].-infty,2.] or x in IRRAT (2,4) ) by A2, XBOOLE_0:def_3;
suppose x in ].-infty,2.] ; ::_thesis: x in ].-infty,4.]
then x <= 2 by XXREAL_1:234;
then x <= 4 by XXREAL_0:2;
hence x in ].-infty,4.] by XXREAL_1:234; ::_thesis: verum
end;
suppose x in IRRAT (2,4) ; ::_thesis: x in ].-infty,4.]
then x < 4 by Th30;
hence x in ].-infty,4.] by XXREAL_1:234; ::_thesis: verum
end;
end;
end;
let A be Subset of R^1; ::_thesis: ( A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ implies A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} )
A3: ].4,5.[ \/ ].5,+infty.[ c= ].4,+infty.[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].4,5.[ \/ ].5,+infty.[ or x in ].4,+infty.[ )
assume A4: x in ].4,5.[ \/ ].5,+infty.[ ; ::_thesis: x in ].4,+infty.[
then reconsider x = x as real number ;
percases ( x in ].4,5.[ or x in ].5,+infty.[ ) by A4, XBOOLE_0:def_3;
suppose x in ].4,5.[ ; ::_thesis: x in ].4,+infty.[
then x > 4 by XXREAL_1:4;
hence x in ].4,+infty.[ by XXREAL_1:235; ::_thesis: verum
end;
suppose x in ].5,+infty.[ ; ::_thesis: x in ].4,+infty.[
then x > 5 by XXREAL_1:235;
then x > 4 by XXREAL_0:2;
hence x in ].4,+infty.[ by XXREAL_1:235; ::_thesis: verum
end;
end;
end;
assume A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ ; ::_thesis: A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}
then A5: A ` = REAL \ ((RAT (2,4)) \/ (].4,5.[ \/ ].5,+infty.[)) by TOPMETR:17, XBOOLE_1:4
.= (REAL \ (RAT (2,4))) \ (].4,5.[ \/ ].5,+infty.[) by XBOOLE_1:41
.= ((].-infty,2.] \/ (IRRAT (2,4))) \/ [.4,+infty.[) \ (].4,5.[ \/ ].5,+infty.[) by Th58 ;
].-infty,4.] misses ].4,+infty.[ by XXREAL_1:91;
then A ` = ([.4,+infty.[ \ (].4,5.[ \/ ].5,+infty.[)) \/ (].-infty,2.] \/ (IRRAT (2,4))) by A5, A1, A3, XBOOLE_1:64, XBOOLE_1:87
.= (].-infty,2.] \/ (IRRAT (2,4))) \/ ({4} \/ {5}) by Th59
.= ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:4 ;
hence A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} ; ::_thesis: verum
end;
theorem :: BORSUK_5:61
for A being Subset of R^1
for a being real number st A = {a} holds
A ` = ].-infty,a.[ \/ ].a,+infty.[ by TOPMETR:17, XXREAL_1:389;
Lm7: ((IRRAT (2,4)) \/ {4}) \/ {5} c= ].1,+infty.[
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((IRRAT (2,4)) \/ {4}) \/ {5} or x in ].1,+infty.[ )
assume A1: x in ((IRRAT (2,4)) \/ {4}) \/ {5} ; ::_thesis: x in ].1,+infty.[
then reconsider x = x as real number ;
A2: ( x in (IRRAT (2,4)) \/ {4} or x in {5} ) by A1, XBOOLE_0:def_3;
percases ( x in IRRAT (2,4) or x in {4} or x in {5} ) by A2, XBOOLE_0:def_3;
suppose x in IRRAT (2,4) ; ::_thesis: x in ].1,+infty.[
then x > 2 by Th30;
then x > 1 by XXREAL_0:2;
hence x in ].1,+infty.[ by XXREAL_1:235; ::_thesis: verum
end;
suppose x in {4} ; ::_thesis: x in ].1,+infty.[
then x = 4 by TARSKI:def_1;
hence x in ].1,+infty.[ by XXREAL_1:235; ::_thesis: verum
end;
suppose x in {5} ; ::_thesis: x in ].1,+infty.[
then x = 5 by TARSKI:def_1;
hence x in ].1,+infty.[ by XXREAL_1:235; ::_thesis: verum
end;
end;
end;
Lm8: ].1,+infty.[ c= [.1,+infty.[
by XXREAL_1:45;
Lm9: ].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[
proof
A1: ].-infty,1.[ c= ].-infty,2.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,1.[ or x in ].-infty,2.] )
assume A2: x in ].-infty,1.[ ; ::_thesis: x in ].-infty,2.]
then reconsider x = x as real number ;
x < 1 by A2, XXREAL_1:233;
then x < 2 by XXREAL_0:2;
hence x in ].-infty,2.] by XXREAL_1:234; ::_thesis: verum
end;
[.1,+infty.[ misses ].-infty,1.[ by XXREAL_1:94;
then A3: ((IRRAT (2,4)) \/ {4}) \/ {5} misses ].-infty,1.[ by Lm7, Lm8, XBOOLE_1:1, XBOOLE_1:63;
].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ /\ (].-infty,2.] \/ (((IRRAT (2,4)) \/ {4}) \/ {5})) by XBOOLE_1:113
.= ].-infty,1.[ /\ ].-infty,2.] by A3, XBOOLE_1:78
.= ].-infty,1.[ by A1, XBOOLE_1:28 ;
hence ].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ ; ::_thesis: verum
end;
Lm10: ].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}
proof
].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].1,+infty.[ /\ (].-infty,2.] \/ (((IRRAT (2,4)) \/ {4}) \/ {5})) by XBOOLE_1:113
.= (].1,+infty.[ /\ ].-infty,2.]) \/ (].1,+infty.[ /\ (((IRRAT (2,4)) \/ {4}) \/ {5})) by XBOOLE_1:23
.= (].1,+infty.[ /\ ].-infty,2.]) \/ (((IRRAT (2,4)) \/ {4}) \/ {5}) by Lm7, XBOOLE_1:28
.= ].1,2.] \/ (((IRRAT (2,4)) \/ {4}) \/ {5}) by XXREAL_1:270
.= ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:113 ;
hence ].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} ; ::_thesis: verum
end;
theorem :: BORSUK_5:62
(].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5}
proof
(].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ \/ (].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5})) by Lm9, XBOOLE_1:23
.= ].-infty,1.[ \/ ((].1,2.] \/ (IRRAT (2,4))) \/ ({4} \/ {5})) by Lm10, XBOOLE_1:4
.= ((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ ({4} \/ {5}) by XBOOLE_1:113 ;
hence (].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:4; ::_thesis: verum
end;
theorem :: BORSUK_5:63
for A being Subset of R^1
for a, b being real number st a <= b & A = {a} \/ [.b,+infty.[ holds
A ` = ].-infty,a.[ \/ ].a,b.[
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a <= b & A = {a} \/ [.b,+infty.[ holds
A ` = ].-infty,a.[ \/ ].a,b.[
let a, b be real number ; ::_thesis: ( a <= b & A = {a} \/ [.b,+infty.[ implies A ` = ].-infty,a.[ \/ ].a,b.[ )
assume that
A1: a <= b and
A2: A = {a} \/ [.b,+infty.[ ; ::_thesis: A ` = ].-infty,a.[ \/ ].a,b.[
A ` = (REAL \ [.b,+infty.[) \ {a} by A2, TOPMETR:17, XBOOLE_1:41
.= ].-infty,b.[ \ {a} by XXREAL_1:224, XXREAL_1:294 ;
hence A ` = ].-infty,a.[ \/ ].a,b.[ by A1, XXREAL_1:349; ::_thesis: verum
end;
theorem :: BORSUK_5:64
for A being Subset of R^1
for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.[ holds
Cl A = ].-infty,b.]
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.[ holds
Cl A = ].-infty,b.]
let a, b be real number ; ::_thesis: ( a < b & A = ].-infty,a.[ \/ ].a,b.[ implies Cl A = ].-infty,b.] )
assume that
A1: a < b and
A2: A = ].-infty,a.[ \/ ].a,b.[ ; ::_thesis: Cl A = ].-infty,b.]
reconsider B = ].-infty,a.[, C = ].a,b.[ as Subset of R^1 by TOPMETR:17;
A3: Cl C = [.a,b.] by A1, Th16;
Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20
.= ].-infty,a.] \/ [.a,b.] by A3, Th51
.= ].-infty,b.] by A1, Th12 ;
hence Cl A = ].-infty,b.] ; ::_thesis: verum
end;
theorem Th65: :: BORSUK_5:65
for A being Subset of R^1
for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.] holds
Cl A = ].-infty,b.]
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.] holds
Cl A = ].-infty,b.]
let a, b be real number ; ::_thesis: ( a < b & A = ].-infty,a.[ \/ ].a,b.] implies Cl A = ].-infty,b.] )
assume that
A1: a < b and
A2: A = ].-infty,a.[ \/ ].a,b.] ; ::_thesis: Cl A = ].-infty,b.]
reconsider B = ].-infty,a.[, C = ].a,b.] as Subset of R^1 by TOPMETR:17;
A3: Cl C = [.a,b.] by A1, Th36;
Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20
.= ].-infty,a.] \/ [.a,b.] by A3, Th51
.= ].-infty,b.] by A1, Th12 ;
hence Cl A = ].-infty,b.] ; ::_thesis: verum
end;
theorem Th66: :: BORSUK_5:66
for A being Subset of R^1
for a, b, c being real number st a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds
Cl A = ].-infty,c.]
proof
let A be Subset of R^1; ::_thesis: for a, b, c being real number st a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds
Cl A = ].-infty,c.]
let a, b, c be real number ; ::_thesis: ( a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} implies Cl A = ].-infty,c.] )
assume that
A1: a < b and
A2: b < c and
A3: A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} ; ::_thesis: Cl A = ].-infty,c.]
reconsider B = ].-infty,a.[, C = ].a,b.], D = IRRAT (b,c), E = {c} as Subset of R^1 by TOPMETR:17;
A4: c in ].-infty,c.] by XXREAL_1:234;
Cl A = (Cl ((B \/ C) \/ D)) \/ (Cl E) by A3, PRE_TOPC:20
.= (Cl ((B \/ C) \/ D)) \/ E by Th38
.= ((Cl (B \/ C)) \/ (Cl D)) \/ E by PRE_TOPC:20
.= (].-infty,b.] \/ (Cl D)) \/ E by A1, Th65
.= (].-infty,b.] \/ [.b,c.]) \/ E by A2, Th32
.= ].-infty,c.] \/ E by A2, Th12
.= ].-infty,c.] by A4, ZFMISC_1:40 ;
hence Cl A = ].-infty,c.] ; ::_thesis: verum
end;
theorem :: BORSUK_5:67
for A being Subset of R^1
for a, b, c, d being real number st a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} holds
Cl A = ].-infty,c.] \/ {d}
proof
let A be Subset of R^1; ::_thesis: for a, b, c, d being real number st a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} holds
Cl A = ].-infty,c.] \/ {d}
let a, b, c, d be real number ; ::_thesis: ( a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} implies Cl A = ].-infty,c.] \/ {d} )
assume that
A1: a < b and
A2: b < c and
A3: A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} ; ::_thesis: Cl A = ].-infty,c.] \/ {d}
reconsider B = ].-infty,a.[, C = ].a,b.], D = IRRAT (b,c), E = {c}, F = {d} as Subset of R^1 by TOPMETR:17;
Cl A = (Cl (((B \/ C) \/ D) \/ E)) \/ (Cl F) by A3, PRE_TOPC:20
.= (Cl (((B \/ C) \/ D) \/ E)) \/ {d} by Th38 ;
hence Cl A = ].-infty,c.] \/ {d} by A1, A2, Th66; ::_thesis: verum
end;
theorem :: BORSUK_5:68
for A being Subset of R^1
for a, b being real number st a <= b & A = ].-infty,a.] \/ {b} holds
A ` = ].a,b.[ \/ ].b,+infty.[
proof
let A be Subset of R^1; ::_thesis: for a, b being real number st a <= b & A = ].-infty,a.] \/ {b} holds
A ` = ].a,b.[ \/ ].b,+infty.[
let a, b be real number ; ::_thesis: ( a <= b & A = ].-infty,a.] \/ {b} implies A ` = ].a,b.[ \/ ].b,+infty.[ )
assume that
A1: a <= b and
A2: A = ].-infty,a.] \/ {b} ; ::_thesis: A ` = ].a,b.[ \/ ].b,+infty.[
A ` = (REAL \ ].-infty,a.]) \ {b} by A2, TOPMETR:17, XBOOLE_1:41
.= ].a,+infty.[ \ {b} by XXREAL_1:224, XXREAL_1:288
.= ].a,b.[ \/ ].b,+infty.[ by A1, XXREAL_1:365 ;
hence A ` = ].a,b.[ \/ ].b,+infty.[ ; ::_thesis: verum
end;
theorem :: BORSUK_5:69
for a, b being real number holds [.a,+infty.[ \/ {b} <> REAL
proof
let a, b be real number ; ::_thesis: [.a,+infty.[ \/ {b} <> REAL
set ab = (min (a,b)) - 1;
A1: (min (a,b)) - 1 < min (a,b) by XREAL_1:146;
min (a,b) <= b by XXREAL_0:17;
then A2: not (min (a,b)) - 1 in {b} by A1, TARSKI:def_1;
min (a,b) <= a by XXREAL_0:17;
then (min (a,b)) - 1 < a by XREAL_1:146, XXREAL_0:2;
then A3: not (min (a,b)) - 1 in [.a,+infty.[ by XXREAL_1:236;
(min (a,b)) - 1 in REAL by XREAL_0:def_1;
hence [.a,+infty.[ \/ {b} <> REAL by A3, A2, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: BORSUK_5:70
for a, b being real number holds ].-infty,a.] \/ {b} <> REAL
proof
let a, b be real number ; ::_thesis: ].-infty,a.] \/ {b} <> REAL
set ab = (max (a,b)) + 1;
A1: (max (a,b)) + 1 > max (a,b) by XREAL_1:29;
max (a,b) >= a by XXREAL_0:25;
then (max (a,b)) + 1 > a by A1, XXREAL_0:2;
then A2: not (max (a,b)) + 1 in ].-infty,a.] by XXREAL_1:234;
max (a,b) >= b by XXREAL_0:25;
then A3: not (max (a,b)) + 1 in {b} by A1, TARSKI:def_1;
(max (a,b)) + 1 in REAL by XREAL_0:def_1;
hence ].-infty,a.] \/ {b} <> REAL by A2, A3, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: BORSUK_5:71
for TS being TopStruct
for A, B being Subset of TS st A <> B holds
A ` <> B `
proof
let TS be TopStruct ; ::_thesis: for A, B being Subset of TS st A <> B holds
A ` <> B `
let A, B be Subset of TS; ::_thesis: ( A <> B implies A ` <> B ` )
assume A1: A <> B ; ::_thesis: A ` <> B `
assume A ` = B ` ; ::_thesis: contradiction
then A = (B `) ` ;
hence contradiction by A1; ::_thesis: verum
end;
theorem :: BORSUK_5:72
for A being Subset of R^1 st REAL = A ` holds
A = {}
proof
reconsider AB = {} R^1 as Subset of R^1 ;
let A be Subset of R^1; ::_thesis: ( REAL = A ` implies A = {} )
assume REAL = A ` ; ::_thesis: A = {}
then AB ` = A ` by TOPMETR:17;
then AB = (A `) ` ;
hence A = {} ; ::_thesis: verum
end;
begin
theorem Th73: :: BORSUK_5:73
for X being compact Subset of R^1
for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above & X9 is bounded_below )
proof
let X be compact Subset of R^1; ::_thesis: for X9 being Subset of REAL st X9 = X holds
( X9 is bounded_above & X9 is bounded_below )
let X9 be Subset of REAL; ::_thesis: ( X9 = X implies ( X9 is bounded_above & X9 is bounded_below ) )
assume X9 = X ; ::_thesis: ( X9 is bounded_above & X9 is bounded_below )
then X9 is compact by JORDAN5A:25;
then X9 is real-bounded by RCOMP_1:10;
hence ( X9 is bounded_above & X9 is bounded_below ) by XXREAL_2:def_11; ::_thesis: verum
end;
theorem Th74: :: BORSUK_5:74
for X being compact Subset of R^1
for X9 being Subset of REAL
for x being real number st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
proof
let X be compact Subset of R^1; ::_thesis: for X9 being Subset of REAL
for x being real number st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
let X9 be Subset of REAL; ::_thesis: for x being real number st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
let x be real number ; ::_thesis: ( x in X9 & X9 = X implies ( lower_bound X9 <= x & x <= upper_bound X9 ) )
assume that
A1: x in X9 and
A2: X9 = X ; ::_thesis: ( lower_bound X9 <= x & x <= upper_bound X9 )
( X9 is bounded_above & X9 is bounded_below ) by A2, Th73;
hence ( lower_bound X9 <= x & x <= upper_bound X9 ) by A1, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum
end;
theorem Th75: :: BORSUK_5:75
for C being non empty connected compact Subset of R^1
for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds
[.(lower_bound C9),(upper_bound C9).] = C9
proof
let C be non empty connected compact Subset of R^1; ::_thesis: for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds
[.(lower_bound C9),(upper_bound C9).] = C9
let C9 be Subset of REAL; ::_thesis: ( C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 implies [.(lower_bound C9),(upper_bound C9).] = C9 )
assume that
A1: C = C9 and
A2: [.(lower_bound C9),(upper_bound C9).] c= C9 ; ::_thesis: [.(lower_bound C9),(upper_bound C9).] = C9
assume [.(lower_bound C9),(upper_bound C9).] <> C9 ; ::_thesis: contradiction
then not C9 c= [.(lower_bound C9),(upper_bound C9).] by A2, XBOOLE_0:def_10;
then consider c being set such that
A3: c in C9 and
A4: not c in [.(lower_bound C9),(upper_bound C9).] by TARSKI:def_3;
reconsider c = c as real number by A3;
A5: c <= upper_bound C9 by A1, A3, Th74;
lower_bound C9 <= c by A1, A3, Th74;
hence contradiction by A4, A5, XXREAL_1:1; ::_thesis: verum
end;
theorem Th76: :: BORSUK_5:76
for A being connected Subset of R^1
for a, b, c being real number st a <= b & b <= c & a in A & c in A holds
b in A
proof
let A be connected Subset of R^1; ::_thesis: for a, b, c being real number st a <= b & b <= c & a in A & c in A holds
b in A
let a, b, c be real number ; ::_thesis: ( a <= b & b <= c & a in A & c in A implies b in A )
assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A ; ::_thesis: b in A
percases ( a = b or b = c or ( a < b & b < c & a in A & c in A ) ) by A1, A2, A3, A4, XXREAL_0:1;
suppose ( a = b or b = c ) ; ::_thesis: b in A
hence b in A by A3, A4; ::_thesis: verum
end;
supposeA5: ( a < b & b < c & a in A & c in A ) ; ::_thesis: b in A
reconsider B = ].-infty,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17;
assume not b in A ; ::_thesis: contradiction
then A c= REAL \ {b} by TOPMETR:17, ZFMISC_1:34;
then A6: A c= ].-infty,b.[ \/ ].b,+infty.[ by XXREAL_1:389;
now__::_thesis:_contradiction
percases ( A c= B or A c= C ) by A6, Th53, CONNSP_1:16;
suppose A c= B ; ::_thesis: contradiction
hence contradiction by A5, XXREAL_1:233; ::_thesis: verum
end;
suppose A c= C ; ::_thesis: contradiction
hence contradiction by A5, XXREAL_1:235; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
theorem Th77: :: BORSUK_5:77
for A being connected Subset of R^1
for a, b being real number st a in A & b in A holds
[.a,b.] c= A
proof
let A be connected Subset of R^1; ::_thesis: for a, b being real number st a in A & b in A holds
[.a,b.] c= A
let a, b be real number ; ::_thesis: ( a in A & b in A implies [.a,b.] c= A )
assume that
A1: a in A and
A2: b in A ; ::_thesis: [.a,b.] c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.] or x in A )
assume x in [.a,b.] ; ::_thesis: x in A
then x in { y where y is Real : ( a <= y & y <= b ) } by RCOMP_1:def_1;
then ex z being Real st
( z = x & a <= z & z <= b ) ;
hence x in A by A1, A2, Th76; ::_thesis: verum
end;
theorem Th78: :: BORSUK_5:78
for X being non empty connected compact Subset of R^1 holds X is non empty closed_interval Subset of REAL
proof
let C be non empty connected compact Subset of R^1; ::_thesis: C is non empty closed_interval Subset of REAL
reconsider C9 = C as non empty Subset of REAL by TOPMETR:17;
C is closed by COMPTS_1:7;
then A1: C9 is closed by JORDAN5A:23;
then A2: upper_bound C9 in C9 by Th73, RCOMP_1:12;
( C9 is bounded_below & C9 is bounded_above ) by Th73;
then C9 is real-bounded by XXREAL_2:def_11;
then A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
lower_bound C9 in C9 by A1, Th73, RCOMP_1:13;
then [.(lower_bound C9),(upper_bound C9).] = C9 by A2, Th75, Th77;
hence C is non empty closed_interval Subset of REAL by A3, MEASURE5:14; ::_thesis: verum
end;
theorem :: BORSUK_5:79
for A being non empty connected compact Subset of R^1 ex a, b being real number st
( a <= b & A = [.a,b.] )
proof
let C be non empty connected compact Subset of R^1; ::_thesis: ex a, b being real number st
( a <= b & C = [.a,b.] )
reconsider C9 = C as non empty closed_interval Subset of REAL by Th78;
A1: lower_bound C9 <= upper_bound C9 by BORSUK_4:28;
A2: C9 = [.(lower_bound C9),(upper_bound C9).] by INTEGRA1:4;
then A3: upper_bound C9 in C by A1, XXREAL_1:1;
lower_bound C9 in C by A2, A1, XXREAL_1:1;
then reconsider p1 = lower_bound C9, p2 = upper_bound C9 as Point of R^1 by A3;
take p1 ; ::_thesis: ex b being real number st
( p1 <= b & C = [.p1,b.] )
take p2 ; ::_thesis: ( p1 <= p2 & C = [.p1,p2.] )
thus p1 <= p2 by BORSUK_4:28; ::_thesis: C = [.p1,p2.]
thus C = [.p1,p2.] by INTEGRA1:4; ::_thesis: verum
end;
registration
let T be TopSpace;
cluster non empty open closed for Element of bool (bool the carrier of T);
existence
ex b1 being Subset-Family of T st
( b1 is open & b1 is closed & not b1 is empty )
proof
reconsider F = {({} T)} as Subset-Family of T by ZFMISC_1:31;
A1: F is closed
proof
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in F or P is closed )
assume P in F ; ::_thesis: P is closed
hence P is closed by TARSKI:def_1; ::_thesis: verum
end;
F is open
proof
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
assume P in F ; ::_thesis: P is open
hence P is open by TARSKI:def_1; ::_thesis: verum
end;
hence ex b1 being Subset-Family of T st
( b1 is open & b1 is closed & not b1 is empty ) by A1; ::_thesis: verum
end;
end;