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

theorem :: BORSUK_5:1

canceled;

::$CT

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

theorem Th2: :: BORSUK_5:3

for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3,x4,x5,x6 are_mutually_distinct holds
card {x1,x2,x3,x4,x5,x6} = 6

proof 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_distinct holds
card {x1,x2,x3,x4,x5,x6,x7} = 7

proof end;

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

theorem :: BORSUK_5:6

for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3 are_mutually_distinct & x4,x5,x6 are_mutually_distinct & {x1,x2,x3} misses {x4,x5,x6} holds
x1,x2,x3,x4,x5,x6 are_mutually_distinct

proof end;

theorem :: BORSUK_5:7

for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6 are_mutually_distinct & {x1,x2,x3,x4,x5,x6} misses {x7} holds
x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct

proof 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_distinct holds
x7,x1,x2,x3,x4,x5,x6 are_mutually_distinct

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_distinct holds
x1,x2,x5,x3,x6,x7,x4 are_mutually_distinct

proof end;

Lm1: R^1 is pathwise_connected

proof 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 b₁ being TopSpace st
( b₁ is connected & not b₁ is empty )

proof end;

end;

theorem :: BORSUK_5:10

for A, B being Subset of R^1
for a, b, c, d being Real st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds
A,B are_separated

proof end;

theorem Th10: :: BORSUK_5:11

for a, b, c being Real st a <= c & c <= b holds
[.a,b.] \/ [.c,+infty.[ = [.a,+infty.[

proof end;

theorem Th11: :: BORSUK_5:12

for a, b, c being Real st a <= c & c <= b holds
].-infty,c.] \/ [.a,b.] = ].-infty,b.]

proof end;

registration

cluster -> real for Element of RAT ;

coherence
for b₁ being Element of RAT holds b₁ 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 st r > 0 holds
Ball (p,r) meets A ) by GOBOARD6:92, TOPMETR:def 6;

theorem Th13: :: BORSUK_5:14

for p, q being Element of RealSpace st q >= p holds
dist (p,q) = q - p

proof end;

theorem Th14: :: BORSUK_5:15

for A being Subset of R^1 st A = RAT holds
Cl A = the carrier of R^1

proof end;

theorem Th15: :: BORSUK_5:16

