The abstract of the Mizar article:

Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space

by

Zbigniew Karno

Received July 26, 1994

MML identifier: TSP_2

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, TSP_1, TEX_4, BOOLE, SUBSET_1, TARSKI, TOPS_1, COLLSP,
      SETFAM_1, FUNCT_1, RELAT_1, NATTRA_1, ORDINAL2, BORSUK_1, TSP_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
      FUNCT_2, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_3, TEX_4, TSP_1;
 constructors TOPS_1, TSEP_1, TEX_2, TEX_3, TEX_4, TSP_1, BORSUK_1, MEMBERED;
 clusters PRE_TOPC, TSP_1, STRUCT_0, RELSET_1, SUBSET_1, BORSUK_1, MEMBERED,
      ZFMISC_1;
 requirements BOOLE, SUBSET;


begin
:: 1. Maximal T_{0} Subsets.

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is T_0 means
:: TSP_2:def 1
 for a, b being Point of X st a in A & b in A holds
           a <> b implies MaxADSet(a) misses MaxADSet(b);
 end;

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is T_0 means
:: TSP_2:def 2
 for a being Point of X st a in A holds A /\ MaxADSet(a) = {a};
end;

definition let X be non empty TopSpace;
  let A be Subset of X;
 redefine attr A is T_0 means
:: TSP_2:def 3
   for a being Point of X st a in A
   ex D being Subset of X
   st D is maximal_anti-discrete & A /\ D = {a};
end;

definition let Y be TopStruct;
  let IT be Subset of Y;
 attr IT is maximal_T_0 means
:: TSP_2:def 4
 IT is T_0 &
  for D being Subset of Y st D is T_0 & IT c= D holds IT = D;
end;

theorem :: TSP_2:1
   for Y0, Y1 being TopStruct, D0 being Subset of Y0,
     D1 being Subset of Y1 st
    the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds
   D0 is maximal_T_0 implies D1 is maximal_T_0;

definition let X be non empty TopSpace;
  let M be Subset of X;
 redefine attr M is maximal_T_0 means
:: TSP_2:def 5
 M is T_0 &
     MaxADSet(M) = the carrier of X;
end;

reserve X for non empty TopSpace;

theorem :: TSP_2:2
 for M being Subset of X holds
   M is maximal_T_0 implies M is dense;

theorem :: TSP_2:3
 for A being Subset of X st A is open or A is closed holds
   A is maximal_T_0 implies A is not proper;

theorem :: TSP_2:4
 for A being empty Subset of X holds A is not maximal_T_0;

theorem :: TSP_2:5
 for M being Subset of X st M is maximal_T_0
  for A being Subset of X st A is closed
  holds A = MaxADSet(M /\ A);

theorem :: TSP_2:6
 for M being Subset of X st M is maximal_T_0
  for A being Subset of X st A is open holds A = MaxADSet(M /\ A);

theorem :: TSP_2:7
   for M being Subset of X st M is maximal_T_0
  for A being Subset of X holds Cl A = MaxADSet(M /\ Cl A);

theorem :: TSP_2:8
   for M being Subset of X st M is maximal_T_0
  for A being Subset of X holds Int A = MaxADSet(M /\ Int A);

definition let X be non empty TopSpace;
  let M be Subset of X;
 redefine attr M is maximal_T_0 means
:: TSP_2:def 6
 for x being Point of X
     ex a being Point of X st a in M & M /\ MaxADSet(x) = {a};
end;

theorem :: TSP_2:9
 for A being Subset of X holds A is T_0 implies
   ex M being Subset of X st A c= M & M is maximal_T_0;

theorem :: TSP_2:10
 ex M being Subset of X st M is maximal_T_0;


begin
:: 2. Maximal Kolmogorov Subspaces.

definition let Y be non empty TopStruct;
  let IT be SubSpace of Y;
 attr IT is maximal_T_0 means
:: TSP_2:def 7
 for A being Subset of Y st A = the carrier of IT holds
                                             A is maximal_T_0;
