:: Some Set Series in Finite Topological Spaces. {F}undamental Concepts :: for Image Processing :: by Masami Tanaka and Yatsuka Nakamura :: :: Received January 26, 2004 :: Copyright (c) 2004-2019 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, FIN_TOPO, TARSKI, PRE_TOPC, FUNCT_1, NUMBERS, ZFMISC_1, STRUCT_0, ARYTM_3, CARD_1, RELAT_1, NAT_1, FINTOPO3, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FIN_TOPO, PRE_TOPC, STRUCT_0, ORDERS_2; constructors NAT_1, FIN_TOPO, RELSET_1, NUMBERS; registrations SUBSET_1, ORDINAL1, RELSET_1, STRUCT_0, FIN_TOPO, XCMPLX_0, NAT_1; requirements SUBSET, NUMERALS, ARITHM, BOOLE; begin reserve T for non empty RelStr, A,B for Subset of T, x,x2,y,z for Element of T; :: The following is definition of "deflation of a set A" :: (A^f is an inflation of A). definition let T; let A be Subset of T; func A^d -> Subset of T equals :: FINTOPO3:def 1 {x where x is Element of T : for y being Element of T st y in A` holds not x in U_FT y}; end; theorem :: FINTOPO3:1 T is filled implies A c= A^f; theorem :: FINTOPO3:2 x in A^d iff for y st y in A` holds not x in U_FT y; theorem :: FINTOPO3:3 T is filled implies A^d c= A; theorem :: FINTOPO3:4 A^d = ((A`)^f)`; theorem :: FINTOPO3:5 A c= B implies A^f c= B^f; theorem :: FINTOPO3:6 A c= B implies A^d c= B^d; theorem :: FINTOPO3:7 (A /\ B)^b c= (A^b) /\ (B^b); theorem :: FINTOPO3:8 (A \/ B)^b = (A^b) \/ (B^b); theorem :: FINTOPO3:9 (A^i) \/ (B^i) c= (A \/ B)^i; theorem :: FINTOPO3:10 (A^i) /\ (B^i) = (A /\ B)^i; theorem :: FINTOPO3:11 (A^f) \/ (B^f) = (A \/ B)^f; theorem :: FINTOPO3:12 (A^d) /\ (B^d) = (A /\ B)^d; definition let T be non empty RelStr; let A be Subset of T; func Fcl(A) -> sequence of bool the carrier of T means :: FINTOPO3:def 2 (for n being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^b) & it.0=A; end; definition let T be non empty RelStr; let A be Subset of T, n be Nat; func Fcl(A,n) -> Subset of T equals :: FINTOPO3:def 3 (Fcl A).n; end; definition let T be non empty RelStr; let A be Subset of T; func Fint(A) -> sequence of bool the carrier of T means :: FINTOPO3:def 4 (for n being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^i) & it.0=A; end; definition let T be non empty RelStr; let A be Subset of T, n be Nat; func Fint(A,n) -> Subset of T equals :: FINTOPO3:def 5 (Fint A).n; end; theorem :: FINTOPO3:13 for n being Nat holds Fcl(A,n+1) = (Fcl(A,n))^b; theorem :: FINTOPO3:14 Fcl(A,0) = A; theorem :: FINTOPO3:15 Fcl(A,1) = A^b; theorem :: FINTOPO3:16 Fcl(A,2) = A^b^b; theorem :: FINTOPO3:17 for n being Nat holds Fcl(A \/ B,n) = Fcl(A,n) \/ Fcl (B,n); theorem :: FINTOPO3:18 for n being Nat holds Fint(A,n+1) = (Fint(A,n))^i; theorem :: FINTOPO3:19 Fint(A,0) = A; theorem :: FINTOPO3:20 Fint(A,1) = A^i; theorem :: FINTOPO3:21 Fint(A,2) = A^i^i; theorem :: FINTOPO3:22 for n being Nat holds Fint(A /\ B,n) = Fint(A,n) /\ Fint(B,n); theorem :: FINTOPO3:23 T is filled implies for n being Nat holds A c= Fcl(A,n); theorem :: FINTOPO3:24 T is filled implies for n being Nat holds Fint(A,n) c= A; theorem :: FINTOPO3:25 T is filled implies for n being Nat holds Fcl(A,n) c= Fcl(A ,n+1); theorem :: FINTOPO3:26 T is filled implies for n being Nat holds Fint(A,n+1) c= Fint(A,n); theorem :: FINTOPO3:27 for n being Nat holds Fint(A`,n)` = Fcl(A,n); theorem :: FINTOPO3:28 for n being Nat holds Fcl(A`,n)` = Fint(A,n); theorem :: FINTOPO3:29 for n being Nat holds Fcl(A,n) \/ Fcl(B,n) = Fint((A \/ B)` ,n)`; theorem :: FINTOPO3:30 for n being Nat holds Fint(A,n) /\ Fint(B,n) = Fcl((A /\ B) `,n)`; :: Function of Inflation Series definition let T be non empty RelStr; let A be Subset of T; func Finf(A) -> sequence of bool(the carrier of T) means :: FINTOPO3:def 6 (for n being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^f) & it.0=A; end; definition let T be non empty RelStr; let A be Subset of T, n be Nat; func Finf(A,n) -> Subset of T equals :: FINTOPO3:def 7 (Finf A).n; end; :: Function of Deflation Series definition let T be non empty RelStr; let A be Subset of T; func Fdfl(A) -> sequence of bool(the carrier of T) means :: FINTOPO3:def 8 (for n being Nat,B being Subset of T st B=it.n holds it.(n+1)=B^d) & it.0=A; end; definition let T be non empty RelStr; let A be Subset of T, n be Nat; func Fdfl(A,n) -> Subset of T equals :: FINTOPO3:def 9 (Fdfl A).n; end; theorem :: FINTOPO3:31 for n being Nat holds Finf(A,n+1) = (Finf(A,n))^f; theorem :: FINTOPO3:32 Finf(A,0) = A; theorem :: FINTOPO3:33 Finf(A,1) = A^f; theorem :: FINTOPO3:34 Finf(A,2) = A^f^f; theorem :: FINTOPO3:35 for n being Nat holds Finf(A \/ B,n) = Finf(A,n) \/ Finf(B, n); theorem :: FINTOPO3:36 T is filled implies for n being Nat holds A c= Finf(A,n); theorem :: FINTOPO3:37 T is filled implies for n being Nat holds Finf(A,n) c= Finf (A,n+1); theorem :: FINTOPO3:38 for n being Nat holds Fdfl(A,n+1) = (Fdfl(A,n))^d; theorem :: FINTOPO3:39 Fdfl(A,0) = A; theorem :: FINTOPO3:40 Fdfl(A,1) = A^d; theorem :: FINTOPO3:41 Fdfl(A,2) = A^d^d; theorem :: FINTOPO3:42 for n being Nat holds Fdfl(A /\ B,n) = Fdfl(A,n) /\ Fdfl(B,n); theorem :: FINTOPO3:43 T is filled implies for n being Nat holds Fdfl(A,n) c= A; theorem :: FINTOPO3:44 T is filled implies for n being Nat holds Fdfl(A,n+1) c= Fdfl(A,n); theorem :: FINTOPO3:45 for n being Nat holds Fdfl(A,n) = Finf(A`,n)`; theorem :: FINTOPO3:46 for n being Nat holds Fdfl(A,n) /\ Fdfl(B,n) = Finf((A /\ B )`,n)`; definition :: n-th neighbourhood of x let T be non empty RelStr, n be Nat, x be Element of T; func U_FT(x,n) -> Subset of T equals :: FINTOPO3:def 10 Finf((U_FT x),n); end; theorem :: FINTOPO3:47 U_FT(x,0) = U_FT x; theorem :: FINTOPO3:48 for n being Nat holds U_FT(x,n+1) = (U_FT(x,n))^f; definition let S, T be non empty RelStr; pred S, T are_mutually_symmetric means :: FINTOPO3:def 11 the carrier of S = the carrier of T & for x being Element of S, y being Element of T holds y in U_FT x iff x in U_FT y; symmetry; end;