:: Formal topological spaces :: by Gang Liu , Yasushi Fuwa and Masayoshi Eguchi :: :: Received October 13, 2000 :: Copyright (c) 2000-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 XBOOLE_0, ORDERS_2, SUBSET_1, TARSKI, FIN_TOPO, RCOMP_1, MARGREL1, XBOOLEAN, STRUCT_0, FUNCT_1, ZFMISC_1, PRE_TOPC, SETFAM_1, FINTOPO2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, FUNCT_1, FUNCT_2, FIN_TOPO, ORDERS_2, PRE_TOPC, MARGREL1; constructors DOMAIN_1, MARGREL1, PRE_TOPC, FIN_TOPO, RELSET_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, FIN_TOPO; requirements SUBSET, BOOLE, NUMERALS; begin :: :: SECTION1 : Some Useful Theorems on Finite Topological Spaces :: reserve FT for non empty RelStr; reserve A for Subset of FT; theorem :: FINTOPO2:1 for FT being non empty RelStr, A,B being Subset of FT holds A c= B implies A^i c= B^i; theorem :: FINTOPO2:2 A^delta = (A^b) /\ ((A^i)`); theorem :: FINTOPO2:3 A^delta = A^b \ A^i; theorem :: FINTOPO2:4 A` is open implies A is closed; theorem :: FINTOPO2:5 A` is closed implies A is open; definition let FT be non empty RelStr; let x be Element of FT; let y be Element of FT; let A be Subset of FT; func P_1(x,y,A) -> Element of BOOLEAN equals :: FINTOPO2:def 1 TRUE if y in U_FT x & y in A otherwise FALSE; end; definition let FT be non empty RelStr; let x be Element of FT; let y be Element of FT; let A be Subset of FT; func P_2(x,y,A) -> Element of BOOLEAN equals :: FINTOPO2:def 2 TRUE if y in U_FT x & y in A` otherwise FALSE; end; theorem :: FINTOPO2:6 for x,y be Element of FT, A be Subset of FT holds P_1(x,y,A) = TRUE iff y in U_FT x & y in A; theorem :: FINTOPO2:7 for x,y be Element of FT, A be Subset of FT holds P_2(x,y,A) = TRUE iff y in U_FT x & y in A`; theorem :: FINTOPO2:8 for x be Element of FT, A be Subset of FT holds x in A^delta iff ex y1,y2 being Element of FT st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE; definition let FT be non empty RelStr; let x be Element of FT; let y be Element of FT; func P_0(x,y) -> Element of BOOLEAN equals :: FINTOPO2:def 3 TRUE if y in U_FT x otherwise FALSE; end; theorem :: FINTOPO2:9 for x,y be Element of FT holds P_0(x,y)=TRUE iff y in U_FT x; theorem :: FINTOPO2:10 for x be Element of FT, A be Subset of FT holds x in A^i iff for y be Element of FT holds (P_0(x,y)=TRUE implies P_1(x,y,A)=TRUE); theorem :: FINTOPO2:11 for x be Element of FT, A be Subset of FT holds x in A^b iff ex y1 being Element of FT st P_1(x,y1,A)=TRUE; definition let FT be non empty RelStr; let x be Element of FT; let A be Subset of FT; func P_A(x,A) -> Element of BOOLEAN equals :: FINTOPO2:def 4 TRUE if x in A otherwise FALSE; end; theorem :: FINTOPO2:12 for x be Element of FT, A be Subset of FT holds P_A(x,A)=TRUE iff x in A; theorem :: FINTOPO2:13 for x be Element of FT, A be Subset of FT holds x in A^deltai iff (ex y1,y2 being Element of FT st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = TRUE; theorem :: FINTOPO2:14 for x be Element of FT, A be Subset of FT holds x in A^deltao iff (ex y1,y2 being Element of FT st P_1(x,y1,A)=TRUE & P_2(x,y2,A)=TRUE) & P_A(x,A) = FALSE; definition let FT be non empty RelStr; let x be Element of FT; let y be Element of FT; func P_e(x,y) -> Element of BOOLEAN equals :: FINTOPO2:def 5 TRUE if x = y otherwise FALSE; end; theorem :: FINTOPO2:15 for x,y be Element of FT holds P_e(x,y)=TRUE iff x = y; theorem :: FINTOPO2:16 for x be Element of FT, A be Subset of FT holds x in A^s iff P_A(x,A)= TRUE & not(ex y being Element of FT st P_1(x,y,A)=TRUE & P_e(x,y)=FALSE ); theorem :: FINTOPO2:17 for x be Element of FT, A be Subset of FT holds x in A^n iff P_A(x,A)= TRUE & ex y being Element of FT st P_1(x,y,A)=TRUE & P_e(x,y)=FALSE; theorem :: FINTOPO2:18 for x be Element of FT, A be Subset of FT holds x in A^f iff ex y being Element of FT st P_A(y,A)=TRUE & P_0(y,x)=TRUE; begin :: :: SECTION2: Formal Topological Spaces :: definition struct ( 1-sorted ) FMT_Space_Str (# carrier -> set, BNbd -> Function of the carrier, bool bool the carrier #); end; registration cluster non empty strict for FMT_Space_Str; end; reserve T for non empty TopStruct; reserve FMT for non empty FMT_Space_Str; reserve x, y for Element of FMT; definition let FMT; let x be Element of FMT; func U_FMT x -> Subset-Family of FMT equals :: FINTOPO2:def 6 ( the BNbd of FMT ).x; end; definition let T; func NeighSp T -> non empty strict FMT_Space_Str means :: FINTOPO2:def 7 the carrier of it = the carrier of T & for x being Point of it holds U_FMT x = {V where V is Subset of T: V in the topology of T & x in V}; end; reserve A, B, W, V for Subset of FMT; definition let IT be non empty FMT_Space_Str; attr IT is Fo_filled means :: FINTOPO2:def 8 for x being Element of IT for D being Subset of IT st D in U_FMT x holds x in D; end; definition let FMT; let A; func A^Fodelta -> Subset of FMT equals :: FINTOPO2:def 9 {x:for W st W in U_FMT x holds W meets A & W meets A`}; end; theorem :: FINTOPO2:19 x in A^Fodelta iff for W st W in U_FMT x holds W meets A & W meets A`; definition let FMT,A; func A^Fob -> Subset of FMT equals :: FINTOPO2:def 10 {x:for W st W in U_FMT x holds W meets A}; end; theorem :: FINTOPO2:20 x in A^Fob iff for W st W in U_FMT x holds W meets A; definition let FMT,A; func A^Foi -> Subset of FMT equals :: FINTOPO2:def 11 {x:ex V st V in U_FMT x & V c= A}; end; theorem :: FINTOPO2:21 x in A^Foi iff ex V st V in U_FMT x & V c= A; definition let FMT,A; func A^Fos -> Subset of FMT equals :: FINTOPO2:def 12 {x:x in A & (ex V st V in U_FMT x & V \ { x} misses A)}; end; theorem :: FINTOPO2:22 x in A^Fos iff x in A & ex V st V in U_FMT x & V \ {x} misses A; definition let FMT,A; func A^Fon -> Subset of FMT equals :: FINTOPO2:def 13 A\(A^Fos); end; theorem :: FINTOPO2:23 x in A^Fon iff x in A & for V st V in U_FMT x holds (V \ {x}) meets A; theorem :: FINTOPO2:24 for FMT being non empty FMT_Space_Str, A, B being Subset of FMT holds A c= B implies A^Fob c= B^Fob; theorem :: FINTOPO2:25 for FMT being non empty FMT_Space_Str, A,B being Subset of FMT holds A c= B implies A^Foi c= B^Foi; theorem :: FINTOPO2:26 ((A^Fob) \/ (B^Fob)) c= (A \/ B)^Fob; theorem :: FINTOPO2:27 (A /\ B)^Fob c= (A^Fob) /\ (B^Fob); theorem :: FINTOPO2:28 ((A^Foi) \/ (B^Foi)) c= (A \/ B)^Foi; theorem :: FINTOPO2:29 (A /\ B)^Foi c= ((A^Foi) /\ (B^Foi)); theorem :: FINTOPO2:30 for FMT being non empty FMT_Space_Str holds (for x being Element of FMT, V1,V2 being Subset of FMT st ((V1 in U_FMT x) & (V2 in U_FMT x)) holds ex W being Subset of FMT st ((W in U_FMT x) & (W c= (V1 /\ V2)))) iff for A,B being Subset of FMT holds (A \/ B)^Fob = ((A^Fob) \/ (B^Fob)); theorem :: FINTOPO2:31 for FMT being non empty FMT_Space_Str holds (for x being Element of FMT, V1,V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st (W in U_FMT x & W c= V1 /\ V2)) iff for A,B being Subset of FMT holds (A^Foi) /\ (B^Foi) = (A /\ B)^Foi; theorem :: FINTOPO2:32 for FMT being non empty FMT_Space_Str, A,B being Subset of FMT holds ( for x being Element of FMT, V1,V2 being Subset of FMT st ((V1 in U_FMT x) & V2 in U_FMT x) holds ex W being Subset of FMT st ((W in U_FMT x) & (W c= (V1 /\ V2 )))) implies (A \/ B)^Fodelta c= ((A^Fodelta) \/ (B^Fodelta)); theorem :: FINTOPO2:33 for FMT being non empty FMT_Space_Str st FMT is Fo_filled holds (for A ,B being Subset of FMT holds (A \/ B)^Fodelta = ((A^Fodelta) \/ (B^Fodelta))) implies for x being Element of FMT, V1,V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st W in U_FMT x & W c= (V1 /\ V2 ); theorem :: FINTOPO2:34 for x be Element of FMT, A being Subset of FMT holds x in A^Fos iff x in A & not x in (A\{x})^Fob; theorem :: FINTOPO2:35 for FMT being non empty FMT_Space_Str holds FMT is Fo_filled iff for A being Subset of FMT holds A c= A^Fob; theorem :: FINTOPO2:36 for FMT being non empty FMT_Space_Str holds FMT is Fo_filled iff for A being Subset of FMT holds A^Foi c= A; theorem :: FINTOPO2:37 ((A`)^Fob)` =A^Foi; theorem :: FINTOPO2:38 ((A`)^Foi)` = A^Fob; theorem :: FINTOPO2:39 A^Fodelta = (A^Fob) /\ ((A`)^Fob); theorem :: FINTOPO2:40 A^Fodelta = (A^Fob) /\ (A^Foi)`; theorem :: FINTOPO2:41 A^Fodelta = (A`)^Fodelta; theorem :: FINTOPO2:42 A^Fodelta = A^Fob \ A^Foi; definition let FMT; let A; func A^Fodel_i -> Subset of FMT equals :: FINTOPO2:def 14 A /\ (A^Fodelta); func A^Fodel_o -> Subset of FMT equals :: FINTOPO2:def 15 A` /\ (A^Fodelta); end; theorem :: FINTOPO2:43 A^Fodelta = (A^Fodel_i) \/ (A^Fodel_o); definition let FMT; let G be Subset of FMT; attr G is Fo_open means :: FINTOPO2:def 16 G = G^Foi; attr G is Fo_closed means :: FINTOPO2:def 17 G = G^Fob; end; theorem :: FINTOPO2:44 A` is Fo_open implies A is Fo_closed; theorem :: FINTOPO2:45 A` is Fo_closed implies A is Fo_open; theorem :: FINTOPO2:46 for FMT being non empty FMT_Space_Str, A,B being Subset of FMT st FMT is Fo_filled holds (for x being Element of FMT holds {x} in U_FMT x ) implies ( A /\ B)^Fob = ((A^Fob) /\ (B^Fob)); theorem :: FINTOPO2:47 for FMT being non empty FMT_Space_Str, A,B being Subset of FMT st FMT is Fo_filled holds (for x being Element of FMT holds {x} in U_FMT x ) implies ( A^Foi) \/ (B^Foi) = (A \/ B)^Foi;