end;

theorem :: TSP_2:11
 for Y being non empty TopStruct, Y0 being SubSpace of Y,
     A being Subset of Y st
   A = the carrier of Y0 holds A is maximal_T_0 iff Y0 is maximal_T_0;

definition let Y be non empty TopStruct;
 cluster maximal_T_0 -> T_0 (non empty SubSpace of Y);
 cluster non T_0 -> non maximal_T_0 (non empty SubSpace of Y);
end;

definition let X be non empty TopSpace;
  let X0 be non empty SubSpace of X;
 redefine attr X0 is maximal_T_0 means
:: TSP_2:def 8
   X0 is T_0 &
   for Y0 being T_0 non empty SubSpace of X st X0 is SubSpace of Y0 holds
                              the TopStruct of X0 = the TopStruct of Y0;
end;

reserve X for non empty TopSpace;

theorem :: TSP_2:12
 for A0 being non empty Subset of X st A0 is maximal_T_0
  ex X0 being strict non empty SubSpace of X st
            X0 is maximal_T_0 & A0 = the carrier of X0;

definition let X be non empty TopSpace;
 cluster maximal_T_0 -> dense SubSpace of X;
 cluster non dense -> non maximal_T_0 SubSpace of X;
 cluster open maximal_T_0 -> non proper SubSpace of X;
 cluster open proper -> non maximal_T_0 SubSpace of X;
 cluster proper maximal_T_0 -> non open SubSpace of X;
 cluster closed maximal_T_0 -> non proper SubSpace of X;
 cluster closed proper -> non maximal_T_0 SubSpace of X;
 cluster proper maximal_T_0 -> non closed SubSpace of X;
end;

theorem :: TSP_2:13
   for Y0 being T_0 non empty SubSpace of X
   ex X0 being strict SubSpace of X st
            Y0 is SubSpace of X0 & X0 is maximal_T_0;

definition let X be non empty TopSpace;
 cluster maximal_T_0 strict non empty SubSpace of X;
end;

definition let X be non empty TopSpace;
 mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X;
end;

theorem :: TSP_2:14
 for X0 being maximal_Kolmogorov_subspace of X
  for G being Subset of X, G0 being Subset of X0
  st G0 = G holds
      G0 is open iff
    MaxADSet(G) is open & G0 = MaxADSet(G) /\ the carrier of X0;

theorem :: TSP_2:15
   for X0 being maximal_Kolmogorov_subspace of X
  for G being Subset of X holds
      G is open iff G = MaxADSet(G) &
    ex G0 being Subset of X0
    st G0 is open & G0 = G /\ the carrier of X0;

theorem :: TSP_2:16
 for X0 being maximal_Kolmogorov_subspace of X
  for F being Subset of X, F0 being Subset of X0
  st F0 = F holds
      F0 is closed iff
    MaxADSet(F) is closed & F0 = MaxADSet(F) /\ the carrier of X0;

theorem :: TSP_2:17
   for X0 being maximal_Kolmogorov_subspace of X
  for F being Subset of X holds
      F is closed iff F = MaxADSet(F) &
    ex F0 being Subset of X0
    st F0 is closed & F0 = F /\ the carrier of X0;


begin
:: 3. Stone Retraction Mapping Theorems.
reserve X for non empty TopSpace,
        X0 for non empty maximal_Kolmogorov_subspace of X;

theorem :: TSP_2:18
 for r being map of X,X0
  for M being Subset of X st M = the carrier of X0 holds
    (for a being Point of X holds M /\ MaxADSet(a) = {r.a}) implies
                          r is continuous map of X,X0;

theorem :: TSP_2:19
   for r being map of X,X0 holds
   (for a being Point of X holds r.a in MaxADSet(a)) implies
                                  r is continuous map of X,X0;

theorem :: TSP_2:20
 for r being continuous map of X,X0
  for M being Subset of X st M = the carrier of X0 holds
    (for a being Point of X holds M /\ MaxADSet(a) = {r.a}) implies
                                                    r is_a_retraction;

