The abstract of the Mizar article:

Finite Topological Spaces

by

Hiroshi Imura, and

Masayoshi Eguchi

Received November 27, 1992

MML identifier: FIN_TOPO

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FINSET_1, BOOLE, ZFMISC_1, FUNCT_1, RELAT_1, ABSVALUE,
      ARYTM_1, CAT_1, FUNCT_2, SUBSET_1, PRE_TOPC, TARSKI, RELAT_2, SETFAM_1,
      CARD_1, FIN_TOPO, HAHNBAN, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, FINSET_1, NAT_1, SETFAM_1, STRUCT_0, RELSET_1, RELAT_1, FUNCT_1,
      FUNCT_2, CQC_LANG, DOMAIN_1, GROUP_1, FINSEQ_1, FINSEQ_4, CARD_1;
 constructors NAT_1, CQC_LANG, DOMAIN_1, GROUP_1, FINSEQ_4, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, INT_1, RELSET_1, STRUCT_0, CQC_LANG, FINSEQ_1, NAT_1,
      XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

theorem :: FIN_TOPO:1
  for A being set,
      f being FinSequence of bool A st
    (for i being Nat st 1 <= i & i < len f holds f/.i c= f/.(i+1))
    for i, j being Nat st
      i <= j & 1 <= i & j <= len f holds f/.i c= f/.j;

theorem :: FIN_TOPO:2
  for A being set,
      f being FinSequence of bool A st
    (for i being Nat st 1 <= i & i < len f holds f/.i c= f/.(i+1))
    for i, j being Nat st
      i < j & 1 <= i & j <= len f & f/.j c= f/.i
    for k being Nat st i <= k & k <= j holds f/.j = f/.k;

theorem :: FIN_TOPO:3
  for F being set st
    F is finite &
    F <> {} & F is c=-linear
      ex m being set st m in F &
        for C being set st C in F holds C c= m;

canceled;

theorem :: FIN_TOPO:5
  for f being Function st
    (for i being Nat holds f.i c= f.(i+1))
    for i, j being Nat st
      i <= j holds f.i c= f.j;

scheme MaxFinSeqEx {X() -> non empty set,
                    A() -> Subset of X(),
                    B() -> Subset of X(),
                    F(Subset of X()) -> Subset of X()}:
  ex f being FinSequence of bool X() st
    len f > 0 &
    f/.1=B() &
    (for i being Nat st i > 0 & i < len f holds f/.(i+1)=F(f/.i)) &
    F(f/.len f)=f/.len f &
    (for i, j being Nat st i > 0 & i < j & j <= len f holds
      f/.i c= A() & f/.i c< f/.j)
  provided
     A() is finite and
     B() c= A() and
     for A being Subset of X() st A c= A() holds A c= F(A) & F(A) c= A();

