:: Finite Topological Spaces. Finite Topology Concepts and Neighbourhoods
:: by Hiroshi Imura and Masayoshi Eguchi
::
:: Received November 27, 1992
:: Copyright (c) 1992-2016 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;
begin
theorem :: FIN_TOPO:1
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;
theorem :: FIN_TOPO:2
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;
scheme :: FIN_TOPO:sch 1
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
A() is finite and
B() c= A() and
for A being Subset of X() st A c= A() holds A c= F(A) & F(A) c= A();
registration
cluster non empty strict for RelStr;
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
:: FIN_TOPO:def 1
Class(the InternalRel of FT,x);
end;
definition
let x be set, y be Subset of {x};
redefine func x.-->y -> Function of {x}, bool {x};
end;
definition
let x be set;
func SinglRel x -> Relation of {x} equals
:: FIN_TOPO:def 2
{[x,x]};
end;
definition
func FT{0} -> strict RelStr equals
:: FIN_TOPO:def 3
RelStr (#{0},SinglRel 0#);
end;
registration
cluster FT{0} -> non empty;
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
:: FIN_TOPO:def 4
for x being Element of IT holds x in U_FT x;
end;
theorem :: FIN_TOPO:3
FT{0} is filled;
registration
cluster FT{0} -> filled finite;
end;
registration
cluster finite filled strict for non empty RelStr;
end;
theorem :: FIN_TOPO:4
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;
reserve A for Subset of FT;
definition
let FT;
let A be Subset of FT;
func A^delta -> Subset of FT equals
:: FIN_TOPO:def 5
{x:U_FT x meets A & U_FT x meets A` };
end;
theorem :: FIN_TOPO:5
x in A^delta iff U_FT x meets A & U_FT x meets A`;
definition
let FT;
let A be Subset of FT;
func A^deltai -> Subset of FT equals
:: FIN_TOPO:def 6
A /\ (A^delta);
func A^deltao -> Subset of FT equals
:: FIN_TOPO:def 7
A` /\ (A^delta);
end;
theorem :: FIN_TOPO:6
A^delta = A^deltai \/ A^deltao;
definition
let FT;
let A be Subset of FT;
func A^i -> Subset of FT equals
:: FIN_TOPO:def 8
{x:U_FT x c= A};
func A^b -> Subset of FT equals
:: FIN_TOPO:def 9
{x:U_FT x meets A};
func A^s -> Subset of FT equals
:: FIN_TOPO:def 10
{x:x in A & U_FT x \ {x} misses A };
end;
definition
let FT;
let A be Subset of FT;
func A^n -> Subset of FT equals
:: FIN_TOPO:def 11
A \ A^s;
func A^f -> Subset of FT equals
:: FIN_TOPO:def 12
{x:ex y st y in A & x in U_FT y};
end;
definition
let IT be non empty RelStr;
attr IT is symmetric means
:: FIN_TOPO:def 13
for x, y being Element of IT holds y in U_FT x implies x in U_FT y;
end;
theorem :: FIN_TOPO:7
x in A^i iff U_FT x c= A;
theorem :: FIN_TOPO:8
x in A^b iff U_FT x meets A;
theorem :: FIN_TOPO:9
x in A^s iff x in A & U_FT x \ {x} misses A;
theorem :: FIN_TOPO:10
x in A^n iff x in A & U_FT x \ {x} meets A;
theorem :: FIN_TOPO:11
x in A^f iff ex y st y in A & x in U_FT y;
theorem :: FIN_TOPO:12
FT is symmetric iff for A holds A^b = A^f;
reserve F for Subset of FT;
definition
let FT;
let IT be Subset of FT;
attr IT is open means
:: FIN_TOPO:def 14
IT = IT^i;
attr IT is closed means
:: FIN_TOPO:def 15
IT = IT^b;
attr IT is connected means
:: FIN_TOPO:def 16
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
:: FIN_TOPO:def 17
meet{F:A c= F & F is closed};
func A^fi -> Subset of FT equals
:: FIN_TOPO:def 18
union{F:A c= F & F is open};
end;
theorem :: FIN_TOPO:13
for FT being filled non empty RelStr, A being Subset of FT holds A c= A^b;
theorem :: FIN_TOPO:14
for FT being non empty RelStr, A, B being Subset of FT holds A
c= B implies A^b c= B^b;
theorem :: FIN_TOPO:15
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;
theorem :: FIN_TOPO:16
((A`)^i)` = A^b;
theorem :: FIN_TOPO:17
((A`)^b)` = A^i;
theorem :: FIN_TOPO:18
A^delta = (A^b) /\ ((A`)^b);
theorem :: FIN_TOPO:19
(A`)^delta = A^delta;
theorem :: FIN_TOPO:20
x in A^s implies not x in (A \ {x})^b;
theorem :: FIN_TOPO:21
A^s <> {} & card A <> 1 implies A is not connected;
theorem :: FIN_TOPO:22
for FT being filled non empty RelStr, A being Subset of FT holds A^i c= A;
theorem :: FIN_TOPO:23
A is open implies A` is closed;
theorem :: FIN_TOPO:24
A is closed implies A` is open;