:: On the Characterization of {H}ausdorff Spaces
:: by Artur Korni{\l}owicz
::
:: Received April 18, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

registration
let X be empty set ;
cluster union X ->  empty ;
coherence
 union X is empty by ZFMISC_1:2;
end;

Lm1: now__::_thesis:_for_S,_T,_x1,_x2_being_set_st_x1_in_S_&_x2_in_T_holds_
<:(pr2_(S,T)),(pr1_(S,T)):>_._(x1,x2)_=_[x2,x1]
let S, T, x1, x2 be set ; ::_thesis: ( x1 in S &amp; x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1] )
assume A1: ( x1 in S &amp; x2 in T ) ; ::_thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1]
A2: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def_7
.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def_4
.= [:S,T:] /\ [:S,T:] by FUNCT_3:def_5
.= [:S,T:] ;
 [x1,x2] in [:S,T:] by A1, ZFMISC_1:87;
hence <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A2, FUNCT_3:def_7
.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, FUNCT_3:def_5
.= [x2,x1] by A1, FUNCT_3:def_4 ;
::_thesis: verum
end;

theorem :: YELLOW12:1
for X, A being set holds (delta X) .: A c= [:A,A:]
proofend;

theorem Th2: :: YELLOW12:2
for X, A being set holds (delta X) " [:A,A:] c= A
proofend;

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

theorem Th4: :: YELLOW12:4
for X, Y being set holds
( dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] &amp; rng <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:Y,X:] )
proofend;

theorem Th5: :: YELLOW12:5
for X, Y, A, B being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] c= [:B,A:]
proofend;

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

theorem Th7: :: YELLOW12:7
for X, Y being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> is one-to-one
proofend;

registration
let X, Y be set ;
cluster<:(pr2 (X,Y)),(pr1 (X,Y)):> ->  one-to-one ;
coherence
 <:(pr2 (X,Y)),(pr1 (X,Y)):> is one-to-one by Th7;
end;

theorem Th8: :: YELLOW12:8
for X, Y being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> " = <:(pr2 (Y,X)),(pr1 (Y,X)):>
proofend;

begin

theorem Th9: :: YELLOW12:9
for L1 being Semilattice
for L2 being non empty RelStr
for x, y being Element of L1
for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) &amp; x = x1 &amp; y = y1 holds
x "/\" y = x1 "/\" y1
proofend;

theorem Th10: :: YELLOW12:10
for L1 being sup-Semilattice
for L2 being non empty RelStr
for x, y being Element of L1
for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) &amp; x = x1 &amp; y = y1 holds
x "\/" y = x1 "\/" y1
proofend;

theorem Th11: :: YELLOW12:11
for L1 being Semilattice
for L2 being non empty RelStr
for X, Y being Subset of L1
for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) &amp; X = X1 &amp; Y = Y1 holds
X "/\" Y = X1 "/\" Y1
proofend;

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

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

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

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

theorem :: YELLOW12:16
for L1, L2 being RelStr
for A being Subset of L1
for J being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) &amp; A = J holds
subrelstr A = subrelstr J
proofend;

theorem :: YELLOW12:17
for L1, L2 being non empty RelStr
for A being SubRelStr of L1
for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) &amp; RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) &amp; A is meet-inheriting holds
J is meet-inheriting
proofend;

theorem :: YELLOW12:18
for L1, L2 being non empty RelStr
for A being SubRelStr of L1
for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) &amp; RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) &amp; A is join-inheriting holds
J is join-inheriting
proofend;

theorem :: YELLOW12:19
for L1 being non empty reflexive antisymmetric up-complete RelStr
for L2 being non empty reflexive RelStr
for X being Subset of L1
for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) &amp; X = Y &amp; X is property(S) holds
Y is property(S)
proofend;

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

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

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

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

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

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

registration
let R be complete Semilattice;
cluster inf_op R ->  infs-preserving ;
coherence
 inf_op R is infs-preserving
proofend;
end;

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

registration
let R be complete sup-Semilattice;
cluster sup_op R ->  sups-preserving ;
coherence
 sup_op R is sups-preserving
proofend;
end;

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

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

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

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

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

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

begin

theorem Th32: :: YELLOW12:32
for S, T being TopStruct
for B being Basis of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is Basis of T
proofend;

