:: On the Characterization of {H}ausdorff Spaces
:: by Artur Korni{\l}owicz
::
:: Received April 18, 1998
:: Copyright (c) 1998-2011 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

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 8
.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def 5
.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 6
.= [:S,T:] ;
[x1,x2] in [:S,T:] by A1, ZFMISC_1:106;
hence <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A2, FUNCT_3:def 8
.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, FUNCT_3:def 6
.= [x2,x1] by A1, FUNCT_3:def 5 ;
:: thesis: verum

end;

theorem :: YELLOW12:1

for X, A being set holds (delta X) .: A c= [:A,A:]

proof end;

theorem Th2: :: YELLOW12:2

for X, A 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 X, Y, A, B 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;

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 #) & 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 closed_under_directed_sups holds
Y is closed_under_directed_sups

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;

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

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 Element of bool (bool the carrier of T);
coherence
for b₁ being Basis of T holds not b₁ 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 V212(T,x) -> non empty Element of bool (bool the carrier of T);
coherence
for b₁ being Basis of x holds not b₁ 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 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:]

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 T_2 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 Refinement of S,T;
existence
ex b₁ being Refinement of S,T st b₁ is strict

proof end;

end;

registration

let S be non empty TopStruct ;
let T be TopStruct ;
cluster non empty strict TopSpace-like Refinement of S,T;
existence
ex b₁ being Refinement of S,T st
( b₁ is strict & not b₁ is empty )

proof end;

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