for A being Subset of R^1
for a, b being Real st A = ].a,b.[ & a <> b holds
Cl A = [.a,b.]

proof end;

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;

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 holds RAT (a,b) = RAT /\ ].a,b.[;

:: deftheorem defines IRRAT BORSUK_5:def 3 :
for a, b being Real holds IRRAT (a,b) = IRRAT /\ ].a,b.[;

theorem Th16: :: BORSUK_5:17

for x being Real holds
( x is irrational iff x in IRRAT )

proof end;

registration

cluster complex real ext-real irrational for object ;

existence
ex b₁ being Real st b₁ is irrational by IRRAT_1:41;

end;

registration

cluster IRRAT -> non empty ;

coherence
not IRRAT is empty by Th16, IRRAT_1:41;

end;

registration

let a be Rational;
let b be irrational Real;

cluster a + b -> irrational ;

coherence
a + b is irrational

proof end;

cluster b + a -> irrational ;

coherence
b + a is irrational ;

end;

theorem :: BORSUK_5:18

for a being Rational
for b being irrational Real holds a + b is irrational ;

registration

let a be irrational Real;

cluster - a -> irrational ;

coherence
- a is irrational

proof end;

end;

theorem :: BORSUK_5:19

for a being irrational Real holds - a is irrational ;

registration

let a be Rational;
let b be irrational Real;

cluster a - b -> irrational ;

coherence
a - b is irrational

proof end;

cluster b - a -> irrational ;

coherence
b - a is irrational

proof end;

end;

theorem :: BORSUK_5:20

for a being Rational
for b being irrational Real holds a - b is irrational ;

theorem :: BORSUK_5:21

for a being Rational
for b being irrational Real holds b - a is irrational ;

theorem Th21: :: BORSUK_5:22

for a being Rational
for b being irrational Real st a <> 0 holds
a * b is irrational

proof end;

theorem Th22: :: BORSUK_5:23

for a being Rational
for b being irrational Real st a <> 0 holds
b / a is irrational

proof end;

registration

cluster real irrational -> non zero for object ;

coherence
for b₁ being Real st b₁ is irrational holds
not b₁ is zero ;

end;

theorem Th23: :: BORSUK_5:24

for a being Rational
for b being irrational Real st a <> 0 holds
a / b is irrational

proof end;

registration

let r be irrational Real;

cluster frac r -> irrational ;

coherence
frac r is irrational

proof end;

end;

theorem :: BORSUK_5:25

for r being irrational Real holds frac r is irrational ;

registration

cluster non zero complex real ext-real non irrational for object ;

existence
not for b₁ being Rational holds b₁ is zero

proof end;

end;

registration

let a be non zero Rational;
let b be irrational Real;

cluster a * b -> irrational ;

coherence
a * b is irrational by Th21;

cluster b * a -> irrational ;

coherence
b * a is irrational ;

cluster a / b -> irrational ;

coherence
a / b is irrational by Th23;

cluster b / a -> irrational ;

coherence
b / a is irrational by Th22;

end;

theorem Th25: :: BORSUK_5:26

for a, b being Real st a < b holds
ex p1, p2 being Rational st
( a < p1 & p1 < p2 & p2 < b )

proof end;

theorem Th26: :: BORSUK_5:27

for a, b being Real st a < b holds
ex p being irrational Real st
( a < p & p < b )

proof end;

theorem Th27: :: BORSUK_5:28

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 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 st a < b & A = IRRAT (a,b) holds
( a in Cl A & b in Cl A )

proof end;

theorem Th28: :: BORSUK_5:29

for a, b, c being Real holds
( c in RAT (a,b) iff ( c is rational & a < c & c < b ) )

proof end;

theorem Th29: :: BORSUK_5:30

for a, b, c being Real holds
( c in IRRAT (a,b) iff ( c is irrational & a < c & c < b ) )

proof end;

theorem Th30: :: BORSUK_5:31

for A being Subset of R^1
for a, b being Real st a < b & A = RAT (a,b) holds
Cl A = [.a,b.]

proof end;

theorem Th31: :: BORSUK_5:32

for A being Subset of R^1
for a, b being Real st a < b & A = IRRAT (a,b) holds
Cl A = [.a,b.]

proof end;

theorem Th32: :: BORSUK_5:33

for T being connected TopSpace
for A being open closed Subset of T holds
( A = {} or A = [#] T )

proof end;

theorem Th33: :: BORSUK_5:34

for A being Subset of R^1 st A is closed & A is open & not A = {} holds
A = REAL

proof end;

theorem Th34: :: BORSUK_5:35

for A being Subset of R^1
for a, b being Real st A = [.a,b.[ & a <> b holds
Cl A = [.a,b.]

proof end;

theorem Th35: :: BORSUK_5:36

for A being Subset of R^1
for a, b being Real st A = ].a,b.] & a <> b holds
Cl A = [.a,b.]

proof end;

theorem :: BORSUK_5:37

for A being Subset of R^1
for a, b, c being Real st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds
Cl A = [.a,c.]

proof end;

theorem Th37: :: BORSUK_5:38

for A being Subset of R^1
for a being Real st A = {a} holds
Cl A = {a}

proof end;

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

Lm4: for a being Real holds ].-infty,a.] is closed

proof end;

Lm5: for a being Real 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:17;

cluster A /\ B -> open for Subset of REAL;

coherence
for b₁ being Subset of REAL st b₁ = A /\ B holds
b₁ is open

proof end;

cluster A \/ B -> open for Subset of REAL;

coherence
for b₁ being Subset of REAL st b₁ = A \/ B holds
b₁ is open

proof end;

end;

Lm6: for a, b being ExtReal holds ].a,b.[ is open

proof end;

theorem Th39: :: BORSUK_5:40

for A being Subset of R^1
for a, b being ExtReal st A = ].a,b.[ holds
A is open

proof end;

theorem Th40: :: BORSUK_5:41

for A being Subset of R^1
for a being Real st A = ].-infty,a.] holds
A is closed

proof end;

theorem Th41: :: BORSUK_5:42

for A being Subset of R^1
for a being Real st A = [.a,+infty.[ holds
A is closed

proof end;

theorem Th42: :: BORSUK_5:43

for a being Real holds [.a,+infty.[ = {a} \/ ].a,+infty.[

proof end;

theorem Th43: :: BORSUK_5:44

for a being Real holds ].-infty,a.] = {a} \/ ].-infty,a.[

proof end;

registration

let a be Real;

cluster K438(a,+infty) -> non empty ;

coherence
not ].a,+infty.[ is empty

proof end;

cluster K437(-infty,a) -> non empty ;

coherence
not ].-infty,a.] is empty by XXREAL_1:234;

cluster K438(-infty,a) -> non empty ;

