:: RCOMP_3 semantic presentation

Lm1: REAL = [#] REAL
by SUBSET_1:def 4;

registration

let X be non empty set ;
cluster [#] X -> non empty ;
coherence by SUBSET_1:def 4;

end;

registration

cluster -> real-membered SubSpace of RealSpace ;
coherence

proof end;

end;

registration

let S be real-membered 1-sorted ;
cluster the carrier of S -> real-membered ;
coherence by BORSUK_6:def 1;

end;

registration

cluster non empty finite real-membered bounded_above bounded_below set ;
existence

proof end;

end;

theorem Th1: :: RCOMP_3:1

for X being non empty real-membered bounded_below set
for Y being closed Subset of REAL st X c= Y holds
inf X in Y

proof end;

theorem Th2: :: RCOMP_3:2

for X being non empty real-membered bounded_above set
for Y being closed Subset of REAL st X c= Y holds
sup X in Y

proof end;

theorem Th3: :: RCOMP_3:3

for X, Y being Subset of REAL holds Cl (X \/ Y) = (Cl X) \/ (Cl Y)

proof end;

registration

let r, s be real number ;
cluster [.r,s.[ -> bounded ;
coherence

proof end;

cluster ].r,s.] -> bounded ;
coherence

proof end;

cluster ].r,s.[ -> bounded ;
coherence

proof end;

end;

registration

let r, s be real number ;
cluster [.r,s.] -> connected ;
coherence

proof end;

cluster [.r,s.[ -> bounded connected ;
coherence

proof end;

cluster ].r,s.] -> bounded connected ;
coherence

proof end;

cluster ].r,s.[ -> bounded connected ;
coherence

proof end;

end;

registration

cluster non empty bounded open connected Element of K10(REAL );
existence

proof end;

end;

theorem Th4: :: RCOMP_3:4

for r, s being real number st r < s holds
inf [.r,s.[ = r

proof end;

theorem Th5: :: RCOMP_3:5

for r, s being real number st r < s holds
sup [.r,s.[ = s

proof end;

theorem Th6: :: RCOMP_3:6

for r, s being real number st r < s holds
inf ].r,s.] = r

proof end;

theorem Th7: :: RCOMP_3:7

for r, s being real number st r < s holds
sup ].r,s.] = s

proof end;

theorem :: RCOMP_3:8

for a, b, r, s being real number st ( a <= b or r <= s ) & [.a,b.] = [.r,s.] holds
( a = r & b = s )

proof end;

theorem :: RCOMP_3:9

for a, b, r, s being real number st ( a < b or r < s ) & ].a,b.[ = ].r,s.[ holds
( a = r & b = s )

proof end;

theorem :: RCOMP_3:10

for a, b, r, s being real number st ( a < b or r < s ) & ].a,b.] = ].r,s.] holds
( a = r & b = s )

proof end;

theorem :: RCOMP_3:11

