:: Finite Topological Spaces. Finite Topology Concepts and Neighbourhoods
:: by Hiroshi Imura and Masayoshi Eguchi
::
:: Received November 27, 1992
:: Copyright (c) 1992-2026 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, FINSEQ_1, ZFMISC_1, SUBSET_1, XXREAL_0, ARYTM_3,
PARTFUN1, TARSKI, NAT_1, CARD_1, XBOOLE_0, FINSET_1, FUNCT_1, RELAT_1,
ORDINAL1, COMPLEX1, ARYTM_1, STRUCT_0, ORDERS_2, EQREL_1, FUNCOP_1,
FUNCT_2, RELAT_2, SETFAM_1, RCOMP_1, FIN_TOPO;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
FINSET_1, SETFAM_1, EQREL_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1,
DOMAIN_1, RELSET_1, FINSEQ_1, INT_2, NAT_1, XXREAL_0, STRUCT_0, ORDERS_2;
constructors DOMAIN_1, FUNCOP_1, REAL_1, INT_2, EQREL_1, FINSEQ_4, ORDERS_2,
RELSET_1, XXREAL_0, MEASURE2, NAT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCOP_1, XREAL_0,
NAT_1, INT_1, STRUCT_0, FINSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, STRUCT_0, ORDINAL1, XBOOLE_0, RELAT_2, ORDERS_2, SETFAM_1;
equalities SUBSET_1, RELAT_1, FUNCOP_1;
expansions TARSKI, XBOOLE_0, ORDERS_2;
theorems NAT_1, TARSKI, FUNCOP_1, SUBSET_1, ZFMISC_1, FINSET_1, INT_1, CARD_1,
FINSEQ_4, FUNCT_1, FUNCT_2, FINSEQ_1, ABSVALUE, RELSET_1, XBOOLE_0,
XBOOLE_1, MEASURE2, XREAL_1, XXREAL_0, ORDINAL1, RELAT_1, EQREL_1,
ORDERS_2, PARTFUN1;
schemes NAT_1, FINSEQ_2, DOMAIN_1;
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 and
A3: 1 <= i and
A4: j <= len f;
consider k be Nat such that
A5: i+k = j by A2,NAT_1:10;
defpred P[Nat] means i+$1 <= j implies f/.i c= f/.(i+$1);
A6: now
let k be Nat;
A7: i+k+1 = i+(k+1);
assume
A8: P[k];
thus P[k+1]
proof
i+k >= i by NAT_1:11;
then
A9: i+k >= 1 by A3,XXREAL_0:2;
assume
A10: i+(k+1) <= j;
then i+k < j by A7,NAT_1:13;
then i+k < len f by A4,XXREAL_0:2;
then f/.(i+k) c= f/.(i+(k+1)) by A1,A7,A9;
hence thesis by A7,A8,A10,NAT_1:13;
end;
end;
A11: P[0];
A12: for k being Nat holds P[k] from NAT_1:sch 2(A11,A6);
thus thesis by A12,A5;
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 1 <= i & j <= len f & f/.j c= f/.i
for k being Nat st i <= 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 < len f holds f/.i c= f/.(i +1);
let i, j be Nat;
assume that
A2: 1 <= i and
A3: j <= len f and
A4: f/.j c= f/.i;
let k be Nat;
assume that
A5: i <= k and
A6: k <= j;
1 <= k by A2,A5,XXREAL_0:2;
then
A7: f/.k c= f/.j by A1,A3,A6,Th1;
defpred P[Nat] means i+$1 <= j implies f/.j c= f/.(i+$1);
A8: now
let k be Nat ;
assume
A9: P[k];
A10: i+k+1 = i+(k+1);
thus P[k+1]
proof
i+k >= i by NAT_1:11;
then
A11: i+k >= 1 by A2,XXREAL_0:2;
assume
A12: i+(k+1) <= j;
then i+k < j by A10,NAT_1:13;
then i+k < len f by A3,XXREAL_0:2;
then f/.(i+k) c= f/.(i+k+1) by A1,A11;
hence thesis by A9,A12,NAT_1:13;
end;
end;
A13: P[0] by A4;
A14: for k being Nat holds P[k] from NAT_1:sch 2(A13,A8);
consider m be Nat such that
A15: k = i + m by A5,NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
k=i+m by A15;
then f/.j c= f/.k by A14,A6;
hence thesis by A7;
end;
scheme
MaxFinSeqEx {X() -> non empty set, A,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
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
deffunc F(Nat,Subset of X()) = F($2);
consider f being sequence of bool X() such that
A4: f.0 = B() and
A5: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 12;
defpred P[Nat] means f.$1 c= A();
A6: now
let n be Nat such that
A7: P[n];
f.(n+1) = F(f.n) by A5;
hence P[n+1] by A3,A7;
end;
A8: P[0] by A2,A4;
A9: for n being Nat holds P[n] from NAT_1:sch 2(A8,A6);
A10: for i being Nat holds f.i c= f.(i+1)
proof
let i be Nat;
f.(i+1) = F(f.i) & f.i c= A() by A5,A9;
hence thesis by A3;
end;
A11: dom f = NAT by FUNCT_2:def 1;
A12: rng f is c=-linear
proof
let B,C be set;
assume B in rng f;
then consider i being object such that
A13: i in NAT and
A14: B = f.i by A11,FUNCT_1:def 3;
reconsider i as Element of NAT by A13;
assume C in rng f;
then consider j being object such that
A15: j in NAT and
A16: C = f.j by A11,FUNCT_1:def 3;
reconsider j as Element of NAT by A15;
i <= j or j <= i;
hence B c= C or C c= B by A10,A14,A16,MEASURE2:18;
end;
A17: rng f c= bool A()
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in rng f;
then x in f.:NAT by RELSET_1:22;
then ex k being Element of NAT st k in NAT & f.k=x by FUNCT_2:65;
then xx c= A() by A9;
hence thesis;
end;
rng f <> {} by A4,A11,FUNCT_1:def 3;
then consider m being set such that
A18: m in rng f and
A19: for C being set st C in rng f holds C c= m by A1,A17,A12,FINSET_1:12;
deffunc G(Nat) = f. |.$1-1.|;
defpred P[set] means $1 in NAT & f.$1=m;
m in f.:NAT by A18,RELSET_1:22;
then ex k being Element of NAT st P[k] by FUNCT_2:65;
then
A20: ex k being Nat st P[k];
consider k being Nat such that
A21: P[k] and
A22: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A20);
consider z being FinSequence of bool X() such that
A23: len z = k+1 and
A24: for j being Nat st j in dom z holds z.j = G(j) from FINSEQ_2:sch 1;
A25: 0+1 <= len z by A23,NAT_1:13;
then
A26: 1 in Seg(k+1) by A23,FINSEQ_1:1;
take z;
thus 0 < len z by A23;
A27: dom z = Seg(k+1) by A23,FINSEQ_1:def 3;
thus z/.1 = z.1 by A25,FINSEQ_4:15
.= f.(|.1-1.|) by A24,A27,A26
.= B() by A4,ABSVALUE:2;
thus
A28: for i being Nat st i > 0 & i < len z holds z/.(i+1)=F(z /.i)
proof
let i be Nat;
assume that
A29: i > 0 and
A30: i < len z;
A31: 0+1 < i+1 & i+1 <= k+1 by A23,A29,A30,NAT_1:13,XREAL_1:6;
then
A32: i+1 in Seg(k+1) by FINSEQ_1:1;
A33: 0+1 <= i by A29,NAT_1:13;
then i in Seg(k+1) by A23,A30,FINSEQ_1:1;
then
A34: z.i = f.(|.i-1.|) & i in dom z by A24,A27;
1-1 <= i-1 by A33,XREAL_1:9;
then
A35: 0 <= (i-1)*1;
thus z/.(i+1) = z.(i+1) by A23,A31,FINSEQ_4:15
.= f.(|.i+1-1.|) by A24,A27,A32
.= f.(|.i-1+1.|)
.= f.(|.i-1.|+|.1.|) by A35,ABSVALUE:11
.= f.(|.i-1.|+1) by ABSVALUE:def 1
.= F(f.(|.i-1.|)) by A5
.= F(z/.i) by A34,PARTFUN1:def 6;
end;
thus F(z/.len z)=z/.len z
proof
k+1 in NAT;
then k+1 in dom f by FUNCT_2:def 1;
then f.(k+1) in rng f by FUNCT_1:def 3;
then
A36: f.(k+1) c= f.k by A19,A21;
reconsider k9=k as Element of NAT by ORDINAL1:def 12;
A37: f.k c= f.(k+1) by A10;
len z = 0 or len z in Seg(len z) by FINSEQ_1:3;
then
A38: len z in dom z by A23,FINSEQ_1:def 3;
A39: z.len z = f.(|.k+1-1.|) by A23,A24,A27,FINSEQ_1:3
.= f.k by ABSVALUE:def 1;
hence F(z/.len z) = F(f.k9) by A38,PARTFUN1:def 6
.= f.(k+1) by A5
.= z.len z by A37,A36,A39
.= z/.len z by A38,PARTFUN1:def 6;
end;
let i, j be Nat;
assume that
A40: 0 < i and
A41: i < j and
A42: j <= len z;
A43: 0+1 <= i by A40,NAT_1:13;
then reconsider l = i-1 as Element of NAT by INT_1:5;
A44: i <= len z by A41,A42,XXREAL_0:2;
then
A45: i in Seg(k+1) by A23,A43,FINSEQ_1:1;
A46: z/.i = z.i by A43,A44,FINSEQ_4:15
.= f.(|.i-1.|) by A24,A27,A45
.= f.l by ABSVALUE:def 1;
hence z/.i c= A() by A9;
A47: for i being Nat st 1 <= i & i < len z holds z/.i c= z/.(i+1)
proof
let i be Nat;
assume that
A48: 1 <= i and
A49: i < len z;
A50: i in Seg(k+1) by A23,A48,A49,FINSEQ_1:1;
A51: 1-1 <= i-1 by A48,XREAL_1:9;
then
A52: i-1 is Element of NAT by INT_1:3;
A53: 1 <= i+1 & i+1 <= len z by A48,A49,NAT_1:13;
then
A54: i+1 in Seg(k+1) by A23,FINSEQ_1:1;
A55: z/.(i+1) = z.(i+1) by A53,FINSEQ_4:15
.= f.(|.i+1-1.|) by A24,A27,A54
.= f.(i-1+1) by ABSVALUE:def 1;
z/.i = z.i by A48,A49,FINSEQ_4:15
.= f.(|.i-1.|) by A24,A27,A50
.= f.(i-1) by A51,ABSVALUE:def 1;
hence thesis by A10,A55,A52;
end;
hence z/.i c= z/.j by A41,A42,A43,Th1;
defpred P[Nat] means i+$1 <= len z implies z/.i = z/.(i+$1);
A56: i <= i+1 & i+1 <= j by A41,NAT_1:13;
k+1 in Seg(k+1) by FINSEQ_1:4;
then
A57: k+1 in dom z by A23,FINSEQ_1:def 3;
A58: i < len z by A41,A42,XXREAL_0:2;
assume z/.i = z/.j;
then
A59: z/.i = z/.(i+1) by A42,A43,A47,A56,Th2
.= F(z/.i) by A28,A40,A58;
A60: now
let n be Nat such that
A61: P[n];
thus P[n+1]
proof
assume i+(n+1) <= len z;
then i+n+1 <= len z;
then i+n < len z by NAT_1:13;
hence z/.i = z/.(i+n+1) by A28,A40,A59,A61
.= z/.(i+(n+1));
end;
end;
consider n0 being Nat such that
A62: i+n0 = len z by A41,A42,NAT_1:10,XXREAL_0:2;
reconsider n0 as Element of NAT by ORDINAL1:def 12;
A63: i+n0=len z by A62;
A64: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A64,A60);
then f.l = z/.(k+1) by A23,A46,A63
.= z.(k+1) by A57,PARTFUN1:def 6
.= f.(|.k+1-1.|) by A24,A27,FINSEQ_1:4
.= m by A21,ABSVALUE:def 1;
then k <= l by A22;
then len z <= l + 1 by A23,XREAL_1:6;
hence contradiction by A41,A42,XXREAL_0:2;
end;
registration
cluster non empty strict for RelStr;
existence
proof
set D = the non empty set,f = the Relation of D;
take RelStr(#D,f#);
thus the carrier of RelStr(#D,f#) is non empty;
thus thesis;
end;
end;
reserve FT for non empty RelStr;
reserve x, y, z for Element of FT;
definition
let FT be RelStr;
let x be Element of FT;
func U_FT x -> Subset of FT equals
Class(the InternalRel of FT,x);
coherence;
end;
definition
let x be set, y be Subset of {x};
redefine func x.-->y -> Function of {x}, bool {x}; :: redefines .--> (FUNCOP_1, definition)
coherence
proof
A1: dom ( x.-->y ) = {x};
rng ( x.-->y ) = {y} by FUNCOP_1:8;
then reconsider R = x.-->y as Relation of {x}, bool {x} by A1,RELSET_1:4;
R is quasi_total by A1,FUNCT_2:def 1;
hence thesis;
end;
end;
definition
let x be set;
func SinglRel x -> Relation of {x} equals
{[x,x]};
coherence
proof
x in {x} by TARSKI:def 1;
hence thesis by RELSET_1:3;
end;
end;
definition
func FT{0} -> strict RelStr equals
RelStr (#{0},SinglRel 0#);
coherence;
end;
registration
cluster FT{0} -> non empty;
coherence;
end;
notation
let IT be non empty RelStr;
synonym IT is filled for IT is reflexive;
end;
definition
let IT be non empty RelStr;
redefine attr IT is filled means :: redefines filled (FIN_TOPO, synonym) → reflexive (ORDERS_2, definition)
:Def4:
for x being Element of IT holds x in U_FT x;
compatibility
proof
thus IT is filled implies for x being Element of IT holds x in U_FT x
proof
assume
A1: IT is filled;
let x be Element of IT;
x <= x by A1,ORDERS_2:1;
then [x,x] in the InternalRel of IT;
hence thesis by EQREL_1:18;
end;
assume
A2: for x being Element of IT holds x in U_FT x;
let x be object;
assume x in the carrier of IT;
then reconsider x as Element of IT;
x in U_FT x by A2;
hence thesis by EQREL_1:18;
end;
end;
theorem Th3:
FT{0} is filled
proof
let x be Element of FT{0};
x = 0 & [0,0] in SinglRel 0 by TARSKI:def 1;
hence thesis by RELAT_1:def 13;
end;
registration
cluster FT{0} -> filled finite;
coherence by Th3;
end;
registration
cluster finite filled strict for non empty RelStr;
existence by Th3;
end;
theorem
for FT being filled non empty RelStr holds the set of all U_FT x where x is
Element of FT is Cover of FT
proof
let FT be filled non empty RelStr;
let a be object;
assume a in the carrier of FT;
then reconsider b = a as Element of FT;
b in U_FT b & U_FT b in the set of all U_FT x where x is Element of FT
by Def4;
hence thesis by TARSKI:def 4;
end;
reserve A for Subset of FT;
definition
let FT;
let A be Subset of FT;
func A^delta -> Subset of FT equals
{x:U_FT x meets A & U_FT x meets A` };
coherence
proof
defpred P[Element of FT] means U_FT $1 meets A & U_FT $1 meets A`;
{ x :P[x]} is Subset of FT from DOMAIN_1:sch 7;
hence thesis;
end;
end;
theorem Th5:
x in A^delta iff U_FT x meets A & U_FT x meets A`
proof
thus x in A^delta implies U_FT x meets A & U_FT x meets A`
proof
assume x in A^delta;
then ex y st y=x & U_FT y meets A & U_FT y meets A`;
hence thesis;
end;
assume U_FT x meets A & U_FT x meets A`;
hence thesis;
end;
definition
let FT;
let A be Subset of FT;
func A^deltai -> Subset of FT equals
A /\ (A^delta);
coherence;
func A^deltao -> Subset of FT equals
A` /\ (A^delta);
coherence;
end;
theorem
A^delta = A^deltai \/ A^deltao
proof
for x being object holds x in A^delta iff x in A^deltai \/ A^deltao
proof
let x be object;
thus x in A^delta implies x in A^deltai \/ A^deltao
proof
assume x in A^delta;
then x in [#](the carrier of FT) /\ (A^delta) by XBOOLE_1:28;
then x in (A \/ A`) /\ (A^delta) by SUBSET_1:10;
hence thesis by XBOOLE_1:23;
end;
assume x in A^deltai \/ A^deltao;
then x in (A \/ A`) /\ (A^delta) by XBOOLE_1:23;
then x in [#](the carrier of FT) /\ (A^delta) by SUBSET_1:10;
hence thesis by XBOOLE_1:28;
end;
hence thesis by TARSKI:2;
end;
definition
let FT;
let A be Subset of FT;
func A^i -> Subset of FT equals
{x:U_FT x c= A};
coherence
proof
defpred P[Element of FT] means U_FT $1 c= A;
{ x:P[x]} is Subset of FT from DOMAIN_1:sch 7;
hence thesis;
end;
func A^b -> Subset of FT equals
{x:U_FT x meets A};
coherence
proof
defpred P[Element of FT] means U_FT $1 meets A;
{ x :P[x]} is Subset of FT from DOMAIN_1:sch 7;
hence thesis;
end;
func A^s -> Subset of FT equals
{x:x in A & U_FT x \ {x} misses A };
coherence
proof
defpred P[Element of FT] means $1 in A & U_FT $1 \ {$1} misses A;
{x:P[x]} is Subset of FT from DOMAIN_1:sch 7;
hence thesis;
end;
end;
definition
let FT;
let A be Subset of FT;
func A^n -> Subset of FT equals
A \ A^s;
coherence;
func A^f -> Subset of FT equals
{x:ex y st y in A & x in U_FT y};
coherence
proof
defpred P[Element of FT] means ex y st y in A & $1 in U_FT y;
{ x :P[x]} is Subset of FT from DOMAIN_1:sch 7;
hence thesis;
end;
end;
definition
let IT be non empty RelStr;
attr IT is symmetric means
for x, y being Element of IT holds y in U_FT x implies x in U_FT y;
end;
theorem Th7:
x in A^i iff U_FT x c= A
proof
thus x in A^i implies U_FT x c= A
proof
assume x in A^i;
then ex y st y=x & U_FT y c= A;
hence thesis;
end;
assume U_FT x c= A;
hence thesis;
end;
theorem Th8:
x in A^b iff U_FT x meets A
proof
thus x in A^b implies U_FT x meets A
proof
assume x in A^b;
then ex y st y = x & U_FT y meets A;
hence thesis;
end;
assume U_FT x meets A;
hence thesis;
end;
theorem Th9:
x in A^s iff x in A & U_FT x \ {x} misses A
proof
thus x in A^s implies x in A & U_FT x \ {x} misses A
proof
assume x in A^s;
then ex y st y = x & y in A & U_FT y \ {y} misses A;
hence thesis;
end;
assume x in A & U_FT x \ {x} misses A;
hence thesis;
end;
theorem
x in A^n iff x in A & U_FT x \ {x} meets A
proof
thus x in A^n implies x in A & U_FT x \ {x} meets A
proof
assume x in A^n;
then x in A & not x in A^s by XBOOLE_0:def 5;
hence thesis;
end;
assume that
A1: x in A and
A2: U_FT x \ {x} meets A;
not x in A^s by A2,Th9;
hence thesis by A1,XBOOLE_0:def 5;
end;
theorem Th11:
x in A^f iff ex y st y in A & x in U_FT y
proof
thus x in A^f implies ex y st y in A & x in U_FT y
proof
assume x in A^f;
then ex y st y = x & ex z st z in A & y in U_FT z;
hence thesis;
end;
assume ex z st z in A & x in U_FT z;
hence thesis;
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 FT;
thus A^b c= A^f
proof
let x be object;
assume
A2: x in A^b;
then reconsider y = x as Element of FT;
U_FT y meets A by A2,Th8;
then consider z be object such that
A3: z in U_FT y /\ A by XBOOLE_0:4;
reconsider z as Element of FT by A3;
z in U_FT y by A3,XBOOLE_0:def 4;
then
A4: y in U_FT z by A1;
z in A by A3,XBOOLE_0:def 4;
hence thesis by A4;
end;
let x be object;
assume
A5: x in A^f;
then reconsider y = x as Element of FT;
consider z such that
A6: z in A and
A7: y in U_FT z by A5,Th11;
z in U_FT y by A1,A7;
then U_FT y meets A by A6,XBOOLE_0:3;
hence thesis;
end;
assume
A8: for A being Subset of FT holds A^b = A^f;
let x, y be Element of FT;
assume y in U_FT x;
then U_FT x meets {y} by ZFMISC_1:48;
then x in {y}^b;
then x in {y}^f by A8;
then ex z st z in {y} & x in U_FT z by Th11;
hence thesis by TARSKI:def 1;
end;
reserve F for Subset of FT;
definition
let FT;
let IT be Subset of FT;
attr IT is open means
IT = IT^i;
attr IT is closed means
IT = IT^b;
attr IT is connected means
for B,C being Subset of FT st IT = B \/ C
& B <> {} & C <> {} & B misses C holds B^b meets C;
end;
definition
let FT;
let A be Subset of FT;
func A^fb -> Subset 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 object;
assume x in FF;
then ex F st x = F & A c= F & F is closed;
hence thesis;
end;
then reconsider FF as Subset-Family of FT;
meet FF is Subset of FT;
hence thesis;
end;
func A^fi -> Subset 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 object;
assume x in FF;
then ex F st x = F & A c= F & F is open;
hence thesis;
end;
then reconsider FF as Subset-Family of FT;
union FF is Subset of FT;
hence thesis;
end;
end;
theorem Th13:
for FT being filled non empty RelStr, A being Subset of FT holds A c= A^b
proof
let FT be filled non empty RelStr;
let A be Subset of FT;
let x be object;
assume
A1: x in A;
then reconsider y=x as Element of FT;
y in U_FT y by Def4;
then U_FT y meets A by A1,XBOOLE_0:3;
hence thesis;
end;
theorem Th14:
for FT being non empty RelStr, A, B being Subset of FT holds A
c= B implies A^b c= B^b
proof
let FT be non empty RelStr;
let A, B be Subset of FT;
assume
A1: A c= B;
let x be object;
assume
A2: x in A^b;
then reconsider y=x as Element of FT;
U_FT y meets A by A2,Th8;
then ex w being object st w in U_FT y & w in A by XBOOLE_0:3;
then U_FT y meets B by A1,XBOOLE_0:3;
hence thesis;
end;
theorem
for FT being filled finite non empty RelStr, A being Subset of FT
holds A is connected iff for x being Element of FT st x in A ex S being
FinSequence of bool the carrier of FT st len S > 0 & S/.1 = {x} & (for i being
Element of 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 RelStr, A be Subset of FT;
thus A is connected implies for x being Element of FT st x in A ex S being
FinSequence of bool the carrier of FT st len S > 0 & S/.1 = {x} & (for i being
Element of NAT st i > 0 & i < len S holds S/.(i+1) = (S/.i)^b /\ A) & A c= S/.
len S
proof
deffunc F(Subset of FT) = $1^b /\ A;
assume
A1: A is connected;
let x be Element of FT;
assume x in A;
then
A2: {x} c= A by ZFMISC_1:31;
A3: for B being Subset of FT st B c= A holds B c= F(B) & F(B) c= A
proof
let B be Subset of FT such that
A4: B c= A;
B c= B^b by Th13;
hence B c= B^b /\ A by A4,XBOOLE_1:19;
thus thesis by XBOOLE_1:17;
end;
A5: A is finite;
consider S being FinSequence of bool the carrier of FT such that
A6: len S > 0 and
A7: S/.1={x} and
A8: for i being Nat st i > 0 & i < len S holds S/.(i+1)=F( S/.i) and
A9: F(S/.len S) = S/.len S and
A10: for i, j being Nat st i > 0 & i < j & j <= len S holds
S/.i c= A & S/.i c< S/.j from MaxFinSeqEx(A5,A2,A3);
consider k being Nat such that
A11: len S = k+1 by A6,NAT_1:6;
set B = S/.len S;
set C = A \ B;
A12: B misses ( A \ B ) by XBOOLE_1:79;
defpred P[Nat] means $1 < len S implies S/.($1+1) <> {};
A13: now
let i be Nat;
assume
A14: P[i];
thus P[i+1]
proof
assume
A15: i + 1 < len S;
then i+1 < i+1+1 & i+1+1 <= len S by NAT_1:13;
then S/.(i+1) c< S/.(i+1+1) by A10;
then S/.(i+1) c= S/.(i+1+1);
hence thesis by A14,A15,NAT_1:13;
end;
end;
A16: P[0] by A7;
A17: for i being Nat holds P[i] from NAT_1:sch 2(A16,A13);
reconsider k as Element of NAT by ORDINAL1:def 12;
k < len S by A11,NAT_1:13;
then
A18: B <> {} by A17,A11;
take S;
thus len S > 0 by A6;
thus S/.1 = {x} by A7;
thus for i being Element of NAT st i > 0 & i < len S holds S/.(i+1) = S/.i
^b /\ A by A8;
assume not A c= S/.len S;
then
A19: C <> {} by XBOOLE_1:37;
B^b /\ C = B^b /\ ( A /\ ( A \ B ) ) by XBOOLE_1:28,36
.= B /\ ( A \ B ) by A9,XBOOLE_1:16
.= {} by A12;
then
A20: B misses C & B^b misses C by XBOOLE_1:79;
B \/ C = B \/ A by XBOOLE_1:39
.= A by A9,XBOOLE_1:12,17;
hence contradiction by A1,A19,A18,A20;
end;
assume
A21: for x being Element of FT st x in A ex S being FinSequence of bool
the carrier of FT st len S > 0 & S/.1 = {x} & (for i being Element of NAT st i
> 0 & i < len S holds S/.(i+1) = S/.i^b /\ A) & A c= S/.len S;
given B, C being Subset of FT such that
A22: A = B \/ C and
A23: B <> {} and
A24: C <> {} and
A25: B misses C and
A26: B^b misses C;
set x = the Element of B;
x in A by A22,A23,XBOOLE_0:def 3;
then consider S being FinSequence of bool the carrier of FT such that
A27: len S > 0 and
A28: S/.1 = {x} and
A29: for i being Element of NAT st i > 0 & i < len S holds S/.(i+1) = (S
/.i)^b /\ A and
A30: A c= S/.len S by A21;
consider k being Nat such that
A31: len S = k + 1 by A27,NAT_1:6;
defpred P[Nat] means $1 < len S implies S/.($1+1) c= B;
B^b /\ C = {} by A26;
then
A32: B^b /\ A = B^b /\ B \/ {} by A22,XBOOLE_1:23
.= B by Th13,XBOOLE_1:28;
A33: now
let i be Nat;
assume
A34: P[i];
thus P[i+1]
proof
assume
A35: i+1 < len S;
then S/.(i+1)^b c= B^b by A34,Th14,NAT_1:13;
then S/.(i+1)^b /\ A c= B^b /\ A by XBOOLE_1:26;
hence thesis by A32,A29,A35;
end;
end;
A36: P[0] by A23,A28,ZFMISC_1:31;
A37: for i being Nat holds P[i] from NAT_1:sch 2(A36,A33);
reconsider k as Element of NAT by ORDINAL1:def 12;
k < len S by A31,NAT_1:13;
then
A38: S/.len S c= B by A37,A31;
A39: B c= A by A22,XBOOLE_1:7;
then S/.len S c= A by A38;
then S/.len S = A by A30;
then
A40: A = B by A39,A38;
B /\ C = {} by A25;
hence contradiction by A22,A24,A40,XBOOLE_1:7,28;
end;
theorem Th16:
((A`)^i)` = A^b
proof
for x being object holds x in ((A`)^i)` iff x in A^b
proof
let x be object;
thus x in ((A`)^i)` implies x in A^b
proof
assume
A1: x in ((A`)^i)`;
then reconsider y=x as Element of FT;
not y in (A`)^i by A1,XBOOLE_0:def 5;
then not U_FT y c= A`;
then consider z being object such that
A2: z in U_FT y and
A3: not z in A`;
z in A by A2,A3,SUBSET_1:29;
then U_FT y meets A by A2,XBOOLE_0:3;
hence thesis;
end;
assume
A4: x in A^b;
then reconsider y=x as Element of FT;
U_FT y meets A by A4,Th8;
then ex z being object st z in U_FT y & z in A by XBOOLE_0:3;
then not U_FT y c= A` by XBOOLE_0:def 5;
then not y in (A`)^i by Th7;
hence thesis by SUBSET_1:29;
end;
hence thesis by TARSKI:2;
end;
theorem Th17:
((A`)^b)` = A^i
proof
for x being object holds x in ((A`)^b)` iff x in A^i
proof
let x be object;
thus x in ((A`)^b)` implies x in A^i
proof
assume
A1: x in ((A`)^b)`;
then reconsider y=x as Element of FT;
not y in (A`)^b by A1,XBOOLE_0:def 5;
then U_FT y misses A`;
then U_FT y /\ A` = {};
then U_FT y \ A = {} by SUBSET_1:13;
then U_FT y c= A by XBOOLE_1:37;
hence thesis;
end;
assume
A2: x in A^i;
then reconsider y=x as Element of FT;
U_FT y c= A by A2,Th7;
then U_FT y \ A = {} by XBOOLE_1:37;
then U_FT y /\ A` = {} by SUBSET_1:13;
then U_FT y misses A`;
then not y in (A`)^b by Th8;
hence thesis by SUBSET_1:29;
end;
hence thesis by TARSKI:2;
end;
theorem
A^delta = (A^b) /\ ((A`)^b)
proof
for x being object holds x in A^delta iff x in (A^b) /\ ((A`)^b)
proof
let x be object;
thus x in A^delta implies x in (A^b) /\ ((A`)^b)
proof
assume
A1: x in A^delta;
then reconsider y=x as Element of FT;
U_FT y meets A` by A1,Th5;
then
A2: x in (A`)^b;
U_FT y meets A by A1,Th5;
then x in A^b;
hence thesis by A2,XBOOLE_0:def 4;
end;
assume
A3: x in (A^b) /\ ((A`)^b);
then reconsider y=x as Element of FT;
x in ((A`)^b) by A3,XBOOLE_0:def 4;
then
A4: U_FT y meets A` by Th8;
x in A^b by A3,XBOOLE_0:def 4;
then U_FT y meets A by Th8;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
theorem
(A`)^delta = A^delta
proof
for x being object holds x in (A`)^delta iff x in A^delta
proof
let x be object;
thus x in (A`)^delta implies x in A^delta
proof
assume
A1: x in (A`)^delta;
then reconsider y=x as Element of FT;
U_FT y meets (A`) & U_FT y meets (A`)` by A1,Th5;
hence thesis;
end;
assume
A2: x in A^delta;
then reconsider y=x as Element of FT;
U_FT y meets (A`)` & U_FT y meets A` by A2,Th5;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
theorem
x in A^s implies not x in (A \ {x})^b
proof
assume x in A^s;
then A misses (U_FT x \ {x}) by Th9;
then A /\ (U_FT x \ {x}) = {};
then
A1: (A /\ U_FT x) \ {x} = {} by XBOOLE_1:49;
now
per cases by A1,ZFMISC_1:58;
suppose
A /\ U_FT x = {};
then A misses U_FT x;
hence (A \ {x}) misses U_FT x by XBOOLE_1:36,63;
end;
suppose
A /\ U_FT x = {x};
then (U_FT x /\ A) \ {x} = {} by XBOOLE_1:37;
then U_FT x /\ (A \ {x}) = {} by XBOOLE_1:49;
hence (A \ {x}) misses U_FT x;
end;
end;
hence thesis by Th8;
end;
theorem
A^s <> {} & card A <> 1 implies A is not connected
proof
assume that
A1: A^s <> {} and
A2: card A <> 1;
consider z being Element of FT such that
A3: z in A^s by A1,SUBSET_1:4;
set C = {z};
set B = A \ {z};
card {z} = 1 & A <> {} by A3,Th9,CARD_1:30;
then
A4: B <> {} by A2,ZFMISC_1:58;
z in A by A3,Th9;
then {z} is Subset of A by SUBSET_1:41;
then
A5: A = B \/ C by XBOOLE_1:45;
A6: (U_FT z \ {z}) misses A by A3,Th9;
A7: B^b misses C
proof
assume B^b meets C;
then consider x being object such that
A8: x in B^b and
A9: x in C by XBOOLE_0:3;
reconsider x as Element of FT by A8;
A10: x = z by A9,TARSKI:def 1;
U_FT x meets B by A8,Th8;
then consider y being object such that
A11: y in U_FT x and
A12: y in B by XBOOLE_0:3;
not x in B by A9,XBOOLE_0:def 5;
then y in U_FT x \ {x} by A11,A12,ZFMISC_1:56;
then (U_FT z \ {z}) meets B by A12,A10,XBOOLE_0:3;
then
A13: ex w being object st w in (U_FT z \ {z}) /\ B by XBOOLE_0:4;
(U_FT z \ {z}) /\ B c= (U_FT z \ {z}) /\ A by XBOOLE_1:26,36;
hence contradiction by A6,A13;
end;
B misses C by XBOOLE_1:79;
hence thesis by A5,A4,A7;
end;
theorem
for FT being filled non empty RelStr, A being Subset of FT holds A^i c= A
proof
let FT be filled non empty RelStr;
let A be Subset of FT;
let x be object;
assume
A1: x in A^i;
then reconsider y=x as Element of FT;
A2: y in U_FT y by Def4;
U_FT y c= A by A1,Th7;
hence thesis by A2;
end;
theorem
A is open implies A` is closed
proof
assume A is open;
then
A1: A = A^i;
A^i = ((A`)^b)` by Th17;
hence thesis by A1;
end;
theorem
A is closed implies A` is open
proof
assume A is closed;
then
A1: A = A^b;
A^b = ((A`)^i)` by Th16;
hence thesis by A1;
end;