:: 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-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, 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;
requirements SUBSET, NUMERALS, ARITHM;
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;