:: 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;