The Mizar article:

Finite Topological Spaces

by
Hiroshi Imura, and
Masayoshi Eguchi

Received November 27, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: FIN_TOPO
[ 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;
 definitions TARSKI, GROUP_1, STRUCT_0, ORDINAL1, XBOOLE_0;
 theorems NAT_1, TARSKI, CQC_LANG, SUBSET_1, AXIOMS, ZFMISC_1, FINSET_1,
      REAL_1, INT_1, CARD_1, FINSEQ_4, FUNCT_1, FUNCT_2, FINSEQ_1, ABSVALUE,
      GROUP_1, RELSET_1, SETFAM_1, ORDINAL1, XBOOLE_0, XBOOLE_1, CARD_2,
      XCMPLX_1;
 schemes RECDEF_1, NAT_1, FINSET_1, FINSEQ_2, COMPLSP1;

begin

theorem Th1:
  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
proof
  let A be set;
  let f be FinSequence of bool A such that
A1:for i being Nat st 1 <= i & i < len f holds f/.i c= f/.(i+1);
  let i, j be Nat such that
    A2:i <= j & 1 <= i & j <= len f;
  defpred P[Nat] means i+$1 <= j implies f/.i c= f/.(i+$1);
  A3:P[0];
  A4:now let k be Nat;
    A5:i+k+1 = i+(k+1) by XCMPLX_1:1;
    assume A6:P[k];
    thus P[k+1]
    proof
    assume A7: i+(k+1) <= j;
    then A8:i+k < j by A5,NAT_1:38;
      i+k >= i by NAT_1:29;
    then i+k >= 1 & i+k < len f by A2,A8,AXIOMS:22;
    then f/.(i+k) c= f/.(i+(k+1)) by A1,A5;
    hence f/.i c= f/.(i+(k+1)) by A5,A6,A7,NAT_1:38,XBOOLE_1:1;
    end;
  end;
  A9:for k being Nat holds P[k] from Ind(A3,A4);
  consider k be Nat such that
A10:i+k = j by A2,NAT_1:28;
  thus thesis by A9,A10;
end;

theorem Th2:
  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
proof
  let A be set;
  let f be FinSequence of bool A such that
    A1:for i being Nat st 1 <= i & i < len f holds f/.i c= f/.(i+1);
  let i, j be Nat; assume
A2:i < j & 1 <= i & j <= len f & f/.j c= f/.i;
  defpred P[Nat] means i+$1 <= j implies f/.j c= f/.(i+$1);
  A3:P[0] by A2;
  A4:now let k be Nat;
    A5:i+k+1 = i+(k+1) by XCMPLX_1:1;
    assume A6:P[k];
    thus P[k+1]
    proof
    assume A7: i+(k+1) <= j;
    then A8:i+k < j by A5,NAT_1:38;
      i+k >= i by NAT_1:29;
    then i+k >= 1 & i+k < len f by A2,A8,AXIOMS:22;
    then f/.(i+k) c= f/.(i+k+1) by A1;
    hence f/.j c= f/.(i+(k+1)) by A5,A6,A7,NAT_1:38,XBOOLE_1:1;
    end;
  end;
  A9:for k being Nat holds P[k] from Ind(A3,A4);
  let k be Nat; assume A10:i <= k & k <= j;
  then consider m be Nat such that
    A11:k = i + m by NAT_1:28;
  A12:f/.j c= f/.k by A9,A10,A11;
    1 <= k by A2,A10,AXIOMS:22;
  then f/.k c= f/.j by A1,A2,A10,Th1;
  hence thesis by A12,XBOOLE_0:def 10;
end;

theorem Th3:
  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
proof
  defpred P[set] means $1 <> {} implies
   ex m being set st m in $1 & for C being set st C in $1 holds C c= m;
  let F be set such that
  A1: F is finite and
  A2: F <> {} and
  A3: F is c=-linear;
  A4: P[{}];
  A5: now let x,B be set such that A6:x in F & B c= F & P[B];
      now per cases;
     suppose A7:not ex y being set st y in B & x c= y;
      assume B \/ {x} <> {};
      take m = x;
         x in {x} by TARSKI:def 1;
      hence m in B \/ {x} by XBOOLE_0:def 2;
      let C be set;
      assume C in B \/ {x};
      then A8: C in B or C in {x} by XBOOLE_0:def 2;
      then C,x are_c=-comparable by A3,A6,ORDINAL1:def 9,TARSKI:def 1;
      then C c= x or x c= C by XBOOLE_0:def 9;
       hence C c= m by A7,A8,TARSKI:def 1;
     suppose ex y being set st y in B & x c= y;
     then consider y being set such that A9: y in B & x c= y;
      assume B \/ {x} <> {};
       consider m being set such that A10:m in B and
       A11: for C being set st C in B holds C c= m by A6,A9;
         y c= m by A9,A11;
       then A12:x c= m by A9,XBOOLE_1:1;
        take m;
      thus m in B \/ {x} by A10,XBOOLE_0:def 2;
      let C be set;
      assume C in B \/ {x};
      then C in B or C in {x} by XBOOLE_0:def 2;
      hence C c= m by A11,A12,TARSKI:def 1;
    end;
   hence P[B \/ {x}];
   end;
     P[F] from Finite(A1,A4,A5);
  hence thesis by A2;
 end;

canceled;

theorem Th5:
  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
proof
  let f be Function such that
    A1:for i being Nat holds f.i c= f.(i+1);
  let i, j be Nat such that
    A2:i <= j;
  defpred P[Nat] means i+$1 <= j implies f.i c= f.(i+$1);
  A3:P[0];
  A4:now let k be Nat;
    A5:i+k+1 = i+(k+1) by XCMPLX_1:1;
    assume A6:P[k];
    thus P[k+1]
    proof
    assume A7: i+(k+1) <= j;
      f.(i+k) c= f.(i+(k+1)) by A1,A5;
    hence f.i c= f.(i+(k+1)) by A5,A6,A7,NAT_1:38,XBOOLE_1:1;
    end;
  end;
  A8:for k being Nat holds P[k] from Ind(A3,A4);
  consider k be Nat such that
    A9:i+k = j by A2,NAT_1:28;
  thus f.i c= f.j by A8,A9;
end;

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
    A1: A() is finite and
    A2: B() c= A() and
    A3: for A being Subset of X() st A c= A() holds A c= F(A) & F(A) c= A()
proof
  deffunc _F(Nat,Subset of X()) = F($2);
  consider f being Function of NAT,bool X() such that
    A4:f.0 = B() and
    A5:for n being Element of NAT holds f.(n+1) = _F(n,f.n) from LambdaRecExD;
    defpred P[Nat] means f.$1 c= A();
  A6:P[0] by A2,A4;
  A7:now
    let n be Nat such that A8:P[n];
      f.(n+1) = F(f.n) by A5;
    hence P[n+1] by A3,A8;
  end;
  A9:for n being Nat holds P[n] from Ind(A6,A7);
  A10:rng f c= bool A()
    proof
      let x be set; assume x in rng f;
      then x in f.:NAT by FUNCT_2:45;
      then ex k being Nat st k in NAT & f.k=x by FUNCT_2:116;
      then x c= A() by A9;
      hence x in bool A();
    end;
    bool A() is finite by A1,FINSET_1:24;
  then A11:rng f is finite by A10,FINSET_1:13;
  A12:dom f = NAT by FUNCT_2:def 1;
  then A13:rng f <> {} by A4,FUNCT_1:def 5;
  A14:for i being Nat holds f.i c= f.(i+1)
    proof
      let i be Nat;
      A15:f.(i+1) = F(f.i) by A5;
        f.i c= A() by A9;
      hence f.i c= f.(i+1) by A3,A15;
    end;
    rng f is c=-linear
    proof
      let B,C be set; assume
        A16:B in rng f & C in rng f;
      then consider i being set such that
        A17:i in NAT & B = f.i by A12,FUNCT_1:def 5;
      consider j being set such that
        A18:j in NAT & C = f.j by A12,A16,FUNCT_1:def 5;
      reconsider i as Nat by A17;
      reconsider j as Nat by A18;
        now per cases;
        case i <= j;
          hence B c= C by A14,A17,A18,Th5;
        case j <= i;
          hence C c= B by A14,A17,A18,Th5;
      end;
      hence B c= C or C c= B;
    end;
  then consider m being set such that
    A19:m in rng f and
    A20:for C being set st C in rng f holds C c= m
      by A11,A13,Th3;
    defpred P[Nat] means $1 in NAT & f.$1=m;
    m in f.:NAT by A19,FUNCT_2:45;
  then A21:ex k being Nat st P[k] by FUNCT_2:116;
  consider k being Nat such that
    A22:P[k] and
    A23:for n being Nat st P[n] holds k <= n from Min(A21);
A24:  k+1 in Seg(k+1) by FINSEQ_1:6;
  A25:k >= 0 by NAT_1:18;
  deffunc G(Nat) = f.(abs($1-1));
  consider z being FinSequence of bool X() such that
A26:  len z = k+1 and
A27:  for j being Nat st j in Seg(k+1) holds
        z.j = G(j) from SeqLambdaD;
  take z;
  thus 0 < len z by A26,NAT_1:19;
  then A28: 0+1 <= len z by NAT_1:38;
  then A29:1 in Seg(k+1) by A26,FINSEQ_1:3;
  thus z/.1 = z.1 by A28,FINSEQ_4:24
               .= f.(abs(1-1)) by A27,A29
               .= B() by A4,ABSVALUE:7;
  thus A30:for i being Nat st i > 0 & i < len z holds z/.(i+1)=F(z/.i)
    proof
      let i be Nat; assume
      A31:i > 0 & i < len z;
      then A32: 0+1 <= i & i <= k+1 by A26,NAT_1:38;
      then A33:i in Seg(k+1) by FINSEQ_1:3;
      then A34:z.i = f.(abs(i-1)) by A27;
        0+1 < i+1 by A31,REAL_1:53;
      then A35:1 <= i+1 & i+1 <= k+1 by A26,A31,NAT_1:38;
      then A36:i+1 in Seg(k+1) by FINSEQ_1:3;
        1-1 <= i-1 by A32,REAL_1:49;
      then A37:0 <= (i-1)*1;
A38:   i in dom z by A26,A33,FINSEQ_1:def 3;
      thus z/.(i+1) = z.(i+1) by A26,A35,FINSEQ_4:24
                   .= f.(abs(i+1-1)) by A27,A36
                   .= f.(abs(i-1+1)) by XCMPLX_1:29
                   .= f.(abs(i-1)+abs(1)) by A37,ABSVALUE:24
                   .= f.(abs(i-1)+1) by ABSVALUE:def 1
                   .= F(f.(abs(i-1))) by A5
                   .= F(z/.i) by A34,A38,FINSEQ_4:def 4;
    end;
  thus F(z/.len z)=z/.len z
    proof
      A39:f.k c= f.(k+1) by A14;
        k+1 in NAT;
      then k+1 in dom f by FUNCT_2:def 1;
      then f.(k+1) in rng f by FUNCT_1:def 5;
      then A40: f.(k+1) c= f.k by A20,A22;
A41:   len z = 0 or len z in Seg(len z) by FINSEQ_1:5;
then A42:   len z in dom z by A26,FINSEQ_1:def 3;
      A43:z.len z = f.(abs(k+1-1)) by A26,A27,A41
                        .= f.(abs(k+(1-1))) by XCMPLX_1:29
                        .= f.k by A25,ABSVALUE:def 1;
      hence F(z/.len z) = F(f.k) by A42,FINSEQ_4:def 4
                         .= f.(k+1) by A5
                         .= z.len z by A39,A40,A43,XBOOLE_0:def 10
                         .= z/.len z by A42,FINSEQ_4:def 4;
    end;
  let i, j be Nat; assume A44:0 < i & i < j & j <= len z;
  then A45: 0+1 <= i by NAT_1:38;
  A46:i <= len z by A44,AXIOMS:22;
  A47:i < len z by A44,AXIOMS:22;
  reconsider l = i-1 as Nat by A45,INT_1:18;
  A48:i in Seg(k+1) by A26,A45,A46,FINSEQ_1:3;
A49:1-1 <= i-1 by A45,REAL_1:49;
  A50:z/.i = z.i by A45,A46,FINSEQ_4:24
            .= f.(abs(i-1)) by A27,A48
            .= f.l by A49,ABSVALUE:def 1;
  hence z/.i c= A() by A9;
  A51:for i being Nat st 1 <= i & i < len z holds z/.i c= z/.(i+1)
    proof
      let i be Nat; assume
      A52:1 <= i & i < len z;
      then A53:i in Seg(k+1) by A26,FINSEQ_1:3;
A54:  1-1 <= i-1 by A52,REAL_1:49;
      A55:z/.i = z.i by A52,FINSEQ_4:24
                  .= f.(abs(i-1)) by A27,A53
                  .= f.(i-1) by A54,ABSVALUE:def 1;
      A56:1 <= i+1 & i+1 <= len z by A52,NAT_1:38;
      then A57:i+1 in Seg(k+1) by A26,FINSEQ_1:3;
A58:  1-1 <= i+1-1 by A56,REAL_1:49;
      A59:z/.(i+1) = z.(i+1) by A56,FINSEQ_4:24
                    .= f.(abs(i+1-1)) by A27,A57
                    .= f.(i+1-1) by A58,ABSVALUE:def 1
                    .= f.(i-1+1) by XCMPLX_1:29;
        i-1 is Nat by A54,INT_1:16;
      hence z/.i c= z/.(i+1) by A14,A55,A59;
    end;
  hence z/.i c= z/.j by A44,A45,Th1;
  assume A60: z/.i = z/.j;
    i <= i+1 & i+1 <= j by A44,NAT_1:38;
  then A61:z/.i = z/.(i+1) by A44,A45,A51,A60,Th2
             .= F(z/.i) by A30,A44,A47;
  defpred P[Nat] means i+$1 <= len z implies z/.i = z/.(i+$1);
  A62:P[0];
  A63:now
      let n be Nat such that A64:P[n];
      thus P[n+1]
      proof
      A65:i+n > 0 by A44,NAT_1:29;
      assume i+(n+1) <= len z;
      then i+n+1 <= len z by XCMPLX_1:1;
      then i+n < len z by NAT_1:38;
      hence z/.i = z/.(i+n+1) by A30,A61,A64,A65
                   .= z/.(i+(n+1)) by XCMPLX_1:1;
      end;
  end;
  A66:for n being Nat holds P[n] from Ind(A62,A63);
  consider n0 being Nat such that A67:i+n0 = len z by A46,NAT_1:28;
A68:  k+1 in dom z by A24,A26,FINSEQ_1:def 3;
    f.l = z/.(k+1) by A26,A50,A66,A67
           .= z.(k+1) by A68,FINSEQ_4:def 4
           .= f.(abs(k+1-1)) by A24,A27
           .= f.(abs(k)) by XCMPLX_1:26
           .= m by A22,A25,ABSVALUE:def 1;
  then k <= l by A23;
  then len z <= l + 1 by A26,AXIOMS:24;
  then len z <= i by XCMPLX_1:27;
  hence contradiction by A44,AXIOMS:22;
end;

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;
 existence
  proof consider D being non empty set,f being Function of D, bool D;
    take FT_Space_Str(#D,f#);
    thus the carrier of FT_Space_Str(#D,f#) is non empty;
    thus thesis;
  end;
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
:Def1:
   ( the Nbd of FT ).x;
  coherence;
end;

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

  redefine func x.-->y -> Function of {x}, bool {x};
  coherence
    proof
A1:   dom ( x.-->y ) = {x} by CQC_LANG:5;
        rng ( x.-->y ) = {y} by CQC_LANG:5;
      then reconsider R = x.-->y as Relation of {x}, bool {x}
            by A1,RELSET_1:11;
        R is quasi_total by A1,FUNCT_2:def 1;
     hence thesis;
    end;
end;

definition
  func FT{0} -> strict FT_Space_Str equals
:Def2:
   FT_Space_Str (#{0},0.-->[#]{0}#);
  coherence;
end;

definition
  cluster FT{0} -> non empty;
  coherence
  proof
   thus the carrier of FT{0} is non empty by Def2;
  end;
end;

definition let IT be non empty FT_Space_Str;
  attr IT is filled means
:Def3:
  for x being Element of IT holds x in U_FT x;
end;

canceled;

theorem Th7:
  FT{0} is filled
proof
    let x be Element of FT{0};
      x = 0 by Def2,TARSKI:def 1;
    then A1: (0.-->[#]{0}).x = [#]{0} by CQC_LANG:6;
      [#]{0} = {0} by SUBSET_1:def 4;
    then x in (the Nbd of FT{0}).x by A1,Def2;
    hence x in U_FT x by Def1;
end;

theorem Th8:
  FT{0} is finite
proof
   rng <*0*> = {0} by FINSEQ_1:55;
  hence the carrier of FT{0} is finite by Def2;
end;

definition
  cluster finite filled strict (non empty FT_Space_Str);
  existence by Th7,Th8;
end;

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

  pred F is_a_cover_of T means
    the carrier of T c= union F;
end;

theorem
    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
proof
  let FT be filled (non empty FT_Space_Str);
  let a be set;
  assume a in the carrier of FT;
  then reconsider b = a as Element of FT;
  A1:b in U_FT b by Def3;
    U_FT b in
   {U_FT x where x is Element of FT : not contradiction};
  hence thesis by A1,TARSKI:def 4;
end;

reserve A for Subset of FT;

definition
  let FT;
  let A be Subset of FT;

  func A^delta -> Subset of FT equals
:Def6:
   {x:U_FT x meets A & U_FT x meets A` };
  coherence
    proof
      defpred P[Element of FT] means
        U_FT $1 meets A & U_FT $1 meets A`;
      deffunc F(Element of FT) = $1;
      {F(x):P[x]} is Subset of FT from SubsetFD;
      hence thesis;
    end;
end;

theorem Th10:
  x in A^delta iff U_FT x meets A & U_FT x meets A`
proof
  thus x in A^delta implies U_FT x meets A & U_FT x meets A`
    proof
      assume x in A^delta;
      then x in {y:U_FT y meets A & U_FT y meets A`} by Def6;
      then ex y st y=x & U_FT y meets A & U_FT y meets A`;
      hence thesis;
    end;
  assume U_FT x meets A & U_FT x meets A`;
  then x in {y:U_FT y meets A & U_FT y meets A`};
  hence thesis by Def6;
end;

definition let FT;
  let A be Subset of FT;
  func A^deltai -> Subset of FT equals
:Def7:
   A /\ (A^delta);
  coherence;

  func A^deltao -> Subset of FT equals
:Def8:
   A` /\ (A^delta);
  coherence;
end;

theorem
    A^delta = A^deltai \/ A^deltao
proof
    for x being set holds x in A^delta iff x in A^deltai \/ A^deltao
    proof
      let x be set;
        A^delta c= (the carrier of FT);
      then A1:A^delta c= [#](the carrier of FT) by SUBSET_1:def 4;
      thus x in A^delta implies x in A^deltai \/ A^deltao
        proof
          assume x in A^delta;
          then x in [#](the carrier of FT) /\ (A^delta) by A1,XBOOLE_1:28;
          then x in (A \/ A`) /\ (A^delta) by SUBSET_1:25;
          then x in A /\ (A^delta) \/ A` /\ (A^delta) by XBOOLE_1:23;
          then x in A^deltai \/ (A` /\ (A^delta)) by Def7;
          hence x in (A^deltai) \/ (A^deltao) by Def8;
        end;
      assume x in A^deltai \/ A^deltao;
      then x in A /\ (A^delta) \/ A^deltao by Def7;
      then x in A /\ (A^delta) \/ A` /\ (A^delta) by Def8;
      then x in (A \/ A`) /\ (A^delta) by XBOOLE_1:23;
      then x in [#](the carrier of FT) /\ (A^delta) by SUBSET_1:25;
      hence x in A^delta by A1,XBOOLE_1:28;
    end;
  hence thesis by TARSKI:2;
end;

definition let FT;
  let A be Subset of FT;
  func A^i -> Subset of FT equals :Def9:
   {x:U_FT x c= A};
  coherence
    proof
      defpred P[Element of FT] means U_FT $1 c= A;
      deffunc F(Element of FT) = $1;
      {F(x):P[x]} is Subset of FT from SubsetFD;
      hence thesis;
    end;

  func A^b -> Subset of FT equals
:Def10:
   {x:U_FT x meets A};
  coherence
    proof
      defpred P[Element of FT] means U_FT $1 meets A;
      deffunc F(Element of FT) = $1;
      {F(x):P[x]} is Subset of FT from SubsetFD;
      hence thesis;
    end;

  func A^s -> Subset of FT equals
:Def11:
   {x:x in A & U_FT x \ {x} misses A };
  coherence
    proof
      defpred P[Element of FT] means
        $1 in A & U_FT $1 \ {$1} misses A;
      deffunc F(Element of FT) = $1;
      {F(x):P[x]} is Subset of FT from SubsetFD;
      hence thesis;
    end;
end;

definition
  let FT;
  let A be Subset of FT;

  func A^n -> Subset of FT equals
:Def12:
   A \ A^s;
  coherence;

  func A^f -> Subset of FT equals
:Def13:
   {x:ex y st y in A & x in U_FT y};
  coherence
    proof
      defpred P[Element of FT] means
        ex y st y in A & $1 in U_FT y;
      deffunc F(Element of FT) = $1;
      {F(x):P[x]} is Subset of FT from SubsetFD;
      hence thesis;
    end;
end;

definition let IT be non empty FT_Space_Str;
  attr IT is symmetric means
:Def14:
  for x, y being Element of IT holds
    y in U_FT x implies x in U_FT y;
end;

theorem Th12:
  x in A^i iff U_FT x c= A
proof
  thus x in A^i implies U_FT x c= A
    proof
      assume x in A^i;
      then x in {y:U_FT y c= A} by Def9;
      then ex y st y=x & U_FT y c= A;
      hence thesis;
    end;
  assume U_FT x c= A;
  then x in {y:U_FT y c= A};
  hence thesis by Def9;
end;

theorem Th13:
  x in A^b iff U_FT x meets A
proof
  thus x in A^b implies U_FT x meets A
    proof
      assume x in A^b;
      then x in {y:U_FT y meets A} by Def10;
      then ex y st y = x & U_FT y meets A;
      hence thesis;
    end;
  assume U_FT x meets A;
  then x in {y:U_FT y meets A};
  hence thesis by Def10;
end;

theorem Th14:
  x in A^s iff x in A & U_FT x \ {x} misses A
proof
  thus x in A^s implies x in A & U_FT x \ {x} misses A
    proof
      assume x in A^s;
      then x in {y:y in A & U_FT y \ {y} misses A} by Def11;
      then ex y st y = x & y in A & U_FT y \ {y} misses A;
      hence thesis;
    end;
  assume x in A & U_FT x \ {x} misses A;
  then x in {y:y in A & U_FT y \ {y} misses A};
  hence thesis by Def11;
end;

theorem
    x in A^n iff x in A & U_FT x \ {x} meets A
proof
  thus x in A^n implies x in A & U_FT x \ {x} meets A
    proof
      assume x in A^n;
      then x in A \ A^s by Def12;
      then x in A & not x in A^s by XBOOLE_0:def 4;
      hence x in A & U_FT x \ {x} meets A by Th14;
    end;
  assume x in A & U_FT x \ {x} meets A;
  then x in A & not x in A^s by Th14;
  then x in A \ A^s by XBOOLE_0:def 4;
  hence thesis by Def12;
end;

theorem Th16:
  x in A^f iff ex y st y in A & x in U_FT y
proof
  thus x in A^f implies ex y st y in A & x in U_FT y
    proof
      assume x in A^f;
      then x in {y:ex z st z in A & y in U_FT z} by Def13;
      then ex y st y = x & ex z st z in A & y in U_FT z;
      hence thesis;
    end;
  assume ex z st z in A & x in U_FT z;
  then x in {y:ex z st z in A & y in U_FT z};
  hence x in A^f by Def13;
end;

theorem
    FT is symmetric iff for A holds A^b = A^f
proof
  thus FT is symmetric implies for A holds A^b = A^f
    proof
      assume A1:FT is symmetric;
      let A be Subset of FT;
      thus A^b c= A^f
        proof
          let x be set;
          assume A2:x in A^b;
          then reconsider y = x as Element of FT;
            U_FT y meets A by A2,Th13;
          then consider z be set such that A3:z in U_FT y /\ A by XBOOLE_0:4;
          reconsider z as Element of FT by A3;
          A4:z in U_FT y & z in A by A3,XBOOLE_0:def 3;
          then y in U_FT z by A1,Def14;
          hence x in A^f by A4,Th16;
        end;
      let x be set;
      assume A5:x in A^f;
      then reconsider y = x as Element of FT;
      consider z such that A6:z in A & y in U_FT z by A5,Th16;
        z in U_FT y by A1,A6,Def14;
      then U_FT y meets A by A6,XBOOLE_0:3;
      hence x in A^b by Th13;
    end;
  assume A7:for A being Subset of FT holds A^b = A^f;
  let x, y be Element of FT;
  assume y in U_FT x;
  then U_FT x meets {y} by ZFMISC_1:54;
  then x in {y}^b by Th13;
  then x in {y}^f by A7;
  then consider z such that A8:z in {y} & x in U_FT z by Th16;
  thus x in U_FT y by A8,TARSKI:def 1;
end;

reserve F for Subset of FT;

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

  attr IT is closed means :Def16:
  IT = IT^b;

  attr IT is connected means :Def17:
  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
     meet{F:A c= F & F is closed};
  coherence
    proof
      set FF = {F:A c= F & F is closed};
        FF c= bool the carrier of FT
        proof
          let x be set;
          assume x in FF;
          then ex F st x = F & A c= F & F is closed;
          hence x in bool the carrier of FT;
        end;
      then reconsider FF as Subset-Family of FT by SETFAM_1:def 7;
        meet FF is Subset of FT;
      hence thesis;
    end;

  func A^fi -> Subset of FT equals
     union{F:A c= F & F is open};
  coherence
    proof
      set FF = {F:A c= F & F is open};
        FF c= bool the carrier of FT
        proof
          let x be set;
          assume x in FF;
          then ex F st x = F & A c= F & F is open;
          hence x in bool the carrier of FT;
        end;
      then reconsider FF as Subset-Family of FT by SETFAM_1:def
7;
        union FF is Subset of FT;
      hence thesis;
    end;
end;

theorem Th18:
  for FT being filled (non empty FT_Space_Str),
      A being Subset of FT holds
    A c= A^b
proof
  let FT be filled (non empty FT_Space_Str);
  let A be Subset of FT;
  let x be set;
  assume A1:x in A;
  then reconsider y=x as Element of FT;
    y in U_FT y by Def3;
  then U_FT y meets A by A1,XBOOLE_0:3;
  hence thesis by Th13;
end;

theorem Th19:
  for FT being non empty FT_Space_Str,
      A, B being Subset of FT holds
    A c= B implies A^b c= B^b
proof
  let FT be non empty FT_Space_Str;
  let A, B be Subset of FT;
  assume A1:A c= B;
  let x be set;
  assume A2:x in A^b;
  then reconsider y=x as Element of FT;
    U_FT y meets A by A2,Th13;
  then consider w being set such that
  A3:w in U_FT y & w in A by XBOOLE_0:3;
    U_FT y meets B by A1,A3,XBOOLE_0:3;
  hence x in B^b by Th13;
end;

theorem
    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
proof
  let FT be filled finite (non empty FT_Space_Str),
      A be Subset of FT;
thus A is connected implies 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
  proof
    assume A1:A is connected;
    let x be Element of FT such that A2:x in A;
    deffunc F(Subset of FT) = $1^b /\ A;
    the carrier of FT is finite & A c= the carrier of FT
     by GROUP_1:def 13;
    then A3: A is finite by FINSET_1:13;
      A4: {x} c= A by A2,ZFMISC_1:37;
      A5:for B being Subset of FT st B c= A
         holds B c= F(B) & F(B) c= A
      proof
        let B be Subset of FT such that A6:B c= A;
          B c= B^b by Th18;
        hence B c= B^b /\ A by A6,XBOOLE_1:19;
        thus B^b /\ A c= A by XBOOLE_1:17;
      end;
    consider S being FinSequence of bool the carrier of FT such that
      A7:len S > 0 and
      A8:S/.1={x} and
      A9:(for i being Nat st i > 0 & i < len S holds S/.(i+1)=F(S/.i))
      and
      A10:F(S/.len S) = S/.len S and
      A11:(for i, j being Nat st i > 0 & i < j & j <= len S holds
           S/.i c= A & S/.i c< S/.j)
        from MaxFinSeqEx(A3,A4,A5);
    take S;
    thus len S > 0 by A7;
    thus S/.1 = {x} by A8;
    thus for i being Nat st
      i > 0 & i < len S holds S/.(i+1) = S/.i^b /\ A by A9;
    set B = S/.len S;
    set C = A \ B;
    A12:B c= A by A10,XBOOLE_1:17;
    A13:B \/ C = B \/ A by XBOOLE_1:39
              .= A by A12,XBOOLE_1:12;
    assume not A c= S/.len S;
    then A14:C <> {} by XBOOLE_1:37;
    defpred P[Nat] means $1 < len S implies S/.($1+1) <> {};
    A15:P[0] by A8;
    A16:now let i be Nat;
         assume A17:P[i];
         thus P[i+1]
         proof
         assume A18:i + 1 < len S;
         A19:i+1 > 0 by NAT_1:19;
         A20:i+1 < i+1+1 by NAT_1:38;
           i+1+1 <= len S by A18,NAT_1:38;
         then S/.(i+1) c< S/.(i+1+1) by A11,A19,A20;
         then S/.(i+1) c= S/.(i+1+1) by XBOOLE_0:def 8;
         hence S/.(i+1+1) <> {} by A17,A18,NAT_1:38,XBOOLE_1:3;
         end;
       end;
    A21:for i being Nat holds P[i] from Ind(A15,A16);
    consider k being Nat such that
      A22:len S = k+1 by A7,NAT_1:22;
      k < len S by A22,NAT_1:38;
    then A23:B <> {} by A21,A22;
    A24:B misses C by XBOOLE_1:79;
A25:  B misses ( A \ B ) by XBOOLE_1:79;
      A \ B c= A by XBOOLE_1:36;
    then B^b /\ C = B^b /\ ( A /\ ( A \ B ) ) by XBOOLE_1:28
            .= B /\ ( A \ B ) by A10,XBOOLE_1:16
            .= {} by A25,XBOOLE_0:def 7;
    then B^b misses C by XBOOLE_0:def 7;
    hence contradiction by A1,A13,A14,A23,A24,Def17;
  end;
  assume A26: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;
  given B, C being Subset of FT such that
    A27:A = B \/ C and
    A28:B <> {} and
    A29:C <> {} and
    A30:B misses C and
    A31:B^b misses C;
  A32: B c= B^b by Th18;
A33:B^b /\ C = {} by A31,XBOOLE_0:def 7;
A34:B /\ C = {} by A30,XBOOLE_0:def 7;
  A35: B^b /\ A = B^b /\ B \/ {} by A27,A33,XBOOLE_1:23
             .= B by A32,XBOOLE_1:28;
  consider x being Element of B;
    x in A by A27,A28,XBOOLE_0:def 2;
  then consider S being FinSequence of bool the carrier of FT such that
    A36:len S > 0 and
    A37:S/.1 = {x} and
    A38:for i being Nat st i > 0 & i < len S holds S/.(i+1) =
(S/.i)^b /\ A and
    A39:A c= S/.len S by A26;
  A40:B c= A by A27,XBOOLE_1:7;
  defpred P[Nat] means $1 < len S implies S/.($1+1) c= B;
  A41:P[0] by A28,A37,ZFMISC_1:37;
  A42:now let i be Nat;
      assume A43:P[i];
      thus P[i+1]
      proof
      assume A44:i+1 < len S;
      then S/.(i+1)^b c= B^b by A43,Th19,NAT_1:38;
      then A45:S/.(i+1)^b /\ A c= B^b /\ A by XBOOLE_1:26;
        i+1 > 0 by NAT_1:19;
      hence S/.(i+1+1) c= B by A35,A38,A44,A45;
      end;
    end;
  A46:for i being Nat holds P[i] from Ind(A41,A42);
  consider k being Nat such that A47:len S = k + 1 by A36,NAT_1:22;
    k < len S by A47,NAT_1:38;
  then A48:S/.len S c= B by A46,A47;
  then S/.len S c= A by A40,XBOOLE_1:1;
  then S/.len S = A by A39,XBOOLE_0:def 10;
  then A = B by A40,A48,XBOOLE_0:def 10;
  then C c= B by A27,XBOOLE_1:7;
  hence contradiction by A29,A34,XBOOLE_1:28;
end;

theorem
   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 by SUBSET_1:50,54;

theorem Th22:
  ((A`)^i)` = A^b
proof
    for x being set holds x in ((A`)^i)` iff x in A^b
    proof
      let x be set;
      thus x in ((A`)^i)` implies x in A^b
        proof
          assume A1:x in ((A`)^i)`;
          then reconsider y=x as Element of FT;
            not y in (A`)^i by A1,SUBSET_1:54;
          then not U_FT y c= A` by Th12;
          then consider z being set such that
            A2:not(z in U_FT y implies z in A`) by TARSKI:def 3;
            z in U_FT y & z in A by A2,SUBSET_1:50;
          then U_FT y meets A by XBOOLE_0:3;
          hence x in A^b by Th13;
        end;
      assume A3:x in A^b;
      then reconsider y=x as Element of FT;
        U_FT y meets A by A3,Th13;
      then consider z being set such that
      A4:z in U_FT y & z in A by XBOOLE_0:3;
        not U_FT y c= A` by A4,SUBSET_1:54;
      then not y in (A`)^i by Th12;
      hence x in ((A`)^i)` by SUBSET_1:50;
    end;
  hence thesis by TARSKI:2;
end;

theorem Th23:
  ((A`)^b)` = A^i
proof
    for x being set holds x in ((A`)^b)` iff x in A^i
    proof
      let x be set;
      thus x in ((A`)^b)` implies x in A^i
        proof
          assume A1:x in ((A`)^b)`;
          then reconsider y=x as Element of FT;
            not y in (A`)^b by A1,SUBSET_1:54;
          then U_FT y misses A` by Th13;
          then U_FT y /\ A` = {} by XBOOLE_0:def 7;
          then U_FT y \ A = {} by SUBSET_1:32;
          then U_FT y c= A by XBOOLE_1:37;
          hence x in A^i by Th12;
        end;
      assume A2:x in A^i;
      then reconsider y=x as Element of FT;
        U_FT y c= A by A2,Th12;
      then U_FT y \ A = {} by XBOOLE_1:37;
      then U_FT y /\ A` = {} by SUBSET_1:32;
      then U_FT y misses A` by XBOOLE_0:def 7;
      then not y in (A`)^b by Th13;
      hence x in ((A`)^b)` by SUBSET_1:50;
    end;
  hence thesis by TARSKI:2;
end;

theorem
    A^delta = (A^b) /\ ((A`)^b)
proof
    for x being set holds x in A^delta iff x in (A^b) /\ ((A`)^b)
    proof
      let x be set;
      thus x in A^delta implies x in (A^b) /\ ((A`)^b)
        proof
          assume A1:x in A^delta;
          then reconsider y=x as Element of FT;
            U_FT y meets A & U_FT y meets A` by A1,Th10;
          then x in A^b & x in (A`)^b by Th13;
          hence x in (A^b) /\ ((A`)^b) by XBOOLE_0:def 3;
        end;
      assume A2: x in (A^b) /\ ((A`)^b);
      then A3:x in A^b & x in ((A`)^b) by XBOOLE_0:def 3;
      reconsider y=x as Element of FT by A2;
        U_FT y meets A & U_FT y meets A` by A3,Th13;
      hence x in A^delta by Th10;
    end;
  hence thesis by TARSKI:2;
end;

theorem
    (A`)^delta = A^delta
proof
    for x being set holds x in (A`)^delta iff x in A^delta
    proof
      let x be set;
      thus x in (A`)^delta implies x in A^delta
        proof
          assume A1:x in (A`)^delta;
          then reconsider y=x as Element of FT;
            U_FT y meets (A`) & U_FT y meets (A`)` by A1,Th10;
          hence x in A^delta by Th10;
        end;
      assume A2:x in A^delta;
      then reconsider y=x as Element of FT;
        U_FT y meets (A`)` & U_FT y meets A` by A2,Th10;
      hence x in (A`)^delta by Th10;
    end;
  hence thesis by TARSKI:2;
end;

theorem
    x in A^s implies not x in (A \ {x})^b
proof
  assume x in A^s;
  then A misses (U_FT x \ {x}) by Th14;
  then A /\ (U_FT x \ {x}) = {} by XBOOLE_0:def 7;
  then A1: (A /\ U_FT x) \ {x} = {} by XBOOLE_1:49;
    now per cases by A1,ZFMISC_1:66;
    suppose A /\ U_FT x = {};
then A2:    A misses U_FT x by XBOOLE_0:def 7;
        (A \ {x}) c= A by XBOOLE_1:36;
      hence (A \ {x}) misses U_FT x by A2,XBOOLE_1:63;
    suppose A /\ U_FT x = {x};
      then (U_FT x /\ A) \ {x} = {} by XBOOLE_1:37;
      then U_FT x /\ (A \ {x}) = {} by XBOOLE_1:49;
      hence (A \ {x}) misses U_FT x by XBOOLE_0:def 7;
  end;
  hence thesis by Th13;
end;

theorem
    A^s <> {} & Card A <> 1 implies A is not connected
proof
  assume A1:A^s <> {} & Card A <> 1;
  then consider z being Element of FT such that
    A2:z in A^s by SUBSET_1:10;
  A3:z in A & (U_FT z \ {z}) misses A by A2,Th14;
  set B = A \ {z};
  set C = {z};
    {z} is Subset of A by A3,SUBSET_1:63;
  then A4:A = B \/ C by XBOOLE_1:45;
A5:  Card {z} = 1 by CARD_1:50,CARD_2:20;
    A <> {} by A2,Th14;
  then A6:B <> {} by A1,A5,ZFMISC_1:66;
  A7:B misses C by XBOOLE_1:79;
    B^b misses C
    proof
      assume B^b meets C;
      then consider x being set such that
      A8:x in B^b & x in C by XBOOLE_0:3;
      reconsider x as Element of FT by A8;
        U_FT x meets B by A8,Th13;
      then consider y being set such that
        A9:y in U_FT x & y in B by XBOOLE_0:3;
      A10:x = z by A8,TARSKI:def 1;
      A11:B c= A by XBOOLE_1:36;
        not x in B by A8,XBOOLE_0:def 4;
      then y in U_FT x \ {x} by A9,ZFMISC_1:64;
      then (U_FT z \ {z}) meets B by A9,A10,XBOOLE_0:3;
      then consider w being set such that
        A12:w in (U_FT z \ {z}) /\ B by XBOOLE_0:4;
        (U_FT z \ {z}) /\ B c= (U_FT z \ {z}) /\ A by A11,XBOOLE_1:26;
      hence contradiction by A3,A12,XBOOLE_0:4;
    end;
  hence thesis by A4,A6,A7,Def17;
end;

theorem
    for FT being filled (non empty FT_Space_Str),
      A being Subset of FT holds
    A^i c= A
proof
  let FT be filled (non empty FT_Space_Str);
  let A be Subset of FT;
  let x be set;
  assume A1:x in A^i;
  then reconsider y=x as Element of FT;
  A2:y in U_FT y by Def3;
    U_FT y c= A by A1,Th12;
  hence x in A by A2;
end;

theorem
    for E being set,
      A, B being Subset of E holds
    A = B iff A` = B`
proof
  let E be set;
  let A, B be Subset of E;
  thus A = B implies A` = B`;
  assume A` = B`;
  hence A = B`` .= B;
end;

theorem
    A is open implies A` is closed
proof
  assume A is open;
  then A1:A = A^i by Def15;
    A^i = ((A`)^b)` by Th23;
  hence thesis by A1,Def16;
end;

theorem
    A is closed implies A` is open
proof
  assume A is closed;
  then A1:A = A^b by Def16;
    A^b = ((A`)^i)` by Th22;
  hence thesis by A1,Def15;
end;

Back to top