:: On the Subcontinua of a Real Line
:: by Adam Grabowski
::
:: Received June 12, 2003
:: Copyright (c) 2003 Association of Mizar Users


begin

theorem :: BORSUK_5:1
canceled;

theorem Th2: :: BORSUK_5:2
for A, B, a being set st A c= B & B c= A \/ {a} & not A \/ {a} = B holds
A = B
proof end;

theorem :: BORSUK_5:3
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}
proof end;

definition
canceled;
canceled;
end;

:: deftheorem BORSUK_5:def 1 :
canceled;

:: deftheorem BORSUK_5:def 2 :
canceled;

theorem Th4: :: BORSUK_5:4
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 end;

theorem :: BORSUK_5:5
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 end;

theorem Th6: :: BORSUK_5:6
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 end;

theorem :: BORSUK_5:7
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 end;

theorem :: BORSUK_5:8
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 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
x7,x1,x2,x3,x4,x5,x6 are_mutually_different
proof end;

theorem :: BORSUK_5:10
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 end;

Lm1: R^1 is arcwise_connected
proof end;

registration
cluster R^1 -> arcwise_connected ;
coherence
R^1 is arcwise_connected by Lm1;
end;

registration
cluster non empty connected TopStruct ;
existence
ex b1 being TopSpace st
( b1 is connected & not b1 is empty )
proof end;
end;

begin

theorem :: BORSUK_5:11
canceled;

theorem :: BORSUK_5:12
canceled;

theorem :: BORSUK_5:13
canceled;

theorem :: BORSUK_5:14
canceled;

theorem :: BORSUK_5:15
canceled;

theorem :: BORSUK_5:16
canceled;

theorem :: BORSUK_5:17
canceled;

theorem :: BORSUK_5:18
canceled;

theorem :: BORSUK_5:19
canceled;

theorem :: BORSUK_5:20
canceled;

theorem :: BORSUK_5:21
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 end;

theorem :: BORSUK_5:22
canceled;

theorem :: BORSUK_5:23
canceled;

theorem :: BORSUK_5:24
canceled;

theorem :: BORSUK_5:25
canceled;

theorem :: BORSUK_5:26
canceled;

theorem :: BORSUK_5:27
canceled;

theorem Th28: :: BORSUK_5:28
for a, b, c being real number st a <= c & c <= b holds
[.a,b.] \/ [.c,+infty .[ = [.a,+infty .[
proof end;

theorem Th29: :: BORSUK_5:29
for a, b, c being real number st a <= c & c <= b holds
].-infty ,c.] \/ [.a,b.] = ].-infty ,b.]
proof end;

registration
cluster -> real Element of RAT ;
coherence
for b1 being Element of RAT holds b1 is real ;
end;

registration
cluster -> real Element of the carrier of RealSpace ;
coherence
for b1 being Element of RealSpace holds b1 is real by METRIC_1:def 14;
end;

theorem :: BORSUK_5:30
canceled;

theorem :: BORSUK_5:31
canceled;

theorem :: BORSUK_5:32
canceled;

theorem :: BORSUK_5:33
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:95, TOPMETR:def 7;

theorem Th34: :: BORSUK_5:34
for p, q being Element of RealSpace st q >= p holds
dist p,q = q - p
proof end;

theorem Th35: :: BORSUK_5:35
for A being Subset of R^1 st A = RAT holds
Cl A = the carrier of R^1
proof 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 end;

begin

registration
cluster number_e -> irrational ;
coherence
number_e is irrational by IRRAT_1:42;
end;

definition
func IRRAT -> Subset of REAL equals :: BORSUK_5:def 3
REAL \ RAT ;
coherence
REAL \ RAT is Subset of REAL ;
end;

:: deftheorem defines IRRAT BORSUK_5:def 3 :
IRRAT = REAL \ RAT ;

