The abstract of the Mizar article:

Baire Spaces, Sober Spaces

by

Andrzej Trybulec

Received January 8, 1997

MML identifier: YELLOW_8

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSUB_1, FINSET_1, SETFAM_1, BOOLE, REALSET1, SUBSET_1, TARSKI,
      FUNCT_1, RELAT_1, CARD_4, CARD_1, CANTOR_1, PRE_TOPC, TOPS_1, TOPS_3,
      WAYBEL_6, YELLOW_6, TSP_1, SETWISEO, URYSOHN1, COMPTS_1, WAYBEL_3,
      YELLOW_8, RLVECT_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, CANTOR_1,
      SETFAM_1, WELLORD2, CARD_1, CARD_4, REALSET1, FINSET_1, FINSUB_1,
      SETWISEO, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_3, TSP_1, URYSOHN1, YELLOW_6,
      COMPTS_1, WAYBEL_3;
 constructors CANTOR_1, TOPS_1, CARD_4, TOPS_3, URYSOHN1, COMPTS_1, REALSET1,
      DOMAIN_1, T_0TOPSP, SETWISEO, WAYBEL_3, MEMBERED;
 clusters SUBSET_1, YELLOW_6, PRE_TOPC, CARD_5, FINSET_1, STRUCT_0, FINSUB_1,
      ARYTM_3, SETFAM_1, MEMBERED, ZFMISC_1;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

theorem :: YELLOW_8:1
 for X,A,B being set st A in Fin X & B c= A holds B in Fin X;

theorem :: YELLOW_8:2
 for X being set, F being Subset-Family of X st F c= Fin X
  holds meet F in Fin X;

definition let X be non empty set;
 redefine attr X is trivial means
:: YELLOW_8:def 1
 for x,y being Element of X holds x = y;
end;

begin :: Families of complements

theorem :: YELLOW_8:3
for X being set, F being Subset-Family of X
 for P being Subset of X holds P` in COMPLEMENT F iff P in F;

theorem :: YELLOW_8:4
 for X being set, F being Subset-Family of X
  holds F,COMPLEMENT F are_equipotent;

theorem :: YELLOW_8:5
 for X,Y being set st X,Y are_equipotent & X is countable holds
 Y is countable;

theorem :: YELLOW_8:6
  for X being set, F being Subset-Family of X
 holds COMPLEMENT COMPLEMENT F = F;

theorem :: YELLOW_8:7
  for X being set, F being Subset-Family of X
 for P being Subset of X holds P` in COMPLEMENT F iff P in F;

theorem :: YELLOW_8:8
for X being set, F,G being Subset-Family of X
  st COMPLEMENT F c= COMPLEMENT G
 holds F c= G;

theorem :: YELLOW_8:9
for X being set, F,G being Subset-Family of X
 holds COMPLEMENT F c= G iff F c= COMPLEMENT G;

theorem :: YELLOW_8:10
for X being set, F,G being Subset-Family of X
  st COMPLEMENT F = COMPLEMENT G
 holds F = G;

definition let X be set; let F,G be Subset of bool X;
  redefine func F \/ G -> Subset-Family of X;
end;

theorem :: YELLOW_8:11
for X being set, F,G being Subset-Family of X
 holds COMPLEMENT(F \/ G) = COMPLEMENT F \/ COMPLEMENT G;

theorem :: YELLOW_8:12
for X being set, F being Subset-Family of X st F = {X}
 holds COMPLEMENT F = {{}};

definition let X be set, F be empty Subset-Family of X;
 cluster COMPLEMENT F -> empty;
end;

theorem :: YELLOW_8:13
 for X being 1-sorted, F being Subset-Family of X,
     P being Subset of X
  holds P in COMPLEMENT F iff P` in F;

theorem :: YELLOW_8:14
   for X being 1-sorted, F being Subset-Family of X,
     P being Subset of X
  holds P` in COMPLEMENT F iff P in F;

theorem :: YELLOW_8:15
 for X being 1-sorted, F being Subset-Family of X
  holds Intersect COMPLEMENT F = (union F)`;

theorem :: YELLOW_8:16
 for X being 1-sorted, F being Subset-Family of X
  holds union COMPLEMENT F = (Intersect F)`;

begin :: Topological preliminaries

theorem :: YELLOW_8:17
   for T being non empty TopSpace, A,B being Subset of T st
  B c= A & A is closed &
   (for C being Subset of T st B c= C & C is closed
    holds A c= C)
 holds A = Cl B;

theorem :: YELLOW_8:18
 for T being TopStruct, B being Basis of T,
     V being Subset of T st V is open
 holds V = union { G where G is Subset of T: G in B & G c= V };

theorem :: YELLOW_8:19
 for T being TopStruct, B being Basis of T,
     S being Subset of T st S in B
  holds S is open;

theorem :: YELLOW_8:20
   for T being non empty TopSpace, B being Basis of T,
     V being Subset of T
 holds Int V = union { G where G is Subset of T: G in B & G c= V };

begin :: Baire Spaces

definition let T be non empty TopStruct, x be Point of T;
 mode Basis of x -> Subset-Family of T means
