:: by Artur Korni{\l}owicz

::

:: Received February 22, 2005

:: Copyright (c) 2005-2019 Association of Mizar Users

registration
end;

registration
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

lower_bound X in Y

for Y being closed Subset of REAL st X c= Y holds

lower_bound 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

upper_bound X in Y

for Y being closed Subset of REAL st X c= Y holds

upper_bound X in Y

proof end;

registration

let r be Real;

let s be ExtReal;

coherence

[.r,s.[ is bounded_below

].s,r.] is bounded_above

end;
let s be ExtReal;

coherence

[.r,s.[ is bounded_below

proof end;

coherence ].s,r.] is bounded_above

proof end;

registration

let r, s be Real;

coherence

[.r,s.[ is real-bounded

].r,s.] is real-bounded

].r,s.[ is real-bounded

end;
coherence

[.r,s.[ is real-bounded

proof end;

coherence ].r,s.] is real-bounded

proof end;

coherence ].r,s.[ is real-bounded

proof end;

registration

ex b_{1} being Subset of REAL st

( b_{1} is open & b_{1} is real-bounded & b_{1} is interval & not b_{1} is empty )
end;

cluster non empty complex-membered ext-real-membered real-membered open real-bounded interval for Element of K34(REAL);

existence ex b

( b

proof end;

theorem Th8: :: RCOMP_3:8

for a, b being Real st a <= b holds

[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}

[.a,b.] /\ ((left_closed_halfline a) \/ (right_closed_halfline b)) = {a,b}

proof end;

Lm1: now :: thesis: for a being Real holds not left_open_halfline a is bounded_below

let a be Real; :: thesis: not left_open_halfline a is bounded_below

assume left_open_halfline a is bounded_below ; :: thesis: contradiction

then consider b being Real such that

A1: b is LowerBound of left_open_halfline a ;

A2: for r being Real st r in left_open_halfline a holds

b <= r by A1, XXREAL_2:def 2;

A3: a - 1 < a - 0 by XREAL_1:15;

then a - 1 in left_open_halfline a by XXREAL_1:233;

then b - 1 < (a - 1) - 0 by A2, XREAL_1:15;

then b - 1 < a by A3, XXREAL_0:2;

then b - 1 in left_open_halfline a by XXREAL_1:233;

then b - 0 <= b - 1 by A1, XXREAL_2:def 2;

hence contradiction by XREAL_1:15; :: thesis: verum

end;
assume left_open_halfline a is bounded_below ; :: thesis: contradiction

then consider b being Real such that

A1: b is LowerBound of left_open_halfline a ;

A2: for r being Real st r in left_open_halfline a holds

b <= r by A1, XXREAL_2:def 2;

A3: a - 1 < a - 0 by XREAL_1:15;

then a - 1 in left_open_halfline a by XXREAL_1:233;

then b - 1 < (a - 1) - 0 by A2, XREAL_1:15;

then b - 1 < a by A3, XXREAL_0:2;

then b - 1 in left_open_halfline a by XXREAL_1:233;

then b - 0 <= b - 1 by A1, XXREAL_2:def 2;

hence contradiction by XREAL_1:15; :: thesis: verum

Lm2: now :: thesis: for a being Real holds not right_open_halfline a is bounded_above

let a be Real; :: thesis: not right_open_halfline a is bounded_above

assume right_open_halfline a is bounded_above ; :: thesis: contradiction

then consider b being Real such that

A1: b is UpperBound of right_open_halfline a ;

A2: a + 0 < a + 1 by XREAL_1:6;

then a + 1 in right_open_halfline a by XXREAL_1:235;

then a + 1 <= b by A1, XXREAL_2:def 1;

then (a + 1) + 0 <= b + 1 by XREAL_1:7;

then a < b + 1 by A2, XXREAL_0:2;

then b + 1 in right_open_halfline a by XXREAL_1:235;

then b + 1 <= b + 0 by A1, XXREAL_2:def 1;

hence contradiction by XREAL_1:6; :: thesis: verum

end;
assume right_open_halfline a is bounded_above ; :: thesis: contradiction

then consider b being Real such that

A1: b is UpperBound of right_open_halfline a ;

A2: a + 0 < a + 1 by XREAL_1:6;

then a + 1 in right_open_halfline a by XXREAL_1:235;

then a + 1 <= b by A1, XXREAL_2:def 1;

then (a + 1) + 0 <= b + 1 by XREAL_1:7;

then a < b + 1 by A2, XXREAL_0:2;

then b + 1 in right_open_halfline a by XXREAL_1:235;

then b + 1 <= b + 0 by A1, XXREAL_2:def 1;

hence contradiction by XREAL_1:6; :: thesis: verum

registration

let a be Real;

coherence

( not left_closed_halfline a is bounded_below & left_closed_halfline a is bounded_above & left_closed_halfline a is interval )

( not left_open_halfline a is bounded_below & left_open_halfline a is bounded_above & left_open_halfline a is interval )

( right_closed_halfline a is bounded_below & not right_closed_halfline a is bounded_above & right_closed_halfline a is interval )

( right_open_halfline a is bounded_below & not right_open_halfline a is bounded_above & right_open_halfline a is interval )

end;
coherence

( not left_closed_halfline a is bounded_below & left_closed_halfline a is bounded_above & left_closed_halfline a is interval )

proof end;

coherence ( not left_open_halfline a is bounded_below & left_open_halfline a is bounded_above & left_open_halfline a is interval )

proof end;

coherence ( right_closed_halfline a is bounded_below & not right_closed_halfline a is bounded_above & right_closed_halfline a is interval )

proof end;

coherence ( right_open_halfline a is bounded_below & not right_open_halfline a is bounded_above & right_open_halfline a is interval )

proof end;

registration

coherence

( [#] REAL is interval & not [#] REAL is bounded_below & not [#] REAL is bounded_above ) ;

end;
( [#] REAL is interval & not [#] REAL is bounded_below & not [#] REAL is bounded_above ) ;

theorem Th13: :: RCOMP_3:13

for X being real-bounded interval Subset of REAL st lower_bound X in X & upper_bound X in X holds

X = [.(lower_bound X),(upper_bound X).]

X = [.(lower_bound X),(upper_bound X).]

proof end;

theorem Th14: :: RCOMP_3:14

for X being real-bounded Subset of REAL st not lower_bound X in X holds

X c= ].(lower_bound X),(upper_bound X).]

X c= ].(lower_bound X),(upper_bound X).]

proof end;

theorem Th15: :: RCOMP_3:15

for X being real-bounded interval Subset of REAL st not lower_bound X in X & upper_bound X in X holds

X = ].(lower_bound X),(upper_bound X).]

