The abstract of the Mizar article:

On the Characterization of Hausdorff Spaces

by

Artur Kornilowicz

Received April 18, 1998

MML identifier: YELLOW12

[ Mizar article, MML identifier index ]

environ

 vocabulary TARSKI, RELAT_1, PARTFUN1, FUNCT_3, BOOLE, FUNCT_1, WAYBEL_0,
      ORDERS_1, LATTICES, YELLOW_0, LATTICE3, ORDINAL2, RELAT_2, WAYBEL_3,
      WAYBEL_2, QUANTAL1, WELLORD1, WAYBEL11, BHSP_3, SETFAM_1, PRE_TOPC,
      CANTOR_1, SUBSET_1, CONNSP_2, TOPS_1, TOPS_2, T_0TOPSP, YELLOW_6,
      YELLOW_9, RLVECT_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, RELAT_1,
      FUNCT_1, RELSET_1, PARTFUN1, MCART_1, FUNCT_3, PRE_TOPC, TOPS_1, TOPS_2,
      CANTOR_1, CONNSP_2, BORSUK_1, T_0TOPSP, WELLORD1, ORDERS_1, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_6,
      YELLOW_8, WAYBEL11, YELLOW_9;
 constructors TOPS_1, TOPS_2, T_0TOPSP, BORSUK_2, CANTOR_1, YELLOW_4, WAYBEL_1,
      WAYBEL_3, WAYBEL11, TOLER_1, ORDERS_3, YELLOW_8, YELLOW_9, XCMPLX_0,
      MEMBERED;
 clusters STRUCT_0, PRE_TOPC, BORSUK_1, RELSET_1, LATTICE3, YELLOW_0, WAYBEL_0,
      YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_9, SUBSET_1, XREAL_0,
      MEMBERED, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin  :: The properties of some functions

 reserve A, B, X, Y for set;

definition let X be empty set;
 cluster union X -> empty;
end;

theorem :: YELLOW12:1
  (delta X).:A c= [:A,A:];

theorem :: YELLOW12:2
(delta X)"[:A,A:] c= A;

theorem :: YELLOW12:3
  for A being Subset of X holds (delta X)"[:A,A:] = A;

theorem :: YELLOW12:4
dom <:pr2(X,Y),pr1(X,Y):> = [:X,Y:] & rng <:pr2(X,Y),pr1(X,Y):> = [:Y,X:];

theorem :: YELLOW12:5
<:pr2(X,Y),pr1(X,Y):>.:[:A,B:] c= [:B,A:];

theorem :: YELLOW12:6
  for A being Subset of X, B being Subset of Y holds
 <:pr2(X,Y),pr1(X,Y):>.:[:A,B:] = [:B,A:];

theorem :: YELLOW12:7
<:pr2(X,Y),pr1(X,Y):> is one-to-one;

definition let X, Y be set;
 cluster <:pr2(X,Y),pr1(X,Y):> -> one-to-one;
end;

theorem :: YELLOW12:8
<:pr2(X,Y),pr1(X,Y):>" = <:pr2(Y,X),pr1(Y,X):>;


begin  :: The properties of the relational structures

theorem :: YELLOW12:9
for L1 being Semilattice, L2 being non empty RelStr
 for x, y being Element of L1, x1, y1 being Element of L2
  st the RelStr of L1 = the RelStr of L2 & x = x1 & y = y1
 holds x "/\" y = x1 "/\" y1;

theorem :: YELLOW12:10
for L1 being sup-Semilattice, L2 being non empty RelStr
 for x, y being Element of L1, x1, y1 being Element of L2
  st the RelStr of L1 = the RelStr of L2 & x = x1 & y = y1
 holds x "\/" y = x1 "\/" y1;

theorem :: YELLOW12:11
for L1 being Semilattice, L2 being non empty RelStr
 for X, Y being Subset of L1, X1, Y1 being Subset of L2
  st the RelStr of L1 = the RelStr of L2 & X = X1 & Y = Y1
 holds X "/\" Y = X1 "/\" Y1;

theorem :: YELLOW12:12
  for L1 being sup-Semilattice, L2 being non empty RelStr
 for X, Y being Subset of L1, X1, Y1 being Subset of L2
  st the RelStr of L1 = the RelStr of L2 & X = X1 & Y = Y1
 holds X "\/" Y = X1 "\/" Y1;