:: YELLOW_8:def 2
 it c= the topology of T & x in Intersect it &
   for S being Subset of T st S is open & x in S
    ex V being Subset of T st V in it & V c= S;
end;

theorem :: YELLOW_8:21
 for T being non empty TopStruct, x being Point of T,
     B being Basis of x, V being Subset of T st V in B
 holds V is open & x in V;

theorem :: YELLOW_8:22
  for T being non empty TopStruct, x being Point of T,
     B being Basis of x, V being Subset of T st
       x in V & V is open
  ex W being Subset of T st W in B & W c= V;

theorem :: YELLOW_8:23
   for T being non empty TopStruct, P being Subset-Family of T st
  P c= the topology of T &
  for x being Point of T ex B being Basis of x st B c= P
 holds P is Basis of T;

definition let T be non empty TopSpace;
 attr T is Baire means
:: YELLOW_8:def 3
 for F being Subset-Family of T st F is countable &
  for S being Subset of T st S in F holds S is everywhere_dense
  ex I being Subset of T st I = Intersect F & I is dense;
end;

theorem :: YELLOW_8:24
   for T being non empty TopSpace holds
  T is Baire iff
  for F being Subset-Family of T st F is countable &
   for S being Subset of T st S in F holds S is nowhere_dense
  holds union F is boundary;

begin :: Sober Spaces

definition let T be TopStruct, S be Subset of T;
 attr S is irreducible means
:: YELLOW_8:def 4
 S is non empty closed &
 for S1,S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2
  holds S1 = S or S2 = S;
end;

definition let T be TopStruct;
 cluster irreducible -> non empty Subset of T;
end;

definition let T be non empty TopSpace, S be Subset of T;
 let p be Point of T;
 pred p is_dense_point_of S means
:: YELLOW_8:def 5
 p in S & S c= Cl{p};
end;

theorem :: YELLOW_8:25
   for T being non empty TopSpace,
     S being Subset of T st S is closed
 for p being Point of T st p is_dense_point_of S
  holds S = Cl{p};

theorem :: YELLOW_8:26
 for T being non empty TopSpace, p being Point of T
  holds Cl{p} is irreducible;

definition let T be non empty TopSpace;
 cluster irreducible Subset of T;
end;

definition let T be non empty TopSpace;
 attr T is sober means
:: YELLOW_8:def 6

 for S being irreducible Subset of T
  ex p being Point of T st p is_dense_point_of S &
   for q being Point of T st q is_dense_point_of S holds p = q;
end;

theorem :: YELLOW_8:27
 for T being non empty TopSpace, p being Point of T
  holds p is_dense_point_of Cl{p};

theorem :: YELLOW_8:28
 for T being non empty TopSpace, p being Point of T
  holds p is_dense_point_of {p};

theorem :: YELLOW_8:29
 for T being non empty TopSpace,
     G,F being Subset of T st G is open & F is closed
 holds F \ G is closed;

theorem :: YELLOW_8:30
 for T being Hausdorff (non empty TopSpace),
     S being irreducible Subset of T
  holds S is trivial;

definition let T be Hausdorff (non empty TopSpace);
 cluster irreducible -> trivial Subset of T;
end;

theorem :: YELLOW_8:31
 for T being Hausdorff (non empty TopSpace) holds T is sober;

definition
 cluster Hausdorff -> sober (non empty TopSpace);
end;

definition
 cluster sober (non empty TopSpace);
end;

theorem :: YELLOW_8:32
 for T being non empty TopSpace holds
  T is T_0 iff for p,q being Point of T st Cl{p} = Cl{q} holds p = q;

theorem :: YELLOW_8:33
 for T being sober (non empty TopSpace) holds T is T_0;

definition
 cluster sober -> T_0 (non empty TopSpace);
end;

definition let X be set;
 func CofinTop X -> strict TopStruct means
:: YELLOW_8:def 7
 the carrier of it = X &
     COMPLEMENT the topology of it = {X} \/ Fin X;
end;

definition let X be non empty set;
 cluster CofinTop X -> non empty;
end;

definition let X be set;
 cluster CofinTop X -> TopSpace-like;
end;

theorem :: YELLOW_8:34
 for X being non empty set, P being Subset of CofinTop X
  holds P is closed iff P = X or P is finite;

theorem :: YELLOW_8:35
 for T being non empty TopSpace st T is_T1
 for p being Point of T holds Cl{p} = {p};

definition let X be non empty set;
 cluster CofinTop X -> being_T1;
end;

definition let X be infinite set;
 cluster CofinTop X -> non sober;
end;

definition
 cluster being_T1 non sober (non empty TopSpace);
end;

begin :: More on regular spaces

theorem :: YELLOW_8:36
 for T being non empty TopSpace holds T is_T3 iff
  for p being Point of T, P being Subset of T st p in Int P
 ex Q being Subset of T st Q is closed & Q c= P & p in Int Q;

theorem :: YELLOW_8:37
   for T being non empty TopSpace st T is_T3 holds
  T is locally-compact iff
   for x being Point of T
    ex Y being Subset of T st x in Int Y & Y is compact;