X = ].(lower_bound X),(upper_bound X).]

proof end;

theorem Th16: :: RCOMP_3:16

for X being real-bounded Subset of REAL st not upper_bound X in X holds

X c= [.(lower_bound X),(upper_bound X).[

X c= [.(lower_bound X),(upper_bound X).[

proof end;

theorem Th17: :: RCOMP_3:17

for X being real-bounded interval Subset of REAL st lower_bound X in X & not upper_bound X in X holds

X = [.(lower_bound X),(upper_bound X).[

X = [.(lower_bound X),(upper_bound X).[

proof end;

theorem Th18: :: RCOMP_3:18

for X being real-bounded Subset of REAL st not lower_bound X in X & not upper_bound X in X holds

X c= ].(lower_bound X),(upper_bound X).[

X c= ].(lower_bound X),(upper_bound X).[

proof end;

theorem Th19: :: RCOMP_3:19

for X being non empty real-bounded interval Subset of REAL st not lower_bound X in X & not upper_bound X in X holds

X = ].(lower_bound X),(upper_bound X).[

X = ].(lower_bound X),(upper_bound X).[

proof end;

theorem Th21: :: RCOMP_3:21

for X being interval Subset of REAL st not X is bounded_below & X is bounded_above & upper_bound X in X holds

X = left_closed_halfline (upper_bound X)

X = left_closed_halfline (upper_bound X)

proof end;

theorem Th22: :: RCOMP_3:22

for X being Subset of REAL st X is bounded_above & not upper_bound X in X holds

X c= left_open_halfline (upper_bound X)

X c= left_open_halfline (upper_bound X)

proof end;

theorem Th23: :: RCOMP_3:23

for X being non empty interval Subset of REAL st not X is bounded_below & X is bounded_above & not upper_bound X in X holds

X = left_open_halfline (upper_bound X)

X = left_open_halfline (upper_bound X)

proof end;

theorem Th25: :: RCOMP_3:25

for X being interval Subset of REAL st X is bounded_below & not X is bounded_above & lower_bound X in X holds

X = right_closed_halfline (lower_bound X)

X = right_closed_halfline (lower_bound X)

proof end;

theorem Th26: :: RCOMP_3:26

for X being Subset of REAL st X is bounded_below & not lower_bound X in X holds

X c= right_open_halfline (lower_bound X)

X c= right_open_halfline (lower_bound X)

proof end;

theorem Th27: :: RCOMP_3:27

for X being non empty interval Subset of REAL st X is bounded_below & not X is bounded_above & not lower_bound X in X holds

X = right_open_halfline (lower_bound X)

X = right_open_halfline (lower_bound X)

proof end;

theorem Th28: :: RCOMP_3:28

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

X = REAL

X = REAL

proof end;

theorem Th29: :: RCOMP_3:29

for X being interval Subset of REAL holds

( X is empty or X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st

( a <= b & X = [.a,b.] ) or ex a, b being Real st

( a < b & X = [.a,b.[ ) or ex a, b being Real st

( a < b & X = ].a,b.] ) or ex a, b being Real st

( a < b & X = ].a,b.[ ) )

( X is empty or X = REAL or ex a being Real st X = left_closed_halfline a or ex a being Real st X = left_open_halfline a or ex a being Real st X = right_closed_halfline a or ex a being Real st X = right_open_halfline a or ex a, b being Real st

( a <= b & X = [.a,b.] ) or ex a, b being Real st

( a < b & X = [.a,b.[ ) or ex a, b being Real st

( a < b & X = ].a,b.] ) or ex a, b being Real st

( a < b & X = ].a,b.[ ) )

proof end;

theorem Th30: :: RCOMP_3:30

for r being Real

for X being non empty interval Subset of REAL holds

( r in X or r <= lower_bound X or upper_bound X <= r )

for X being non empty interval Subset of REAL holds

( r in X or r <= lower_bound X or upper_bound X <= r )

proof end;

theorem Th31: :: RCOMP_3:31

for X, Y being non empty real-bounded interval Subset of REAL st lower_bound X <= lower_bound Y & upper_bound Y <= upper_bound X & ( lower_bound X = lower_bound Y & lower_bound Y in Y implies lower_bound X in X ) & ( upper_bound X = upper_bound Y & upper_bound Y in Y implies upper_bound X in X ) holds

Y c= X

Y c= X

proof end;

registration

ex b_{1} being Subset of REAL st

( b_{1} is open & b_{1} is closed & b_{1} is interval & not b_{1} is empty & not b_{1} is real-bounded )
end;

cluster non empty complex-membered ext-real-membered real-membered closed open non real-bounded interval for Element of K34(REAL);

existence ex b

( b

proof end;

registration

let T be real-membered TopStruct ;

let X be interval Subset of T;

coherence

T | X is interval by PRE_TOPC:def 5;

end;
let X be interval Subset of T;

coherence

T | X is interval by PRE_TOPC:def 5;

registration

coherence

for b_{1} being Subset of R^1 st b_{1} is connected holds

b_{1} is interval
by BORSUK_5:77;

coherence

for b_{1} being Subset of R^1 st b_{1} is interval holds

b_{1} is connected

end;
for b

b

coherence

for b

b

proof end;

theorem :: RCOMP_3:40

for r, s being Real st r <= s holds

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

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

proof end;

theorem Th41: :: RCOMP_3:41

for a, b, r, s being Real 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.[

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 Th42: :: RCOMP_3:42

for a, b, r, s being Real 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.[

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 Th43: :: RCOMP_3:43

for r, s being Real

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 interval )

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 interval )

proof end;

registration

let T be TopSpace;

existence

ex b_{1} being Subset of T st

( b_{1} is open & b_{1} is closed & b_{1} is connected )

end;
existence

ex b

( b

proof end;

registration

let T be non empty connected TopSpace;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is open & b_{1} is closed & b_{1} is connected )

end;
existence

ex b

( not b

proof end;

theorem Th44: :: RCOMP_3:44

for r, s being Real 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 st

( r < a & a <= s & X = [.r,a.[ ) or ex a being Real st

( r <= a & a < s & X = ].a,s.] ) or ex a, b being Real st

( r <= a & a < b & b <= s & X = ].a,b.[ ) )

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 st

( r < a & a <= s & X = [.r,a.[ ) or ex a being Real st

( r <= a & a < s & X = ].a,s.] ) or ex a, b being Real st

( r <= a & a < b & b <= s & X = ].a,b.[ ) )

proof end;

deffunc H

defpred S

theorem Th45: :: RCOMP_3:45

for T being 1-sorted

for F being finite Subset-Family of T

for F1 being Subset-Family of T st F is 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 ) ) } holds

F1 is Cover of T

for F being finite Subset-Family of T

for F1 being Subset-Family of T st F is 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 ) ) } holds

F1 is Cover of T

proof end;

theorem Th46: :: RCOMP_3:46

for S being 1 -element 1-sorted

for s being Point of S

for F being Subset-Family of S st F is Cover of S holds

{s} in F

for s being Point of S

for F being Subset-Family of S st F is Cover of S holds

{s} in F

proof end;

:: deftheorem defines connected RCOMP_3:def 1 :

for T being TopStruct

for F being Subset-Family of T holds

( F is connected iff for X being Subset of T st X in F holds

X is connected );

for T being TopStruct

for F being Subset-Family of T holds

( F is connected iff for X being Subset of T st X in F holds

X is connected );

registration

let T be TopSpace;

existence

ex b_{1} being Subset-Family of T st

( not b_{1} is empty & b_{1} is open & b_{1} is closed & b_{1} is connected )

end;
existence

ex b

( not b

proof end;

Lm3: for r, s being Real

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 Nat st 1 <= n holds

( ( n <= len <*[.r,s.]*> implies not <*[.r,s.]*> /. n is empty ) & ( n + 1 <= len <*[.r,s.]*> implies ( lower_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 1)) & upper_bound (<*[.r,s.]*> /. n) <= upper_bound (<*[.r,s.]*> /. (n + 1)) & lower_bound (<*[.r,s.]*> /. (n + 1)) < upper_bound (<*[.r,s.]*> /. n) ) ) & ( n + 2 <= len <*[.r,s.]*> implies upper_bound (<*[.r,s.]*> /. n) <= lower_bound (<*[.r,s.]*> /. (n + 2)) ) ) ) )

