:: Finite Topological Spaces. Finite Topology Concepts and Neighbourhoods
:: by Hiroshi Imura and Masayoshi Eguchi
::
:: Received November 27, 1992
:: Copyright (c) 1992 Association of Mizar Users
environ
vocabulary FIN_TOPO, FUNC, FAM_OP, TOPCON, CAT1, SUB_OP, FUNC_REL, BOOLE,
RCOMP, BORSUK, SFAMILY, GRAPH, FINSEQ, PI, CARDINAL, REAL_1, ANAL,
UNIALG, RELATION;
constructors REAL_1, NAT_1, SUBSET_1, SETFAM_1, CQC_LANG, DOMAIN_1, GROUP_1,
FINSEQ_4;
requirements ARYTM, SUBSET;
notation ARYTM, FINSET_1, TARSKI, BOOLE, REAL_1, NAT_1, SUBSET_1, STRUCT_0,
SETFAM_1, RELSET_1, RELAT_1, FUNCT_1, FUNCT_2, CQC_LANG, DOMAIN_1,
GROUP_1, FINSEQ_1, FINSEQ_4, CARD_1;
clusters SUBSET_1, INT_1, RELSET_1, STRUCT_0, ARYTM, CQC_LANG, FINSEQ_1;
definitions TARSKI, BOOLE, GROUP_1, STRUCT_0;
theorems NAT_1, TARSKI, CQC_LANG, SUBSET_1, AXIOMS, BOOLE, ZFMISC_1, FINSET_1,
REAL_1, REAL_2, INT_1, CARD_1, FINSEQ_4, FUNCT_1, FUNCT_2, FINSEQ_1,
ANAL_1, GROUP_1, CARD_5, RELSET_1;
schemes RECDEF_1, NAT_1, FINSET_1, FINSEQ_2, COMPLSP1;
begin
theorem
Th1:
for A being set,
f being FinSequence of bool A st
(for i being Nat st 1 ó i & i < len f holds ã(f,i) c= ã(f,i+1))
for i, j being Nat st
i ó j & 1 ó i & j ó len f holds ã(f,i) c= ã(f,j)
proof
let A be set;
let f be FinSequence of bool A such that
A1:for i being Nat st 1 ó i & i < len f holds ã(f,i) c= ã(f,i+1);
let i, j be Nat such that
A2:i ó j & 1 ó i & j ó len f;
A3:i+0 ó j implies ã(f,i) c= ã(f,i+0);
A4:now let k be Nat;
A5:i+k+1 = i+(k+1) by AXIOMS:13;
assume A6:i+k ó j implies ã(f,i) c= ã(f,i+k);
assume i+(k+1) ó j;
then A7:i+k < j by NAT_1:38,A5;
i+k ò i by NAT_1:29;
then i+k ò 1 & i+k < len f by AXIOMS:22, A2, A7;
then ã(f,i+k) c= ã(f,i+(k+1)) by A1, A5;
hence ã(f,i) c= ã(f,i+(k+1)) by BOOLE:29, A7,A6;
end;
A8:for k being Nat st i+k ó j holds ã(f,i) c= ã(f,i+k) from Ind(A3,A4);
consider k be Nat such that
A9:i+k = j by A2, NAT_1:28;
thus ã(f,i) c= ã(f,j) by A8, A9;
end;
theorem
Th2:
for A being set,
f being FinSequence of bool A st
(for i being Nat st 1 ó i & i < len f holds ã(f,i) c= ã(f,i+1))
for i, j being Nat st
i < j & 1 ó i & j ó len f & ã(f,j) c= ã(f,i)
for k being Nat st i ó k & k ó j holds ã(f,j) = ã(f,k)
proof
let A be set;
let f be FinSequence of bool A such that
A1:for i being Nat st 1 ó i & i < len f holds ã(f,i) c= ã(f,i+1);
let i, j be Nat ; assume
A2:i < j & 1 ó i & j ó len f & ã(f,j) c= ã(f,i);
then A3:i+0 ó j implies ã(f,j) c= ã(f,i+0);
A4:now let k be Nat;
A5:i+k+1 = i+(k+1) by AXIOMS:13;
assume A6:i+k ó j implies ã(f,j) c= ã(f,i+k);
assume i+(k+1) ó j;
then A7:i+k < j by NAT_1:38,A5;
i+k ò i by NAT_1:29;
then i+k ò 1 & i+k < len f by AXIOMS:22, A2, A7;
then ã(f,i+k) c= ã(f,i+k+1) by A1;
hence ã(f,j) c= ã(f,i+(k+1)) by BOOLE:29, A7,A6, A5;
end;
A8:for k being Nat st i+k ó j holds ã(f,j) c= ã(f,i+k) from Ind(A3,A4);
let k be Nat ; assume A9:i ó k & k ó j;
then consider m be Nat such that
A10:k = i + m by NAT_1:28;
A11:ã(f,j) c= ã(f,k) by A8, A10, A9;
1 ó k by A2, A9, AXIOMS:22;
then ã(f,k) c= ã(f,j) by A9, Th1, A1, A2;
hence ã(f,j) = ã(f,k) by BOOLE:def 8, A11;
end;
theorem Th3:
for F being set st
F is finite &
F <> í &
for B, C being set st
B î F & C î F holds B c= C or C c= B
ex m being set st
m î F &
for C being set st C î F holds C c= m
proof
defpred P[set] means $1 <> í implies
ex m being set st m î $1 & for C being set st C î $1 holds C c= m;
let F be set such that
A1: F is finite and
A2: F <> í and
A3: for B,C being set st B î F & C î F holds B c= C or C c= B;
A4: P[í];
A5: now let x,B be set such that A6:x î F & B c= F & P[B];
now per cases; :: we have to prove P[BU{x}]
suppose A7:not ex y being set st y î B & x c= y;
assume B U {x} <> í;
take m = x;
x î {x} by TARSKI:def 1;
hence m î B U {x} by BOOLE:def 2;
let C be set;
assume C î B U {x};
then A8: CîB or Cî{x} by BOOLE:def 2;
then not x c= C or C=x by A7,TARSKI:def 1;
hence C c= m by A6,A3,A8,TARSKI:def 1;
suppose ex y being set st y î B & x c= y;
then consider y being set such that A9: y î B & x c= y;
assume B U {x} <> í;
consider m being set such that A10:m î B and
A11: for C being set st C î B holds C c= m by A6,A9;
y c= m by A11,A9;
then A12:x c= m by A9,BOOLE:29;
take m;
thus m î B U {x} by A10,BOOLE:def 2;
let C be set;
assume C î B U {x};
then C î B or C î {x} by BOOLE:def 2;
hence C c= m by A11,A12,TARSKI:def 1;
end;
hence P[B U {x}];
end;
P[F] from Finite(A1,A4,A5);
hence thesis by A2;
end;
canceled;
theorem
Th5:
for f being Function st
(for i being Nat holds f.i c= f.(i+1))
for i, j being Nat st
i ó j holds f.i c= f.j
proof
let f be Function such that
A1:for i being Nat holds f.i c= f.(i+1);
let i, j be Nat such that
A2:i ó j;
A3:i+0 ó j implies f.i c= f.(i+0);
A4:now let k be Nat;
A5:i+k+1 = i+(k+1) by AXIOMS:13;
assume A6:i+k ó j implies f.i c= f.(i+k);
assume A7: i+(k+1) ó j;
f.(i+k) c= f.(i+(k+1)) by A1, A5;
hence f.i c= f.(i+(k+1)) by BOOLE:29, A7,NAT_1:38,A5,A6;
end;
A8:for k being Nat st i+k ó j holds f.i c= f.(i+k) from Ind(A3,A4);
consider k be Nat such that
A9:i+k = j by A2, NAT_1:28;
thus f.i c= f.j by A8, A9;
end;
scheme MaxFinSeqEx {X() -> non empty set,
A() -> Subset of X(),
B() -> Subset of X(),
F(Subset of X()) -> Subset of X()}:
ex f being FinSequence of bool X() st
len f > 0 &
ã(f,1)=B() &
(for i being Nat st i > 0 & i < len f holds ã(f,i+1)=F(ã(f,i))) &
F(ã(f,len f))=ã(f,len f) &
(for i, j being Nat st i > 0 & i < j & j ó len f holds
ã(f,i) c= A() & ã(f,i) c= ã(f,j) & ã(f,i) <> ã(f,j))
provided
A1: A() is finite and
A2: B() c= A() and
A3: for A being Subset of X() st A c= A() holds A c= F(A) & F(A) c= A()
proof
consider f being Function of NAT,bool X() such that
A4:f.0 = B() and
A5:for n being (Element of NAT), x being Element of bool X() st
x=f.n holds f.(n+1) = F(x) from LambdaRecExD;
A6:f.0 c= A() by A4, A2;
A7:now
let n be Nat such that A8:f.n c= A();
f.(n+1) = F(f.n) by A5;
hence f.(n+1) c= A() by A3, A8;
end;
A9:for n being Nat holds f.n c= A() from Ind(A6,A7);
A10:rng f c= bool A()
proof
let x be set ; assume
x î rng f;
then x î føNAT by FUNCT_2:104;
then ex k being Nat st k î NAT & f.k=x by FUNCT_2:116;
then x c= A() by A9;
hence x î bool A();
end ;
bool A() is finite by FINSET_1:24, A1;
then A11:rng f is finite by FINSET_1:13, A10;
A12:dom f = NAT by FUNCT_2:94;
then A13:rng f <> í by FUNCT_1:11,A4;
A14:for i being Nat holds f.i c= f.(i+1)
proof
let i be Nat;
A15:f.(i+1) = F(f.i) by A5;
f.i c= A() by A9;
hence f.i c= f.(i+1) by A15,A3;
end;
for B, C being set st B î rng f & C î rng f holds B c= C or C c= B
proof
let B,C be set ; assume
A16:B î rng f & C î rng f;
then consider i being set such that
A17:i î NAT & B = f.i by FUNCT_1:11, A12;
consider j being set such that
A18:j î NAT & C = f.j by FUNCT_1:11, A12, A16;
reconsider i as Nat by A17;
reconsider j as Nat by A18;
now per cases;
case i ó j ;
hence B c= C by A17, A18,Th5,A14;
case j ó i ;
hence C c= B by A17, A18,Th5,A14;
end;
hence B c= C or C c= B;
end;
then consider m being set such that
A19:m î rng f and
A20:for C being set st C î rng f holds C c= m by A11, A13, Th3;
m î føNAT by FUNCT_2:104, A19;
then A21:ex k being Nat st k î NAT & f.k=m by FUNCT_2:116;
consider k being Nat such that
A22:k î NAT & f.k=m and
A23:for n being Nat st n î NAT & f.n=m holds k ó n from Min(A21);
A24: k+1 î Seg(k+1) by FINSEQ_1:6;
A25:k ò 0 by NAT_1:18;
consider z being FinSequence of bool X() such that
A26: len z = k+1 and
A27: for j being Nat st j î Seg(k+1) holds z.j = f.(³.j-1.³) from SeqLambdaD;
take z;
k+1 <> 0 by NAT_1:21;
hence A28:0 < len z by NAT_1:19, A26;
then A29: 0+1 ó len z by NAT_1:38;
then A30:1 î Seg(k+1) by FINSEQ_1:3, A26;
thus ã(z,1) = z.1 by FINSEQ_4:24, A29
.= f.(³.1-1.³) by A27, A30
.= f.(³.0.³) by REAL_1:36
.= B() by ANAL_1:7,A4;
thus A31:for i being Nat st i > 0 & i < len z holds ã(z,i+1)=F(ã(z,i))
proof
let i be Nat ; assume
A32:i > 0 & i < len z;
then A33: 0+1 ó i & i ó k+1 by NAT_1:38, A26;
then A34:i î Seg(k+1) by FINSEQ_1:3;
then A35:z.i = f.(³.i-1.³) by A27;
0+1 < i+1 by REAL_1:59, A32;
then A36:1 ó i+1 & i+1 ó k+1 by NAT_1:38, A32, A26;
then A37:i+1 î Seg(k+1) by FINSEQ_1:3;
1-1 ó i-1 by REAL_1:49, A33;
then A38:0 ó (i-1)ù1 by REAL_1:36;
A39: i î dom z by A34,A26,FINSEQ_1:def 3;
thus ã(z,i+1) = z.(i+1) by FINSEQ_4:24, A36, A26
.= f.(³.i+1-1.³) by A27, A37
.= f.(³.i-1+1.³) by REAL_2:22
.= f.(³.i-1.³+³.1.³) by ANAL_1:24, A38
.= f.(³.i-1.³+1) by ANAL_1:2
.= F(f.(³.i-1.³)) by A5
.= F(ã(z,i)) by A39,FINSEQ_4:def 4,A35;
end;
thus F(ã(z,len z))=ã(z,len z)
proof
A40:f.k c= f.(k+1) by A14;
k+1 î NAT ;
then k+1 î dom f by FUNCT_2:94;
then f.(k+1) î rng f by FUNCT_1:12;
then A41: f.(k+1) c= f.k by A22, A20;
A42: len z = 0 or len z î Seg(len z) by FINSEQ_1:5; then
A43: len z î dom z by A28,FINSEQ_1:def 3;
A44:z.len z = f.(³.k+1-1.³) by A26,A27,A28,A42
.= f.(³.k+(1-1).³) by REAL_1:17
.= f.(³.k+0.³) by REAL_1:36
.= f.(³.k.³)
.= f.k by A25, ANAL_1:1;
hence F(ã(z,len z)) = F(f.k) by A43,FINSEQ_4:def 4
.= f.(k+1) by A5
.= z.len z by A41,A40,BOOLE:def 8,A44
.= ã(z,len z) by A43,FINSEQ_4:def 4;
end;
let i, j be Nat ; assume A45:0 < i & i < j & j ó len z;
then A46: 0+1 ó i by NAT_1:38;
A47:i ó len z by A45, AXIOMS:22;
A48:i < len z by A45, AXIOMS:22 ;
reconsider l = i-1 as Nat by INT_1:18,A46;
A49:i î Seg(k+1) by A46, A47, A26, FINSEQ_1:3;
1-1 ó i-1 by A46, REAL_1:49;
then A50:0 ó i-1 by REAL_1:36;
A51:ã(z,i) = z.i by FINSEQ_4:24, A46, A47
.= f.(³.i-1.³) by A27, A49
.= f.l by ANAL_1:1, A50;
hence ã(z,i) c= A() by A9;
A52:for i being Nat st 1 ó i & i < len z holds ã(z,i) c= ã(z,i+1)
proof
let i be Nat ; assume
A53:1 ó i & i < len z;
then A54:i î Seg(k+1) by FINSEQ_1:3, A26;
1-1 ó i-1 by A53, REAL_1:49;
then A55:0 ó i-1 by REAL_1:36;
A56:ã(z,i) = z.i by FINSEQ_4:24, A53
.= f.(³.i-1.³) by A27, A54
.= f.(i-1) by ANAL_1:1, A55;
A57:1 ó i+1 & i+1 ó len z by NAT_1:38, A53;
then A58:i+1 î Seg(k+1) by A26, FINSEQ_1:3;
1-1 ó i+1-1 by A57, REAL_1:49;
then A59:0 ó i+1-1 by REAL_1:36;
A60:ã(z,i+1) = z.(i+1) by FINSEQ_4:24, A57
.= f.(³.i+1-1.³) by A27, A58
.= f.(i+1-1) by ANAL_1:1, A59
.= f.(i-1+1) by REAL_2:22;
i-1 is Nat by INT_1:16, A55;
hence ã(z,i) c= ã(z,i+1) by A56, A60,A14;
end;
hence ã(z,i) c= ã(z,j) by Th1, A45, A46;
assume A61: ã(z,i) = ã(z,j) ;
i ó i+1 & i+1 ó j by NAT_1:38, A45;
then A62:ã(z,i) = ã(z,i+1) by A61,Th2,A52,A46,A45
.= F(ã(z,i)) by A31, A48, A45 ;
A63:i+0 ó len z implies ã(z,i) = ã(z,i+0);
A64:now
let n be Nat such that A65:i+n ó len z implies ã(z,i) = ã(z,i+n) ;
i+n ò i by NAT_1:29 ;
then A66:i+n > 0 by AXIOMS:22, A45 ;
assume i+(n+1) ó len z ;
then i+n+1 ó len z by AXIOMS:13;
then i+n < len z by NAT_1:38 ;
hence ã(z,i) = ã(z,i+n+1) by A62,A65,A31, A66
.= ã(z,i+(n+1)) by AXIOMS:13;
end;
A67:for n being Nat st i+n ó len z holds ã(z,i) = ã(z,i+n) from Ind(A63,A64
) ;
consider n0 being Nat such that A68:i+n0 = len z by NAT_1:28, A47 ;
A69: k+1 î dom z by A26,A24,FINSEQ_1:def 3;
f.l = ã(z,k+1) by A51, A26,A67,A68
.= z.(k+1) by A69,FINSEQ_4:def 4
.= f.(³.k+1-1.³) by A27, A24
.= f.(³.k.³) by REAL_2:11
.= m by ANAL_1:1,A25,A22 ;
then k ó l by A23 ;
then len z ó l + 1 by REAL_1:53, A26 ;
then len z ó i by REAL_2:12 ;
hence contradiction by A45,AXIOMS:22;
end ;
struct ( 1-sorted ) FT_Space_Str
® carrier -> set,
Nbd -> Function of the carrier, bool the carrier¯;
definition
cluster non empty strict FT_Space_Str;
existence
proof consider D being non empty set,f being Function of D, bool D;
take FT_Space_Str®D,f¯;
thus the carrier of FT_Space_Str®D,f¯ is non empty;
thus thesis;
end;
end;
reserve FT for non empty FT_Space_Str;
reserve x, y, z for Element of the carrier of FT;
definition
let FT be non empty FT_Space_Str;
let x be Element of the carrier of FT;
func U_FT x -> Subset of the carrier of FT equals
:Def1:
( the Nbd of FT ).x;
correctness;
end;
theorem
for FT being non empty FT_Space_Str,
x being Element of the carrier of FT holds
U_FT x = ( the Nbd of FT ).x by Def1;
definition
let x be set,
y be Subset of {x};
redefine func x.-->y -> Function of {x}, bool {x};
coherence
proof
A1: dom ( x.-->y ) = {x} by CQC_LANG:5;
A2: rng ( x.-->y ) = {y} by CQC_LANG:5;
rng ( x.-->y ) c= bool{x}
proof let a be set; thus thesis by A2; end;
then reconsider R = x.-->y as Relation of {x}, bool {x} by A1
,RELSET_1:11;
R is quasi_total by A1,FUNCT_2:def 1;
hence thesis;
end;
end;
definition
func FT{0} -> strict FT_Space_Str equals
:Def2:
FT_Space_Str ®{0},0.-->ê{0}¯;
correctness;
end;
definition
cluster FT{0} -> non empty;
coherence
proof
thus the carrier of FT{0} is non empty by Def2;
end;
end;
definition let IT be non empty FT_Space_Str;
attr IT is filled means
:Def3:
for x being Element of the carrier of IT holds x î U_FT x ;
end;
theorem Th7:
FT{0} is filled
proof
A1:FT{0} = FT_Space_Str ®{0},0.-->ê{0}¯ by Def2;
let x be Element of the carrier of FT{0};
x = 0 by TARSKI:def 1, A1;
then A2: (0.-->ê{0}).x = ê{0} by CQC_LANG:6;
ê{0} = {0} by SUBSET_1:def 4;
then x î (the Nbd of FT{0}).x by A2, A1;
hence x î U_FT x by Def1;
end;
theorem Th8:
FT{0} is finite
proof
A1: rng <*0*> = {0} by FINSEQ_1:55;
FT{0} = FT_Space_Str ®{0},0.-->ê{0}¯ by Def2;
hence the carrier of FT{0} is finite by A1;
end;
definition
cluster finite filled strict (non empty FT_Space_Str);
existence by Th7, Th8;
end;
definition
let T be 1-sorted,
F be set;
canceled;
pred F is_a_cover_of T means
the carrier of T c= union F;
end;
theorem
for FT being filled (non empty FT_Space_Str) holds
{U_FT x where x is Element of the carrier of FT : not contradiction}
is_a_cover_of FT
proof
let FT be filled (non empty FT_Space_Str);
let a be set;
assume a î the carrier of FT;
then reconsider b = a as Element of the carrier of FT;
A1:b î U_FT b by Def3;
U_FT b î
{U_FT x where x is Element of the carrier of FT : not contradiction};
hence thesis by A1, TARSKI:def 4;
::a î union { U_FT x where x is Element of the carrier of FT : not contradiction };
end;
reserve A, B, C for Subset of the carrier of FT;
definition
let FT;
let A be Subset of the carrier of FT;
func A^ë -> Subset of the carrier of FT equals
:Def6:
{x:U_FT x ï A <> í & U_FT x ï A` <> í};
coherence
proof
set B = {x:U_FT x ï A <> í & U_FT x ï A` <> í};
B is Subset of the carrier of FT from SubsetFD;
hence thesis;
end;
correctness;
end;
theorem Th10:
x î A^ë iff U_FT x ï A <> í & U_FT x ï A` <> í
proof
thus x î A^ë implies U_FT x ï A <> í & U_FT x ï A` <> í
proof
assume x î A^ë;
then x î {y:U_FT y ï A <> í & U_FT y ï A` <> í} by Def6;
then ex y st y=x & U_FT y ï A <> í & U_FT y ï A` <> í;
hence thesis;
end;
assume U_FT x ï A <> í & U_FT x ï A` <> í;
then x î {y:U_FT y ï A <> í & U_FT y ï A` <> í};
hence x î A^ë by Def6;
end;
definition
let FT;
let A be Subset of the carrier of FT;
func A^ëi -> Subset of the carrier of FT equals
:Def7:
A ï (A^ë);
correctness;
func A^ëo -> Subset of the carrier of FT equals
:Def8:
A` ï (A^ë);
correctness;
end;
theorem
A^ë = A^ëi U A^ëo
proof
for x being set holds x î A^ë iff x î A^ëi U A^ëo
proof
let x be set;
A^ë c= (the carrier of FT);
then A1:A^ë c= ê(the carrier of FT) by SUBSET_1:20;
thus x î A^ë implies x î A^ëi U A^ëo
proof
assume x î A^ë;
then x î ê(the carrier of FT) ï (A^ë) by BOOLE:42, A1;
then x î (A U A`) ï (A^ë) by SUBSET_1:25;
then x î A ï (A^ë) U A` ï (A^ë) by BOOLE:70;
then x î A^ëi U (A` ï (A^ë)) by Def7;
hence x î (A^ëi) U (A^ëo) by Def8;
end;
assume x î A^ëi U A^ëo;
then x î A ï (A^ë) U A^ëo by Def7;
then x î A ï (A^ë) U A` ï (A^ë) by Def8;
then x î (A U A`) ï (A^ë) by BOOLE:70;
then x î ê(the carrier of FT) ï (A^ë) by SUBSET_1:25;
hence x î A^ë by BOOLE:42, A1;
end;
hence A^ë = A^ëi U A^ëo by TARSKI:2;
end;
definition
let FT;
let A be Subset of the carrier of FT;
func A^i -> Subset of the carrier of FT equals
:Def9:
{x:U_FT x c= A};
coherence
proof
set B = {x:U_FT x c= A};
B is Subset of the carrier of FT from SubsetFD;
hence thesis;
end;
correctness;
func A^b -> Subset of the carrier of FT equals
:Def10:
{x:U_FT x ï A <> í};
coherence
proof
set B = {x:U_FT x ï A <> í};
B is Subset of the carrier of FT from SubsetFD;
hence thesis;
end;
correctness;
func A^s -> Subset of the carrier of FT equals
:Def11:
{x:x î A & (U_FT x \ {x}) ï A = í};
coherence
proof
set B = {x:x î A & (U_FT x \ {x}) ï A = í};
B is Subset of the carrier of FT from SubsetFD;
hence thesis ;
end;
correctness;
end;
definition
let FT;
let A be Subset of the carrier of FT;
func A^n -> Subset of the carrier of FT equals
:Def12:
A \ A^s;
correctness;
func A^f -> Subset of the carrier of FT equals
:Def13:
{x:ex y st y î A & x î U_FT y};
coherence
proof
set B = {x:ex y st y î A & x î U_FT y};
B is Subset of the carrier of FT from SubsetFD;
hence thesis ;
end;
correctness;
end;
definition let IT be non empty FT_Space_Str;
attr IT is symmetric means
:Def14:
for x, y being Element of the carrier of IT holds
y î U_FT x implies x î U_FT y ;
end;
theorem Th12:
x î A^i iff U_FT x c= A
proof
thus x î A^i implies U_FT x c= A
proof
assume x î A^i ;
then x î {y:U_FT y c= A} by Def9;
then ex y st y=x & U_FT y c= A;
hence thesis ;
end;
assume U_FT x c= A;
then x î {y:U_FT y c= A};
hence x î A^i by Def9;
end;
theorem Th13:
x î A^b iff U_FT x ï A <> í
proof
thus x î A^b implies U_FT x ï A <> í
proof
assume x î A^b ;
then x î {y:U_FT y ï A <> í} by Def10 ;
then ex y st y = x & U_FT y ï A <> í;
hence thesis ;
end;
assume U_FT x ï A <> í ;
then x î {y:U_FT y ï A <> í} ;
hence x î A^b by Def10;
end;
theorem Th14:
x î A^s iff x î A & (U_FT x \ {x}) ï A = í
proof
thus x î A^s implies x î A & (U_FT x \ {x}) ï A = í
proof
assume x î A^s ;
then x î {y:y î A & (U_FT y \ {y}) ï A = í} by Def11;
then ex y st y = x & y î A & (U_FT y \ {y}) ï A = í;
hence thesis;
end;
assume x î A & (U_FT x \ {x}) ï A = í;
then x î {y:y î A & (U_FT y \ {y}) ï A = í};
hence x î A^s by Def11;
end;
theorem
x î A^n iff x î A & (U_FT x \ {x}) ï A <> í
proof
thus x î A^n implies x î A & (U_FT x \ {x}) ï A <> í
proof
assume x î A^n;
then x î A \ A^s by Def12;
then x î A & not x î A^s by BOOLE:def 4;
hence x î A & (U_FT x \ {x}) ï A <> í by Th14;
end;
assume x î A & (U_FT x \ {x}) ï A <> í;
then x î A & not x î A^s by Th14;
then x î A \ A^s by BOOLE:def 4;
hence x î A^n by Def12;
end;
theorem Th16:
x î A^f iff ex y st y î A & x î U_FT y
proof
thus x î A^f implies ex y st y î A & x î U_FT y
proof
assume x î A^f ;
then x î {y:ex z st z î A & y î U_FT z} by Def13 ;
then ex y st y = x & ex z st z î A & y î U_FT z ;
hence thesis ;
end;
assume ex z st z î A & x î U_FT z ;
then x î {y:ex z st z î A & y î U_FT z} ;
hence x î A^f by Def13 ;
end;
theorem
FT is symmetric iff for A holds A^b = A^f
proof
thus FT is symmetric implies for A holds A^b = A^f
proof
assume A1:FT is symmetric ;
let A be Subset of the carrier of FT ;
thus A^b c= A^f
proof
let x be set ;
assume A2:x î A^b ;
then reconsider y = x as Element of the carrier of FT;
U_FT y ï A <> í by Th13, A2 ;
then consider z such that A3:z î U_FT y ï A by SUBSET_1:10 ;
A4:z î U_FT y & z î A by BOOLE:def 3 , A3 ;
then y î U_FT z by Def14 , A1 ;
hence x î A^f by Th16 , A4 ;
end;
let x be set ;
assume A5:x î A^f ;
then reconsider y = x as Element of the carrier of FT;
consider z such that A6:z î A & y î U_FT z by Th16, A5 ;
z î U_FT y by Def14, A1, A6 ;
then U_FT y ï A <> í by BOOLE:def 3, A6 ;
hence x î A^b by Th13;
end;
assume A7:for A being Subset of the carrier of FT holds A^b = A^f ;
let x, y be Element of the carrier of FT ;
assume y î U_FT x ;
then U_FT x ï {y} <> í by ZFMISC_1:54 ;
then x î {y}^b by Th13 ;
then x î {y}^f by A7 ;
then consider z such that A8:z î {y} & x î U_FT z by Th16 ;
thus x î U_FT y by A8,TARSKI:def 1;
end;
reserve F, G for Subset of the carrier of FT ;
definition let FT;
let IT be Subset of the carrier of FT;
attr IT is open means
:Def15:
IT = IT^i ;
attr IT is closed means
:Def16:
IT = IT^b ;
attr IT is connected means
:Def17:
for B,C being Subset of the carrier of FT st
IT = B U C & B <> í & C <> í & B ï C = í holds B^b ï C <> í ;
end;
definition let FT; let A be Subset of the carrier of FT ;
func A^fb -> Subset of the carrier of FT equals
meet{F:A c= F & F is closed} ;
coherence
proof
set FF = {F:A c= F & F is closed} ;
FF c= bool the carrier of FT
proof
let x be set ;
assume x î FF ;
then ex F st x = F & A c= F & F is closed ;
hence x î bool the carrier of FT ;
end;
then reconsider FF as Subset-Family of the carrier of FT;
meet FF is Subset of the carrier of FT ;
hence thesis ;
end;
correctness ;
func A^fi -> Subset of the carrier of FT equals
union{F:A c= F & F is open} ;
coherence
proof
set FF = {F:A c= F & F is open} ;
FF c= bool the carrier of FT
proof
let x be set ;
assume x î FF ;
then ex F st x = F & A c= F & F is open ;
hence x î bool the carrier of FT ;
end;
then reconsider FF as Subset-Family of the carrier of FT;
union FF is Subset of the carrier of FT ;
hence thesis ;
end;
correctness ;
end;
theorem
Th18:
for FT being filled (non empty FT_Space_Str),
A being Subset of the carrier of FT holds
A c= A^b
proof
let FT be filled (non empty FT_Space_Str);
let A be Subset of the carrier of FT;
let x be set;
assume A1:x î A;
then reconsider y=x as Element of the carrier of FT;
y î U_FT y by Def3;
then U_FT y ï A <> í by A1, BOOLE:def 3;
hence x î A^b by Th13;
end;
theorem
Th19:
for FT being non empty FT_Space_Str,
A, B being Subset of the carrier of FT holds
A c= B implies A^b c= B^b
proof
let FT be non empty FT_Space_Str;
let A, B be Subset of the carrier of FT;
assume A1:A c= B;
let x be set;
assume A2:x î A^b;
then reconsider y=x as Element of the carrier of FT;
U_FT y ï A <> í by Th13, A2;
then consider w being Element of the carrier of FT such that
A3:w î (U_FT y ï A) by SUBSET_1:10;
w î U_FT y & w î A by BOOLE:def 3, A3;
then U_FT y ï B <> í by BOOLE:def 3,A1;
hence x î B^b by Th13;
end;
theorem
for FT being filled finite (non empty FT_Space_Str),
A being Subset of the carrier of FT holds
A is connected iff for x being Element of the carrier of FT st x î A
ex S being FinSequence of bool the carrier of FT st
len S > 0 &
ã(S,1) = {x} &
(for i being Nat st i > 0 & i < len S holds ã(S,i+1) = ã(S,i)^b ï A) &
A c= ã(S,len S)
proof
let FT be filled finite (non empty FT_Space_Str),
A being Subset of the carrier of FT;
thus A is connected implies for x being Element of the carrier of FT st x î A
ex S being FinSequence of bool the carrier of FT st
len S > 0 &
ã(S,1) = {x} &
(for i being Nat st i > 0 & i < len S holds ã(S,i+1) = ã(S,i)^b ï A) &
A c= ã(S,len S)
proof
assume A1:A is connected;
let x be Element of the carrier of FT such that A2:x î A ;
the carrier of FT is finite & A c= the carrier of FT
by GROUP_1:def 13;
then A3: A is finite by FINSET_1:13 ;
A4: {x} c= A by ZFMISC_1:37, A2 ;
A5:for B being Subset of the carrier of FT st B c= A
holds B c= B^b ï A & B^b ï A c= A
proof
let B be Subset of the carrier of FT such that A6:B c= A ;
B c= B^b by Th18 ;
hence B c= B^b ï A by BOOLE:39, A6 ;
thus B^b ï A c= A by BOOLE:37 ;
end;
consider S being FinSequence of bool the carrier of FT such that
A7:len S > 0 and
A8:ã(S,1)={x} and
A9:(for i being Nat st i > 0 & i < len S holds ã(S,i+1)=ã(S,i)^b ï A) and
A10:ã(S,len S)^b ï A = ã(S,len S) and
A11:(for i, j being Nat st i > 0 & i < j & j ó len S holds
ã(S,i) c= A & ã(S,i) c= ã(S,j) & ã(S,i) <> ã(S,j))
from MaxFinSeqEx(A3,A4,A5) ;
take S ;
thus len S > 0 by A7 ;
thus ã(S,1) = {x} by A8 ;
thus for i being Nat st
i > 0 & i < len S holds ã(S,i+1) = ã(S,i)^b ï A by A9;
set B = ã(S,len S) ;
set C = A \ B ;
A12:B c= A by BOOLE:37, A10 ;
A13:B U C = B U A by BOOLE:79
.= A by BOOLE:35, A12 ;
assume not A c= ã(S,len S) ;
then A14:C <> í by BOOLE:45 ;
A15:0 < len S implies ã(S,0 + 1) <> í by A8 ;
A16:now let i be Nat ;
assume A17:i < len S implies ã(S,i+1) <> í ;
assume A18:i + 1 < len S ;
i+1 <> 0 by NAT_1:21;
then A19:i+1 > 0 by NAT_1:19;
A20:i+1 < i+1+1 by NAT_1:38;
i+1+1 ó len S by NAT_1:38, A18;
then ã(S,i+1) c= ã(S,i+1+1) by A11, A19, A20;
hence ã(S,i+1+1) <> í by BOOLE:30, NAT_1:38,A17,A18 ;
end ;
A21:for i being Nat st i < len S holds ã(S,i+1) <> í from Ind(A15,A16) ;
consider k being Nat such that
A22:len S = k+1 by NAT_1:22,A7 ;
k < len S by NAT_1:38, A22 ;
then A23:B <> í by A21, A22 ;
A24:B ï C = í by BOOLE:78 ;
A \ B c= A by BOOLE:49 ;
then B^b ï C = B^b ï ( A ï ( A \ B ) ) by BOOLE:42
.= B ï ( A \ B ) by BOOLE:67,A10
.= í by BOOLE:78 ;
hence contradiction by A1, Def17, A13, A14, A23, A24 ;
end ;
assume A25:for x being Element of the carrier of FT st x î A
ex S being FinSequence of bool the carrier of FT st
len S > 0 &
ã(S,1) = {x} &
(for i being Nat st i > 0 & i < len S holds
ã(S,i+1) = ã(S,i)^b ï A) &
A c= ã(S,len S) ;
::assume A is not connected ;
given B, C being Subset of the carrier of FT such that
A26:A = B U C and
A27:B <> í and
A28:C <> í and
A29:B ï C = í and
A30:B^b ï C = í;
A31: B c= B^b by Th18 ;
A32: B^b ï A = B^b ï B U í by A26,A30, BOOLE:70
.= B^b ï B by BOOLE:60
.= B by BOOLE:42, A31 ;
consider x being Element of B ;
x î A by A26, BOOLE:def 2,A27 ;
then consider S being FinSequence of bool the carrier of FT such that
A33:len S > 0 and
A34:ã(S,1) = {x} and
A35:for i being Nat st i > 0 & i < len S holds ã(S,i+1) = ã(S,i)^b ï A and
A36:A c= ã(S,len S) by A25 ;
A37:B c= A by A26, BOOLE:31 ;
A38:0 < len S implies ã(S,0+1) c= B by ZFMISC_1:37, A34, A27 ;
A39:now let i be Nat ;
assume A40:i < len S implies ã(S,i+1) c= B ;
assume A41:i+1 < len S ;
then ã(S,i+1)^b c= B^b by Th19,A40,NAT_1:38 ;
then A42:ã(S,i+1)^b ï A c= B^b ï A by BOOLE:40 ;
i+1 <> 0 by NAT_1:21 ;
then i+1 > 0 by NAT_1:19 ;
hence ã(S,i+1+1) c= B by A42, A32,A35,A41 ;
end;
A43:for i being Nat st i < len S holds ã(S,i+1) c= B from Ind(A38,A39);
consider k being Nat such that A44:len S = k + 1 by NAT_1:22,A33 ;
k < len S by NAT_1:38, A44 ;
then A45:ã(S,len S) c= B by A43, A44 ;
then ã(S,len S) c= A by BOOLE:29, A37 ;
then ã(S,len S) = A by BOOLE:def 8, A36 ;
then A = B by BOOLE:def 8, A37, A45 ;
then C c= B by A26, BOOLE:31 ;
hence contradiction by A28,BOOLE:42,A29 ;
end;
theorem
Th21:
for E being non empty set,
A being Subset of E,
x being Element of E holds
x î A` iff not x î A
proof
let E be non empty set;
let A be Subset of E;
let x be Element of E;
thus x î A` implies not x î A by SUBSET_1:53;
assume not x î A;
then x î E \ A by BOOLE:def 4;
hence x î A` by SUBSET_1:23;
end;
theorem
Th22:
((A`)^i)` = A^b
proof
for x being set holds x î ((A`)^i)` iff x î A^b
proof
let x be set;
thus x î ((A`)^i)` implies x î A^b
proof
assume A1:x î ((A`)^i)`;
then reconsider y=x as Element of the carrier of FT;
not y î (A`)^i by SUBSET_1:53, A1;
then not U_FT y c= A` by Th12;
then consider z being set such that
A2:not(z î U_FT y implies z î A`) by TARSKI:def 3;
z î (U_FT y) & z î A by Th21, A2;
then U_FT y ï A <> í by BOOLE:def 3;
hence x î A^b by Th13;
end;
assume A3:x î A^b;
then reconsider y=x as Element of the carrier of FT;
U_FT y ï A <> í by Th13, A3;
then consider z being Element of the carrier of FT such that
A4:z î U_FT y ï A by SUBSET_1:10;
z î U_FT y & z î A by BOOLE:def 3, A4;
then not U_FT y c= A` by Th21;
then not y î (A`)^i by Th12;
hence x î ((A`)^i)` by Th21;
end;
hence ((A`)^i)` = A^b by TARSKI:2;
end;
theorem
Th23:
((A`)^b)` = A^i
proof
for x being set holds x î ((A`)^b)` iff x î A^i
proof
let x be set;
thus x î ((A`)^b)` implies x î A^i
proof
assume A1:x î ((A`)^b)`;
then reconsider y=x as Element of the carrier of FT;
not y î (A`)^b by SUBSET_1:53, A1;
then U_FT y ï A` = í by Th13;
then U_FT y \ A = í by SUBSET_1:32;
then U_FT y c= A by BOOLE:45;
hence x î A^i by Th12;
end;
assume A2:x î A^i;
then reconsider y=x as Element of the carrier of FT;
U_FT y c= A by Th12, A2;
then U_FT y \ A = í by BOOLE:45;
then U_FT y ï A` = í by SUBSET_1:32;
then not y î (A`)^b by Th13;
hence x î ((A`)^b)` by Th21;
end;
hence ((A`)^b)` = A^i by TARSKI:2;
end;
theorem
A^ë = ((A^b) ï ((A`)^b))
proof
for x being set holds x î A^ë iff x î ((A^b) ï ((A`)^b))
proof
let x be set;
thus x î A^ë implies x î ((A^b) ï ((A`)^b))
proof
assume A1:x î A^ë;
then reconsider y=x as Element of the carrier of FT;
U_FT y ï A <> í & U_FT y ï A` <> í by Th10, A1;
then x î (A^b) & x î ((A`)^b) by Th13;
hence x î ((A^b) ï ((A`)^b)) by BOOLE:def 3;
end;
assume x î ((A^b) ï ((A`)^b));
then A2:x î A^b & x î (A`)^b by BOOLE:def 3;
then reconsider y=x as Element of the carrier of FT;
U_FT y ï A <> í & U_FT y ï A` <> í by Th13, A2;
hence x î A^ë by Th10;
end;
hence A^ë = ((A^b) ï ((A`)^b)) by TARSKI:2;
end;
theorem
(A`)^ë = A^ë
proof
for x being set holds x î (A`)^ë iff x î A^ë
proof
let x be set;
thus x î (A`)^ë implies x î A^ë
proof
assume A1:x î (A`)^ë;
then reconsider y=x as Element of the carrier of FT;
U_FT y ï (A`) <> í & U_FT y ï (A`)` <> í by Th10, A1;
then U_FT y ï A` <> í & U_FT y ï A <> í by SUBSET_1:24;
hence x î A^ë by Th10;
end;
assume A2:x î A^ë;
then reconsider y=x as Element of the carrier of FT;
U_FT y ï A <> í & U_FT y ï A` <> í by Th10, A2;
then U_FT y ï (A`)` <> í & U_FT y ï A` <> í by SUBSET_1:24;
hence x î (A`)^ë by Th10;
end;
hence (A`)^ë = A^ë by TARSKI:2;
end;
theorem
x î A^s implies not x î (A \ {x})^b
proof
assume x î A^s;
then A ï (U_FT x \ {x}) = í by Th14;
then A1: (A ï U_FT x) \ {x} = í by BOOLE:116;
now per cases by A1,ZFMISC_1:66;
suppose A2:A ï U_FT x = í;
(A \ {x}) c= A by BOOLE:49;
hence (A \ {x}) ï U_FT x = í by BOOLE:55, A2;
suppose A ï U_FT x = {x};
then (U_FT x ï A) \ {x} = í by BOOLE:45;
hence (A \ {x}) ï U_FT x = í by BOOLE:116;
end;
hence not x î (A \ {x})^b by Th13;
end;
theorem
A^s <> í & Card A <> 1 implies A is not connected
proof
assume A1:A^s <> í & Card A <> 1;
then consider z being Element of the carrier of FT such that
A2:z î A^s by SUBSET_1:10;
A3:z î A & (U_FT z \ {z}) ï A = í by Th14, A2;
set B = A \ {z};
set C = {z};
{z} is Subset of A by SUBSET_1:62, A3;
then A4:A = B U C by BOOLE:54;
A5: Card {z} = 1 by CARD_1:50,CARD_5:4;
A <> í by Th14,A2;
then A6:B <> í by ZFMISC_1:66,A5,A1;
A7:B ï C = í by BOOLE:78;
B^b ï C = í
proof
assume B^b ï C <> í;
then consider x being Element of the carrier of FT such that
A8:x î B^b ï C by SUBSET_1:10;
A9:x î B^b & x î C by BOOLE:def 3, A8;
then U_FT x ï B <> í by Th13;
then consider y being Element of the carrier of FT such that
A10:y î (U_FT x) ï B by SUBSET_1:10;
A11:x = z by TARSKI:def 1, A9;
A12:B c= A by BOOLE:49;
A13:not x î B by A9,BOOLE:def 4;
A14:y î U_FT x & y î B by BOOLE:def 3, A10;
then y î U_FT x \ {x} by ZFMISC_1:64,A13;
then (U_FT z \ {z}) ï B <> í by BOOLE:def 3, A14, A11;
then consider w being Element of the carrier of FT such that
A15:w î (U_FT z \ {z}) ï B by SUBSET_1:10;
(U_FT z \ {z}) ï B c= (U_FT z \ {z}) ï A by BOOLE:40, A12;
hence contradiction by A3,A15;
end;
hence A is not connected by Def17, A4, A6, A7;
end;
theorem
for FT being filled (non empty FT_Space_Str),
A being Subset of the carrier of FT holds
A^i c= A
proof
let FT be filled (non empty FT_Space_Str);
let A be Subset of the carrier of FT;
let x be set;
assume A1:x î A^i;
then reconsider y=x as Element of the carrier of FT;
A2:y î U_FT y by Def3;
U_FT y c= A by Th12, A1;
hence x î A by A2;
end;
theorem
for E being set,
A, B being Subset of E holds
A = B iff A` = B`
proof
let E be set;
let A, B be Subset of E;
thus A = B implies A` = B`;
assume A` = B`;
hence A = B`` by SUBSET_1:24
.= B by SUBSET_1:24;
end;
theorem
A is open implies A` is closed
proof
assume A is open;
then A1:A = A^i by Def15;
A^i = ((A`)^b)` by Th23;
then A` = (A`)^b by A1,SUBSET_1:24;
hence A` is closed by Def16;
end;
theorem
A is closed implies A` is open
proof
assume A is closed;
then A1:A = A^b by Def16;
A^b = ((A`)^i)` by Th22;
then A` = (A`)^i by A1,SUBSET_1:24;
hence A` is open by Def15;
end;