theorem :: TSP_2:21
 for r being continuous map of X,X0 holds
   (for a being Point of X holds r.a in MaxADSet(a)) implies
                                                r is_a_retraction;

theorem :: TSP_2:22
 ex r being continuous map of X,X0 st r is_a_retraction;

theorem :: TSP_2:23
   X0 is_a_retract_of X;

definition let X be non empty TopSpace,
    X0 be non empty maximal_Kolmogorov_subspace of X;
 func Stone-retraction(X,X0) -> continuous map of X,X0 means
:: TSP_2:def 9
 it is_a_retraction;
end;

theorem :: TSP_2:24
   for a being Point of X, b being Point of X0 st a = b holds
                      (Stone-retraction(X,X0))" Cl {b} = Cl {a};

theorem :: TSP_2:25
 for a being Point of X, b being Point of X0 st a = b holds
                      (Stone-retraction(X,X0))" {b} = MaxADSet(a);

theorem :: TSP_2:26
 for E being Subset of X, F being Subset of X0
 st F = E holds
                      (Stone-retraction(X,X0))" (F) = MaxADSet(E);

definition let X be non empty TopSpace,
      X0 be non empty maximal_Kolmogorov_subspace of X;
 redefine func Stone-retraction(X,X0) -> continuous map of X,X0 means
:: TSP_2:def 10
 for M being Subset of X st M = the carrier of X0
    for a being Point of X holds M /\ MaxADSet(a) = {it.a};
end;

definition let X be non empty TopSpace,
      X0 be non empty maximal_Kolmogorov_subspace of X;
 redefine func Stone-retraction(X,X0) -> continuous map of X,X0 means
:: TSP_2:def 11
 for a being Point of X holds it.a in MaxADSet(a);
end;

theorem :: TSP_2:27
 for a being Point of X holds
   (Stone-retraction(X,X0))" {(Stone-retraction(X,X0)).a} = MaxADSet(a);

theorem :: TSP_2:28
   for a being Point of X holds
   (Stone-retraction(X,X0)).: {a} = (Stone-retraction(X,X0)).: MaxADSet(a);

definition let X be non empty TopSpace,
    X0 be non empty maximal_Kolmogorov_subspace of X;
 redefine func Stone-retraction(X,X0) -> continuous map of X,X0 means
:: TSP_2:def 12
 for M being Subset of X st M = the carrier of X0
    for A being Subset of X holds M /\ MaxADSet(A) = it.: A;
end;

theorem :: TSP_2:29
 for A being Subset of X holds
   (Stone-retraction(X,X0))"((Stone-retraction(X,X0)).: A) = MaxADSet(A);

theorem :: TSP_2:30
   for A being Subset of X holds
   (Stone-retraction(X,X0)).: A = (Stone-retraction(X,X0)).: MaxADSet(A);

theorem :: TSP_2:31
   for A, B being Subset of X holds
  (Stone-retraction(X,X0)).:(A \/ B) =
          (Stone-retraction(X,X0)).:(A) \/ (Stone-retraction(X,X0)).:(B);

theorem :: TSP_2:32
   for A, B being Subset of X st A is open or B is open holds
  (Stone-retraction(X,X0)).:(A /\ B) =
          (Stone-retraction(X,X0)).:(A) /\ (Stone-retraction(X,X0)).:(B);

theorem :: TSP_2:33
   for A, B being Subset of X st A is closed or B is closed holds
  (Stone-retraction(X,X0)).:(A /\ B) =
          (Stone-retraction(X,X0)).:(A) /\ (Stone-retraction(X,X0)).:(B);

theorem :: TSP_2:34
   for A being Subset of X holds
   A is open implies (Stone-retraction(X,X0)).:(A) is open;

theorem :: TSP_2:35
   for A being Subset of X holds
   A is closed implies (Stone-retraction(X,X0)).:(A) is closed;