:: Connectedness and Continuous Sequences in Finite Topological Spaces
:: by Yatsuka Nakamura
::
:: Received August 18, 2006
:: Copyright (c) 2006-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, ORDERS_2, SUBSET_1, RELAT_2, FIN_TOPO, TARSKI,
CONNSP_1, PRE_TOPC, STRUCT_0, RELAT_1, RCOMP_1, FINSEQ_1, ORDINAL2,
XXREAL_0, NAT_1, ARYTM_3, FUNCT_1, ORDINAL4, PARTFUN1, CARD_1, ARYTM_1,
BORSUK_2, RFINSEQ, FINTOPO3, FINTOPO6;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, XXREAL_0,
NAT_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1,
STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1, FINTOPO4,
PRE_TOPC, RFINSEQ;
constructors DOMAIN_1, EQREL_1, RFINSEQ, RFUNCT_3, NAT_D, FIN_TOPO, FINTOPO3,
FINTOPO4, REAL_1, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0,
FIN_TOPO, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FIN_TOPO;
equalities STRUCT_0, SUBSET_1, FIN_TOPO, FINSEQ_1;
expansions TARSKI, XBOOLE_0, FIN_TOPO;
theorems NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, RELSET_1, XBOOLE_0, XBOOLE_1,
FIN_TOPO, FINTOPO3, ENUMSET1, FINTOPO4, FINSEQ_6, JORDAN4, TARSKI,
XREAL_1, SUBSET_1, PRE_TOPC, RFINSEQ, FINSEQ_3, FINSEQ_5, REVROT_1,
ORDINAL1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D;
schemes NAT_1, RELSET_1;
begin :: Connectedness and Subspaces
reserve FT for non empty RelStr,
A,B,C for Subset of FT;
registration
let FT;
cluster empty -> connected for Subset of FT;
coherence;
end;
::$CT
theorem Th1:
({}FT)^b={}
proof
assume not thesis;
then consider x being object such that
A1: x in ({}FT)^b by XBOOLE_0:def 1;
ex y being Element of FT st x=y & U_FT y meets {}FT by A1;
hence contradiction;
end;
registration
let FT;
cluster ({}FT)^b -> empty;
coherence by Th1;
end;
theorem
for A being Subset of FT st for B,C being Subset of FT st A = B
\/ C & B <> {} & C <> {} & B misses C holds B^b meets C & B meets C^b holds A
is connected;
definition
let FT be non empty RelStr;
attr FT is connected means
[#]FT is connected;
end;
theorem Th3:
for A being Subset of FT holds A is connected implies for A2, B2
being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated holds
A2 = {}FT or B2 = {}FT
proof
let A be Subset of FT;
assume
A1: A is connected;
let A2, B2 be Subset of FT;
assume that
A2: A = A2 \/ B2 & A2 misses B2 and
A3: A2,B2 are_separated;
A2^b misses B2 by A3,FINTOPO4:def 1;
hence thesis by A1,A2;
end;
theorem Th4:
FT is connected implies for A, B being Subset of FT st [#]FT = A
\/ B & A misses B & A,B are_separated holds A = {}FT or B = {}FT
proof
assume FT is connected;
then
A1: [#]FT is connected;
let A, B be Subset of FT;
assume that
A2: [#]FT = A \/ B & A misses B and
A3: A,B are_separated;
A^b misses B by A3,FINTOPO4:def 1;
hence thesis by A1,A2;
end;
theorem Th5:
for A,B being Subset of FT st FT is symmetric & A^b misses B
holds A misses B^b
proof
let A,B be Subset of FT;
assume that
A1: FT is symmetric and
A2: A^b misses B;
assume A meets B^b;
then consider x being object such that
A3: x in A and
A4: x in B^b by XBOOLE_0:3;
consider y being Element of FT such that
A5: x=y and
A6: U_FT y meets B by A4;
consider z being object such that
A7: z in U_FT y and
A8: z in B by A6,XBOOLE_0:3;
reconsider z2=z as Element of FT by A7;
y in U_FT z2 by A1,A7;
then U_FT z2 meets A by A3,A5,XBOOLE_0:3;
then
A9: z in A^b;
A^b /\ B={} by A2;
hence contradiction by A8,A9,XBOOLE_0:def 4;
end;
theorem Th6:
for A being Subset of FT st FT is symmetric & for A2, B2 being
Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated holds A2 = {}
FT or B2 = {}FT holds A is connected
proof
let A be Subset of FT;
assume
A1: FT is symmetric;
assume
A2: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2
are_separated holds A2 = {}FT or B2 = {}FT;
for B,C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses
C holds B^b meets C & B meets C^b
proof
let B,C be Subset of FT;
assume A = B \/ C & B <> {} & C <> {} & B misses C;
then not B,C are_separated by A2;
then not(B^b misses C & B misses (C^b)) by FINTOPO4:def 1;
hence thesis by A1,Th5;
end;
hence thesis;
end;
definition
let T be RelStr;
mode SubSpace of T -> RelStr means
:Def2:
the carrier of it c= the carrier
of T & for x being Element of it st x in the carrier of it holds U_FT x =Im(the
InternalRel of T,x) /\ the carrier of it;
existence
proof
for x being Element of T st x in the carrier of T holds U_FT x =Im(the
InternalRel of T,x)/\ the carrier of T by XBOOLE_1:28;
hence thesis;
end;
end;
Lm1: for T being RelStr holds the RelStr of T is SubSpace of T
proof
let T be RelStr;
set S = the RelStr of T;
for x being Element of S st x in the carrier of S holds U_FT x =Im(the
InternalRel of T,x)/\ (the carrier of T) by XBOOLE_1:28;
hence thesis by Def2;
end;
registration
let T be RelStr;
cluster strict for SubSpace of T;
existence
proof
the RelStr of T is SubSpace of T by Lm1;
hence thesis;
end;
end;
registration
let T be non empty RelStr;
cluster strict non empty for SubSpace of T;
existence
proof
the RelStr of T is SubSpace of T & the RelStr of T is non empty by Lm1;
hence thesis;
end;
end;
definition
let T be non empty RelStr, P be non empty Subset of T;
func T|P -> strict non empty SubSpace of T means
:Def3:
[#]it = P;
existence
proof
deffunc F(set) = Im(the InternalRel of T,$1) /\ P;
A1: for x being Element of T st x in P holds F(x) c= P by XBOOLE_1:17;
consider G being Relation of P such that
A2: for y being Element of T st y in P holds Im(G,y)=F(y) from
RELSET_1:sch 3(A1);
set FS=RelStr(# P,G #);
for x being Element of FS st x in the carrier of FS holds U_FT x =Im(
the InternalRel of T,x)/\ (the carrier of FS) by A2;
then
[#]FS = the carrier of FS & FS is strict non empty SubSpace of T by Def2;
hence thesis;
end;
uniqueness
proof
let Z1,Z2 be strict non empty SubSpace of T;
assume that
A3: [#] Z1 = P and
A4: [#] Z2 = P;
reconsider R1 = the InternalRel of Z1, R2 = the InternalRel of Z2 as
Relation of P by A3,A4;
for z being set st z in P holds Im(R1,z) = Im(R2,z)
proof
let z be set;
assume
A5: z in P;
then reconsider z1=z as Element of Z1 by A3;
reconsider z2=z as Element of Z2 by A4,A5;
thus Im(R1,z) = U_FT z1
.= Im(the InternalRel of T,z1)/\ (the carrier of Z1) by Def2
.= U_FT z2 by A3,A4,Def2
.= Im(R2,z);
end;
hence thesis by A3,A4,RELSET_1:31;
end;
end;
theorem Th7:
for X being non empty SubSpace of FT st FT is filled holds X is filled
proof
let X be non empty SubSpace of FT;
assume
A1: FT is filled;
let x be Element of X;
the carrier of X c= the carrier of FT by Def2;
then reconsider x2=x as Element of FT;
A2: U_FT x= (U_FT x2) /\ ([#]X) by Def2;
x2 in U_FT x2 by A1;
hence thesis by A2,XBOOLE_0:def 4;
end;
registration
let FT be filled non empty RelStr;
cluster -> filled for non empty SubSpace of FT;
coherence by Th7;
end;
theorem
for X being non empty SubSpace of FT st FT is symmetric holds X is symmetric
proof
let X be non empty SubSpace of FT;
assume
A1: FT is symmetric;
for x, y being Element of X holds y in U_FT x implies x in U_FT y
proof
let x, y be Element of X;
assume
A2: y in U_FT x;
the carrier of X c= the carrier of FT by Def2;
then reconsider x2=x, y2=y as Element of FT;
A3: U_FT x=U_FT x2 /\ ([#]X) & U_FT y=U_FT y2 /\ ([#]X) by Def2;
y2 in U_FT x2 implies x2 in U_FT y2 by A1;
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem Th9:
for X9 being SubSpace of FT, A being Subset of X9 holds A is Subset of FT
proof
let X9 be SubSpace of FT, A be Subset of X9;
the carrier of X9 c= the carrier of FT by Def2;
hence thesis by XBOOLE_1:1;
end;
theorem
for P being Subset of FT holds P is closed iff P` is open
proof
let P be Subset of FT;
P` is open implies P`` is closed by FIN_TOPO:23;
hence thesis by FIN_TOPO:24;
end;
theorem
for A being Subset of FT holds A is open iff (for z being Element of
FT st U_FT z c= A holds z in A)& for x being Element of FT st x in A holds U_FT
x c= A
proof
let A be Subset of FT;
hereby
assume A is open;
then
A1: A = A^i;
hence for z being Element of FT st U_FT z c= A holds z in A;
for x being Element of FT st x in A holds U_FT x c= A
proof
let x be Element of FT;
assume x in A;
then ex y being Element of FT st x=y & U_FT y c= A by A1;
hence thesis;
end;
hence for x being Element of FT st x in A holds U_FT x c= A;
end;
assume that
A2: for z being Element of FT st U_FT z c= A holds z in A and
A3: for x being Element of FT st x in A holds U_FT x c= A;
A4: A c= { y where y is Element of FT: U_FT y c= A}
proof
let u be object;
assume
A5: u in A;
then reconsider y2=u as Element of FT;
U_FT y2 c= A by A3,A5;
hence thesis;
end;
{ y where y is Element of FT: U_FT y c= A} c= A
proof
let u be object;
assume u in { y where y is Element of FT: U_FT y c= A};
then ex y being Element of FT st y=u & U_FT y c= A;
hence thesis by A2;
end;
then A = A^i by A4;
hence thesis;
end;
theorem Th12:
for X9 being non empty SubSpace of FT, A being Subset of FT, A1
being Subset of X9 st A = A1 holds A1^b = (A^b) /\ ([#]X9)
proof
let X9 be non empty SubSpace of FT, A be Subset of FT, A1 be Subset of X9
such that
A1: A = A1;
A2: (A^b) /\ ([#]X9) c= A1^b
proof
let u be object;
assume
A3: u in (A^b) /\ ([#]X9);
then u in A^b by XBOOLE_0:def 4;
then consider y2 being Element of FT such that
A4: u=y2 and
A5: (U_FT y2) meets A;
reconsider y3=y2 as Element of X9 by A3,A4;
consider z being object such that
A6: z in (U_FT y2) and
A7: z in A by A5,XBOOLE_0:3;
U_FT y3=(U_FT y2) /\ [#]X9 by Def2;
then z in U_FT y3 by A1,A6,A7,XBOOLE_0:def 4;
then (U_FT y3) meets A1 by A1,A7,XBOOLE_0:3;
hence thesis by A4;
end;
A1^b c= (A^b) /\ ([#]X9)
proof
reconsider Y=X9 as non empty RelStr;
let x be object;
assume x in A1^b;
then consider y being Element of Y such that
A8: y=x and
A9: U_FT y meets A1;
y in the carrier of X9 & the carrier of Y c= the carrier of FT by Def2;
then reconsider z=y as Element of FT;
U_FT y =Im(the InternalRel of FT,y)/\ (the carrier of X9) by Def2;
then U_FT z meets A by A1,A9,XBOOLE_1:74;
then z in {u where u is Element of FT: U_FT u meets A};
hence thesis by A8,XBOOLE_0:def 4;
end;
hence thesis by A2;
end;
theorem
for X9 being non empty SubSpace of FT, P1,Q1 being Subset of FT, P,Q
being Subset of X9 st P=P1 & Q=Q1 holds P,Q are_separated implies P1,Q1
are_separated
proof
let X9 be non empty SubSpace of FT, P1,Q1 be Subset of FT, P,Q be Subset of
X9 such that
A1: P = P1 & Q = Q1;
reconsider P2 = P, Q2 = Q as Subset of FT by Th9;
assume
A2: P,Q are_separated;
then P^b misses Q by FINTOPO4:def 1;
then
A3: (P^b) /\ Q = {};
P misses (Q^b) by A2,FINTOPO4:def 1;
then
A4: P /\ (Q^b) = {};
P /\ (Q^b) = P /\ (([#] X9) /\ (Q2^b)) by Th12
.= P /\ [#] X9 /\ (Q2^b) by XBOOLE_1:16
.= P2 /\ (Q2^b) by XBOOLE_1:28;
then
A5: P2 misses Q2^b by A4;
(P^b) /\ Q = ((P2^b) /\ ([#](X9))) /\ Q by Th12
.= (P2^b) /\ (Q /\ [#] X9) by XBOOLE_1:16
.= (P2^b) /\ Q2 by XBOOLE_1:28;
then (P2^b) misses Q2 by A3;
hence thesis by A1,A5,FINTOPO4:def 1;
end;
theorem
for X9 being non empty SubSpace of FT, P,Q being Subset of FT, P1,Q1
being Subset of X9 st P=P1 & Q=Q1 & P \/ Q c= [#](X9) holds P,Q are_separated
implies P1,Q1 are_separated
proof
let X9 be non empty SubSpace of FT, P,Q be Subset of FT, P1,Q1 be Subset of
X9 such that
A1: P = P1 & Q = Q1 and
A2: P \/ Q c= [#](X9);
P c= P \/ Q & Q c= P \/ Q by XBOOLE_1:7;
then reconsider P2 = P, Q2 = Q as Subset of X9 by A2,XBOOLE_1:1;
assume
A3: P,Q are_separated;
then P misses (Q^b) by FINTOPO4:def 1;
then
A4: P /\ (Q^b) = {};
P2 /\ (Q2^b) = P2 /\ (([#] X9) /\ (Q^b)) by Th12
.= (P2 /\ [#] X9) /\ (Q^b) by XBOOLE_1:16
.= P /\ (Q^b) by XBOOLE_1:28;
then
A5: P2 misses (Q2^b) by A4;
P2^b = (P^b) /\ [#] X9 by Th12;
then
A6: (P2^b) /\ Q2 = (P^b) /\ (Q2 /\ [#] X9) by XBOOLE_1:16
.= (P^b) /\ Q by XBOOLE_1:28;
P^b misses Q by A3,FINTOPO4:def 1;
then (P^b) /\ Q = {};
then (P2^b) misses Q2 by A6;
hence thesis by A1,A5,FINTOPO4:def 1;
end;
theorem Th15:
for A being non empty Subset of FT holds A is connected iff FT|A is connected
proof
let A be non empty Subset of FT;
A1: [#](FT|A)=A by Def3;
thus A is connected implies (FT|A) is connected
proof
assume
A2: A is connected;
for B2,C2 being Subset of (FT|A) st [#](FT|A) = B2 \/ C2 & B2 <> {} &
C2 <> {} & B2 misses C2 holds B2^b meets C2
proof
let B2,C2 be Subset of (FT|A);
A3: ([#](FT|A))/\ C2=C2 by XBOOLE_1:28;
the carrier of (FT|A)=[#](FT|A) .=A by Def3;
then reconsider B3=B2, C3=C2 as Subset of FT by XBOOLE_1:1;
assume [#](FT|A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2;
then
A4: B3^b meets C3 by A1,A2;
B2^b /\ C2= B3^b /\ [#](FT|A)/\ C2 by Th12
.= B3^b /\ C3 by A3,XBOOLE_1:16;
then B2^b /\ C2 <> {} by A4;
hence thesis;
end;
then [#](FT|A) is connected;
hence thesis;
end;
assume (FT|A) is connected;
then
A5: [#](FT|A) is connected;
let B,C be Subset of FT;
assume that
A6: A = B \/ C and
A7: B <> {} & C <> {} & B misses C;
A8: [#](FT|A) =A by Def3;
then reconsider B2=B as Subset of (FT|A) by A6,XBOOLE_1:7;
reconsider C2=C as Subset of (FT|A) by A6,A8,XBOOLE_1:7;
([#](FT|A))/\ C2=C2 & B2^b=B^b /\ [#](FT|A) by Th12,XBOOLE_1:28;
then
A9: B^b /\ C = B2^b /\ C2 by XBOOLE_1:16;
B2^b meets C2 by A5,A6,A7,A8;
hence B^b /\ C <> {} by A9;
end;
theorem
for FT being filled non empty RelStr, A being non empty Subset of FT
st FT is symmetric holds A is connected iff for P,Q being Subset of FT st A = P
\/ Q & P misses Q & P,Q are_separated holds P = {}FT or Q = {}FT
proof
let FT be filled non empty RelStr, A be non empty Subset of FT;
assume
A1: FT is symmetric;
now
assume not A is connected;
then not FT|A is connected by Th15;
then not [#](FT|A) is connected;
then consider P,Q being Subset of FT|A such that
A2: [#](FT|A) = P \/ Q and
A3: P <> {} & Q <> {} and
A4: P misses Q and
A5: P^b misses Q;
reconsider P1 = P, Q1 = Q as Subset of FT by Th9;
take P1,Q1;
thus A = P1 \/ Q1 & P1 misses Q1 by A2,A4,Def3;
A6: P^b=P1^b /\ [#](FT|A) by Th12;
([#](FT|A))/\ Q1=Q1 by XBOOLE_1:28;
then P1^b /\ Q1=P1^b /\ ([#](FT|A))/\ Q by XBOOLE_1:16
.={} by A5,A6;
then P1^b misses Q1;
hence P1,Q1 are_separated & P1 <> {}FT & Q1 <> {}FT by A1,A3,FINTOPO4:10;
end;
hence thesis by Th3;
end;
theorem
for A being Subset of FT st FT is filled connected & A <> {} & A` <>
{} holds A^delta <>{}
proof
let A be Subset of FT;
assume that
A1: FT is filled connected and
A2: A <> {} & A` <>{};
A3: now
assume A^b meets A`;
then consider x being object such that
A4: x in A^b and
A5: x in A` by XBOOLE_0:3;
reconsider x as Element of FT by A4;
x in U_FT x by A1;
then
A6: U_FT x meets A` by A5,XBOOLE_0:3;
U_FT x meets A by A4,FIN_TOPO:8;
hence ex z being Element of FT st U_FT z meets A & U_FT z meets A` by A6;
end;
A7: now
assume A meets (A`)^b;
then consider x being object such that
A8: x in (A`)^b and
A9: x in A by XBOOLE_0:3;
reconsider x as Element of FT by A8;
x in U_FT x by A1;
then
A10: U_FT x meets A by A9,XBOOLE_0:3;
U_FT x meets A` by A8,FIN_TOPO:8;
hence ex z being Element of FT st U_FT z meets A & U_FT z meets A` by A10;
end;
{}={}FT & A \/ A` = [#]FT by XBOOLE_1:45;
then not A,A` are_separated by A1,A2,Th4,XBOOLE_1:79;
hence thesis by A3,A7,FINTOPO4:def 1,FIN_TOPO:5;
end;
theorem
for A being Subset of FT st FT is filled symmetric & FT is connected &
A <> {} & A` <> {} holds A^deltai <>{}
proof
let A be Subset of FT;
assume that
A1: FT is filled symmetric and
A2: FT is connected & A <> {} & A` <>{};
A3: now
assume A^b meets A`;
then consider x being object such that
A4: x in A^b and
A5: x in A` by XBOOLE_0:3;
reconsider x as Element of FT by A4;
U_FT x meets A by A4,FIN_TOPO:8;
then consider y being object such that
A6: y in U_FT x and
A7: y in A by XBOOLE_0:3;
reconsider y as Element of FT by A6;
y in U_FT y by A1;
then
A8: U_FT y meets A by A7,XBOOLE_0:3;
x in U_FT y by A1,A6;
then U_FT y meets A` by A5,XBOOLE_0:3;
then y in A^delta by A8;
hence thesis by A7,XBOOLE_0:def 4;
end;
A9: now
assume A meets (A`)^b;
then consider x being object such that
A10: x in (A`)^b and
A11: x in A by XBOOLE_0:3;
reconsider x as Element of FT by A10;
x in U_FT x by A1;
then
A12: U_FT x meets A by A11,XBOOLE_0:3;
U_FT x meets A` by A10,FIN_TOPO:8;
then x in A^delta by A12;
hence thesis by A11,XBOOLE_0:def 4;
end;
{}={}FT & A \/ A` = [#]FT by XBOOLE_1:45;
then not A,A` are_separated by A2,Th4,XBOOLE_1:79;
hence thesis by A3,A9,FINTOPO4:def 1;
end;
theorem
for A being Subset of FT st FT is filled symmetric & FT is connected &
A <> {} & A` <>{} holds A^deltao <>{}
proof
let A be Subset of FT;
assume that
A1: FT is filled symmetric and
A2: FT is connected & A <> {} & A` <>{};
A3: now
assume A meets (A`)^b;
then consider x being object such that
A4: x in (A`)^b and
A5: x in A by XBOOLE_0:3;
reconsider x as Element of FT by A4;
U_FT x meets A` by A4,FIN_TOPO:8;
then consider y being object such that
A6: y in U_FT x and
A7: y in A` by XBOOLE_0:3;
reconsider y as Element of FT by A6;
y in U_FT y by A1;
then
A8: U_FT y meets A` by A7,XBOOLE_0:3;
x in U_FT y by A1,A6;
then U_FT y meets A by A5,XBOOLE_0:3;
then y in A^delta by A8;
hence thesis by A7,XBOOLE_0:def 4;
end;
A9: now
assume A^b meets A`;
then consider x being object such that
A10: x in A^b and
A11: x in A` by XBOOLE_0:3;
reconsider x as Element of FT by A10;
x in U_FT x by A1;
then
A12: U_FT x meets A` by A11,XBOOLE_0:3;
U_FT x meets A by A10,FIN_TOPO:8;
then x in A^delta by A12;
hence thesis by A11,XBOOLE_0:def 4;
end;
{}={}FT & A \/ A` = [#]FT by XBOOLE_1:45;
then not A,A` are_separated by A2,Th4,XBOOLE_1:79;
hence thesis by A9,A3,FINTOPO4:def 1;
end;
theorem
for A being Subset of FT holds A^deltai misses A^deltao
proof
let A be Subset of FT;
A misses A` by XBOOLE_1:79;
then
A1: A /\ A` = {};
thus A^deltai /\ (A^deltao) = A /\ ((A^delta) /\ A`) /\ (A^delta) by
XBOOLE_1:16
.= A /\ A` /\ (A^delta) /\ (A^delta) by XBOOLE_1:16
.= {} by A1;
end;
theorem
for FT being filled non empty RelStr, A being Subset of FT holds A
^deltao=(A^b) \ A
proof
let FT be filled non empty RelStr,A be Subset of FT;
A1: A` /\ ((A`)^b)=A` by FIN_TOPO:13,XBOOLE_1:28;
thus A^deltao=A` /\ ((A^b) /\ ((A`)^b)) by FIN_TOPO:18
.= (A^b) /\ (A` /\ ((A`)^b)) by XBOOLE_1:16
.= A^b \ A by A1,SUBSET_1:13;
end;
theorem
for A, B being Subset of FT st A,B are_separated holds A^deltao misses B
proof
let A,B be Subset of FT;
assume A,B are_separated;
then
A1: A^b misses B by FINTOPO4:def 1;
thus (A^deltao)/\ B = A` /\ ((A^delta) /\ B) by XBOOLE_1:16
.= A` /\ ((A^b) /\ ((A`)^b)/\ B) by FIN_TOPO:18
.= A` /\ (((A`)^b) /\ ((A^b)/\ B)) by XBOOLE_1:16
.= A` /\ (((A`)^b) /\ ({})) by A1
.= {};
end;
theorem
for A, B being Subset of FT st FT is filled & A misses B & A^deltao
misses B & B^deltao misses A holds A,B are_separated
proof
let A, B be Subset of FT;
assume that
A1: FT is filled and
A2: A /\ B = {} and
A3: (A^deltao)/\ B = {} and
A4: (B^deltao)/\ A = {};
B` /\ ((B^delta) /\ A) = {} by A4,XBOOLE_1:16;
then B` /\ ((B^b) /\ ((B`)^b)/\ A) = {} by FIN_TOPO:18;
then B` /\ (((B`)^b) /\ ((B^b)/\ A)) = {} by XBOOLE_1:16;
then
A5: B` /\ ((B`)^b) /\ ((B^b)/\ A) = {} by XBOOLE_1:16;
B` /\ ((B`)^b)=B` by A1,FIN_TOPO:13,XBOOLE_1:28;
then B` misses ((B^b)/\ A) by A5;
then ((B^b)/\ A) c= B by SUBSET_1:24;
then ((B^b)/\ A)/\ A c= B /\ A by XBOOLE_1:26;
then (B^b)/\ (A/\ A) c= B /\ A by XBOOLE_1:16;
then B^b /\ A ={} by A2,XBOOLE_1:3;
then
A6: A misses B^b;
A` /\ ((A^delta) /\ B) = {} by A3,XBOOLE_1:16;
then A` /\ ((A^b) /\ ((A`)^b)/\ B) = {} by FIN_TOPO:18;
then A` /\ (((A`)^b) /\ ((A^b)/\ B)) = {} by XBOOLE_1:16;
then
A7: A` /\ ((A`)^b) /\ ((A^b)/\ B) = {} by XBOOLE_1:16;
A` /\ ((A`)^b)=A` by A1,FIN_TOPO:13,XBOOLE_1:28;
then A` misses ((A^b)/\ B) by A7;
then ((A^b)/\ B) c= A by SUBSET_1:24;
then ((A^b)/\ B)/\ B c= A /\ B by XBOOLE_1:26;
then (A^b)/\ (B/\ B) c= A /\ B by XBOOLE_1:16;
then A^b /\ B ={} by A2,XBOOLE_1:3;
then A^b misses B;
hence thesis by A6,FINTOPO4:def 1;
end;
theorem Th24:
for x being Point of FT holds {x} is connected
proof
let x be Point of FT;
assume not {x} is connected;
then consider P,Q being Subset of FT such that
A1: {x} = P \/ Q and
A2: P <> {} and
A3: Q <> {} and
A4: P misses Q and
not(P^b meets Q & P meets Q^b);
P <> Q
by A2,A4;
hence contradiction by A1,A2,A3,ZFMISC_1:38;
end;
registration
let FT;
let x be Point of FT;
cluster {x} -> connected for Subset of FT;
coherence by Th24;
end;
definition
let FT be non empty RelStr, A be Subset of FT;
pred A is_a_component_of FT means
A is connected & for B being Subset
of FT st B is connected holds A c= B implies A = B;
end;
theorem
for A being Subset of FT st A is_a_component_of FT holds A <> {}FT
proof
let A be Subset of FT;
set x = the Point of FT;
{} c= {x};
hence thesis;
end;
theorem
A is closed & B is closed & A misses B implies A,B are_separated
by FINTOPO4:def 1;
theorem Th27:
FT is filled & [#]FT = A \/ B & A,B are_separated implies A is open closed
proof
assume that
A1: FT is filled and
A2: [#]FT = A \/ B and
A3: A,B are_separated;
B c= B^b by A1,FIN_TOPO:13;
then A misses (B^b) implies B^b = B by A2,XBOOLE_1:73;
then
A4: B is closed by A3,FINTOPO4:def 1;
A c= A^b by A1,FIN_TOPO:13;
then
A5: A^b misses B implies A^b = A by A2,XBOOLE_1:73;
B`= A by A1,A2,A3,FINTOPO4:6,PRE_TOPC:5;
hence thesis by A3,A5,A4,FINTOPO4:def 1,FIN_TOPO:24;
end;
theorem Th28:
for A,B,A1,B1 being Subset of FT holds A,B are_separated & A1 c=
A & B1 c= B implies A1,B1 are_separated
proof
let A,B,A1,B1 be Subset of FT;
assume that
A1: A,B are_separated and
A2: A1 c= A and
A3: B1 c= B;
A misses (B^b) by A1,FINTOPO4:def 1;
then
A4: A/\(B^b)={};
B1^b c= B^b by A3,FIN_TOPO:14;
then A1 /\ (B1^b) = {}FT by A2,A4,XBOOLE_1:3,27;
then
A5: A1 misses (B1^b);
A^b misses B by A1,FINTOPO4:def 1;
then
A6: A^b /\ B={};
A1^b c= A^b by A2,FIN_TOPO:14;
then (A1^b) /\ B1 = {}FT by A3,A6,XBOOLE_1:3,27;
then (A1^b) misses B1;
hence thesis by A5,FINTOPO4:def 1;
end;
theorem Th29:
A,B are_separated & A,C are_separated implies A,B \/ C are_separated
proof
assume that
A1: A,B are_separated and
A2: A,C are_separated;
A3: (A^b) misses C by A2,FINTOPO4:def 1;
(A^b) misses B by A1,FINTOPO4:def 1;
then
A4: (A^b) /\ B = {};
(A^b) /\ (B \/ C) = ((A^b) /\ B) \/ ((A^b) /\ C) by XBOOLE_1:23
.= {} by A3,A4;
then
A5: (A^b) misses (B \/ C);
A misses (B^b) by A1,FINTOPO4:def 1;
then
A6: A /\ (B^b) = {};
A7: A misses (C^b) by A2,FINTOPO4:def 1;
A /\ ((B \/ C)^b) = A /\ ((B^b) \/ (C^b)) by FINTOPO3:8
.= (A /\ (B^b)) \/ (A /\ (C^b)) by XBOOLE_1:23
.= {} by A7,A6;
then A misses ((B \/ C)^b);
hence thesis by A5,FINTOPO4:def 1;
end;
theorem
FT is filled symmetric & ( for A, B being Subset of FT st [#]FT = A \/
B & A <> {}FT & B <> {}FT & A is closed & B is closed holds A meets B) implies
FT is connected
proof
assume
A1: FT is filled symmetric;
assume
A2: for A, B being Subset of FT st [#]FT = A \/ B & A <> {}FT & B <> {}
FT & A is closed & B is closed holds A meets B;
assume not FT is connected;
then not [#]FT is connected;
then consider P, Q being Subset of FT such that
A3: [#]FT = P \/ Q and
A4: P misses Q and
A5: P,Q are_separated and
A6: P <> {}FT & Q <> {}FT by A1,Th6;
P is closed & Q is closed by A1,A3,A5,Th27;
hence contradiction by A2,A3,A4,A6;
end;
theorem
FT is connected implies for A, B being Subset of FT st [#]FT = A \/ B
& A <> {}FT & B <> {}FT & A is closed & B is closed holds A meets B
proof
assume
A1: [#]FT is connected;
given A, B being Subset of FT such that
A2: [#]FT = A \/ B & A <> {}FT & B <> {}FT & A is closed & B is closed &
A misses B;
thus contradiction by A1,A2;
end;
theorem Th32:
FT is filled & A is connected & A c= B \/ C & B,C are_separated
implies A c= B or A c= C
proof
assume that
A1: FT is filled and
A2: A is connected and
A3: A c= B \/ C and
A4: B,C are_separated;
A5: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23
.= A by A3,XBOOLE_1:28;
assume that
A6: not A c= B and
A7: not A c= C;
A meets B by A3,A7,XBOOLE_1:73;
then
A8: A /\ B <> {};
A meets C by A3,A6,XBOOLE_1:73;
then
A9: A /\ C <> {};
A10: A /\ B c= B & A /\ C c= C by XBOOLE_1:17;
then {}FT={} & (A /\ B) misses (A /\ C) by A1,A4,Th28,FINTOPO4:6;
hence contradiction by A2,A4,A8,A9,A10,A5,Th3,Th28;
end;
theorem Th33:
for A,B being Subset of FT st FT is symmetric & A is connected &
B is connected & not A,B are_separated holds A \/ B is connected
proof
let A,B be Subset of FT;
assume that
A1: FT is symmetric and
A2: A is connected and
A3: B is connected and
A4: not A,B are_separated;
given P,Q being Subset of FT such that
A5: A \/ B = P \/ Q and
A6: P <> {} and
A7: Q <> {} and
A8: P misses Q and
A9: P^b misses Q;
set P2=A/\P,Q2=A/\Q;
A10: P2 misses Q2 by A8,XBOOLE_1:76;
A11: Q^b misses P by A1,A9,Th5;
A12: now
assume that
A13: A c= Q and
A14: B c= P;
per cases by A4,FINTOPO4:def 1;
suppose
A^b meets B;
then Q^b meets B by A13,FIN_TOPO:14,XBOOLE_1:63;
hence contradiction by A11,A14,XBOOLE_1:63;
end;
suppose
A meets (B^b);
then not A^b misses B by A1,Th5;
then Q^b meets B by A13,FIN_TOPO:14,XBOOLE_1:63;
hence contradiction by A11,A14,XBOOLE_1:63;
end;
end;
A15: now
assume
A16: A/\P={};
then
A17: A/\Q=A/\P \/ A/\Q .=A/\(P\/Q) by XBOOLE_1:23
.=A by A5,XBOOLE_1:21;
A18: now
assume B/\Q={};
then B/\P=B/\Q \/ B/\P .=B/\(Q\/P) by XBOOLE_1:23
.=B by A5,XBOOLE_1:21;
hence contradiction by A12,A17,XBOOLE_1:18;
end;
set P3=B/\P,Q3=B/\Q;
A19: P3\/Q3=B/\(P\/Q) by XBOOLE_1:23
.=B by A5,XBOOLE_1:21;
A20: P3 misses Q3 by A8,XBOOLE_1:76;
P3^b c= P^b & Q3 c= Q by FIN_TOPO:14,XBOOLE_1:17;
then
A21: P3^b misses Q3 by A9,XBOOLE_1:64;
B/\P=A/\P \/ B/\P by A16
.=(A\/B)/\P by XBOOLE_1:23
.=P by A5,XBOOLE_1:21;
hence contradiction by A3,A6,A18,A19,A20,A21;
end;
A22: now
assume that
A23: A c= P and
A24: B c= Q;
A25: A^b c= P^b by A23,FIN_TOPO:14;
per cases by A4,FINTOPO4:def 1;
suppose
A^b meets B;
hence contradiction by A9,A24,A25,XBOOLE_1:64;
end;
suppose
A meets (B^b);
then not A^b misses B by A1,Th5;
hence contradiction by A9,A24,A25,XBOOLE_1:64;
end;
end;
A26: now
assume
A27: A/\Q={};
then
A28: A/\P=A/\Q \/ A/\P .=A/\(Q\/P) by XBOOLE_1:23
.=A by A5,XBOOLE_1:21;
A29: now
assume B/\P={};
then B/\Q=B/\P \/ B/\Q .=B/\(P\/Q) by XBOOLE_1:23
.=B by A5,XBOOLE_1:21;
hence contradiction by A22,A28,XBOOLE_1:18;
end;
set P3=B/\Q,Q3=B/\P;
A30: Q3\/P3=B/\(P\/Q) by XBOOLE_1:23
.=B by A5,XBOOLE_1:21;
A31: P3 misses Q3 by A8,XBOOLE_1:76;
P3^b c= Q^b & Q3 c= P by FIN_TOPO:14,XBOOLE_1:17;
then
A32: P3^b misses Q3 by A11,XBOOLE_1:64;
B/\Q=A/\Q \/ B/\Q by A27
.=(A\/B)/\Q by XBOOLE_1:23
.=Q by A5,XBOOLE_1:21;
hence contradiction by A3,A7,A29,A30,A31,A32;
end;
P2^b c= P^b & Q2 c= Q by FIN_TOPO:14,XBOOLE_1:17;
then
A33: P2^b misses Q2 by A9,XBOOLE_1:64;
P2\/Q2=A/\(P\/Q) by XBOOLE_1:23
.=A by A5,XBOOLE_1:21;
hence contradiction by A2,A15,A26,A10,A33;
end;
theorem Th34:
for A,C being Subset of FT st FT is symmetric & C is connected &
C c= A & A c=C^b holds A is connected
proof
let A,C be Subset of FT;
assume that
A1: FT is symmetric and
A2: C is connected and
A3: C c= A and
A4: A c= C^b;
let P2,Q2 be Subset of FT;
assume that
A5: A=P2\/Q2 and
A6: P2<>{} and
A7: Q2<>{} and
A8: P2 misses Q2;
assume
A9: not thesis;
set x2 = the Element of Q2;
A10: x2 in Q2 by A7;
Q2 c= Q2 \/P2 by XBOOLE_1:7;
then Q2 c= C^b by A4,A5;
then x2 in C^b by A10;
then consider z2 being Element of FT such that
A11: z2=x2 and
A12: U_FT z2 meets C;
set y3 = the Element of U_FT z2 /\ C;
A13: U_FT z2 /\ C <> {} by A12;
then y3 in U_FT z2 /\ C;
then reconsider y4=y3 as Element of FT;
y3 in U_FT z2 by A13,XBOOLE_0:def 4;
then z2 in U_FT y4 by A1;
then z2 in U_FT y4 /\ Q2 by A7,A11,XBOOLE_0:def 4;
then
A14: U_FT y4 meets Q2;
set P3=P2/\C,Q3=Q2/\C;
A15: C = A /\ C by A3,XBOOLE_1:28
.=P3 \/ Q3 by A5,XBOOLE_1:23;
set x = the Element of P2;
A16: x in P2 by A6;
P2 c= P2\/Q2 by XBOOLE_1:7;
then P2 c= C^b by A4,A5;
then x in C^b by A16;
then consider z being Element of FT such that
A17: z=x and
A18: U_FT z meets C;
set y = the Element of U_FT z /\ C;
A19: U_FT z /\ C <> {} by A18;
then y in U_FT z /\ C;
then reconsider y2=y as Element of FT;
y in U_FT z by A19,XBOOLE_0:def 4;
then z in U_FT y2 by A1;
then z in (U_FT y2)/\P2 by A6,A17,XBOOLE_0:def 4;
then (U_FT y2) meets P2;
then
A20: y2 in P2^b;
A21: y4 in C by A13,XBOOLE_0:def 4;
A22: now
assume Q3={};
then
A23: y4 in P2 by A21,A15,XBOOLE_0:def 4;
consider w being Element of FT such that
A24: w=y4 and
A25: U_FT w meets Q2 by A14;
consider s being object such that
A26: s in U_FT w and
A27: s in Q2 by A25,XBOOLE_0:3;
reconsider s2=s as Element of FT by A26;
w in U_FT s2 by A1,A26;
then U_FT s2 meets P2 by A23,A24,XBOOLE_0:3;
then s2 in P2^b;
hence contradiction by A9,A27,XBOOLE_0:3;
end;
A28: P3 c= P2 by XBOOLE_1:17;
A29: y2 in C by A19,XBOOLE_0:def 4;
A30: now
assume P3={};
then y2 in Q2 by A29,A15,XBOOLE_0:def 4;
then y2 in P2^b /\ Q2 by A20,XBOOLE_0:def 4;
hence contradiction by A9;
end;
P3 misses Q2 by A8,XBOOLE_1:17,63;
then P3 misses Q3 by XBOOLE_1:17,63;
then P3^b meets Q3 by A2,A15,A30,A22;
then P2^b meets Q3 by A28,FIN_TOPO:14,XBOOLE_1:63;
hence contradiction by A9,XBOOLE_1:17,63;
end;
theorem Th35:
for C being Subset of FT st FT is filled symmetric & C is
connected holds C^b is connected
proof
let C be Subset of FT;
assume that
A1: FT is filled symmetric and
A2: C is connected;
C c= C^b by A1,FIN_TOPO:13;
hence thesis by A1,A2,Th34;
end;
theorem Th36:
FT is filled symmetric connected & A is connected & [#]FT \ A =
B \/ C & B,C are_separated implies A \/ B is connected
proof
assume that
A1: FT is filled symmetric and
A2: FT is connected and
A3: A is connected and
A4: [#]FT \ A = B \/ C and
A5: B,C are_separated;
A6: [#]FT is connected by A2;
now
let P,Q be Subset of FT such that
A7: A \/ B = P \/ Q and
P misses Q and
A8: P,Q are_separated;
A9: [#]FT = A \/ (B \/ C) by A4,XBOOLE_1:45
.= P \/ Q \/ C by A7,XBOOLE_1:4;
A10: now
A11: [#]FT = P \/ (Q \/ C) by A9,XBOOLE_1:4;
assume A c= Q;
then P misses A by A1,A8,Th28,FINTOPO4:6;
then P c= B by A7,XBOOLE_1:7,73;
then
A12: P,C are_separated by A5,Th28;
then P misses Q \/ C by A1,A8,Th29,FINTOPO4:6;
hence P = {}FT or Q = {}FT by A6,A8,A12,A11,Th3,Th29;
end;
now
A13: [#]FT = Q \/ (P \/ C) by A9,XBOOLE_1:4;
assume A c= P;
then Q misses A by A1,A8,Th28,FINTOPO4:6;
then Q c= B by A7,XBOOLE_1:7,73;
then
A14: Q,C are_separated by A5,Th28;
then Q misses P\/C by A1,A8,Th29,FINTOPO4:6;
hence P = {}FT or Q = {}FT by A6,A8,A14,A13,Th3,Th29;
end;
hence P = {}FT or Q = {}FT by A1,A3,A7,A8,A10,Th32,XBOOLE_1:7;
end;
hence thesis by A1,Th6;
end;
theorem Th37:
for X9 being non empty SubSpace of FT, A being Subset of FT, B
being Subset of X9 st A = B holds A is connected iff B is connected
proof
let X9 be non empty SubSpace of FT, A8 be Subset of FT, B8 be Subset of X9;
assume
A1: A8 = B8;
per cases;
suppose
A8={};
hence thesis by A1;
end;
suppose
A2: A8<>{};
then reconsider A=A8 as non empty Subset of FT;
reconsider B=B8 as non empty Subset of X9 by A1,A2;
reconsider X = X9 as non empty RelStr;
A3: now
assume not A8 is connected;
then consider P,Q being Subset of FT such that
A4: A8 = P \/ Q and
A5: P <> {} & Q <> {} & P misses Q and
A6: P^b misses Q;
Q c= A8 by A4,XBOOLE_1:7;
then reconsider Q9=Q as Subset of X by A1,XBOOLE_1:1;
P c= A8 by A4,XBOOLE_1:7;
then reconsider P9=P as Subset of X by A1,XBOOLE_1:1;
A7: Q9 c= the carrier of X;
P9^b=P^b /\ [#]X by Th12;
then P9^b /\ Q9 =P^b /\ ([#]X /\ Q) by XBOOLE_1:16
.=P^b /\ Q by A7,XBOOLE_1:28
.={} by A6;
then (P9^b) misses Q9;
hence not B8 is connected by A1,A4,A5;
end;
now
assume not B is connected;
then consider P,Q being Subset of X9 such that
A8: B8 = P \/ Q & P <> {} & Q <> {} & P misses Q and
A9: P^b misses Q;
the carrier of X c= the carrier of FT by Def2;
then reconsider Q9=Q as Subset of FT by XBOOLE_1:1;
the carrier of X c= the carrier of FT by Def2;
then reconsider P9=P as Subset of FT by XBOOLE_1:1;
A10: P^b=P9^b /\ [#]X by Th12;
P9^b /\ Q9 =P9^b /\ ([#]X /\ Q) by XBOOLE_1:28
.=P^b /\ Q by A10,XBOOLE_1:16
.={} by A9;
then (P9^b) misses Q9;
hence not A is connected by A1,A8;
end;
hence thesis by A3;
end;
end;
theorem
for A being Subset of FT st FT is filled symmetric & A
is_a_component_of FT holds A is closed
proof
let A be Subset of FT;
assume that
A1: FT is filled symmetric and
A2: A is_a_component_of FT;
A is connected by A2;
then
A3: A^b is connected by A1,Th35;
A c= A^b by A1,FIN_TOPO:13;
hence A = A^b by A2,A3;
end;
theorem Th39:
for A,B being Subset of FT st FT is symmetric & A
is_a_component_of FT & B is_a_component_of FT holds A = B or A,B are_separated
proof
let A,B be Subset of FT;
assume that
A1: FT is symmetric and
A2: A is_a_component_of FT and
A3: B is_a_component_of FT;
A4: A is connected by A2;
assume that
A5: A <> B and
A6: not A,B are_separated;
B is connected by A3;
then A \/ B is connected by A1,A6,A4,Th33;
then B c= A \/ B & A = A \/ B by A2,XBOOLE_1:7;
hence contradiction by A3,A5,A4;
end;
theorem
for A,B being Subset of FT st FT is filled symmetric & A
is_a_component_of FT & B is_a_component_of FT holds A = B or A misses B by Th39
,FINTOPO4:6;
theorem
for C being Subset of FT st FT is filled symmetric & C is connected
holds for S being Subset of FT st S is_a_component_of FT holds C misses S or C
c= S
proof
let C be Subset of FT;
assume
A1: FT is filled symmetric & C is connected;
let S be Subset of FT;
assume
A2: S is_a_component_of FT;
A3: S c= C \/ S by XBOOLE_1:7;
assume
A4: C meets S;
S is connected by A2;
then C \/ S is connected by A1,A4,Th33,FINTOPO4:6;
then S = C \/ S by A2,A3;
hence thesis by XBOOLE_1:7;
end;
definition
let FT be non empty RelStr, A be non empty Subset of FT, B be Subset of FT;
pred B is_a_component_of A means
ex B1 being Subset of FT|A st B1 = B & B1 is_a_component_of FT|A;
end;
theorem
for D being non empty Subset of FT st FT is filled symmetric & D=[#]FT
\ A holds FT is connected & A is connected & C is_a_component_of D implies [#]
FT \ C is connected
proof
let D be non empty Subset of FT;
assume that
A1: FT is filled symmetric and
A2: D=[#]FT \ A and
A3: FT is connected and
A4: A is connected and
A5: C is_a_component_of D;
consider C1 being Subset of FT|D such that
A6: C1 = C and
A7: C1 is_a_component_of FT|D by A5;
reconsider C2 = C1 as Subset of FT by A6;
C1 c= [#](FT|D);
then C1 c= [#]FT \ A by A2,Def3;
then
A8: ([#]FT \ A)` c= C2` by SUBSET_1:12;
then
A9: A c= C2` by PRE_TOPC:3;
A10: A c= [#]FT \ C2 by A8,PRE_TOPC:3;
A11: C1 is connected by A7;
now
A misses C1 by A9,SUBSET_1:23;
then
A12: A /\ C1 = {};
let P,Q be Subset of FT such that
A13: [#]FT \ C = P \/ Q and
A14: P misses Q and
A15: P,Q are_separated;
A16: C is connected by A6,A11,Th37;
A17: now
assume
A18: A c= Q;
P c= Q` by A14,SUBSET_1:23;
then Q misses Q` & A /\ P c= Q /\ Q` by A18,XBOOLE_1:27,79;
then
A19: A /\ P c= {};
(C \/ P ) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23
.= {} by A6,A12,A19,XBOOLE_1:3;
then C \/ P misses A;
then C \/ P c= A` by SUBSET_1:23;
then C \/ P c= [#](FT|D) by A2,Def3;
then reconsider C1P1 = C \/ P as Subset of FT|D;
C \/ P is connected by A1,A3,A13,A15,A16,Th36;
then
A20: C1P1 is connected by Th37;
C c= C1 \/ P by A6,XBOOLE_1:7;
then C1P1 = C1 by A6,A7,A20;
then
A21: P c= C by A6,XBOOLE_1:7;
P c= [#]FT \ C by A13,XBOOLE_1:7;
then C misses C` & P c= C /\ ([#]FT \ C) by A21,XBOOLE_1:19,79;
then P c= {};
hence P = {}FT by XBOOLE_1:3;
end;
A22: P misses P` by XBOOLE_1:79;
A23: Q c= [#]FT \ C by A13,XBOOLE_1:7;
now
assume
A24: A c= P;
Q c= P` by A14,SUBSET_1:23;
then A /\ Q c= P /\ P` by A24,XBOOLE_1:27;
then
A25: A /\ Q c= {} by A22;
(C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23
.= {} by A6,A12,A25,XBOOLE_1:3;
then (C \/ Q) misses A;
then C \/ Q c= A` by SUBSET_1:23;
then C \/ Q c= [#](FT|D) by A2,Def3;
then reconsider C1Q1 = C \/ Q as Subset of FT|D;
C \/ Q is connected by A1,A3,A13,A15,A16,Th36;
then
A26: C1Q1 is connected by Th37;
C1 c= C1 \/ Q by XBOOLE_1:7;
then C1Q1 = C1 by A6,A7,A26;
then Q c= C by A6,XBOOLE_1:7;
then C misses C` & Q c= C /\ ([#]FT \ C) by A23,XBOOLE_1:19,79;
then Q c= {};
hence Q = {}FT by XBOOLE_1:3;
end;
hence P = {}FT or Q = {}FT by A1,A4,A6,A10,A13,A15,A17,Th32;
end;
hence thesis by A1,Th6;
end;
begin ::Continuous Finite Sequences and Minimum Path
definition
let FT;
let f be FinSequence of FT;
attr f is continuous means
1<=len f & for i being Nat,x1 being
Element of FT st 1<=i & i is continuous
by FINSEQ_1:39;
registration
let FT;
let x be Element of FT;
cluster <*x*> -> continuous for FinSequence of FT;
coherence by Lm2;
end;
theorem Th43:
for f being FinSequence of FT,x,y being Element of FT st f is
continuous & y=f.(len f) & x in U_FT y holds f^(<*x*>) is continuous
proof
let f be FinSequence of FT,x,y be Element of FT;
assume that
A1: f is continuous and
A2: y=f.(len f) and
A3: x in U_FT y;
reconsider g=f^(<*x*>) as FinSequence of FT;
A4: dom f=Seg len f by FINSEQ_1:def 3;
A5: len (<*x*>)=1 by FINSEQ_1:39;
A6: for i being Nat,x1 being Element of FT st 1<=i & i=len f;
len g=len f+1 by A5,FINSEQ_1:22;
then
A14: i<=len f by A8,NAT_1:13;
then
A15: i=len f by A13,XXREAL_0:1;
i in dom f by A4,A7,A14;
then x1=y by A2,A9,A15,FINSEQ_1:def 7;
hence x2 in U_FT x1 by A3,A15,FINSEQ_1:42;
end;
end;
hence thesis;
end;
len (f^<*x*>)=len f+len (<*x*>) by FINSEQ_1:22
.=len f+1 by FINSEQ_1:39;
then len (f^<*x*>)>=1 by NAT_1:11;
hence thesis by A6;
end;
theorem Th44:
for f,g being FinSequence of FT st f is continuous & g is
continuous & g.1 in U_FT (f/.(len f)) holds f^g is continuous
proof
let f,g be FinSequence of FT;
assume that
A1: f is continuous and
A2: g is continuous and
A3: g.1 in U_FT (f/.(len f));
A4: len (f^g)=len f+len g by FINSEQ_1:22;
len g>=1 by A2;
then len (f^g)>=0+1 by A4,XREAL_1:7;
hence len (f^g)>=1;
let i be Nat,x1 be Element of FT;
set g2=f^g;
A5: dom f=Seg len f by FINSEQ_1:def 3;
A6: len f>=1 by A1;
assume that
A7: 1<=i and
A8: i=len f;
then
A14: i+1>len f by NAT_1:13;
A15: ilen f;
set j=i-'len f;
A22: i-len f>0 by A21,XREAL_1:50;
then
A23: i-'len f=i-len f by XREAL_0:def 2;
then j+1=i+1-len f;
then
A24: x2=g.(j+1) by A14,A16,A17,FINSEQ_1:24;
A25: i-len f=len f+1 by A21,NAT_1:13;
then
A26: x1=g.j by A9,A15,A23,FINSEQ_1:23;
i-'len f>=0+1 by A22,A23,NAT_1:13;
hence thesis by A2,A23,A24,A26,A25;
end;
end;
end;
definition
let FT;
let A be Subset of FT;
attr A is arcwise_connected means
for x1,x2 being Element of FT st x1
in A & x2 in A ex f being FinSequence of FT st f is continuous & rng f c=A & f.
1=x1 & f.(len f)=x2;
end;
registration
let FT;
cluster empty -> arcwise_connected for Subset of FT;
coherence;
end;
Lm3: for x being Element of FT holds {x} is arcwise_connected
proof
let x be Element of FT;
set A={x};
A1: rng (<*x*>) c= A by FINSEQ_1:39;
A2: <*x*>.1=x by FINSEQ_1:40;
then
A3: <*x*>.(len <*x*>)=x by FINSEQ_1:40;
for x1,x2 being Element of FT st x1 in A & x2 in A ex f being
FinSequence of FT st f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2
proof
let x1,x2 be Element of FT;
assume x1 in A & x2 in A;
then x1=x & x2=x by TARSKI:def 1;
hence thesis by A2,A3,A1;
end;
hence thesis;
end;
registration
let FT;
let x be Element of FT;
cluster {x} -> arcwise_connected for Subset of FT;
coherence by Lm3;
end;
theorem
for A being Subset of FT st FT is symmetric holds A is connected iff A
is arcwise_connected
proof
let A be Subset of FT;
assume
A1: FT is symmetric;
now
assume not A is arcwise_connected;
then consider x1,x2 being Element of FT such that
A2: x1 in A and
A3: x2 in A and
A4: not(ex f being FinSequence of FT st f is continuous & rng f c=A &
f. 1=x1 & f.(len f)=x2);
A5: {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
proof
let x be object;
assume x in {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};
then
ex z being Element of FT st x=z & z in A & ex f being FinSequence of
FT st f is continuous & rng f c= A & f.1= x1 & f.(len f)=z;
hence thesis;
end;
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;
A6: G misses (A\G) by XBOOLE_1:79;
A7: now
assume G^b meets (A\G);
then consider u being object such that
A8: u in G^b and
A9: u in (A\G) by XBOOLE_0:3;
A10: not u in G by A9,XBOOLE_0:def 5;
consider x being Element of FT such that
A11: u=x and
A12: U_FT x meets G by A8;
consider y being object such that
A13: y in U_FT x and
A14: y in G by A12,XBOOLE_0:3;
consider z2 being Element of FT such that
A15: y=z2 and
z2 in A and
A16: ex f being FinSequence of FT st f is continuous & rng f c= A &
f.1= x1 & f.(len f)=z2 by A14;
consider f being FinSequence of FT such that
A17: f is continuous and
A18: rng f c= A and
A19: f.1=x1 and
A20: f.(len f)=z2 by A16;
reconsider g=f^(<*x*>) as FinSequence of FT;
A21: rng g =rng f \/ rng (<*x*>) by FINSEQ_1:31
.=rng f \/ {x} by FINSEQ_1:38;
A22: u in A by A9,XBOOLE_0:def 5;
then {x} c= A by A11,ZFMISC_1:31;
then
A23: rng g c= A by A18,A21,XBOOLE_1:8;
1<=len f by A17;
then 1 in dom f by FINSEQ_3:25;
then
A24: g.(len f+1)=x & g.1=x1 by A19,FINSEQ_1:42,def 7;
x in U_FT z2 by A1,A13,A15;
then
A25: g is continuous by A17,A20,Th43;
len g=len f+len (<*x*>) by FINSEQ_1:22
.=len f+1 by FINSEQ_1:39;
hence contradiction by A22,A10,A11,A25,A24,A23;
end;
A26: now
{x1} c= A by A2,ZFMISC_1:31;
then
A27: rng (<*x1*>) c= A by FINSEQ_1:38;
assume
A28: G={};
A29: (<*x1*>).1=x1 by FINSEQ_1:40;
then (<*x1*>).(len (<*x1*>))=x1 by FINSEQ_1:39;
then x1 in G by A2,A27,A29;
hence contradiction by A28;
end;
A30: now
assume A\G={};
then A c= G by XBOOLE_1:37;
then G=A by A5;
then ex z being Element of FT st z=x2 & z in A & ex f being FinSequence
of FT st f is continuous & rng f c= A & f.1= x1 & f.(len f)=z by A3;
hence contradiction by A4;
end;
A= G \/ (A\G) by A5,XBOOLE_1:45;
hence not A is connected by A30,A26,A6,A7;
end;
hence A is connected implies A is arcwise_connected;
now
assume not A is connected;
then consider P,Q being Subset of FT such that
A31: A=P\/Q and
A32: P<>{} and
A33: Q<>{} and
A34: P misses Q and
A35: P^b misses Q;
set q0 = the Element of Q;
q0 in Q by A33;
then reconsider q1=q0 as Element of FT;
set p0 = the Element of P;
p0 in P by A32;
then reconsider p1=p0 as Element of FT;
A36: p1 in A & q1 in A by A31,A32,A33,XBOOLE_0:def 3;
thus now
assume A is arcwise_connected;
then consider f being FinSequence of FT such that
A37: f is continuous and
A38: rng f c=A and
A39: f.1=p1 and
A40: f.(len f)=q1 by A36;
defpred P[Nat] means 1<=$1 & $1<=len f & f.$1 in P;
len f>=1 by A37;
then
A41: ex k being Nat st P[k] by A32,A39;
A42: for k being Nat st P[k] holds k <= len f;
consider i0 being Nat such that
A43: P[i0] & for n being Nat st P[n] holds n <= i0 from NAT_1:sch 6(
A42,A41 );
i0<>len f by A33,A34,A40,A43,XBOOLE_0:3;
then
A44: i0= 1 by A2,FINSEQ_1:59;
let i be Nat,x11 be Element of FT;
assume that
A4: 1<=i and
A5: i0 by A2,XREAL_1:50;
then
A4: len g-k=len g -'k by XREAL_0:def 2;
A5: len (g/^k)=len g-k by A2,RFINSEQ:def 1;
A6: for i being Nat,x11 being Element of FT st 1<=i & i=0+1 by A3,A4,NAT_1:13;
hence thesis by A5,A4,A6;
end;
definition
let FT;
let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
pred g is_minimum_path_in A,x1,x2 means
g is continuous & rng g c=A &
g.1=x1 & g.len g=x2 & for h being FinSequence of FT st h is continuous & rng h
c=A & h.1=x1 & h.len h=x2 holds len g <= len h;
end;
theorem
for A being Subset of FT, x being Element of FT st x in A holds <*x*>
is_minimum_path_in A,x,x
proof
let A be Subset of FT, x be Element of FT;
assume
A1: x in A;
thus <*x*> is continuous;
{x} c= A by A1,ZFMISC_1:31;
hence rng <*x*> c= A by FINSEQ_1:38;
len <*x*> =1 by FINSEQ_1:40;
hence thesis by FINSEQ_1:40;
end;
Lm4: for f being FinSequence of FT,A being Subset of FT, x1,x2 being Element
of FT st f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2 ex g being
FinSequence of FT st g is continuous & rng g c=A & g.1=x1 & g.(len g)=x2 & for
h being FinSequence of FT st h is continuous & rng h c=A & h.1=x1 & h.(len h)=
x2 holds len g <= len h
proof
let f be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
defpred P[Nat] means ex g being FinSequence of FT st g is continuous & rng g
c=A & g.1=x1 & g.(len g)=x2 & $1=len g;
assume f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2;
then
A1: ex k being Nat st P[k];
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from NAT_1
:sch 5(A1);
then consider k0 being Nat such that
A2: P[k0] and
A3: for n being Nat st P[n] holds k0 <= n;
consider g0 being FinSequence of FT such that
A4: g0 is continuous & rng g0 c=A & g0.1=x1 & g0.(len g0)=x2 and
A5: k0=len g0 by A2;
for h being FinSequence of FT st h is continuous & rng h c=A & h.1=x1 &
h.(len h)=x2 holds len g0 <= len h by A3,A5;
hence thesis by A4;
end;
theorem
for A being Subset of FT holds A is arcwise_connected iff for x1,x2
being Element of FT st x1 in A & x2 in A ex g being FinSequence of FT st g
is_minimum_path_in A,x1,x2
proof
let A be Subset of FT;
thus A is arcwise_connected implies for x1,x2 being Element of FT st x1 in A
& x2 in A ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
proof
assume
A1: A is arcwise_connected;
thus for x1,x2 being Element of FT st x1 in A & x2 in A ex g being
FinSequence of FT st g is_minimum_path_in A,x1,x2
proof
let x1,x2 be Element of FT;
assume x1 in A & x2 in A;
then
ex f being FinSequence of FT st f is continuous & rng f c= A & f.1=x1
& f.(len f)=x2 by A1;
then consider g2 being FinSequence of FT such that
A2: g2 is continuous & rng g2 c=A & g2.1=x1 & g2.(len g2)=x2 & for h
being FinSequence of FT st h is continuous & rng h c=A & h.1= x1 & h.(len h)=x2
holds len g2 <= len h by Lm4;
g2 is_minimum_path_in A,x1,x2 by A2;
hence thesis;
end;
end;
assume
A3: for x1,x2 being Element of FT st x1 in A & x2 in A ex g being
FinSequence of FT st g is_minimum_path_in A,x1,x2;
for x1,x2 being Element of FT st x1 in A & x2 in A ex f being
FinSequence of FT st f is continuous & rng f c=A & f.1=x1 & f.len f=x2
proof
let x1,x2 be Element of FT;
assume x1 in A & x2 in A;
then consider g being FinSequence of FT such that
A4: g is_minimum_path_in A,x1,x2 by A3;
A5: g.1=x1 & g.(len g)=x2 by A4;
g is continuous & rng g c=A by A4;
hence thesis by A5;
end;
hence thesis;
end;
theorem
for A being Subset of FT,x1,x2 being Element of FT st ex f being
FinSequence of FT st f is continuous & rng f c=A & f.1=x1 & f.len f=x2 ex g
being FinSequence of FT st g is_minimum_path_in A,x1,x2
proof
let A be Subset of FT,x1,x2 be Element of FT;
given f being FinSequence of FT such that
A1: f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2;
consider g2 being FinSequence of FT such that
A2: g2 is continuous & rng g2 c=A & g2.1=x1 & g2.(len g2)=x2 & for h
being FinSequence of FT st h is continuous & rng h c=A & h.1= x1 & h.(len h)=x2
holds len g2 <= len h by A1,Lm4;
g2 is_minimum_path_in A,x1,x2 by A2;
hence thesis;
end;
theorem Th51:
for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT, k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1<=k &
k<=len g holds g|k is continuous & rng (g|k) c=A & (g|k).1=x1 & (g|k).(len (g|k
))=g/.k
proof
let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT, k be
Element of NAT;
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: 1<=k and
A3: k<=len g;
A4: k in dom g by A2,A3,FINSEQ_3:25;
g is continuous by A1;
hence g|k is continuous by A2,Th46;
A5: rng (g|k) c= rng g by FINSEQ_5:19;
rng g c=A by A1;
hence rng (g|k) c=A by A5;
g.1=x1 by A1;
hence (g|k).1=x1 by A2,FINSEQ_3:112;
len (g|k)=k by A3,FINSEQ_1:59;
hence (g|k).(len (g|k))=g.k by FINSEQ_3:112
.=g/.k by A4,PARTFUN1:def 6;
end;
theorem Th52:
for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT, k being Element of NAT st g is_minimum_path_in A,x1,x2 & k0 by A2,XREAL_1:50;
then len g-'k=len g -k by XREAL_0:def 2;
then len g-k>=0+1 by A7,NAT_1:13;
then 1 in dom (g/^k) by A5,FINSEQ_3:25;
hence (g/^k).1=g.(1+k) by A2,RFINSEQ:def 1
.=g/.(1+k) by A6,PARTFUN1:def 6;
A8: len g-k>0 by A2,XREAL_1:50;
then
A9: len g-k=len g-'k by XREAL_0:def 2;
then len g-'k>=0+1 by A8,NAT_1:13;
then len g-'k in dom (g/^k) by A5,A9,FINSEQ_3:25;
hence (g/^k).(len (g/^k))=g.(len g-'k+k) by A2,A9,A3,RFINSEQ:def 1
.=x2 by A1,A9;
end;
theorem
for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT st g is_minimum_path_in A,x1,x2 holds for k being Nat st 1<=k & k
<=len g holds g|k is_minimum_path_in A,x1,g/.k
proof
let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
assume
A1: g is_minimum_path_in A,x1,x2;
then
A2: rng g c=A;
A3: g is continuous by A1;
then
A4: 1<=len g;
A5: g.(len g)=x2 by A1;
let k be Nat;
assume that
A6: 1<=k and
A7: k<=len g;
reconsider k as Element of NAT by ORDINAL1:def 12;
A8: (g|k).1=x1 & (g|k).(len (g|k))=g/.k by A1,A6,A7,Th51;
A9: g|k is continuous & rng (g|k) c=A by A1,A6,A7,Th51;
now
per cases by A7,XXREAL_0:1;
suppose
A10: k len h by A9,A8;
reconsider s=h^(g/^k) as FinSequence of FT;
A19: len s=len h +len(g/^k) by FINSEQ_1:22;
rng s = rng h \/ rng (g/^k) by FINSEQ_1:31;
then
A20: rng s c= A by A15,A13,XBOOLE_1:8;
A21: g/^k is continuous by A1,A10,Th52;
then 1<= len (g/^k);
then len (g/^k) in dom (g/^k) by FINSEQ_3:25;
then
A22: s.(len s)=(g/^k).(len (g/^k)) by A19,FINSEQ_1:def 7
.=x2 by A5,A10,JORDAN4:6;
A23: 1<=len h by A14;
then 1 in dom h by FINSEQ_3:25;
then
A24: s.1=x1 by A16,FINSEQ_1:def 7;
len h in dom h by A23,FINSEQ_3:25;
then h.len h=h/.len h by PARTFUN1:def 6;
then (g/^k).1 in U_FT (h/.(len h)) by A3,A6,A10,A17,A12,A11;
then
A25: s is continuous by A14,A21,Th44;
g=(g|k)^(g/^k) by RFINSEQ:8;
then len g=len (g|k) + len (g/^k) by FINSEQ_1:22;
then len sy2 by FUNCT_1:def 4;
reconsider n1=y1,n2=y2 as Element of NAT by A7,A8;
A11: dom g=Seg len g by FINSEQ_1:def 3;
then
A12: 1<=n1 by A7,FINSEQ_1:1;
A13: n2 <=len g by A8,A11,FINSEQ_1:1;
A14: 1<=n2 by A8,A11,FINSEQ_1:1;
A15: n1 <=len g by A7,A11,FINSEQ_1:1;
per cases by A10,XXREAL_0:1;
suppose
A16: n1>n2;
set k=len g-'n1;
set g2=(g|n2)^(g/^n1);
A17: len (g/^n1)=len g-n1 by A15,RFINSEQ:def 1;
A18: len g-n1>=0 by A15,XREAL_1:48;
then
A19: len g-'n1=len g-n1 by XREAL_0:def 2;
A20: len (g|n2)=n2 by A13,FINSEQ_1:59;
then
A21: g2.1=(g|n2).1 by A14,FINSEQ_1:64
.=g.1 by A14,FINSEQ_3:112;
A22: len g2=len (g|n2)+len (g/^n1) by FINSEQ_1:22
.=n2+(len g-n1) by A15,A20,RFINSEQ:def 1;
per cases by A15,XXREAL_0:1;
suppose
n1= 1 by A22,A24;
let i be Nat,z1 be Element of FT;
assume that
A26: 1<=i and
A27: i=n2;
i-n2n2;
then
A39: i-n2>0 by XREAL_1:50;
then i-'n2=i-n2 by XREAL_0:def 2;
then
A40: 0+1<=i-'n2 by A39,NAT_1:13;
then
A41: i-'n2 in dom (g/^n1) by A17,A35,FINSEQ_3:25;
thus z1=(g/^n1).(i-'n2) by A17,A28,A35,A37,A40,FINSEQ_1:65
.=g.(i-'n2+n1) by A15,A41,RFINSEQ:def 1;
end;
suppose
A42: i=n2;
hence z1=(g|n2).n2 by A20,A26,A28,FINSEQ_1:64
.=g.(0+n1) by A9,FINSEQ_3:112
.=g.(i-'n2+n1) by A42,XREAL_1:232;
end;
end;
i-'n2=n2;
i-n2n2;
then
A66: i-n2>0 by XREAL_1:50;
then i-'n2=i-n2 by XREAL_0:def 2;
then
A67: 0+1<=i-'n2 by A66,NAT_1:13;
then
A68: i-'n2 in dom (g/^n1) by A51,A62,FINSEQ_3:25;
thus z1=(g/^n1).(i-'n2) by A51,A55,A62,A64,A67,FINSEQ_1:65
.=g.(i-'n2+n1) by A15,A68,RFINSEQ:def 1;
end;
suppose
A69: i=n2;
hence z1=(g|n2).n2 by A20,A53,A55,FINSEQ_1:64
.=g.(0+n1) by A9,FINSEQ_3:112
.=g.(i-'n2+n1) by A69,XREAL_1:232;
end;
end;
i-'n2n1;
set k=len g-'n2;
set g2=(g|n1)^(g/^n2);
A76: len (g/^n2)=len g-n2 by A13,RFINSEQ:def 1;
len g-n2>=0 by A13,XREAL_1:48;
then
A77: len g-'n2=len g-n2 by XREAL_0:def 2;
A78: len (g|n1)=n1 by A15,FINSEQ_1:59;
then
A79: g2.1=(g|n1).1 by A12,FINSEQ_1:64
.=x1 by A5,A12,FINSEQ_3:112;
A80: len g2=len (g|n1)+len (g/^n2) by FINSEQ_1:22
.=n1+(len g-n2) by A13,A78,RFINSEQ:def 1;
per cases by A13,XXREAL_0:1;
suppose
n2= 1 by A80,A82;
let i be Nat,z1 be Element of FT;
assume that
A84: 1<=i and
A85: i=n1;
i-n1n1;
then
A97: i-n1>0 by XREAL_1:50;
then i-'n1=i-n1 by XREAL_0:def 2;
then
A98: 0+1<=i-'n1 by A97,NAT_1:13;
then
A99: i-'n1 in dom (g/^n2) by A76,A93,FINSEQ_3:25;
thus z1=(g/^n2).(i-'n1) by A76,A86,A93,A95,A98,FINSEQ_1:65
.=g.(i-'n1+n2) by A13,A99,RFINSEQ:def 1;
end;
suppose
A100: i=n1;
hence z1=(g|n1).n1 by A78,A84,A86,FINSEQ_1:64
.=g.(0+n2) by A9,FINSEQ_3:112
.=g.(i-'n1+n2) by A100,XREAL_1:232;
end;
end;
i-'n1= 1 by A7,A11,A80,A108,FINSEQ_1:1;
let i be Nat,z1 be Element of FT;
assume that
A111: 1<=i and
A112: i=n1;
i-n1n1;
then
A124: i-n1>0 by XREAL_1:50;
then i-'n1=i-n1 by XREAL_0:def 2;
then
A125: 0+1<=i-'n1 by A124,NAT_1:13;
then
A126: i-'n1 in dom (g/^n2) by A109,A120,FINSEQ_3:25;
thus z1=(g/^n2).(i-'n1) by A109,A113,A120,A122,A125,FINSEQ_1:65
.=g.(i-'n1+n2) by A13,A126,RFINSEQ:def 1;
end;
suppose
A127: i=n1;
hence z1=(g|n1).n1 by A78,A111,A113,FINSEQ_1:64
.=g.(0+n2) by A9,FINSEQ_3:112
.=g.(i-'n1+n2) by A127,XREAL_1:232;
end;
end;
i-'n1j & f.j in
U_FT y holds i=j+1 or j=i+1;
end;
theorem Th55:
for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is
inv_continuous
proof
let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: FT is symmetric;
A3: g.1=x1 by A1;
A4: g.(len g)=x2 by A1;
A5: g is continuous by A1;
hence 1<=len g;
let i2,j2 be Nat,y be Element of FT;
assume that
A6: 1<=i2 and
A7: i2<=len g and
A8: 1<=j2 and
A9: j2<= len g and
A10: y=g.i2 and
A11: i2<>j2 and
A12: g.j2 in U_FT y;
A13: rng g c=A by A1;
hereby
assume that
A14: i2<>j2+1 and
A15: j2<>i2+1;
per cases by A11,XXREAL_0:1;
suppose
A16: i2n2 by A8,XREAL_1:233;
1=0 by A21,XREAL_1:48;
then
A24: len g-'n1=len g-n1 by XREAL_0:def 2;
A25: len g2=len (g|n2)+len (g/^n1) by FINSEQ_1:22
.=n2+(len g-n1) by A21,A19,RFINSEQ:def 1;
A26: g2.1=(g|n2).1 by A6,A19,FINSEQ_1:64
.=x1 by A3,A6,FINSEQ_3:112;
now
per cases by A21,XXREAL_0:1;
suppose
n1= 1 by A25,A28;
let i be Nat,z1 be Element of FT;
assume that
A30: 1<=i and
A31: i=n2;
i-n2n2;
then
A44: i-n2>0 by XREAL_1:50;
then i-'n2=i-n2 by XREAL_0:def 2;
then
A45: 0+1<=i-'n2 by A44,NAT_1:13;
then
A46: i-'n2 in dom (g/^n1) by A22,A39,FINSEQ_3:25;
A47: z2=(g/^n1).(i-'n2+1) by A40,A42,FINSEQ_1:65,NAT_1:12
.=g.(i-'n2+1+n1) by A21,A43,RFINSEQ:def 1
.=g.(i-'n2+n1+1);
A48: 1<=i-'n2+n1 & i-'n2+n1n2 by A6,XREAL_1:233;
1=0 by A60,XREAL_1:48;
then
A63: len g-'n1=len g-n1 by XREAL_0:def 2;
A64: len g2=len (g|n2)+len (g/^n1) by FINSEQ_1:22
.=n2+(len g-n1) by A60,A58,RFINSEQ:def 1;
A65: g2.1=(g|n2).1 by A8,A58,FINSEQ_1:64
.=x1 by A3,A8,FINSEQ_3:112;
now
per cases by A60,XXREAL_0:1;
suppose
n1= 1 by A64,A67;
let i be Nat,z1 be Element of FT;
assume that
A69: 1<=i and
A70: i=n2;
i-n2n2;
then
A83: i-n2>0 by XREAL_1:50;
then i-'n2=i-n2 by XREAL_0:def 2;
then
A84: 0+1<=i-'n2 by A83,NAT_1:13;
then
A85: i-'n2 in dom (g/^n1) by A61,A78,FINSEQ_3:25;
A86: z2=(g/^n1).(i-'n2+1) by A79,A81,FINSEQ_1:65,NAT_1:12
.=g.(i-'n2+1+n1) by A60,A82,RFINSEQ:def 1
.=g.(i-'n2+n1+1);
A87: 1<=i-'n2+n1 & i-'n2+n1x2
holds (for i being Nat st 1*x2;
A4: dom g=Seg len g by FINSEQ_1:def 3;
A5: g is continuous by A1;
then
A6: 1<=len g;
then
A7: len g in dom g by A4;
then
A8: g.len g=g/.len g by PARTFUN1:def 6;
A9: g is inv_continuous by A1,A2,Th55;
then
A10: 1<=len g;
thus for i being Nat st 1**=1 implies not g.(i+1) in Finf(B0,i-'1))
proof
let g be FinSequence of FT,A be non empty Subset of FT, x1,x2 be Element of
FT, B0 be Subset of FT|A;
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: FT is filled symmetric and
A3: B0={x1};
A4: rng g c=A by A1;
defpred P[Nat] means $1+1 <=len g implies g.($1+1) in Finf(B0,$1) & ($1>=1
implies not g.($1+1) in Finf(B0,$1-'1));
defpred Q[Nat] means for y being Element of FT st y in Finf(B0,$1
) holds ex h being FinSequence of FT st h is continuous & rng h c= A & h.1=x1 &
h.len h=y & len h <= $1+1;
A5: [#](FT|A)=A by Def3;
A6: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A7: Q[k];
for y being Element of FT st y in Finf(B0,k+1) holds ex h being
FinSequence of FT st h is continuous & rng h c= A & h.1=x1 & h.len h=y & len h
<= k+1+1
proof
let y be Element of FT;
A8: Finf(B0,k+1)=(Finf(B0,k))^f by FINTOPO3:31;
assume y in Finf(B0,k+1);
then consider x being Element of FT|A such that
A9: x=y and
A10: ex y2 being Element of FT|A st y2 in Finf(B0,k) & x in U_FT y2 by A8;
A11: [#](FT|A)=A by Def3;
then
A12: {y} c= A by A9,ZFMISC_1:31;
consider y2 being Element of FT|A such that
A13: y2 in Finf(B0,k) and
A14: x in U_FT y2 by A10;
y2 in the carrier of (FT|A);
then reconsider y3=y2 as Element of FT by A11;
consider h2 being FinSequence of FT such that
A15: h2 is continuous and
A16: rng h2 c= A and
A17: h2.1=x1 and
A18: h2.len h2=y3 and
A19: len h2 <= k+1 by A7,A13;
U_FT y2=(U_FT y3)/\ A by A11,Def2;
then
A20: y in U_FT y3 by A9,A14,XBOOLE_0:def 4;
reconsider h3=h2^(<*y*>) as FinSequence of FT;
rng(h2^(<*y*>)) = rng h2 \/ rng (<*y*>) & rng (<*y*>)={y} by FINSEQ_1:31
,39;
then
A21: rng h3 c= A by A16,A12,XBOOLE_1:8;
1<= len h2 by A15;
then 1 in dom h2 by FINSEQ_3:25;
then
A22: h3.1=x1 by A17,FINSEQ_1:def 7;
len (<*y*>)=1 by FINSEQ_1:40;
then
A23: len h3=len h2 +1 by FINSEQ_1:22;
then
A24: h3.len h3=y by FINSEQ_1:42;
len h3<=k+1+1 by A19,A23,XREAL_1:6;
hence thesis by A15,A18,A20,A21,A22,A24,Th43;
end;
hence thesis;
end;
A25: g.1=x1 by A1;
then
A26: g.1 in {x1} by TARSKI:def 1;
A27: g.(len g)=x2 by A1;
A28: g is continuous by A1;
then 1<=len g;
then 1 in dom g by FINSEQ_3:25;
then x1 in rng g by A25,FUNCT_1:def 3;
then
A29: {x1} c= A by A4,ZFMISC_1:31;
for y being Element of FT st y in Finf(B0,0) holds ex h being
FinSequence of FT st h is continuous & rng h c= A & h.1=x1 & h.len h=y & len h
<= 0+1
proof
let y be Element of FT;
A30: len (<*x1*>)=1 by FINSEQ_1:40;
assume y in Finf(B0,0);
then y in {x1} by A3,FINTOPO3:32;
then
A31: y=x1 by TARSKI:def 1;
rng (<*x1*>)={x1} & (<*x1*>).1=x1 by FINSEQ_1:39,40;
hence thesis by A29,A31,A30;
end;
then
A32: Q[0];
A33: for k being Nat holds Q[k] from NAT_1:sch 2(A32,A6);
A34: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A35: P[k];
per cases;
suppose
k+1+1>len g;
hence thesis;
end;
suppose
A36: k+1+1<=len g;
A37: 1<=k+1 by NAT_1:12;
then 10;
then k>=0+1 by NAT_1:13;
then k=k-'1+1 by XREAL_1:235;
hence g.(k+1+1) in Finf(B0,k-'1)^f by A43,FINTOPO3:31;
end;
end;
then consider x being Element of FT|A such that
A45: g.(k+1+1)=x and
ex y being Element of FT|A st y in Finf(B0,k-'1) & x in U_FT y;
x in A by A5;
then reconsider x3=x as Element of FT;
consider h being FinSequence of FT such that
A46: h is continuous and
A47: rng h c= A and
A48: h.1=x1 and
A49: h.len h=x3 and
A50: len h <= k+1 by A33,A43,A45;
reconsider s=h^(g/^(k+1+1)) as FinSequence of FT;
A51: len s=len h +len(g/^(k+1+1)) by FINSEQ_1:22;
g=(g|(k+1+1))^(g/^(k+1+1)) by RFINSEQ:8;
then
A52: len g=len (g|(k+1+1)) + len (g/^(k+1+1)) by FINSEQ_1:22;
A53: 1<=len h by A46;
then len h in dom h by FINSEQ_3:25;
then
A54: h.(len h)=h/.(len h) by PARTFUN1:def 6;
len (g|(k+1+1))=k+1+1 by A36,FINSEQ_1:59;
then
A55: len (g|(k+1+1))>len h by A50,NAT_1:13;
then
A56: len s=1+(k+1+1) by NAT_1:13;
then 1<=len g -(k+1+1) by XREAL_1:19;
then 1<=len (g/^(k+1+1)) by A57,RFINSEQ:def 1;
then
A58: 1 in dom (g/^(k+1+1)) by FINSEQ_3:25;
A59: g.(k+1+1)=g/.(k+1+1) by A41,PARTFUN1:def 6;
A60: g/^(k+1+1) is continuous by A28,A57,Th47;
then 1<= len (g/^(k+1+1));
then len (g/^(k+1+1)) in dom (g/^(k+1+1)) by FINSEQ_3:25;
then
A61: s.(len s)=(g/^(k+1+1)).(len (g/^(k+1+1))) by A51,FINSEQ_1:def 7
.=x2 by A27,A57,JORDAN4:6;
1<=k+1+1 by NAT_1:12;
then g.(k+1+1+1) in U_FT (g/.(k+1+1)) by A28,A57,A59;
then (g/^(k+1+1)).1 in U_FT (h/.(len h)) by A45,A49,A54,A57,A59,A58,
RFINSEQ:def 1;
then
A62: s is continuous by A46,A60,Th44;
1 in dom h by A53,FINSEQ_3:25;
then
A63: s.1=x1 by A48,FINSEQ_1:def 7;
rng (g/^(k+1+1)) c= rng g by FINSEQ_5:33;
then
A64: rng (g/^(k+1+1)) c= A by A4;
rng s = rng h \/ rng (g/^(k+1+1)) by FINSEQ_1:31;
then rng s c= A by A47,A64,XBOOLE_1:8;
hence contradiction by A1,A56,A62,A63,A61;
end;
suppose
A65: k+1+1>=len g;
then g/^(k+1+1)=<*>the carrier of FT by FINSEQ_5:32;
then
A66: s=h by FINSEQ_1:34;
k+1+1=len g by A36,A65,XXREAL_0:1;
hence contradiction by A1,A45,A46,A47,A48,A49,A55,A51,A52,A66;
end;
end;
[#](FT|A)=A by Def3;
then
A67: U_FT y0 = U_FT(g/.(k+1))/\ A by A40,Def2;
g.(k+1+1) in U_FT (g/.(k+1)) by A28,A39,A37,A40;
then g.(k+1+1) in U_FT y0 by A4,A67,A38,XBOOLE_0:def 4;
then
A68: g.(k+1+1) in (Finf(B0,k))^f by A35,A36,NAT_1:13;
k+1-'1=k+1-1 by NAT_D:37
.=k;
hence thesis by A68,A42,FINTOPO3:31;
end;
end;
let i be Element of NAT;
assume i < len g;
then
A69: i+1<=len g by NAT_1:13;
Finf({x1},0)={x1} by FINTOPO3:32
.=Finf(B0,0) by A3,FINTOPO3:32;
then
A70: P[0] by A26,FINTOPO3:32;
for j being Nat holds P[j] from NAT_1:sch 2(A70,A34);
hence thesis by A69;
end;
*