definition
let a, b be real number ;
func RAT a,b -> Subset of REAL equals :: BORSUK_5:def 4
RAT /\ ].a,b.[;
coherence
RAT /\ ].a,b.[ is Subset of REAL ;
func IRRAT a,b -> Subset of REAL equals :: BORSUK_5:def 5
IRRAT /\ ].a,b.[;
coherence
IRRAT /\ ].a,b.[ is Subset of REAL ;
end;

:: deftheorem defines RAT BORSUK_5:def 4 :
for a, b being real number holds RAT a,b = RAT /\ ].a,b.[;

:: deftheorem defines IRRAT BORSUK_5:def 5 :
for a, b being real number holds IRRAT a,b = IRRAT /\ ].a,b.[;

theorem Th37: :: BORSUK_5:37
for x being real number holds
( x is irrational iff x in IRRAT )
proof end;

registration
cluster real irrational set ;
existence
ex b1 being real number st b1 is irrational by IRRAT_1:42;
end;

registration
cluster IRRAT -> non empty ;
coherence
not IRRAT is empty by Th37, IRRAT_1:42;
end;

theorem Th38: :: BORSUK_5:38
for a being rational number
for b being real irrational number holds a + b is irrational
proof end;

theorem Th39: :: BORSUK_5:39
for a being real irrational number holds - a is irrational
proof end;

theorem Th40: :: BORSUK_5:40
for a being rational number
for b being real irrational number holds a - b is irrational
proof end;

theorem Th41: :: BORSUK_5:41
for a being rational number
for b being real irrational number holds b - a is irrational
proof end;

theorem Th42: :: BORSUK_5:42
for a being rational number
for b being real irrational number st a <> 0 holds
a * b is irrational
proof end;

theorem Th43: :: BORSUK_5:43
for a being rational number
for b being real irrational number st a <> 0 holds
b / a is irrational
proof end;

registration
cluster real irrational -> non zero real set ;
coherence
for b1 being real number st b1 is irrational holds
not b1 is empty
proof end;
end;

theorem Th44: :: BORSUK_5:44
for a being rational number
for b being real irrational number st a <> 0 holds
a / b is irrational
proof end;

theorem Th45: :: BORSUK_5:45
for r being real irrational number holds frac r is irrational
proof end;

registration
let r be real irrational number ;
cluster frac r -> irrational ;
coherence
frac r is irrational by Th45;
end;

registration
let a be real irrational number ;
cluster - a -> irrational ;
coherence
- a is irrational by Th39;
end;

registration
let a be rational number ;
let b be real irrational number ;
cluster a + b -> irrational ;
coherence
a + b is irrational by Th38;
cluster b + a -> irrational ;
coherence
b + a is irrational ;
cluster a - b -> irrational ;
coherence
a - b is irrational by Th40;
cluster b - a -> irrational ;
coherence
b - a is irrational by Th41;
end;

registration
cluster non zero rational set ;
existence
not for b1 being rational number holds b1 is empty
proof end;
end;

registration
let a be non zero rational number ;
let b be real irrational number ;
cluster a * b -> irrational ;
coherence
a * b is irrational by Th42;
cluster b * a -> irrational ;
coherence
b * a is irrational ;
cluster a / b -> irrational ;
coherence
a / b is irrational by Th44;
cluster b / a -> irrational ;
coherence
b / a is irrational by Th43;
end;

theorem :: BORSUK_5:46
canceled;

theorem Th47: :: BORSUK_5:47
for a, b being real number st a < b holds
ex p1, p2 being rational number st
( a < p1 & p1 < p2 & p2 < b )
proof end;

theorem :: BORSUK_5:48
canceled;

theorem :: BORSUK_5:49
canceled;

theorem Th50: :: BORSUK_5:50
for a, b being real number st a < b holds
ex p being real irrational number st
( a < p & p < b )
proof end;

theorem Th51: :: BORSUK_5:51
for A being Subset of R^1 st A = IRRAT holds
Cl A = the carrier of R^1
proof 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 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 end;

theorem Th52: :: BORSUK_5:52
for a, b, c being real number holds
( c in RAT a,b iff ( not c is irrational & a < c & c < b ) )
proof end;

theorem Th53: :: BORSUK_5:53
for a, b, c being real number holds
( c in IRRAT a,b iff ( c is irrational & a < c & c < b ) )
proof end;

theorem Th54: :: BORSUK_5:54
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 end;

theorem Th55: :: BORSUK_5:55
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 end;

theorem Th56: :: BORSUK_5:56
for T being connected TopSpace
for A being open closed Subset of T holds
( A = {} or A = [#] T )
proof end;

theorem Th57: :: BORSUK_5:57
for A being Subset of R^1 st A is closed & A is open & not A = {} holds
A = REAL
proof end;

begin

theorem Th58: :: BORSUK_5:58
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 end;

theorem Th59: :: BORSUK_5:59
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 end;

theorem :: BORSUK_5:60
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 end;

theorem Th61: :: BORSUK_5:61
for A being Subset of R^1
for a being real number st A = {a} holds
Cl A = {a}
proof end;

theorem Th62: :: BORSUK_5:62
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 end;

Lm4: for a being real number holds ].-infty ,a.] is closed
proof end;

Lm5: for a being real number holds [.a,+infty .[ is closed
proof end;

registration
let A, B be open Subset of REAL ;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:24;
cluster A /\ B -> open Subset of REAL ;
coherence
for b1 being Subset of REAL st b1 = A /\ B holds
b1 is open
proof end;
cluster A \/ B -> open Subset of REAL ;
coherence
for b1 being Subset of REAL st b1 = A \/ B holds
b1 is open
proof end;
end;

Lm6: for a, b being ext-real number holds ].a,b.[ is open
proof end;

theorem Th63: :: BORSUK_5:63
for A being Subset of R^1
for a, b being ext-real number st A = ].a,b.[ holds
A is open
proof end;

theorem :: BORSUK_5:64
canceled;

theorem Th65: :: BORSUK_5:65
for A being Subset of R^1
for a being real number st A = ].-infty ,a.] holds
A is closed
proof end;

theorem Th66: :: BORSUK_5:66
for A being Subset of R^1
for a being real number st A = [.a,+infty .[ holds
A is closed
proof end;

theorem Th67: :: BORSUK_5:67
for a being real number holds [.a,+infty .[ = {a} \/ ].a,+infty .[
proof end;

theorem Th68: :: BORSUK_5:68
for a being real number holds ].-infty ,a.] = {a} \/ ].-infty ,a.[
proof end;

registration
let a be real number ;
cluster K486(a,+infty ) -> non empty ;
coherence
not ].a,+infty .[ is empty
proof end;
cluster K485(-infty ,a) -> non empty ;
coherence
not ].-infty ,a.] is empty by XXREAL_1:234;
cluster K486(-infty ,a) -> non empty ;
coherence
not ].-infty ,a.[ is empty
proof end;
cluster K484(a,+infty ) -> non empty ;
coherence
not [.a,+infty .[ is empty by XXREAL_1:236;
end;

theorem :: BORSUK_5:69
canceled;

theorem :: BORSUK_5:70
canceled;

theorem Th71: :: BORSUK_5:71
for a being real number holds ].a,+infty .[ <> REAL
proof end;

theorem :: BORSUK_5:72
for a being real number holds [.a,+infty .[ <> REAL
proof end;

theorem :: BORSUK_5:73
for a being real number holds ].-infty ,a.] <> REAL
proof end;

theorem Th74: :: BORSUK_5:74
for a being real number holds ].-infty ,a.[ <> REAL
proof end;

theorem Th75: :: BORSUK_5:75
for A being Subset of R^1
for a being real number st A = ].a,+infty .[ holds
Cl A = [.a,+infty .[
proof end;

theorem :: BORSUK_5:76
for a being real number holds Cl ].a,+infty .[ = [.a,+infty .[
proof end;

theorem Th77: :: BORSUK_5:77
for A being Subset of R^1
for a being real number st A = ].-infty ,a.[ holds
Cl A = ].-infty ,a.]
proof end;

theorem :: BORSUK_5:78
for a being real number holds Cl ].-infty ,a.[ = ].-infty ,a.]
proof end;

theorem Th79: :: BORSUK_5:79
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 end;

theorem :: BORSUK_5:80
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 end;

theorem Th81: :: BORSUK_5:81
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 end;

theorem :: BORSUK_5:82
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 end;

theorem :: BORSUK_5:83
canceled;

theorem Th84: :: BORSUK_5:84
for a, b being real number holds IRRAT a,b misses RAT a,b
proof end;

Lm7: for a, b being real number st b <= a holds
RAT a,b = {}
proof end;

Lm8: for a, b being real number st b <= a holds
REAL = ].-infty ,a.] \/ [.b,+infty .[
proof end;

theorem Th85: :: BORSUK_5:85
for a, b being real number holds REAL \ (RAT a,b) = (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[
proof end;

theorem :: BORSUK_5:86
canceled;

theorem :: BORSUK_5:87
canceled;

theorem Th88: :: BORSUK_5:88
for a, b being real number st a < b holds
[.a,+infty .[ \ (].a,b.[ \/ ].b,+infty .[) = {a} \/ {b}
proof end;

theorem :: BORSUK_5:89
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 end;

theorem :: BORSUK_5:90
for A being Subset of R^1
for a being real number st A = {a} holds
A ` = ].-infty ,a.[ \/ ].a,+infty .[ by TOPMETR:24, XXREAL_1:389;

Lm9: ((IRRAT 2,4) \/ {4}) \/ {5} c= ].1,+infty .[
proof end;

Lm10: ].1,+infty .[ c= [.1,+infty .[
by XXREAL_1:45;

Lm11: ].-infty ,1.[ /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ].-infty ,1.[
proof end;

Lm12: ].1,+infty .[ /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}
proof end;

theorem :: BORSUK_5:91
canceled;

theorem :: BORSUK_5:92
(].-infty ,1.[ \/ ].1,+infty .[) /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = (((].-infty ,1.[ \/ ].1,2.]) \/ (IRRAT 2,4)) \/ {4}) \/ {5}
proof end;

theorem :: BORSUK_5:93
canceled;

theorem :: BORSUK_5:94
canceled;

theorem :: BORSUK_5:95
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 end;

theorem :: BORSUK_5:96
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 end;

theorem Th97: :: BORSUK_5:97
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 end;

theorem :: BORSUK_5:98
canceled;

theorem :: BORSUK_5:99
canceled;

theorem Th100: :: BORSUK_5:100
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 end;

theorem :: BORSUK_5:101
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 end;

theorem :: BORSUK_5:102
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 end;

theorem :: BORSUK_5:103
for a, b being real number holds [.a,+infty .[ \/ {b} <> REAL
proof end;

theorem :: BORSUK_5:104
for a, b being real number holds ].-infty ,a.] \/ {b} <> REAL
proof end;

theorem :: BORSUK_5:105
for TS being TopStruct
for A, B being Subset of TS st A <> B holds
A ` <> B `
proof end;

theorem :: BORSUK_5:106
for A being Subset of R^1 st REAL = A ` holds
A = {}
proof end;

begin

theorem Th107: :: BORSUK_5:107
for X being compact Subset of R^1
for X' being Subset of REAL st X' = X holds
( X' is bounded_above & X' is bounded_below )
proof end;

theorem Th108: :: BORSUK_5:108
for X being compact Subset of R^1
for X' being Subset of REAL
for x being real number st x in X' & X' = X holds
( inf X' <= x & x <= sup X' )
proof end;

theorem Th109: :: BORSUK_5:109
for C being non empty connected compact Subset of R^1
for C' being Subset of REAL st C = C' & [.(inf C'),(sup C').] c= C' holds
[.(inf C'),(sup C').] = C'
proof end;

theorem Th110: :: BORSUK_5:110
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 end;

theorem Th111: :: BORSUK_5:111
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 end;

theorem Th112: :: BORSUK_5:112
for X being non empty connected compact Subset of R^1 holds X is non empty closed-interval Subset of REAL
proof end;

theorem :: BORSUK_5:113
for A being non empty connected compact Subset of R^1 ex a, b being real number st
( a <= b & A = [.a,b.] )
proof end;

registration
let T be TopSpace;
cluster non empty open closed 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 end;
end;