proof end;

theorem Th47: :: RCOMP_3:47

for L being TopSpace

for G, G1 being Subset-Family of L st G is 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 ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } holds

ALL has_lower_Zorn_property_wrt RelIncl ALL

for G, G1 being Subset-Family of L st G is 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 ) ) } & ALL = { C where C is Subset-Family of L : ( C is Cover of L & C c= G1 ) } holds

ALL has_lower_Zorn_property_wrt RelIncl ALL

proof end;

theorem Th48: :: RCOMP_3:48

for L being TopSpace

for G, ALL being set st ALL = { C where C is Subset-Family of L : ( C is 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 )

for G, ALL being set st ALL = { C where C is Subset-Family of L : ( C is 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;

registration

let X be Subset-Family of REAL;

coherence

for b_{1} being Element of X holds b_{1} is real-membered

end;
coherence

for b

proof end;

definition

let r, s be Real;

let F be Subset-Family of (Closed-Interval-TSpace (r,s));

assume that

A1: F is Cover of (Closed-Interval-TSpace (r,s)) and

A2: F is open and

A3: F is connected and

A4: r <= s ;

ex b_{1} being FinSequence of bool REAL st

( rng b_{1} c= F & union (rng b_{1}) = [.r,s.] & ( for n being Nat st 1 <= n holds

( ( n <= len b_{1} implies not b_{1} /. n is empty ) & ( n + 1 <= len b_{1} implies ( lower_bound (b_{1} /. n) <= lower_bound (b_{1} /. (n + 1)) & upper_bound (b_{1} /. n) <= upper_bound (b_{1} /. (n + 1)) & lower_bound (b_{1} /. (n + 1)) < upper_bound (b_{1} /. n) ) ) & ( n + 2 <= len b_{1} implies upper_bound (b_{1} /. n) <= lower_bound (b_{1} /. (n + 2)) ) ) ) & ( [.r,s.] in F implies b_{1} = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being Real st

( r < p & p <= s & b_{1} . 1 = [.r,p.[ ) & ex p being Real st

( r <= p & p < s & b_{1} . (len b_{1}) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len b_{1} holds

ex p, q being Real st

( r <= p & p < q & q <= s & b_{1} . n = ].p,q.[ ) ) ) ) )

end;
let F be Subset-Family of (Closed-Interval-TSpace (r,s));

assume that

A1: F is 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 Nat st 1 <= n holds

( ( n <= len it implies not it /. n is empty ) & ( n + 1 <= len it implies ( lower_bound (it /. n) <= lower_bound (it /. (n + 1)) & upper_bound (it /. n) <= upper_bound (it /. (n + 1)) & lower_bound (it /. (n + 1)) < upper_bound (it /. n) ) ) & ( n + 2 <= len it implies upper_bound (it /. n) <= lower_bound (it /. (n + 2)) ) ) ) & ( [.r,s.] in F implies it = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being Real st

( r < p & p <= s & it . 1 = [.r,p.[ ) & ex p being Real st

( r <= p & p < s & it . (len it) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len it holds

ex p, q being Real st

( r <= p & p < q & q <= s & it . n = ].p,q.[ ) ) ) ) );

existence ( rng it c= F & union (rng it) = [.r,s.] & ( for n being Nat st 1 <= n holds

( ( n <= len it implies not it /. n is empty ) & ( n + 1 <= len it implies ( lower_bound (it /. n) <= lower_bound (it /. (n + 1)) & upper_bound (it /. n) <= upper_bound (it /. (n + 1)) & lower_bound (it /. (n + 1)) < upper_bound (it /. n) ) ) & ( n + 2 <= len it implies upper_bound (it /. n) <= lower_bound (it /. (n + 2)) ) ) ) & ( [.r,s.] in F implies it = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being Real st

( r < p & p <= s & it . 1 = [.r,p.[ ) & ex p being Real st

( r <= p & p < s & it . (len it) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len it holds

ex p, q being Real st

( r <= p & p < q & q <= s & it . n = ].p,q.[ ) ) ) ) );

ex b

( rng b

( ( n <= len b

( r < p & p <= s & b

( r <= p & p < s & b

ex p, q being Real st

( r <= p & p < q & q <= s & b

proof end;

:: deftheorem Def2 defines IntervalCover RCOMP_3:def 2 :

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s)) st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

for b_{4} being FinSequence of bool REAL holds

( b_{4} is IntervalCover of F iff ( rng b_{4} c= F & union (rng b_{4}) = [.r,s.] & ( for n being Nat st 1 <= n holds

( ( n <= len b_{4} implies not b_{4} /. n is empty ) & ( n + 1 <= len b_{4} implies ( lower_bound (b_{4} /. n) <= lower_bound (b_{4} /. (n + 1)) & upper_bound (b_{4} /. n) <= upper_bound (b_{4} /. (n + 1)) & lower_bound (b_{4} /. (n + 1)) < upper_bound (b_{4} /. n) ) ) & ( n + 2 <= len b_{4} implies upper_bound (b_{4} /. n) <= lower_bound (b_{4} /. (n + 2)) ) ) ) & ( [.r,s.] in F implies b_{4} = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being Real st

( r < p & p <= s & b_{4} . 1 = [.r,p.[ ) & ex p being Real st

( r <= p & p < s & b_{4} . (len b_{4}) = ].p,s.] ) & ( for n being Nat st 1 < n & n < len b_{4} holds

ex p, q being Real st

( r <= p & p < q & q <= s & b_{4} . n = ].p,q.[ ) ) ) ) ) );

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s)) st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

for b

( b

( ( n <= len b

( r < p & p <= s & b

( r <= p & p < s & b

ex p, q being Real st

( r <= p & p < q & q <= s & b

theorem :: RCOMP_3:49

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s)) st F is 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

for F being Subset-Family of (Closed-Interval-TSpace (r,s)) st F is 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 Th50: :: RCOMP_3:50

for r being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,r))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,r)) & F is open & F is connected holds

C = <*[.r,r.]*>

for F being Subset-Family of (Closed-Interval-TSpace (r,r))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,r)) & F is open & F is connected holds

C = <*[.r,r.]*>

proof end;

theorem Th51: :: RCOMP_3:51

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

1 <= len C

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

1 <= len C

proof end;

theorem Th52: :: RCOMP_3:52

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

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

C = <*[.r,s.]*>

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

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

C = <*[.r,s.]*>

proof end;

theorem :: RCOMP_3:53

for r, s being Real

for n, m being Nat

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is 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

lower_bound (C /. n) <= lower_bound (C /. m)

for n, m being Nat

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is 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

lower_bound (C /. n) <= lower_bound (C /. m)

proof end;

theorem :: RCOMP_3:54

for r, s being Real

for n, m being Nat

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is 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

upper_bound (C /. n) <= upper_bound (C /. m)

for n, m being Nat

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is 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

upper_bound (C /. n) <= upper_bound (C /. m)

proof end;

theorem Th55: :: RCOMP_3:55

for r, s being Real

for n being Nat

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n + 1 <= len C holds

not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty

for n being Nat

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n + 1 <= len C holds

not ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ is empty

proof end;

theorem :: RCOMP_3:56

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

lower_bound (C /. 1) = r

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

lower_bound (C /. 1) = r

proof end;

theorem Th57: :: RCOMP_3:57

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

r in C /. 1

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

r in C /. 1

proof end;

theorem :: RCOMP_3:58

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

upper_bound (C /. (len C)) = s

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

upper_bound (C /. (len C)) = s

proof end;

theorem Th59: :: RCOMP_3:59

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

s in C /. (len C)

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

s in C /. (len C)

proof end;

definition

let r, s be Real;

let F be Subset-Family of (Closed-Interval-TSpace (r,s));

let C be IntervalCover of F;

assume A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ;

ex b_{1} being FinSequence of REAL st

( len b_{1} = (len C) + 1 & b_{1} . 1 = r & b_{1} . (len b_{1}) = s & ( for n being Nat st 1 <= n & n + 1 < len b_{1} holds

b_{1} . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) )

end;
let F be Subset-Family of (Closed-Interval-TSpace (r,s));

let C be IntervalCover of F;

assume A1: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & 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 Nat st 1 <= n & n + 1 < len it holds

it . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) );

existence ( len it = (len C) + 1 & it . 1 = r & it . (len it) = s & ( for n being Nat st 1 <= n & n + 1 < len it holds

it . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) );

ex b

( len b

b

proof end;

:: deftheorem Def3 defines IntervalCoverPts RCOMP_3:def 3 :

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

for b_{5} being FinSequence of REAL holds

( b_{5} is IntervalCoverPts of C iff ( len b_{5} = (len C) + 1 & b_{5} . 1 = r & b_{5} . (len b_{5}) = s & ( for n being Nat st 1 <= n & n + 1 < len b_{5} holds

b_{5} . (n + 1) in ].(lower_bound (C /. (n + 1))),(upper_bound (C /. n)).[ ) ) );

for r, s being Real

for F being Subset-Family of (Closed-Interval-TSpace (r,s))

for C being IntervalCover of F st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

for b

( b

b

theorem Th60: :: RCOMP_3:60

for r, s being Real

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

2 <= len G

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds

2 <= len G

proof end;

theorem Th61: :: RCOMP_3:61

for r, s being Real

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 holds

G = <*r,s*>

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & len C = 1 holds

G = <*r,s*>

proof end;

theorem Th62: :: RCOMP_3:62

for r, s being Real

for n being Nat

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 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) < upper_bound (C /. n)

for n being Nat

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 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) < upper_bound (C /. n)

proof end;

theorem Th63: :: RCOMP_3:63

for r, s being Real

for n being Nat

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 < n & n <= len C holds

lower_bound (C /. n) < G . n

for n being Nat

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 < n & n <= len C holds

lower_bound (C /. n) < G . n

proof end;

theorem Th64: :: RCOMP_3:64

for r, s being Real

for n being Nat

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C holds

G . n <= lower_bound (C /. (n + 1))

for n being Nat

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len C holds

G . n <= lower_bound (C /. (n + 1))

proof end;

theorem Th65: :: RCOMP_3:65

for r, s being Real

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r < s holds

G is increasing

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r < s holds

G is increasing

proof end;

theorem :: RCOMP_3:66

for r, s being Real

for n being Nat

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len G holds

[.(G . n),(G . (n + 1)).] c= C . n

for n being Nat

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 Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s & 1 <= n & n < len G holds

[.(G . n),(G . (n + 1)).] c= C . n

proof end;