:: Properties of Connected Subsets of the Real Line
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: RCOMP_3:1
theorem Th2: :: RCOMP_3:2
theorem Th3: :: RCOMP_3:3
theorem Th4: :: RCOMP_3:4
theorem Th5: :: RCOMP_3:5
theorem Th6: :: RCOMP_3:6
theorem Th7: :: RCOMP_3:7
theorem :: RCOMP_3:8
canceled;
theorem :: RCOMP_3:9
canceled;
theorem :: RCOMP_3:10
canceled;
theorem :: RCOMP_3:11
canceled;
theorem :: RCOMP_3:12
canceled;
theorem :: RCOMP_3:13
canceled;
theorem :: RCOMP_3:14
canceled;
theorem :: RCOMP_3:15
canceled;
theorem :: RCOMP_3:16
canceled;
theorem :: RCOMP_3:17
canceled;
theorem :: RCOMP_3:18
canceled;
theorem :: RCOMP_3:19
canceled;
theorem Th20: :: RCOMP_3:20
theorem Th21: :: RCOMP_3:21
theorem Th22: :: RCOMP_3:22
theorem Th23: :: RCOMP_3:23
theorem Th24: :: RCOMP_3:24
theorem Th25: :: RCOMP_3:25
theorem Th26: :: RCOMP_3:26
theorem Th27: :: RCOMP_3:27
theorem Th28: :: RCOMP_3:28
theorem Th29: :: RCOMP_3:29
theorem Th30: :: RCOMP_3:30
theorem Th31: :: RCOMP_3:31
theorem Th32: :: RCOMP_3:32
theorem Th33: :: RCOMP_3:33
theorem Th34: :: RCOMP_3:34
theorem Th35: :: RCOMP_3:35
theorem Th36: :: RCOMP_3:36
theorem Th37: :: RCOMP_3:37
theorem Th38: :: RCOMP_3:38
theorem Th39: :: RCOMP_3:39
theorem Th40: :: RCOMP_3:40
theorem Th41: :: RCOMP_3:41
theorem Th42: :: RCOMP_3:42
theorem Th43: :: RCOMP_3:43
theorem Th44: :: RCOMP_3:44
theorem :: RCOMP_3:45
theorem Th46: :: RCOMP_3:46
theorem Th47: :: RCOMP_3:47
theorem :: RCOMP_3:48
theorem :: RCOMP_3:49
theorem Th50: :: RCOMP_3:50
theorem Th51: :: RCOMP_3:51
theorem Th52: :: RCOMP_3:52
theorem :: RCOMP_3:53
theorem Th54: :: RCOMP_3:54
theorem Th55: :: RCOMP_3:55
theorem Th56: :: RCOMP_3:56
theorem Th57: :: RCOMP_3:57
deffunc H1( set ) -> set = $1;
defpred S1[ set , set ] means $1 c= $2;
theorem :: RCOMP_3:58
theorem Th59: :: RCOMP_3:59
theorem Th60: :: RCOMP_3:60
:: deftheorem Def1 defines connected RCOMP_3:def 1 :
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 ( 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)) ) ) ) )
theorem Th61: :: RCOMP_3:61
theorem Th62: :: RCOMP_3:62
definition
let r,
s be
real number ;
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
natural number 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 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
ex b1 being FinSequence of bool REAL st
( rng b1 c= F & union (rng b1) = [.r,s.] & ( for n being natural number st 1 <= n holds
( ( n <= len b1 implies not b1 /. n is empty ) & ( n + 1 <= len b1 implies ( lower_bound (b1 /. n) <= lower_bound (b1 /. (n + 1)) & upper_bound (b1 /. n) <= upper_bound (b1 /. (n + 1)) & lower_bound (b1 /. (n + 1)) < upper_bound (b1 /. n) ) ) & ( n + 2 <= len b1 implies upper_bound (b1 /. n) <= lower_bound (b1 /. (n + 2)) ) ) ) & ( [.r,s.] in F implies b1 = <*[.r,s.]*> ) & ( not [.r,s.] in F implies ( ex p being real number st
( r < p & p <= s & b1 . 1 = [.r,p.[ ) & ex p being real number st
( r <= p & p < s & b1 . (len b1) = ].p,s.] ) & ( for n being natural number st 1 < n & n < len b1 holds
ex p, q being real number st
( r <= p & p < q & q <= s & b1 . n = ].p,q.[ ) ) ) ) )
end;
:: deftheorem Def2 defines IntervalCover RCOMP_3:def 2 :
for
r,
s being
real number 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
b4 being
FinSequence of
bool REAL holds
(
b4 is
IntervalCover of
F iff (
rng b4 c= F &
union (rng b4) = [.r,s.] & ( for
n being
natural number st 1
<= n holds
( (
n <= len b4 implies not
b4 /. n is
empty ) & (
n + 1
<= len b4 implies (
lower_bound (b4 /. n) <= lower_bound (b4 /. (n + 1)) &
upper_bound (b4 /. n) <= upper_bound (b4 /. (n + 1)) &
lower_bound (b4 /. (n + 1)) < upper_bound (b4 /. n) ) ) & (
n + 2
<= len b4 implies
upper_bound (b4 /. n) <= lower_bound (b4 /. (n + 2)) ) ) ) & (
[.r,s.] in F implies
b4 = <*[.r,s.]*> ) & ( not
[.r,s.] in F implies ( ex
p being
real number st
(
r < p &
p <= s &
b4 . 1
= [.r,p.[ ) & ex
p being
real number st
(
r <= p &
p < s &
b4 . (len b4) = ].p,s.] ) & ( for
n being
natural number st 1
< n &
n < len b4 holds
ex
p,
q being
real number st
(
r <= p &
p < q &
q <= s &
b4 . n = ].p,q.[ ) ) ) ) ) );
theorem :: RCOMP_3:63
theorem Th64: :: RCOMP_3:64
theorem Th65: :: RCOMP_3:65
theorem Th66: :: RCOMP_3:66
theorem :: RCOMP_3:67
theorem :: RCOMP_3:68
theorem Th69: :: RCOMP_3:69
theorem :: RCOMP_3:70
theorem Th71: :: RCOMP_3:71
theorem :: RCOMP_3:72
theorem Th73: :: RCOMP_3:73
:: deftheorem Def3 defines IntervalCoverPts RCOMP_3:def 3 :
theorem Th74: :: RCOMP_3:74
theorem Th75: :: RCOMP_3:75
theorem Th76: :: RCOMP_3:76
theorem Th77: :: RCOMP_3:77
theorem Th78: :: RCOMP_3:78
theorem Th79: :: RCOMP_3:79
theorem :: RCOMP_3:80