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