let FT1, FT2 be non empty RelStr ; for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
let A be Subset of FT1; for B being Subset of FT2
for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
let B be Subset of FT2; for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
let f be Function of FT1,FT2; ( A is connected & f is_continuous 0 & B = f .: A implies B is connected )
assume that
A1:
A is connected
and
A2:
f is_continuous 0
and
A3:
B = f .: A
; B is connected
for B2, C2 being Subset of FT2 st B = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 holds
B2 ^b meets C2
proof
let B2,
C2 be
Subset of
FT2;
( B = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 implies B2 ^b meets C2 )
assume that A4:
B = B2 \/ C2
and A5:
B2 <> {}
and A6:
C2 <> {}
and A7:
B2 misses C2
;
B2 ^b meets C2
reconsider C1 =
f " C2 as
Subset of
FT1 ;
reconsider C10 =
C1 /\ A as
Subset of
FT1 ;
reconsider B1 =
f " B2 as
Subset of
FT1 ;
reconsider B10 =
B1 /\ A as
Subset of
FT1 ;
A8:
C10 c= C1
by XBOOLE_1:17;
set x6 = the
Element of
C2;
the
Element of
C2 in B
by A4, A6, XBOOLE_0:def 3;
then consider z6 being
object such that A9:
z6 in dom f
and A10:
z6 in A
and A11:
the
Element of
C2 = f . z6
by A3, FUNCT_1:def 6;
z6 in f " C2
by A6, A9, A11, FUNCT_1:def 7;
then A12:
C10 <> {}
by A10, XBOOLE_0:def 4;
set x5 = the
Element of
B2;
the
Element of
B2 in B
by A4, A5, XBOOLE_0:def 3;
then consider z5 being
object such that A13:
z5 in dom f
and A14:
z5 in A
and A15:
the
Element of
B2 = f . z5
by A3, FUNCT_1:def 6;
A c= the
carrier of
FT1
;
then A16:
A c= dom f
by FUNCT_2:def 1;
B2 /\ C2 = {}
by A7, XBOOLE_0:def 7;
then
f " (B2 /\ C2) = {}
;
then
(
B10 c= B1 &
(f " B2) /\ (f " C2) = {} )
by FUNCT_1:68, XBOOLE_1:17;
then
B10 /\ C10 = {}
by A8, XBOOLE_1:3, XBOOLE_1:27;
then A17:
B10 misses C10
by XBOOLE_0:def 7;
(f " B2) \/ (f " C2) = f " (f .: A)
by A3, A4, RELAT_1:140;
then
A c= B1 \/ C1
by A16, FUNCT_1:76;
then
A c= A /\ (B1 \/ C1)
by XBOOLE_1:19;
then A18:
A c= B10 \/ C10
by XBOOLE_1:23;
(
B10 c= A &
C10 c= A )
by XBOOLE_1:17;
then
B10 \/ C10 c= A
by XBOOLE_1:8;
then A19:
A = B10 \/ C10
by A18, XBOOLE_0:def 10;
z5 in f " B2
by A5, A13, A15, FUNCT_1:def 7;
then
B10 <> {}
by A14, XBOOLE_0:def 4;
then
B10 ^b meets C10
by A1, A19, A12, A17;
then A20:
(B10 ^b) /\ C10 <> {}
by XBOOLE_0:def 7;
reconsider B20 =
f .: B1 as
Subset of
FT2 ;
A21:
dom f = the
carrier of
FT1
by FUNCT_2:def 1;
f .: B1 c= B2
then A22:
B20 ^b c= B2 ^b
by FIN_TOPO:14;
f .: (B1 ^b) c= B20 ^b
by A2, Th16;
then
f .: (B1 ^b) c= B2 ^b
by A22;
then A23:
(
(f .: (B1 ^b)) /\ (f .: C1) c= (f .: (B1 ^b)) /\ C2 &
(f .: (B1 ^b)) /\ C2 c= (B2 ^b) /\ C2 )
by FUNCT_1:75, XBOOLE_1:26;
B10 ^b c= B1 ^b
by FIN_TOPO:14, XBOOLE_1:17;
then
(B1 ^b) /\ C1 <> {}
by A8, A20, XBOOLE_1:3, XBOOLE_1:27;
then
f .: ((B1 ^b) /\ C1) <> {}
by A21, RELAT_1:119;
then
(f .: (B1 ^b)) /\ (f .: C1) <> {}
by RELAT_1:121, XBOOLE_1:3;
then
(B2 ^b) /\ C2 <> {}
by A23;
hence
B2 ^b meets C2
by XBOOLE_0:def 7;
verum
end;
hence
B is connected
; verum