definition
  struct ( 1-sorted ) FT_Space_Str
     (# carrier -> set,
            Nbd -> Function of the carrier, bool the carrier #);
end;

definition
 cluster non empty strict FT_Space_Str;
end;

reserve FT for non empty FT_Space_Str;
reserve x, y, z for Element of FT;

definition
  let FT be non empty FT_Space_Str;
  let x be Element of FT;

  func U_FT x -> Subset of FT equals
:: FIN_TOPO:def 1

   ( the Nbd of FT ).x;
end;

definition
  let x be set,
      y be Subset of {x};

  redefine func x.-->y -> Function of {x}, bool {x};
end;

definition
  func FT{0} -> strict FT_Space_Str equals
:: FIN_TOPO:def 2

   FT_Space_Str (#{0},0.-->[#]{0}#);
end;

definition
  cluster FT{0} -> non empty;
end;

definition let IT be non empty FT_Space_Str;
  attr IT is filled means
:: FIN_TOPO:def 3

  for x being Element of IT holds x in U_FT x;
end;

canceled;

theorem :: FIN_TOPO:7
  FT{0} is filled;

theorem :: FIN_TOPO:8
  FT{0} is finite;

definition
  cluster finite filled strict (non empty FT_Space_Str);
end;

definition
  let T be 1-sorted,
      F be set;
 canceled;

  pred F is_a_cover_of T means
:: FIN_TOPO:def 5
    the carrier of T c= union F;
end;

theorem :: FIN_TOPO:9
    for FT being filled (non empty FT_Space_Str) holds
    {U_FT x where x is Element of FT : not contradiction}
     is_a_cover_of FT;

reserve A for Subset of FT;

definition
  let FT;
  let A be Subset of FT;

  func A^delta -> Subset of FT equals
:: FIN_TOPO:def 6

   {x:U_FT x meets A & U_FT x meets A` };
end;

theorem :: FIN_TOPO:10
  x in A^delta iff U_FT x meets A & U_FT x meets A`;

definition let FT;
  let A be Subset of FT;
  func A^deltai -> Subset of FT equals
:: FIN_TOPO:def 7

   A /\ (A^delta);

  func A^deltao -> Subset of FT equals
:: FIN_TOPO:def 8

   A` /\ (A^delta);
end;

theorem :: FIN_TOPO:11
    A^delta = A^deltai \/ A^deltao;

definition let FT;
  let A be Subset of FT;
  func A^i -> Subset of FT equals
:: FIN_TOPO:def 9
   {x:U_FT x c= A};

  func A^b -> Subset of FT equals
:: FIN_TOPO:def 10

   {x:U_FT x meets A};

  func A^s -> Subset of FT equals
:: FIN_TOPO:def 11

   {x:x in A & U_FT x \ {x} misses A };
end;

definition
  let FT;
  let A be Subset of FT;

  func A^n -> Subset of FT equals
:: FIN_TOPO:def 12

   A \ A^s;

  func A^f -> Subset of FT equals
:: FIN_TOPO:def 13

   {x:ex y st y in A & x in U_FT y};
end;

definition let IT be non empty FT_Space_Str;
  attr IT is symmetric means
:: FIN_TOPO:def 14

  for x, y being Element of IT holds
    y in U_FT x implies x in U_FT y;
end;

theorem :: FIN_TOPO:12
  x in A^i iff U_FT x c= A;

theorem :: FIN_TOPO:13
  x in A^b iff U_FT x meets A;

theorem :: FIN_TOPO:14
  x in A^s iff x in A & U_FT x \ {x} misses A;

theorem :: FIN_TOPO:15
    x in A^n iff x in A & U_FT x \ {x} meets A;

theorem :: FIN_TOPO:16
  x in A^f iff ex y st y in A & x in U_FT y;

theorem :: FIN_TOPO:17
    FT is symmetric iff for A holds A^b = A^f;

reserve F for Subset of FT;

definition let FT;
  let IT be Subset of FT;
  attr IT is open means
:: FIN_TOPO:def 15
  IT = IT^i;

  attr IT is closed means
:: FIN_TOPO:def 16
  IT = IT^b;

  attr IT is connected means
:: FIN_TOPO:def 17
  for B,C being Subset of FT st
    IT = B \/ C & B <> {} & C <> {} & B misses C holds B^b meets C;
end;

definition let FT; let A be Subset of FT;
  func A^fb -> Subset of FT equals
:: FIN_TOPO:def 18
     meet{F:A c= F & F is closed};

  func A^fi -> Subset of FT equals
:: FIN_TOPO:def 19
     union{F:A c= F & F is open};
end;

theorem :: FIN_TOPO:18
  for FT being filled (non empty FT_Space_Str),
      A being Subset of FT holds
    A c= A^b;

theorem :: FIN_TOPO:19
  for FT being non empty FT_Space_Str,
      A, B being Subset of FT holds
    A c= B implies A^b c= B^b;

theorem :: FIN_TOPO:20
    for FT being filled finite (non empty FT_Space_Str),
      A being Subset of FT holds
    A is connected iff for x being Element of FT st x in A
    ex S being FinSequence of bool the carrier of FT st
      len S > 0 &
      S/.1 = {x} &
      (for i being Nat st i > 0 & i < len S holds S/.(i+1) = (S/.i)^b /\ A) &
      A c= S/.len S;

theorem :: FIN_TOPO:21
   for E being non empty set,
      A being Subset of E,
      x being Element of E holds
    x in A` iff not x in A;

theorem :: FIN_TOPO:22
  ((A`)^i)` = A^b;

theorem :: FIN_TOPO:23
  ((A`)^b)` = A^i;

theorem :: FIN_TOPO:24
    A^delta = (A^b) /\ ((A`)^b);

theorem :: FIN_TOPO:25
    (A`)^delta = A^delta;

theorem :: FIN_TOPO:26
    x in A^s implies not x in (A \ {x})^b;

theorem :: FIN_TOPO:27
    A^s <> {} & Card A <> 1 implies A is not connected;

theorem :: FIN_TOPO:28
    for FT being filled (non empty FT_Space_Str),
      A being Subset of FT holds
    A^i c= A;

theorem :: FIN_TOPO:29
    for E being set,
      A, B being Subset of E holds
    A = B iff A` = B`;

theorem :: FIN_TOPO:30
    A is open implies A` is closed;

theorem :: FIN_TOPO:31
    A is closed implies A` is open;