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


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}
proofend;

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
proofend;

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
proofend;

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 &amp; x1 <> x5 &amp; x1 <> x6 &amp; x2 <> x4 &amp; x2 <> x5 &amp; x2 <> x6 &amp; x3 <> x4 &amp; x3 <> x5 &amp; x3 <> x6 )
proofend;

theorem :: BORSUK_5:6
for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3 are_mutually_different &amp; x4,x5,x6 are_mutually_different &amp; {x1,x2,x3} misses {x4,x5,x6} holds
x1,x2,x3,x4,x5,x6 are_mutually_different
proofend;

theorem :: BORSUK_5:7
for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6 are_mutually_different &amp; {x1,x2,x3,x4,x5,x6} misses {x7} holds
x1,x2,x3,x4,x5,x6,x7 are_mutually_different
proofend;

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
proofend;

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
proofend;

Lm1:  R^1 is pathwise_connected
proofend;

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 &amp; not b1 is empty )
proofend;
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 &amp; b <= c &amp; c < d &amp; A = [.a,b.[ &amp; B = ].c,d.] holds
A,B are_separated
proofend;

theorem Th11: :: BORSUK_5:11
for a, b, c being real number st a <= c &amp; c <= b holds
[.a,b.] \/ [.c,+infty.[ = [.a,+infty.[
proofend;

theorem Th12: :: BORSUK_5:12
for a, b, c being real number st a <= c &amp; c <= b holds
].-infty,c.] \/ [.a,b.] = ].-infty,b.]
proofend;

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
proofend;

theorem Th15: :: BORSUK_5:15
for A being Subset of R^1 st A = RAT holds
Cl A = the carrier of R^1
proofend;

theorem Th16: :: BORSUK_5:16
for A being Subset of R^1
for a, b being real number st A = ].a,b.[ &amp; a <> b holds
Cl A = [.a,b.]
proofend;

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 )
proofend;

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
proofend;
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
proofend;
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
proofend;
clusterb - a ->  irrational ;
coherence
 b - a is irrational
proofend;
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
proofend;

theorem Th23: :: BORSUK_5:23
for a being rational number
for b being real irrational number st a <> 0 holds
b / a is irrational
proofend;

registration
cluster real irrational  ->  non zero real for set ;
coherence
 for b1 being real number st b1 is irrational holds
not b1 is zero
proofend;
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
proofend;

registration
let r be real irrational number ;
cluster frac r ->  irrational ;
coherence
 frac r is irrational
proofend;
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
proofend;
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 &amp; p1 < p2 &amp; p2 < b )
proofend;

theorem Th27: :: BORSUK_5:27
for a, b being real number st a < b holds
ex p being real irrational number st
( a < p &amp; p < b )
proofend;

theorem Th28: :: BORSUK_5:28
for A being Subset of R^1 st A = IRRAT holds
Cl A = the carrier of R^1
proofend;

Lm2:  for A being Subset of R^1
for a, b being real number st a < b &amp; A = RAT (a,b) holds
( a in Cl A &amp; b in Cl A )
proofend;

Lm3:  for A being Subset of R^1
for a, b being real number st a < b &amp; A = IRRAT (a,b) holds
( a in Cl A &amp; b in Cl A )
proofend;

theorem Th29: :: BORSUK_5:29
for a, b, c being real number holds
( c in RAT (a,b) iff ( c is rational &amp; a < c &amp; c < b ) )
proofend;

theorem Th30: :: BORSUK_5:30
for a, b, c being real number holds
( c in IRRAT (a,b) iff ( c is irrational &amp; a < c &amp; c < b ) )
proofend;

theorem Th31: :: BORSUK_5:31
for A being Subset of R^1
for a, b being real number st a < b &amp; A = RAT (a,b) holds
Cl A = [.a,b.]
proofend;

theorem Th32: :: BORSUK_5:32
for A being Subset of R^1
for a, b being real number st a < b &amp; A = IRRAT (a,b) holds
Cl A = [.a,b.]
proofend;

