:: Finite Topological Spaces. Finite Topology Concepts and Neighbourhoods :: by Hiroshi Imura and Masayoshi Eguchi :: :: Received November 27, 1992 :: Copyright (c) 1992-2021 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;