:: On the Characterization of {H}ausdorff Spaces
::  by Artur Korni{\l}owicz
::
:: Received April 18, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, TARSKI, RELAT_1, PARTFUN1, MCART_1, ZFMISC_1, FUNCT_1,
      FUNCT_3, SUBSET_1, WAYBEL_0, ORDERS_2, LATTICES, LATTICE3, YELLOW_0,
      ORDINAL2, EQREL_1, RELAT_2, WAYBEL_3, WAYBEL_2, STRUCT_0, WELLORD1,
      WAYBEL11, XXREAL_0, REWRITE1, SETFAM_1, PRE_TOPC, RLVECT_3, CANTOR_1,
      RCOMP_1, CONNSP_2, TOPS_1, TOPS_2, T_0TOPSP, COMPTS_1, YELLOW_9, FUNCT_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, MCART_1, FUNCT_3, DOMAIN_1,
      STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CANTOR_1, CONNSP_2,
      BORSUK_1, BORSUK_2, T_0TOPSP, WELLORD1, ORDERS_2, LATTICE3, YELLOW_0,
      WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_8, WAYBEL11,
      YELLOW_9;
 constructors SETFAM_1, TOLER_1, TOPS_1, TOPS_2, T_0TOPSP, CANTOR_1, BORSUK_2,
      ORDERS_3, YELLOW_4, WAYBEL_3, YELLOW_8, WAYBEL11, YELLOW_9, CONNSP_2,
      DOMAIN_1, COMPTS_1, WAYBEL_2;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, BORSUK_1, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_9,
      PRE_TOPC, TOPS_1, BORSUK_2, FUNCT_2;
 requirements SUBSET, BOOLE;


begin  :: The properties of some functions

reserve A, B, X, Y for set;

registration
  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;

registration
  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 is property(S) holds Y is
  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;

definition
  let L be non empty RelStr;
  let f be Function of [:L,L:], L;
  let a,b be Element of L;
  redefine func f.(a,b) -> Element of L;
end;

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;

registration
  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;

registration
  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;

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;

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

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

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

theorem :: YELLOW12:36
  for S1, T1, S2, T2 being TopSpace, f being Function of S1, S2, g being
Function 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 Function of T, [:T,T:];

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

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

theorem :: YELLOW12:41
  for f being continuous Function of T, S, g being continuous
  Function of T, R holds <:f,g:> is continuous Function 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 Function of [:S,T:],[:T,S:];

theorem :: YELLOW12:43
  for f being Function 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 being_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 Function 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;

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

registration
  let S be non empty TopStruct, T be TopStruct;
  cluster strict non empty for Refinement of S, T;
  cluster strict non empty for 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:];