theorem Th33: :: YELLOW12:33
for S, T being TopStruct
for B being prebasis of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is prebasis of T
proofend;

theorem Th34: :: YELLOW12:34
for T being non empty TopSpace
for J being Basis of T holds not J is empty
proofend;

registration
let T be non empty TopSpace;
cluster open quasi_basis  ->  non empty for Element of bool (bool the carrier of T);
coherence
 for b1 being Basis of T holds not b1 is empty by Th34;
end;

theorem Th35: :: YELLOW12:35
for T being non empty TopSpace
for x being Point of T
for J being Basis of x holds not J is empty
proofend;

registration
let T be non empty TopSpace;
let x be Point of T;
cluster open V225(T,x)  ->  non empty for Element of bool (bool the carrier of T);
coherence
 for b1 being Basis of x holds not b1 is empty by Th35;
end;

theorem :: YELLOW12:36
for S1, T1, S2, T2 being TopSpace
for f being Function of S1,S2
for g being Function of T1,T2 st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of T1, the topology of T1 #) &amp; TopStruct(# the carrier of S2, the topology of S2 #) = TopStruct(# the carrier of T2, the topology of T2 #) &amp; f = g &amp; f is continuous holds
g is continuous
proofend;

theorem Th37: :: YELLOW12:37
for T being non empty TopSpace holds 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  }
proofend;

theorem Th38: :: YELLOW12:38
for T being non empty TopSpace holds delta the carrier of T is continuous Function of T,[:T,T:]
proofend;

theorem Th39: :: YELLOW12:39
for S, T being non empty TopSpace holds pr1 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],S
proofend;

theorem Th40: :: YELLOW12:40
for S, T being non empty TopSpace holds pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T
proofend;

theorem Th41: :: YELLOW12:41
for T, S, R being non empty TopSpace
for f being continuous Function of T,S
for g being continuous Function of T,R holds <:f,g:> is continuous Function of T,[:S,R:]
proofend;

theorem Th42: :: YELLOW12:42
for S, T being non empty TopSpace holds <:(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:]
proofend;

theorem Th43: :: YELLOW12:43
for S, T being non empty TopSpace
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
proofend;

theorem :: YELLOW12:44
for S, T being non empty TopSpace holds [:S,T:],[:T,S:] are_homeomorphic
proofend;

theorem Th45: :: YELLOW12:45
for S being non empty TopSpace
for T being non empty Hausdorff 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 ) &amp; ( for X being Subset of S st X =  {  p where p is Point of S : f . p = g . p  }  holds
X is closed ) )
proofend;

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

registration
let S, T be TopStruct ;
cluster strict TopSpace-like for Refinement of S,T;
existence
 ex b1 being Refinement of S,T st b1 is strict
proofend;
end;

registration
let S be non empty TopStruct ;
let T be TopStruct ;
cluster non empty strict TopSpace-like for Refinement of S,T;
existence
 ex b1 being Refinement of S,T st
( b1 is strict &amp; not b1 is empty )
proofend;
cluster non empty strict TopSpace-like for Refinement of T,S;
existence
 ex b1 being Refinement of T,S st
( b1 is strict &amp; not b1 is empty )
proofend;
end;

theorem :: YELLOW12:47
for R, S, T being TopStruct holds
( R is Refinement of S,T iff TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T )
proofend;

theorem Th48: :: YELLOW12:48
for S1, S2, T1, T2 being non empty TopSpace
for R being Refinement of [:S1,T1:],[:S2,T2:] st the carrier of S1 = the carrier of S2 &amp; the carrier of T1 = the carrier of T2 holds
{  ([: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 &amp; U2 is open &amp; V1 is open &amp; V2 is open )  }  is Basis of R
proofend;

theorem Th49: :: YELLOW12:49
for S1, S2, T1, T2 being non empty TopSpace
for R being Refinement of [:S1,T1:],[:S2,T2:]
for R1 being Refinement of S1,S2
for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 &amp; the carrier of T1 = the carrier of T2 holds
( the carrier of [:R1,R2:] = the carrier of R &amp; the topology of [:R1,R2:] = the topology of R )
proofend;

theorem :: YELLOW12:50
for S1, S2, T1, T2 being non empty TopSpace
for R1 being Refinement of S1,S2
for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 &amp; the carrier of T1 = the carrier of T2 holds
[:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:]
proofend;