Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Formal Topological Spaces

**by****Gang Liu,****Yasushi Fuwa, and****Masayoshi Eguchi**- Received October 13, 2000
- MML identifier: FINTOPO2

- [ Mizar article, MML identifier index ]

environ vocabulary FIN_TOPO, BOOLE, SUBSET_1, PRE_TOPC, MARGREL1, FUNCT_1, FINTOPO2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, FUNCT_1, FUNCT_2, FIN_TOPO, PRE_TOPC, MARGREL1; constructors DOMAIN_1, FIN_TOPO, PRE_TOPC, MARGREL1; clusters SUBSET_1, RELSET_1, STRUCT_0, FIN_TOPO, PRE_TOPC, XBOOLE_0; requirements SUBSET, BOOLE; begin :: :: SECTION1 : Some Useful Theorems on Finite Topological Spaces :: reserve FT for non empty FT_Space_Str; reserve A for Subset of FT; theorem :: FINTOPO2:1 for FT being non empty FT_Space_Str, 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 FT_Space_Str; 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 FT_Space_Str; 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 FT_Space_Str; 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 FT_Space_Str; 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 FT_Space_Str; 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; definition cluster non empty strict 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 of bool the carrier 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; canceled; theorem :: FINTOPO2:20 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:21 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:22 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:23 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:24 x in A^Fon iff x in A & (for V st V in U_FMT x holds (V \ {x}) meets A); theorem :: FINTOPO2:25 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:26 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:27 ((A^Fob) \/ (B^Fob)) c= (A \/ B)^Fob; theorem :: FINTOPO2:28 (A /\ B)^Fob c= (A^Fob) /\ (B^Fob); theorem :: FINTOPO2:29 ((A^Foi) \/ (B^Foi)) c= (A \/ B)^Foi; theorem :: FINTOPO2:30 (A /\ B)^Foi c= ((A^Foi) /\ (B^Foi)); 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 \/ B)^Fob = ((A^Fob) \/ (B^Fob)); theorem :: FINTOPO2:32 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:33 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:34 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:35 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:36 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:37 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:38 ((A`)^Fob)` =A^Foi; theorem :: FINTOPO2:39 ((A`)^Foi)` = A^Fob; theorem :: FINTOPO2:40 A^Fodelta = (A^Fob) /\ ((A`)^Fob); theorem :: FINTOPO2:41 A^Fodelta = (A^Fob) /\ (A^Foi)`; theorem :: FINTOPO2:42 A^Fodelta = (A`)^Fodelta; theorem :: FINTOPO2:43 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:44 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:45 A` is Fo_open implies A is Fo_closed; theorem :: FINTOPO2:46 A` is Fo_closed implies A is Fo_open; 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 /\ B)^Fob = ((A^Fob) /\ (B^Fob)); theorem :: FINTOPO2:48 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;

Back to top