for a, b, r, s being real number st ( a < b or r < s ) & [.a,b.[ = [.r,s.[ holds
( a = r & b = s )

proof end;

theorem Th12: :: RCOMP_3:12

for a, b, r, s being real number st a < b & [.a,b.[ c= [.r,s.] holds
( r <= a & b <= s )

proof end;

theorem :: RCOMP_3:13

for a, b, r, s being real number st a < b & [.a,b.[ c= [.r,s.[ holds
( r <= a & b <= s )

proof end;

theorem Th14: :: RCOMP_3:14

for a, b, r, s being real number st a < b & ].a,b.] c= [.r,s.] holds
( r <= a & b <= s )

proof end;

theorem :: RCOMP_3:15

for a, b, r, s being real number st a < b & ].a,b.] c= ].r,s.] holds
( r <= a & b <= s )

proof end;

theorem Th16: :: RCOMP_3:16

for a, b being real number holds [.a,b.] ` = (left_open_halfline a) \/ (right_open_halfline b)

proof end;

theorem Th17: :: RCOMP_3:17

for a, b being real number holds ].a,b.[ ` = (left_closed_halfline a) \/ (right_closed_halfline b)

proof end;

theorem Th18: :: RCOMP_3:18

for a, b being real number holds [.a,b.[ ` = (left_open_halfline a) \/ (right_closed_halfline b)

proof end;

theorem Th19: :: RCOMP_3:19

for a, b being real number holds ].a,b.] ` = (left_closed_halfline a) \/ (right_open_halfline b)

proof end;

theorem Th20: :: RCOMP_3:20

for a, b being real number st a <= b holds
[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}

proof end;

Lm2: now

let a be real number ; :: thesis:
assume left_open_halfline a is bounded_below ; :: thesis:
then consider b being real number such that
A1: for r being real number st r in left_open_halfline a holds
b <= r by SEQ_4:def 2;
A2: a - 1 < a - 0 by XREAL_1:17;
then a - 1 in left_open_halfline a by BORSUK_5:17;
then b <= a - 1 by A1;
then b - 1 < (a - 1) - 0 by XREAL_1:17;
then b - 1 < a by A2, XREAL_1:2;
then b - 1 in left_open_halfline a by BORSUK_5:17;
then b - 0 <= b - 1 by A1;
hence contradiction by XREAL_1:17; :: thesis:

end;

Lm3: now

let a be real number ; :: thesis:
assume right_open_halfline a is bounded_above ; :: thesis:
then consider b being real number such that
A1: for r being real number st r in right_open_halfline a holds
r <= b by SEQ_4:def 1;
A2: a + 0 < a + 1 by XREAL_1:8;
then a + 1 in right_open_halfline a by BORSUK_5:14;
then a + 1 <= b by A1;
then (a + 1) + 0 <= b + 1 by XREAL_1:9;
then a < b + 1 by A2, XREAL_1:2;
then b + 1 in right_open_halfline a by BORSUK_5:14;
then b + 1 <= b + 0 by A1;
hence contradiction by XREAL_1:8; :: thesis:

end;

registration

let a be real number ;
cluster left_closed_halfline a -> bounded_above non bounded_below connected ;
coherence

proof end;

cluster left_open_halfline a -> bounded_above non bounded_below connected ;
coherence

proof end;

cluster right_closed_halfline a -> non bounded_above bounded_below connected ;
coherence

proof end;

cluster right_open_halfline a -> non bounded_above bounded_below connected ;
coherence

proof end;

end;

theorem Th21: :: RCOMP_3:21

for a being real number holds sup (left_closed_halfline a) = a

proof end;

theorem Th22: :: RCOMP_3:22

for a being real number holds sup (left_open_halfline a) = a

proof end;

theorem Th23: :: RCOMP_3:23

for a being real number holds inf (right_closed_halfline a) = a

proof end;

theorem Th24: :: RCOMP_3:24

for a being real number holds inf (right_open_halfline a) = a

proof end;

registration

cluster [#] REAL -> non empty non bounded_above non bounded_below connected ;
coherence

proof end;

end;

theorem Th25: :: RCOMP_3:25

for X being bounded connected Subset of REAL st inf X in X & sup X in X holds
X = [.(inf X),(sup X).]

proof end;

theorem Th26: :: RCOMP_3:26

for X being bounded Subset of REAL st not inf X in X holds
X c= ].(inf X),(sup X).]

proof end;

theorem Th27: :: RCOMP_3:27

for X being bounded connected Subset of REAL st not inf X in X & sup X in X holds
X = ].(inf X),(sup X).]

proof end;

theorem Th28: :: RCOMP_3:28

for X being bounded Subset of REAL st not sup X in X holds
X c= [.(inf X),(sup X).[

proof end;

theorem Th29: :: RCOMP_3:29

for X being bounded connected Subset of REAL st inf X in X & not sup X in X holds
X = [.(inf X),(sup X).[

proof end;

theorem Th30: :: RCOMP_3:30

for X being bounded Subset of REAL st not inf X in X & not sup X in X holds
X c= ].(inf X),(sup X).[

proof end;

theorem Th31: :: RCOMP_3:31

for X being non empty bounded connected Subset of REAL st not inf X in X & not sup X in X holds
X = ].(inf X),(sup X).[

proof end;

theorem Th32: :: RCOMP_3:32

for X being Subset of REAL st X is bounded_above holds
X c= left_closed_halfline (sup X)

proof end;

theorem Th33: :: RCOMP_3:33

for X being connected Subset of REAL st not X is bounded_below & X is bounded_above & sup X in X holds
X = left_closed_halfline (sup X)

proof end;

theorem Th34: :: RCOMP_3:34

for X being Subset of REAL st X is bounded_above & not sup X in X holds
X c= left_open_halfline (sup X)

proof end;

theorem Th35: :: RCOMP_3:35

for X being non empty connected Subset of REAL st not X is bounded_below & X is bounded_above & not sup X in X holds
X = left_open_halfline (sup X)

proof end;

theorem Th36: :: RCOMP_3:36

for X being Subset of REAL st X is bounded_below holds
X c= right_closed_halfline (inf X)

proof end;

theorem Th37: :: RCOMP_3:37

for X being connected Subset of REAL st X is bounded_below & not X is bounded_above & inf X in X holds
X = right_closed_halfline (inf X)

proof end;

theorem Th38: :: RCOMP_3:38

for X being Subset of REAL st X is bounded_below & not inf X in X holds
X c= right_open_halfline (inf X)

proof end;

theorem Th39: :: RCOMP_3:39

for X being non empty connected Subset of REAL st X is bounded_below & not X is bounded_above & not inf X in X holds
X = right_open_halfline (inf X)

proof end;

theorem Th40: :: RCOMP_3:40

for X being connected Subset of REAL st not X is bounded_above & not X is bounded_below holds
X = REAL

proof end;

theorem Th41: :: RCOMP_3:41

for X being connected Subset of REAL holds
( X is empty or X = REAL or ex a being real number st X = left_closed_halfline a or ex a being real number st X = left_open_halfline a or ex a being real number st X = right_closed_halfline a or ex a being real number st X = right_open_halfline a or ex a, b being real number st
( a <= b & X = [.a,b.] ) or ex a, b being real number st
( a < b & X = [.a,b.[ ) or ex a, b being real number st
( a < b & X = ].a,b.] ) or ex a, b being real number st
( a < b & X = ].a,b.[ ) )

proof end;

theorem Th42: :: RCOMP_3:42

for r being real number
for X being non empty connected Subset of REAL holds
( r in X or r <= inf X or sup X <= r )

proof end;

theorem Th43: :: RCOMP_3:43

for X, Y being non empty bounded connected Subset of REAL st inf X <= inf Y & sup Y <= sup X & ( inf X = inf Y & inf Y in Y implies inf X in X ) & ( sup X = sup Y & sup Y in Y implies sup X in X ) holds
Y c= X

proof end;

registration

cluster non empty non bounded closed open connected Element of K10(REAL );
existence

proof end;

end;

theorem Th44: :: RCOMP_3:44

for a, b being real number
for X being Subset of R^1 st a <= b & X = [.a,b.] holds
Fr X = {a,b}

proof end;

theorem :: RCOMP_3:45

for a, b being real number
for X being Subset of R^1 st a < b & X = ].a,b.[ holds
Fr X = {a,b}

proof end;

theorem Th46: :: RCOMP_3:46

for a, b being real number
for X being Subset of R^1 st a < b & X = [.a,b.[ holds
Fr X = {a,b}

proof end;

theorem Th47: :: RCOMP_3:47

for a, b being real number
for X being Subset of R^1 st a < b & X = ].a,b.] holds
Fr X = {a,b}

proof end;

theorem :: RCOMP_3:48

for a, b being real number
for X being Subset of R^1 st X = [.a,b.] holds
Int X = ].a,b.[

proof end;

theorem :: RCOMP_3:49

for a, b being real number
for X being Subset of R^1 st X = ].a,b.[ holds
Int X = ].a,b.[

proof end;

theorem Th50: :: RCOMP_3:50

for a, b being real number
for X being Subset of R^1 st X = [.a,b.[ holds
Int X = ].a,b.[

proof end;

theorem Th51: :: RCOMP_3:51

for a, b being real number
for X being Subset of R^1 st X = ].a,b.] holds
Int X = ].a,b.[

proof end;

registration

let X be convex Subset of R^1 ;
cluster R^1 | X -> convex ;
coherence

proof end;

end;

registration

let A be connected Subset of REAL ;
cluster R^1 A -> convex ;
coherence

proof end;

end;

theorem Th52: :: RCOMP_3:52

for X being Subset of R^1
for Y being Subset of REAL st X = Y holds
( X is connected iff Y is connected )

proof end;

registration

let r be real number ;
cluster Closed-Interval-TSpace r,r -> trivial ;
coherence

proof end;

end;

theorem :: RCOMP_3:53

for r, s being real number st r <= s holds
for A being Subset of (Closed-Interval-TSpace r,s) holds A is bounded Subset of REAL

proof end;

theorem Th54: :: RCOMP_3:54

for r, s, a, b being real number st r <= s holds
for X being Subset of (Closed-Interval-TSpace r,s) st X = [.a,b.[ & r < a & b <= s holds
Int X = ].a,b.[

proof end;

theorem Th55: :: RCOMP_3:55

for r, s, a, b being real number st r <= s holds
for X being Subset of (Closed-Interval-TSpace r,s) st X = ].a,b.] & r <= a & b < s holds
Int X = ].a,b.[

proof end;

theorem Th56: :: RCOMP_3:56

for r, s being real number
for X being Subset of (Closed-Interval-TSpace r,s)
for Y being Subset of REAL st X = Y holds
( X is connected iff Y is connected )

proof end;

registration

let T be TopSpace;
cluster open closed connected Element of K10(the carrier of T);
existence

proof end;

end;

registration

let T be non empty connected TopSpace;
cluster non empty open closed connected Element of K10(the carrier of T);
existence

proof end;

end;

theorem Th57: :: RCOMP_3:57

for r, s being real number st r <= s holds
for X being open connected Subset of (Closed-Interval-TSpace r,s) holds
( X is empty or X = [.r,s.] or ex a being real number st
( r < a & a <= s & X = [.r,a.[ ) or ex a being real number st
( r <= a & a < s & X = ].a,s.] ) or ex a, b being real number st
( r <= a & a < b & b <= s & X = ].a,b.[ ) )

proof end;

deffunc H₁( set ) -> set = $1;

defpred S₁[ set , set ] means $1 c= $2;

theorem Th58: :: RCOMP_3:58

for T being 1-sorted
for F being Subset-Family of T holds
( F is_a_cover_of T iff F is_a_cover_of [#] T )

proof end;

theorem Th59: :: RCOMP_3:59

for T being 1-sorted
for F being finite Subset-Family of T
for F1 being Subset-Family of T st F is_a_cover_of T & F1 = F \ { X where X is Subset of T : ( X in F & ex Y being Subset of T st
( Y in F & X c= Y & X <> Y ) ) } holds
F1 is_a_cover_of T

proof end;

theorem Th60: :: RCOMP_3:60

for S being non empty trivial 1-sorted
for s being Point of S
for F being Subset-Family of S st F is_a_cover_of S holds
{s} in F

proof end;

definition

let T be TopStruct ;
let F be Subset-Family of T;
attr F is connected means :Def1: :: RCOMP_3:def 1
for X being Subset of T st X in F holds
X is connected;

end;

:: deftheorem Def1 defines connected RCOMP_3:def 1 :

registration

let T be TopSpace;
cluster non empty open closed connected Element of K10(K10(the carrier of T));
existence

proof end;

end;

Lm4: for r, s being real number
for F being Subset-Family of (Closed-Interval-TSpace r,s) st [.r,s.] in F & r <= s holds
( rng <*[.r,s.]*> c= F & union (rng <*[.r,s.]*>) = [.r,s.] & ( for n being natural number st 1 <= n holds
( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( inf (<*[.r,s.]*> /. n) <= inf (<*[.r,s.]*> /. (n + 1)) & sup (<*[.r,s.]*> /. n) <= sup (<*[.r,s.]*> /. (n + 1)) & inf (<*[.r,s.]*> /. (n + 1)) < sup (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies sup (<*[.r,s.]*> /. n) <= inf (<*[.r,s.]*> /. (n + 2)) ) ) ) )

proof end;

theorem Th61: :: RCOMP_3:61

for L being TopSpace
for G, G1 being Subset-Family of L st G is_a_cover_of L & G is finite holds
for ALL being set st G1 = G \ { X where X is Subset of L : ( X in G & ex Y being Subset of L st
( Y in G & X c= Y & X <> Y ) ) } & ALL = { C where C is Subset-Family of L : ( C is_a_cover_of L & C c= G1 ) } holds
ALL has_lower_Zorn_property_wrt RelIncl ALL

proof end;

theorem Th62: :: RCOMP_3:62

for L being TopSpace
for G, ALL being set st ALL = { C where C is Subset-Family of L : ( C is_a_cover_of L & C c= G ) } holds
for M being set st M is_minimal_in RelIncl ALL & M in field (RelIncl ALL) holds
for A1 being Subset of L st A1 in M holds
for A2, A3 being Subset of L holds
( not A2 in M or not A3 in M or not A1 c= A2 \/ A3 or not A1 <> A2 or not A1 <> A3 )

proof end;

definition

let r, s be real number ;
let F be Subset-Family of (Closed-Interval-TSpace r,s);
assume that
A1: F is_a_cover_of Closed-Interval-TSpace r,s and
A2: F is open and
A3: F is connected and
A4: r <= s ;
mode IntervalCover of F -> FinSequence of bool REAL means :Def2: :: RCOMP_3:def 2
( rng it c= F & union (rng it) = [.r,s.] & ( for n being natural number st 1 <= n holds
( ( n <= len it implies not it /. n is empty ) & ( n + 1 <= len it implies ( inf (it /. n) <= inf (it /. (n + 1)) & sup (it /. n) <= sup (it /. (n + 1)) & inf (it /. (n + 1)) < sup (it /. n) ) ) & ( n + 2 <= len it implies sup (it /. n) <= inf (it /. (n + 2)) ) ) ) & ( [.r,s.] in F implies it = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being real number st
( r < p & p <= s & it . 1 = [.r,p.[ ) & ex p being real number st
( r <= p & p < s & it . (len it) = ].p,s.] ) & ( for n being natural number st 1 < n & n < len it holds
ex p, q being real number st
( r <= p & p < q & q <= s & it . n = ].p,q.[ ) ) ) ) );
existence

proof end;

end;

:: deftheorem Def2 defines IntervalCover RCOMP_3:def 2 :

theorem :: RCOMP_3:63

for r, s being real number
for F being Subset-Family of (Closed-Interval-TSpace r,s) st F is_a_cover_of Closed-Interval-TSpace r,s & F is open & F is connected & r <= s & [.r,s.] in F holds
<*[.r,s.]*> is IntervalCover of F

proof end;

theorem Th64: :: RCOMP_3:64

for r being real number
for F being Subset-Family of (Closed-Interval-TSpace r,r)
for C being IntervalCover of F st F is_a_cover_of Closed-Interval-TSpace r,r & F is open & F is connected holds
C = <*[.r,r.]*>

proof end;

theorem Th65: :: RCOMP_3:65

for r, s being real number
for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F st F is_a_cover_of Closed-Interval-TSpace r,s & F is open & F is connected & r <= s holds
1 <= len C

proof end;

theorem Th66: :: RCOMP_3:66

proof end;

theorem :: RCOMP_3:67

for r, s being real number
for n, m being natural number
for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F st F is_a_cover_of Closed-Interval-TSpace r,s & F is open & F is connected & r <= s & n in dom C & m in dom C & n < m holds
inf (C /. n) <= inf (C /. m)

proof end;

theorem :: RCOMP_3:68

proof end;

theorem Th69: :: RCOMP_3:69

for r, s being real number
for n being natural number
for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F st F is_a_cover_of Closed-Interval-TSpace r,s & F is open & F is connected & r <= s & 1 <= n & n + 1 <= len C holds
not ].(inf (C /. (n + 1))),(sup (C /. n)).[ is empty

proof end;

theorem :: RCOMP_3:70

proof end;

theorem Th71: :: RCOMP_3:71

proof end;

theorem :: RCOMP_3:72

proof end;

theorem Th73: :: RCOMP_3:73

proof end;

definition

let r, s be real number ;
let F be Subset-Family of (Closed-Interval-TSpace r,s);
let C be IntervalCover of F;
assume that
A1: F is_a_cover_of Closed-Interval-TSpace r,s and
A2: F is open and
A3: F is connected and
A4: r <= s ;
mode IntervalCoverPts of C -> FinSequence of REAL means :Def3: :: RCOMP_3:def 3
( len it = (len C) + 1 & it . 1 = r & it . (len it) = s & ( for n being natural number st 1 <= n & n + 1 < len it holds
it . (n + 1) in ].(inf (C /. (n + 1))),(sup (C /. n)).[ ) );
existence

proof end;

end;

:: deftheorem Def3 defines IntervalCoverPts RCOMP_3:def 3 :

theorem Th74: :: RCOMP_3:74

for r, s being real number
for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is_a_cover_of Closed-Interval-TSpace r,s & F is open & F is connected & r <= s holds
2 <= len G

proof end;

theorem Th75: :: RCOMP_3:75

proof end;

theorem Th76: :: RCOMP_3:76

for r, s being real number
for n being natural number
for F being Subset-Family of (Closed-Interval-TSpace r,s)
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is_a_cover_of Closed-Interval-TSpace r,s & F is open & F is connected & r <= s & 1 <= n & n + 1 < len G holds
G . (n + 1) < sup (C /. n)

proof end;

theorem Th77: :: RCOMP_3:77

proof end;

theorem Th78: :: RCOMP_3:78

proof end;

theorem Th79: :: RCOMP_3:79

proof end;

theorem :: RCOMP_3:80

proof end;