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


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 & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1] )
assume A1: ( x1 in S & 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 A, X being set holds (delta X) .: A c= [:A,A:]
proof end;

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

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

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

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

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:]
proof end;

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

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)):>
proof end;

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 #) & x = x1 & y = y1 holds
x "/\" y = x1 "/\" y1
proof end;

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 #) & x = x1 & y = y1 holds
x "\/" y = x1 "\/" y1
proof end;

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 #) & X = X1 & Y = Y1 holds
X "/\" Y = X1 "/\" Y1
proof end;

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 #) & X = X1 & Y = Y1 holds
X "\/" Y = X1 "\/" Y1
proof end;

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 #) & x = y holds
( waybelow x = waybelow y & wayabove x = wayabove y )
proof end;

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
proof end;

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
proof end;

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 #) & A = J holds
subrelstr A = subrelstr J
proof end;

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 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is meet-inheriting holds
J is meet-inheriting
proof end;

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 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting holds
J is join-inheriting
proof end;

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 #) & X = Y & X is property(S) holds
Y is property(S)
proof end;

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 #) & X = Y & X is directly_closed holds
Y is directly_closed
proof end;

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
proof end;

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 ~)
proof end;

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

definition
let L be non empty RelStr ;
let f be Function of [:L,L:],L;
let a, b be Element of L;
:: original: .
redefine func f . (a,b) -> Element of L;
coherence
f . (a,b) is Element of L
proof end;
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
proof end;

registration
let R be complete Semilattice;
cluster inf_op R -> infs-preserving ;
coherence
inf_op R is infs-preserving
proof end;
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
proof end;

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

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

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

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

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
proof end;

registration
let T be non empty TopSpace;
let x be Point of T;
cluster open V228(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 #) & TopStruct(# the carrier of S2, the topology of S2 #) = TopStruct(# the carrier of T2, the topology of T2 #) & f = g & f is continuous holds
g is continuous
proof end;

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 }
proof end;

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

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
proof end;

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
proof end;

theorem Th41: :: YELLOW12:41
for R, S, T 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:]
proof end;

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:]
proof end;

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
proof end;

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

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 ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds
X is closed ) )
proof end;

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 )
proof end;

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
proof end;
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 & not b1 is empty )
proof end;
cluster non empty strict TopSpace-like for Refinement of T,S;
existence
ex b1 being Refinement of T,S st
( b1 is strict & not b1 is empty )
proof end;
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 )
proof end;

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 & 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 & U2 is open & V1 is open & V2 is open ) } is Basis of R
proof end;

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 & the carrier of T1 = the carrier of T2 holds
( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R )
proof end;

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 & the carrier of T1 = the carrier of T2 holds
[:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:]
proof end;