theorem :: YELLOW12:13
for L1 being antisymmetric up-complete (non empty reflexive RelStr),
    L2 being non empty reflexive RelStr,
    x being Element of L1, y being Element of L2
  st the RelStr of L1 = the RelStr of L2 & x = y
 holds waybelow x = waybelow y & wayabove x = wayabove y;

theorem :: YELLOW12:14
  for L1 being meet-continuous Semilattice, L2 being non empty reflexive RelStr
 st the RelStr of L1 = the RelStr of L2 holds L2 is meet-continuous;

theorem :: YELLOW12:15
  for L1 being continuous antisymmetric (non empty reflexive RelStr),
    L2 being non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2
  holds L2 is continuous;

theorem :: YELLOW12:16
  for L1, L2 being RelStr, A being Subset of L1, J being Subset of L2
  st the RelStr of L1 = the RelStr of L2 & A = J holds
 subrelstr A = subrelstr J;

theorem :: YELLOW12:17
  for L1, L2 being non empty RelStr,
    A being SubRelStr of L1, J being SubRelStr of L2
 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the RelStr of J &
    A is meet-inheriting holds
 J is meet-inheriting;

theorem :: YELLOW12:18
  for L1, L2 being non empty RelStr,
    A being SubRelStr of L1, J being SubRelStr of L2
 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the RelStr of J &
    A is join-inheriting holds
 J is join-inheriting;

theorem :: YELLOW12:19
  for L1 being up-complete antisymmetric (non empty reflexive RelStr),
    L2 being non empty reflexive RelStr,
    X being Subset of L1, Y being Subset of L2
  st the RelStr of L1 = the RelStr of L2 & X = Y & X has_the_property_(S)
 holds Y has_the_property_(S);

theorem :: YELLOW12:20
  for L1 being up-complete antisymmetric (non empty reflexive RelStr),
    L2 being non empty reflexive RelStr,
    X being Subset of L1, Y being Subset of L2
  st the RelStr of L1 = the RelStr of L2 & X = Y & X is directly_closed
 holds Y is directly_closed;

theorem :: YELLOW12:21
  for N being antisymmetric with_infima RelStr, D, E being Subset of N
 for X being upper Subset of N st D misses X holds D "/\" E misses X;

theorem :: YELLOW12:22
  for R being reflexive non empty RelStr holds
 id the carrier of R c= (the InternalRel of R) /\ the InternalRel of (R~);

theorem :: YELLOW12:23
  for R being antisymmetric RelStr holds
 (the InternalRel of R) /\ the InternalRel of (R~) c= id the carrier of R;

theorem :: YELLOW12:24
for R being upper-bounded Semilattice, X being Subset of [:R,R:] st
 ex_inf_of (inf_op R).:X,R holds inf_op R preserves_inf_of X;

definition let R be complete Semilattice;
 cluster inf_op R -> infs-preserving;
end;

theorem :: YELLOW12:25
for R being lower-bounded sup-Semilattice, X being Subset of [:R,R:] st
 ex_sup_of (sup_op R).:X,R holds sup_op R preserves_sup_of X;

definition let R be complete sup-Semilattice;
 cluster sup_op R -> sups-preserving;
end;

theorem :: YELLOW12:26
  for N being Semilattice, A being Subset of N st
 subrelstr A is meet-inheriting holds A is filtered;

theorem :: YELLOW12:27
  for N being sup-Semilattice, A being Subset of N st
 subrelstr A is join-inheriting holds A is directed;

theorem :: YELLOW12:28
  for N being transitive RelStr, A, J being Subset of N
 st A is_coarser_than uparrow J holds uparrow A c= uparrow J;

theorem :: YELLOW12:29
  for N being transitive RelStr, A, J being Subset of N
 st A is_finer_than downarrow J holds downarrow A c= downarrow J;

theorem :: YELLOW12:30
  for N being non empty reflexive RelStr
 for x being Element of N, X being Subset of N st x in X holds
  uparrow x c= uparrow X;

theorem :: YELLOW12:31
  for N being non empty reflexive RelStr
 for x being Element of N, X being Subset of N st x in X holds
  downarrow x c= downarrow X;


