let r, s be Real; ( r <= s implies ex B being Basis of (Closed-Interval-TSpace (r,s)) st
( ex f being ManySortedSet of (Closed-Interval-TSpace (r,s)) st
for y being Point of (Closed-Interval-MSpace (r,s)) holds
( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) ) )
set L = Closed-Interval-TSpace (r,s);
set M = Closed-Interval-MSpace (r,s);
assume A1:
r <= s
; ex B being Basis of (Closed-Interval-TSpace (r,s)) st
( ex f being ManySortedSet of (Closed-Interval-TSpace (r,s)) st
for y being Point of (Closed-Interval-MSpace (r,s)) holds
( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) )
defpred S1[ object , object ] means ex x being Point of (Closed-Interval-TSpace (r,s)) ex y being Point of (Closed-Interval-MSpace (r,s)) ex B being Basis of st
( $1 = x & x = y & $2 = B & B = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } );
A2:
Closed-Interval-TSpace (r,s) = TopSpaceMetr (Closed-Interval-MSpace (r,s))
by TOPMETR:def 7;
A3:
for i being object st i in the carrier of (Closed-Interval-TSpace (r,s)) holds
ex j being object st S1[i,j]
proof
let i be
object ;
( i in the carrier of (Closed-Interval-TSpace (r,s)) implies ex j being object st S1[i,j] )
assume
i in the
carrier of
(Closed-Interval-TSpace (r,s))
;
ex j being object st S1[i,j]
then reconsider i =
i as
Point of
(Closed-Interval-TSpace (r,s)) ;
reconsider m =
i as
Point of
(Closed-Interval-MSpace (r,s)) by A2, TOPMETR:12;
reconsider j =
i as
Element of
(TopSpaceMetr (Closed-Interval-MSpace (r,s))) by A2;
set B =
Balls j;
A4:
ex
y being
Point of
(Closed-Interval-MSpace (r,s)) st
(
y = j &
Balls j = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } )
by FRECHET:def 1;
reconsider B1 =
Balls j as
Basis of
by A2;
take
Balls j
;
S1[i, Balls j]
take
i
;
ex y being Point of (Closed-Interval-MSpace (r,s)) ex B being Basis of st
( i = i & i = y & Balls j = B & B = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } )
take
m
;
ex B being Basis of st
( i = i & i = m & Balls j = B & B = { (Ball (m,(1 / n))) where n is Nat : n <> 0 } )
take
B1
;
( i = i & i = m & Balls j = B1 & B1 = { (Ball (m,(1 / n))) where n is Nat : n <> 0 } )
thus
(
i = i &
i = m &
Balls j = B1 &
B1 = { (Ball (m,(1 / n))) where n is Nat : n <> 0 } )
by A4;
verum
end;
consider f being ManySortedSet of the carrier of (Closed-Interval-TSpace (r,s)) such that
A5:
for i being object st i in the carrier of (Closed-Interval-TSpace (r,s)) holds
S1[i,f . i]
from PBOOLE:sch 3(A3);
for x being Element of (Closed-Interval-TSpace (r,s)) holds f . x is Basis of
then reconsider B = Union f as Basis of (Closed-Interval-TSpace (r,s)) by TOPGEN_2:2;
take
B
; ( ex f being ManySortedSet of (Closed-Interval-TSpace (r,s)) st
for y being Point of (Closed-Interval-MSpace (r,s)) holds
( f . y = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) )
hereby for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected
take f =
f;
for x being Point of (Closed-Interval-MSpace (r,s)) holds
( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f )let x be
Point of
(Closed-Interval-MSpace (r,s));
( f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } & B = Union f ) the
carrier of
(Closed-Interval-MSpace (r,s)) =
[.r,s.]
by A1, TOPMETR:10
.=
the
carrier of
(Closed-Interval-TSpace (r,s))
by A1, TOPMETR:18
;
then
S1[
x,
f . x]
by A5;
hence
(
f . x = { (Ball (x,(1 / n))) where n is Nat : n <> 0 } &
B = Union f )
;
verum
end;
let X be Subset of (Closed-Interval-TSpace (r,s)); ( X in B implies X is connected )
assume
X in B
; X is connected
then
X in union (rng f)
by CARD_3:def 4;
then consider Z being set such that
A6:
X in Z
and
A7:
Z in rng f
by TARSKI:def 4;
consider x being object such that
A8:
x in dom f
and
A9:
f . x = Z
by A7, FUNCT_1:def 3;
consider x1 being Point of (Closed-Interval-TSpace (r,s)), y being Point of (Closed-Interval-MSpace (r,s)), B1 being Basis of such that
x = x1
and
x1 = y
and
A10:
( f . x = B1 & B1 = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } )
by A5, A8;
consider n being Nat such that
A11:
X = Ball (y,(1 / n))
and
n <> 0
by A6, A9, A10;
reconsider X1 = X as Subset of R^1 by PRE_TOPC:11;
( Ball (y,(1 / n)) = [.r,s.] or Ball (y,(1 / n)) = [.r,(y + (1 / n)).[ or Ball (y,(1 / n)) = ].(y - (1 / n)),s.] or Ball (y,(1 / n)) = ].(y - (1 / n)),(y + (1 / n)).[ )
by A1, Th1;
then
X1 is connected
by A11;
hence
X is connected
by CONNSP_1:23; verum