theorem Th33: :: BORSUK_5:33
for T being connected TopSpace
for A being open closed Subset of T holds
( A = {} or A = [#] T )
proofend;

theorem Th34: :: BORSUK_5:34
for A being Subset of R^1 st A is closed &amp; A is open &amp; not A = {} holds
A = REAL
proofend;

begin

theorem Th35: :: BORSUK_5:35
for A being Subset of R^1
for a, b being real number st A = [.a,b.[ &amp; a <> b holds
Cl A = [.a,b.]
proofend;

theorem Th36: :: BORSUK_5:36
for A being Subset of R^1
for a, b being real number st A = ].a,b.] &amp; a <> b holds
Cl A = [.a,b.]
proofend;

theorem :: BORSUK_5:37
for A being Subset of R^1
for a, b, c being real number st A = [.a,b.[ \/ ].b,c.] &amp; a < b &amp; b < c holds
Cl A = [.a,c.]
proofend;

theorem Th38: :: BORSUK_5:38
for A being Subset of R^1
for a being real number st A = {a} holds
Cl A = {a}
proofend;

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 )
proofend;

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

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

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
proofend;
clusterA \/ B ->  open for Subset of REAL;
coherence
 for b1 being Subset of REAL st b1 = A \/ B holds
b1 is open
proofend;
end;

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

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
proofend;

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
proofend;

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
proofend;

theorem Th43: :: BORSUK_5:43
for a being real number holds [.a,+infty.[ = {a} \/ ].a,+infty.[
proofend;

theorem Th44: :: BORSUK_5:44
for a being real number holds ].-infty,a.] = {a} \/ ].-infty,a.[
proofend;

registration
let a be real number ;
clusterK451(a,+infty) ->  non empty ;
coherence
 not ].a,+infty.[ is empty
proofend;
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
proofend;
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
proofend;

theorem :: BORSUK_5:46
for a being real number holds [.a,+infty.[ <> REAL
proofend;

theorem :: BORSUK_5:47
for a being real number holds ].-infty,a.] <> REAL
proofend;

theorem Th48: :: BORSUK_5:48
for a being real number holds ].-infty,a.[ <> REAL
proofend;

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.[
proofend;

theorem :: BORSUK_5:50
for a being real number holds Cl ].a,+infty.[ = [.a,+infty.[
proofend;

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.]
proofend;

theorem :: BORSUK_5:52
for a being real number holds Cl ].-infty,a.[ = ].-infty,a.]
proofend;

theorem Th53: :: BORSUK_5:53
for A, B being Subset of R^1
for b being real number st A = ].-infty,b.[ &amp; B = ].b,+infty.[ holds
A,B are_separated
proofend;

theorem :: BORSUK_5:54
for A being Subset of R^1
for a, b being real number st a < b &amp; A = [.a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[
proofend;

theorem Th55: :: BORSUK_5:55
for A being Subset of R^1
for a, b being real number st a < b &amp; A = ].a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[
proofend;

theorem :: BORSUK_5:56
for A being Subset of R^1
for a, b, c being real number st a < b &amp; b < c &amp; A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds
Cl A = [.a,+infty.[
proofend;

theorem Th57: :: BORSUK_5:57
for a, b being real number holds IRRAT (a,b) misses RAT (a,b)
proofend;

theorem Th58: :: BORSUK_5:58
for a, b being real number holds REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
proofend;

theorem Th59: :: BORSUK_5:59
for a, b being real number st a < b holds
[.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b}
proofend;

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}
proofend;

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.[
proofend;

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

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

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

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

theorem :: BORSUK_5:63
for A being Subset of R^1
for a, b being real number st a <= b &amp; A = {a} \/ [.b,+infty.[ holds
A ` = ].-infty,a.[ \/ ].a,b.[
proofend;

theorem :: BORSUK_5:64
for A being Subset of R^1
for a, b being real number st a < b &amp; A = ].-infty,a.[ \/ ].a,b.[ holds
Cl A = ].-infty,b.]
proofend;

theorem Th65: :: BORSUK_5:65
for A being Subset of R^1
for a, b being real number st a < b &amp; A = ].-infty,a.[ \/ ].a,b.] holds
Cl A = ].-infty,b.]
proofend;

theorem Th66: :: BORSUK_5:66
for A being Subset of R^1
for a, b, c being real number st a < b &amp; b < c &amp; A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds
Cl A = ].-infty,c.]
proofend;

theorem :: BORSUK_5:67
for A being Subset of R^1
for a, b, c, d being real number st a < b &amp; b < c &amp; A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} holds
Cl A = ].-infty,c.] \/ {d}
proofend;

theorem :: BORSUK_5:68
for A being Subset of R^1
for a, b being real number st a <= b &amp; A = ].-infty,a.] \/ {b} holds
A ` = ].a,b.[ \/ ].b,+infty.[
proofend;

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

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

theorem :: BORSUK_5:71
for TS being TopStruct
for A, B being Subset of TS st A <> B holds
A ` <> B `
proofend;

theorem :: BORSUK_5:72
for A being Subset of R^1 st REAL = A ` holds
A = {}
proofend;

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 &amp; X9 is bounded_below )
proofend;

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 &amp; X9 = X holds
( lower_bound X9 <= x &amp; x <= upper_bound X9 )
proofend;

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 &amp; [.(lower_bound C9),(upper_bound C9).] c= C9 holds
[.(lower_bound C9),(upper_bound C9).] = C9
proofend;

theorem Th76: :: BORSUK_5:76
for A being connected Subset of R^1
for a, b, c being real number st a <= b &amp; b <= c &amp; a in A &amp; c in A holds
b in A
proofend;

theorem Th77: :: BORSUK_5:77
for A being connected Subset of R^1
for a, b being real number st a in A &amp; b in A holds
[.a,b.] c= A
proofend;

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
proofend;

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

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 &amp; b1 is closed &amp; not b1 is empty )
proofend;
end;