coherence
not ].-infty,a.[ is empty

proof end;

cluster K436(a,+infty) -> non empty ;

coherence
not [.a,+infty.[ is empty by XXREAL_1:236;

end;

theorem Th44: :: BORSUK_5:45

for a being Real holds ].a,+infty.[ <> REAL by XREAL_0:def 1, XXREAL_1:235;

theorem :: BORSUK_5:46

for a being Real holds [.a,+infty.[ <> REAL

proof end;

theorem :: BORSUK_5:47

for a being Real holds ].-infty,a.] <> REAL

proof end;

theorem Th47: :: BORSUK_5:48

for a being Real holds ].-infty,a.[ <> REAL by XREAL_0:def 1, XXREAL_1:233;

theorem Th48: :: BORSUK_5:49

for A being Subset of R^1
for a being Real st A = ].a,+infty.[ holds
Cl A = [.a,+infty.[

proof end;

theorem :: BORSUK_5:50

for a being Real holds Cl ].a,+infty.[ = [.a,+infty.[

proof end;

theorem Th50: :: BORSUK_5:51

for A being Subset of R^1
for a being Real st A = ].-infty,a.[ holds
Cl A = ].-infty,a.]

proof end;

theorem :: BORSUK_5:52

for a being Real holds Cl ].-infty,a.[ = ].-infty,a.]

proof end;

theorem Th52: :: BORSUK_5:53

for A, B being Subset of R^1
for b being Real st A = ].-infty,b.[ & B = ].b,+infty.[ holds
A,B are_separated

proof end;

theorem :: BORSUK_5:54

for A being Subset of R^1
for a, b being Real st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[

proof end;

theorem Th54: :: BORSUK_5:55

for A being Subset of R^1
for a, b being Real st a < b & A = ].a,b.[ \/ ].b,+infty.[ holds
Cl A = [.a,+infty.[

proof end;

theorem :: BORSUK_5:56

for A being Subset of R^1
for a, b, c being Real st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds
Cl A = [.a,+infty.[

proof end;

theorem Th56: :: BORSUK_5:57

for a, b being Real holds IRRAT (a,b) misses RAT (a,b)

proof end;

theorem Th57: :: BORSUK_5:58

for a, b being Real holds REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[

proof end;

theorem Th58: :: BORSUK_5:59

for a, b being Real st a < b holds
[.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b}

proof 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 end;

theorem :: BORSUK_5:61

for A being Subset of R^1
for a being Real 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 end;

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

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

proof end;

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

proof 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 end;

theorem :: BORSUK_5:63

for A being Subset of R^1
for a, b being Real st a <= b & A = {a} \/ [.b,+infty.[ holds
A ` = ].-infty,a.[ \/ ].a,b.[

proof end;

theorem :: BORSUK_5:64

for A being Subset of R^1
for a, b being Real st a < b & A = ].-infty,a.[ \/ ].a,b.[ holds
Cl A = ].-infty,b.]

proof end;

theorem Th64: :: BORSUK_5:65

for A being Subset of R^1
for a, b being Real st a < b & A = ].-infty,a.[ \/ ].a,b.] holds
Cl A = ].-infty,b.]

proof end;

theorem Th65: :: BORSUK_5:66

for A being Subset of R^1
for a, b, c being Real st a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds
Cl A = ].-infty,c.]

proof end;

theorem :: BORSUK_5:67

for A being Subset of R^1
for a, b, c, d being Real 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:68

for A being Subset of R^1
for a, b being Real st a <= b & A = ].-infty,a.] \/ {b} holds
A ` = ].a,b.[ \/ ].b,+infty.[

proof end;

theorem :: BORSUK_5:69

for a, b being Real holds [.a,+infty.[ \/ {b} <> REAL

proof end;

theorem :: BORSUK_5:70

for a, b being Real holds ].-infty,a.] \/ {b} <> REAL

proof end;

theorem :: BORSUK_5:71

for TS being TopStruct
for A, B being Subset of TS st A <> B holds
A ` <> B `

proof end;

theorem :: BORSUK_5:72

for A being Subset of R^1 st REAL = A ` holds
A = {}

proof end;

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

theorem Th73: :: BORSUK_5:74

for X being compact Subset of R^1
for X9 being Subset of REAL
for x being Real st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )

proof end;

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

theorem Th75: :: BORSUK_5:76

for A being connected Subset of R^1
for a, b, c being Real st a <= b & b <= c & a in A & c in A holds
b in A

proof end;

theorem Th76: :: BORSUK_5:77

for A being connected Subset of R^1
for a, b being Real st a in A & b in A holds
[.a,b.] c= A

proof end;

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

theorem :: BORSUK_5:79

for A being non empty connected compact Subset of R^1 ex a, b being Real st
( a <= b & A = [.a,b.] )

proof end;

registration

let T be TopSpace;

cluster non empty open closed for Element of bool (bool the carrier of T);

existence
ex b₁ being Subset-Family of T st
( b₁ is open & b₁ is closed & not b₁ is empty )

proof end;

end;