let FT be non empty RelStr ; :: thesis: for A being Subset of FT st FT is symmetric holds
( A is connected iff A is arcwise_connected )
let A be Subset of FT; :: thesis: ( FT is symmetric implies ( A is connected iff A is arcwise_connected ) )
assume A1:
FT is symmetric
; :: thesis: ( A is connected iff A is arcwise_connected )
now assume
not
A is
arcwise_connected
;
:: thesis: not A is connectedthen consider x1,
x2 being
Element of
FT such that A2:
(
x1 in A &
x2 in A & ( for
f being
FinSequence of
FT holds
( not
f is
continuous or not
rng f c= A or not
f . 1
= x1 or not
f . (len f) = x2 ) ) )
by Def7;
A3:
{ z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } c= A
then reconsider G =
{ z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } as
Subset of
FT by XBOOLE_1:1;
A11:
A = G \/ (A \ G)
by A3, XBOOLE_1:45;
A12:
G misses A \ G
by XBOOLE_1:79;
now assume
G ^b meets A \ G
;
:: thesis: contradictionthen consider u being
set such that A13:
(
u in G ^b &
u in A \ G )
by XBOOLE_0:3;
A14:
(
u in G ^b &
u in A & not
u in G )
by A13, XBOOLE_0:def 5;
consider x being
Element of
FT such that A15:
(
u = x &
U_FT x meets G )
by A13;
consider y being
set such that A16:
(
y in U_FT x &
y in G )
by A15, XBOOLE_0:3;
consider z2 being
Element of
FT such that A17:
(
y = z2 &
z2 in A & ex
f being
FinSequence of
FT st
(
f is
continuous &
rng f c= A &
f . 1
= x1 &
f . (len f) = z2 ) )
by A16;
consider f being
FinSequence of
FT such that A18:
(
f is
continuous &
rng f c= A &
f . 1
= x1 &
f . (len f) = z2 )
by A17;
reconsider g =
f ^ <*x*> as
FinSequence of
FT ;
A19:
len g =
(len f) + (len <*x*>)
by FINSEQ_1:35
.=
(len f) + 1
by FINSEQ_1:56
;
x in U_FT z2
by A1, A16, A17, FIN_TOPO:def 15;
then A20:
(
g is
continuous &
g . ((len f) + 1) = x )
by A18, Th44, FINSEQ_1:59;
1
<= len f
by A18, Def6;
then
1
in dom f
by FINSEQ_3:27;
then A21:
g . 1
= x1
by A18, FINSEQ_1:def 7;
A22:
rng g =
(rng f) \/ (rng <*x*>)
by FINSEQ_1:44
.=
(rng f) \/ {x}
by FINSEQ_1:55
;
{x} c= A
by A14, A15, ZFMISC_1:37;
then
rng g c= A
by A18, A22, XBOOLE_1:8;
hence
contradiction
by A14, A15, A19, A20, A21;
:: thesis: verum end; hence
not
A is
connected
by A5, A7, A11, A12, FIN_TOPO:def 18;
:: thesis: verum end;
hence
( A is connected implies A is arcwise_connected )
; :: thesis: ( A is arcwise_connected implies A is connected )
now assume
not
A is
connected
;
:: thesis: ( not A is arcwise_connected & not A is arcwise_connected )then consider P,
Q being
Subset of
FT such that A23:
(
A = P \/ Q &
P <> {} &
Q <> {} &
P misses Q &
P ^b misses Q )
by FIN_TOPO:def 18;
consider p0 being
Element of
P;
p0 in P
by A23;
then reconsider p1 =
p0 as
Element of
FT ;
A24:
p1 in A
by A23, XBOOLE_0:def 3;
consider q0 being
Element of
Q;
q0 in Q
by A23;
then reconsider q1 =
q0 as
Element of
FT ;
A25:
q1 in A
by A23, XBOOLE_0:def 3;
hereby :: thesis: not A is arcwise_connected
assume
A is
arcwise_connected
;
:: thesis: contradictionthen consider f being
FinSequence of
FT such that A26:
(
f is
continuous &
rng f c= A &
f . 1
= p1 &
f . (len f) = q1 )
by A24, A25, Def7;
A27:
len f >= 1
by A26, Def6;
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= len f &
f . $1
in P );
A28:
ex
k being
Nat st
S1[
k]
by A23, A26, A27;
A29:
for
k being
Nat st
S1[
k] holds
k <= len f
;
consider i0 being
Nat such that A30:
(
S1[
i0] & ( for
n being
Nat st
S1[
n] holds
n <= i0 ) )
from NAT_1:sch 6(A29, A28);
reconsider u0 =
f . i0 as
Element of
FT by A30;
i0 <> len f
by A23, A26, A30, XBOOLE_0:3;
then A31:
i0 < len f
by A30, XXREAL_0:1;
then A32:
i0 + 1
<= len f
by NAT_1:13;
A33:
1
< i0 + 1
by A30, NAT_1:13;
i0 + 1
in dom f
by A32, A33, FINSEQ_3:27;
then A35:
f . (i0 + 1) in rng f
by FUNCT_1:def 5;
then A36:
f . (i0 + 1) in Q
by A23, A26, A34, XBOOLE_0:def 3;
reconsider z0 =
f . (i0 + 1) as
Element of
FT by A35;
z0 in U_FT u0
by A26, A30, A31, Def6;
then
f . i0 in U_FT z0
by A1, FIN_TOPO:def 15;
then
U_FT z0 meets P
by A30, XBOOLE_0:3;
then
z0 in P ^b
;
hence
contradiction
by A23, A36, XBOOLE_0:3;
:: thesis: verum
end; hence
not
A is
arcwise_connected
;
:: thesis: verum end;
hence
( A is arcwise_connected implies A is connected )
; :: thesis: verum