begin  :: On the Hausdorff Spaces

 reserve R, S, T for non empty TopSpace;

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

definition let T be TopSpace;
 cluster the TopStruct of T -> TopSpace-like;
end;

theorem :: YELLOW12:32
for S, T being TopStruct, B being Basis of S st
 the TopStruct of S = the TopStruct of T holds B is Basis of T;

theorem :: YELLOW12:33
for S, T being TopStruct, B being prebasis of S st
 the TopStruct of S = the TopStruct of T holds B is prebasis of T;

theorem :: YELLOW12:34
for J being Basis of T holds J is non empty;

definition let T be non empty TopSpace;
 cluster -> non empty Basis of T;
end;

theorem :: YELLOW12:35
for x being Point of T, J being Basis of x holds J is non empty;

definition let T be non empty TopSpace,
               x be Point of T;
 cluster -> non empty Basis of x;
end;

theorem :: YELLOW12:36
  for S1, T1, S2, T2 being non empty TopSpace,
    f being map of S1, S2, g being map of T1, T2 st
  the TopStruct of S1 = the TopStruct of T1 &
  the TopStruct of S2 = the TopStruct of T2 & f = g & f is continuous holds
 g is continuous;

theorem :: YELLOW12:37
id the carrier of T =
  {p where p is Point of [:T,T:]: pr1(the carrier of T,the carrier of T).p
                                = pr2(the carrier of T,the carrier of T).p};

theorem :: YELLOW12:38
delta the carrier of T is continuous map of T, [:T,T:];

theorem :: YELLOW12:39
pr1(the carrier of S,the carrier of T) is continuous map of [:S,T:], S;

theorem :: YELLOW12:40
pr2(the carrier of S,the carrier of T) is continuous map of [:S,T:], T;

theorem :: YELLOW12:41
for f being continuous map of T, S,
    g being continuous map of T, R holds
 <:f,g:> is continuous map of T, [:S,R:];

theorem :: YELLOW12:42
<:pr2(the carrier of S,the carrier of T),
 pr1(the carrier of S,the carrier of T):> is continuous map of [:S,T:],[:T,S:];

theorem :: YELLOW12:43
for f being map of [:S,T:], [:T,S:]
 st f = <:pr2(the carrier of S,the carrier of T),
          pr1(the carrier of S,the carrier of T):> holds
 f is_homeomorphism;

theorem :: YELLOW12:44
  [:S,T:], [:T,S:] are_homeomorphic;

theorem :: YELLOW12:45
for T being Hausdorff (non empty TopSpace)
 for f, g being continuous map of S, T holds
  (for X being Subset of S st X = {p where p is Point of S: f.p <> g.p}
       holds X is open) &
  for X being Subset of S st X = {p where p is Point of S: f.p = g.p}
       holds X is closed;

theorem :: YELLOW12:46
  T is Hausdorff iff
 for A being Subset of [:T,T:] st A = id the carrier of T
  holds A is closed;

definition let S, T be TopStruct;
 cluster strict Refinement of S, T;
end;

definition let S be non empty TopStruct, T be TopStruct;
 cluster strict non empty Refinement of S, T;
 cluster strict non empty Refinement of T, S;
end;

theorem :: YELLOW12:47
  for R, S, T being TopStruct holds
 R is Refinement of S, T iff the TopStruct of R is Refinement of S, T;

reserve S1, S2, T1, T2 for non empty TopSpace,
        R for Refinement of [:S1,T1:], [:S2,T2:],
        R1 for Refinement of S1, S2,
        R2 for Refinement of T1, T2;

theorem :: YELLOW12:48
the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2
 implies
 { [:U1,V1:] /\ [:U2,V2:] where U1 is Subset of S1,
                               U2 is Subset of S2,
                               V1 is Subset of T1,
                               V2 is Subset of T2 :
       U1 is open & U2 is open & V1 is open & V2 is open } is Basis of R;

theorem :: YELLOW12:49
the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2
  implies
 the carrier of [:R1,R2:] = the carrier of R &
 the topology of [:R1,R2:] = the topology of R;

theorem :: YELLOW12:50
  the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2
 implies [:R1,R2:] is Refinement of [:S1,T1:], [:S2,T2:];