:: On the Characterization of {H}ausdorff Spaces
:: by Artur Korni{\l}owicz
::
:: Received April 18, 1998
:: Copyright (c) 1998-2016 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;
definitions TARSKI, FUNCT_1, PRE_TOPC, TOPS_2, BORSUK_1, T_0TOPSP, LATTICE3,
YELLOW_0, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL11, XBOOLE_0;
equalities LATTICE3, WAYBEL_3, SUBSET_1, BINOP_1, STRUCT_0;
expansions TARSKI, FUNCT_1, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0;
theorems FUNCT_1, FUNCT_2, FUNCT_3, RELAT_1, TOPS_1, TOPS_2, TOPS_3, PRE_TOPC,
CONNSP_2, BORSUK_1, ZFMISC_1, TARSKI, ORDERS_2, YELLOW_0, YELLOW_2,
YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_7, YELLOW_8,
YELLOW_9, WAYBEL_8, WAYBEL_3, TEX_2, SETFAM_1, CANTOR_1, XBOOLE_0,
XBOOLE_1, EQREL_1, XTUPLE_0;
begin :: The properties of some functions
reserve A, B, X, Y for set;
registration
let X be empty set;
cluster union X -> empty;
coherence by ZFMISC_1:2;
end;
Lm1: now
let S, T, x1, x2 be set such that
A1: x1 in S & x2 in T;
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;
end;
theorem
(delta X).:A c= [:A,A:]
proof
set f = delta X;
let y be object;
assume y in f.:A;
then consider x being object such that
A1: x in dom f and
A2: x in A and
A3: y = f.x by FUNCT_1:def 6;
y = [x,x] by A1,A3,FUNCT_3:def 6;
hence thesis by A2,ZFMISC_1:def 2;
end;
theorem Th2:
(delta X)"[:A,A:] c= A
proof
set f = delta X;
let x be object;
assume x in f"[:A,A:];
then f.x in [:A,A:] & f.x = [x,x] by FUNCT_1:def 7,FUNCT_3:def 6;
hence thesis by ZFMISC_1:87;
end;
theorem
for A being Subset of X holds (delta X)"[:A,A:] = A
proof
let A be Subset of X;
set f = delta X;
thus f"[:A,A:] c= A by Th2;
let x be object;
assume
A1: x in A;
then f.x = [x,x] by FUNCT_3:def 6;
then dom f = X & f.x in [:A,A:] by A1,FUNCT_3:def 6,ZFMISC_1:87;
hence thesis by A1,FUNCT_1:def 7;
end;
theorem Th4:
dom <:pr2(X,Y),pr1(X,Y):> = [:X,Y:] & rng <:pr2(X,Y),pr1(X,Y):> = [:Y,X:]
proof
set f = <:pr2(X,Y),pr1(X,Y):>;
thus
A1: dom f = dom pr2(X,Y) /\ dom pr1(X,Y) by FUNCT_3:def 7
.= dom pr2(X,Y) /\ [:X,Y:] by FUNCT_3:def 4
.= [:X,Y:] /\ [:X,Y:] by FUNCT_3:def 5
.= [:X,Y:];
rng f c= [:rng pr2(X,Y),rng pr1(X,Y):] by FUNCT_3:51;
hence rng f c= [:Y,X:] by XBOOLE_1:1;
let y be object;
assume y in [:Y,X:];
then consider y1, y2 being object such that
A2: y1 in Y & y2 in X and
A3: y = [y1,y2] by ZFMISC_1:def 2;
A4: [y2,y1] in dom f by A1,A2,ZFMISC_1:87;
f.(y2,y1) = y by A2,A3,Lm1;
hence thesis by A4,FUNCT_1:def 3;
end;
theorem Th5:
<:pr2(X,Y),pr1(X,Y):>.:[:A,B:] c= [:B,A:]
proof
set f = <:pr2(X,Y),pr1(X,Y):>;
let y be object;
assume y in f.:[:A,B:];
then consider x being object such that
A1: x in dom f and
A2: x in [:A,B:] and
A3: y = f.x by FUNCT_1:def 6;
consider x1, x2 being object such that
A4: x1 in A & x2 in B and
A5: x = [x1,x2] by A2,ZFMISC_1:def 2;
dom f = [:X,Y:] by Th4;
then x1 in X & x2 in Y by A1,A5,ZFMISC_1:87;
then f.(x1,x2) = [x2,x1] by Lm1;
hence thesis by A3,A4,A5,ZFMISC_1:87;
end;
theorem
for A being Subset of X, B being Subset of Y holds <:pr2(X,Y),pr1(X,Y)
:>.:[:A,B:] = [:B,A:]
proof
let A be Subset of X, B be Subset of Y;
set f = <:pr2(X,Y),pr1(X,Y):>;
A1: dom f = [:X,Y:] by Th4;
thus f.:[:A,B:] c= [:B,A:] by Th5;
let y be object;
assume y in [:B,A:];
then consider y1, y2 being object such that
A2: y1 in B & y2 in A and
A3: y = [y1,y2] by ZFMISC_1:def 2;
[y2,y1] in [:A,B:] & f.(y2,y1) = [y1,y2] by A2,Lm1,ZFMISC_1:87;
hence thesis by A1,A3,FUNCT_1:def 6;
end;
theorem Th7:
<:pr2(X,Y),pr1(X,Y):> is one-to-one
proof
set f = <:pr2(X,Y),pr1(X,Y):>;
let x, y be object such that
A1: x in dom f and
A2: y in dom f and
A3: f.x = f.y;
A4: dom f = [:X,Y:] by Th4;
then consider x1, x2 being object such that
A5: x1 in X & x2 in Y and
A6: x = [x1,x2] by A1,ZFMISC_1:def 2;
consider y1, y2 being object such that
A7: y1 in X & y2 in Y and
A8: y = [y1,y2] by A4,A2,ZFMISC_1:def 2;
A9: f.(y1,y2) = [y2,y1] by A7,Lm1;
A10: f.(x1,x2) = [x2,x1] by A5,Lm1;
then x1 = y1 by A3,A6,A8,A9,XTUPLE_0:1;
hence thesis by A3,A6,A8,A10,A9,XTUPLE_0:1;
end;
registration
let X, Y be set;
cluster <:pr2(X,Y),pr1(X,Y):> -> one-to-one;
coherence by Th7;
end;
theorem Th8:
<:pr2(X,Y),pr1(X,Y):>" = <:pr2(Y,X),pr1(Y,X):>
proof
set f = <:pr2(X,Y),pr1(X,Y):>, g = <:pr2(Y,X),pr1(Y,X):>;
A1: dom (f") = rng f by FUNCT_1:32
.= [:Y,X:] by Th4;
A2: now
let x be object;
assume x in [:Y,X:];
then consider x1, x2 being object such that
A3: x1 in Y & x2 in X and
A4: x = [x1,x2] by ZFMISC_1:def 2;
A5: g.(x1,x2) = [x2,x1] & f.(x2,x1) = [x1,x2] by A3,Lm1;
dom f = [:X,Y:] by Th4;
then [x2,x1] in dom f by A3,ZFMISC_1:87;
hence f".x = g.x by A4,A5,FUNCT_1:32;
end;
dom g = [:Y,X:] by Th4;
hence thesis by A1,A2;
end;
begin :: The properties of the relational structures
theorem Th9:
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
proof
let L1 be Semilattice, L2 be non empty RelStr, x, y be Element of L1, x1, y1
be Element of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: x = x1 & y = y1;
A3: L2 is with_infima Poset by A1,WAYBEL_8:12,13,14,YELLOW_7:14;
A4: ex_inf_of {x,y}, L1 by YELLOW_0:21;
thus x "/\" y = inf{x,y} by YELLOW_0:40
.= inf{x1,y1} by A1,A2,A4,YELLOW_0:27
.= x1 "/\" y1 by A3,YELLOW_0:40;
end;
theorem Th10:
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
proof
let L1 be sup-Semilattice, L2 be non empty RelStr, x, y be Element of L1, x1
, y1 be Element of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: x = x1 & y = y1;
A3: L2 is with_suprema Poset by A1,WAYBEL_8:12,13,14,YELLOW_7:15;
A4: ex_sup_of {x,y}, L1 by YELLOW_0:20;
thus x "\/" y = sup{x,y} by YELLOW_0:41
.= sup{x1,y1} by A1,A2,A4,YELLOW_0:26
.= x1 "\/" y1 by A3,YELLOW_0:41;
end;
theorem Th11:
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
proof
let L1 be Semilattice, L2 be non empty RelStr, X, Y be Subset of L1, X1, Y1
be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = X1 & Y = Y1;
set XY = { x "/\" y where x, y is Element of L1 : x in X & y in Y }, XY1 = {
x "/\" y where x, y is Element of L2 : x in X1 & y in Y1 };
A3: XY = XY1
proof
hereby
let a be object;
assume a in XY;
then consider x, y being Element of L1 such that
A4: a = x "/\" y and
A5: x in X & y in Y;
reconsider x1 = x, y1 = y as Element of L2 by A1;
a = x1 "/\" y1 by A1,A4,Th9;
hence a in XY1 by A2,A5;
end;
let a be object;
assume a in XY1;
then consider x, y being Element of L2 such that
A6: a = x "/\" y and
A7: x in X1 & y in Y1;
reconsider x1 = x, y1 = y as Element of L1 by A1;
a = x1 "/\" y1 by A1,A6,Th9;
hence thesis by A2,A7;
end;
thus X "/\" Y = XY by YELLOW_4:def 4
.= X1 "/\" Y1 by A3,YELLOW_4:def 4;
end;
theorem
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
proof
let L1 be sup-Semilattice, L2 be non empty RelStr, X, Y be Subset of L1, X1,
Y1 be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = X1 & Y = Y1;
set XY = { x "\/" y where x, y is Element of L1 : x in X & y in Y }, XY1 = {
x "\/" y where x, y is Element of L2 : x in X1 & y in Y1 };
A3: XY = XY1
proof
hereby
let a be object;
assume a in XY;
then consider x, y being Element of L1 such that
A4: a = x "\/" y and
A5: x in X & y in Y;
reconsider x1 = x, y1 = y as Element of L2 by A1;
a = x1 "\/" y1 by A1,A4,Th10;
hence a in XY1 by A2,A5;
end;
let a be object;
assume a in XY1;
then consider x, y being Element of L2 such that
A6: a = x "\/" y and
A7: x in X1 & y in Y1;
reconsider x1 = x, y1 = y as Element of L1 by A1;
a = x1 "\/" y1 by A1,A6,Th10;
hence thesis by A2,A7;
end;
thus X "\/" Y = XY by YELLOW_4:def 3
.= X1 "\/" Y1 by A3,YELLOW_4:def 3;
end;
theorem Th13:
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
proof
let L1 be antisymmetric up-complete non empty reflexive RelStr, L2 be non
empty reflexive RelStr, x be Element of L1, y be Element of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: x = y;
hereby
hereby
let a be object;
assume a in waybelow x;
then consider z being Element of L1 such that
A3: a = z and
A4: z << x;
reconsider w = z as Element of L2 by A1;
L2 is antisymmetric by A1,WAYBEL_8:14;
then w << y by A1,A2,A4,WAYBEL_8:8;
hence a in waybelow y by A3;
end;
let a be object;
assume a in waybelow y;
then consider z being Element of L2 such that
A5: a = z and
A6: z << y;
reconsider w = z as Element of L1 by A1;
L2 is up-complete antisymmetric by A1,WAYBEL_8:14,15;
then w << x by A1,A2,A6,WAYBEL_8:8;
hence a in waybelow x by A5;
end;
hereby
let a be object;
assume a in wayabove x;
then consider z being Element of L1 such that
A7: a = z and
A8: z >> x;
reconsider w = z as Element of L2 by A1;
L2 is antisymmetric by A1,WAYBEL_8:14;
then w >> y by A1,A2,A8,WAYBEL_8:8;
hence a in wayabove y by A7;
end;
let a be object;
assume a in wayabove y;
then consider z being Element of L2 such that
A9: a = z and
A10: z >> y;
reconsider w = z as Element of L1 by A1;
L2 is up-complete antisymmetric by A1,WAYBEL_8:14,15;
then w >> x by A1,A2,A10,WAYBEL_8:8;
hence thesis by A9;
end;
theorem
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
proof
let L1 be meet-continuous Semilattice, L2 be non empty reflexive RelStr;
assume
A1: the RelStr of L1 = the RelStr of L2;
hence L2 is up-complete by WAYBEL_8:15;
let x be Element of L2, D be non empty directed Subset of L2;
reconsider E = D as non empty directed Subset of L1 by A1,WAYBEL_0:3;
reconsider y = x as Element of L1 by A1;
A2: {x} "/\" D = {y} "/\" E by A1,Th11;
reconsider yy = {y} as non empty directed Subset of L1 by WAYBEL_0:5;
A3: ex_sup_of yy "/\" E, L1 by WAYBEL_0:75;
ex_sup_of E, L1 by WAYBEL_0:75;
then sup D = sup E by A1,YELLOW_0:26;
hence x "/\" sup D = y "/\" sup E by A1,Th9
.= sup ({y} "/\" E) by WAYBEL_2:def 6
.= sup ({x} "/\" D) by A1,A2,A3,YELLOW_0:26;
end;
theorem
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
proof
let L1 be continuous antisymmetric non empty reflexive RelStr, L2 be non
empty reflexive RelStr such that
A1: the RelStr of L1 = the RelStr of L2;
hereby
let y be Element of L2;
reconsider x = y as Element of L1 by A1;
waybelow x = waybelow y by A1,Th13;
hence waybelow y is non empty directed by A1,WAYBEL_0:3;
end;
thus L2 is up-complete by A1,WAYBEL_8:15;
let y be Element of L2;
reconsider x = y as Element of L1 by A1;
A2: ex_sup_of waybelow x, L1 & x = sup waybelow x by WAYBEL_0:75,WAYBEL_3:def 5
;
waybelow x = waybelow y by A1,Th13;
hence thesis by A1,A2,YELLOW_0:26;
end;
theorem
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
proof
let L1, L2 be RelStr, A be Subset of L1, J be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: A = J;
A3: the carrier of subrelstr A = A by YELLOW_0:def 15
.= the carrier of subrelstr J by A2,YELLOW_0:def 15;
then
the InternalRel of subrelstr A = (the InternalRel of L2)|_2(the carrier
of subrelstr J) by A1,YELLOW_0:def 14
.= the InternalRel of subrelstr J by YELLOW_0:def 14;
hence thesis by A3;
end;
theorem
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
proof
let L1, L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2
such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: the RelStr of A = the RelStr of J and
A3: for x, y being Element of L1 st x in the carrier of A & y in the
carrier of A & ex_inf_of {x,y},L1 holds inf {x,y} in the carrier of A;
let x, y be Element of L2 such that
A4: x in the carrier of J & y in the carrier of J and
A5: ex_inf_of {x,y},L2;
reconsider x1 = x, y1 = y as Element of L1 by A1;
inf {x1,y1} in the carrier of A by A1,A2,A3,A4,A5,YELLOW_0:14;
hence thesis by A1,A2,A5,YELLOW_0:27;
end;
theorem
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
proof
let L1, L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2
such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: the RelStr of A = the RelStr of J and
A3: for x, y being Element of L1 st x in the carrier of A & y in the
carrier of A & ex_sup_of {x,y},L1 holds sup {x,y} in the carrier of A;
let x, y be Element of L2 such that
A4: x in the carrier of J & y in the carrier of J and
A5: ex_sup_of {x,y},L2;
reconsider x1 = x, y1 = y as Element of L1 by A1;
sup {x1,y1} in the carrier of A by A1,A2,A3,A4,A5,YELLOW_0:14;
hence thesis by A1,A2,A5,YELLOW_0:26;
end;
theorem
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)
proof
let L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non
empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = Y and
A3: for D being non empty directed Subset of L1 st sup D in X ex y being
Element of L1 st y in D & for x being Element of L1 st x in D & x >= y holds x
in X;
let E be non empty directed Subset of L2 such that
A4: sup E in Y;
reconsider D = E as non empty directed Subset of L1 by A1,WAYBEL_0:3;
ex_sup_of D, L1 by WAYBEL_0:75;
then sup D in X by A1,A2,A4,YELLOW_0:26;
then consider y being Element of L1 such that
A5: y in D and
A6: for x being Element of L1 st x in D & x >= y holds x in X by A3;
reconsider y2 = y as Element of L2 by A1;
take y2;
thus y2 in E by A5;
let x2 be Element of L2;
assume x2 in E & x2 >= y2;
hence thesis by A1,A2,A6,YELLOW_0:1;
end;
theorem
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
proof
let L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non
empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 such that
A1: the RelStr of L1 = the RelStr of L2 and
A2: X = Y and
A3: for D being non empty directed Subset of L1 st D c= X holds sup D in X;
let E be non empty directed Subset of L2 such that
A4: E c= Y;
reconsider D = E as non empty directed Subset of L1 by A1,WAYBEL_0:3;
ex_sup_of D, L1 & sup D in X by A2,A3,A4,WAYBEL_0:75;
hence thesis by A1,A2,YELLOW_0:26;
end;
theorem
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
proof
let N be antisymmetric with_infima RelStr, D, E be Subset of N, X be upper
Subset of N such that
A1: D /\ X = {};
assume (D "/\" E) /\ X <> {};
then consider k being object such that
A2: k in (D "/\" E) /\ X by XBOOLE_0:def 1;
reconsider k as Element of N by A2;
A3: D "/\" E = { d "/\" e where d, e is Element of N : d in D & e in E } & k
in D "/\" E by A2,XBOOLE_0:def 4,YELLOW_4:def 4;
A4: k in X by A2,XBOOLE_0:def 4;
consider d, e being Element of N such that
A5: k = d "/\" e and
A6: d in D and
e in E by A3;
d "/\" e <= d by YELLOW_0:23;
then d in X by A4,A5,WAYBEL_0:def 20;
hence thesis by A1,A6,XBOOLE_0:def 4;
end;
theorem
for R being reflexive non empty RelStr holds id the carrier of R c= (
the InternalRel of R) /\ the InternalRel of (R~)
proof
let R be reflexive non empty RelStr;
let a be object;
assume
A1: a in id the carrier of R;
then consider y, z being object such that
A2: a = [y,z] by RELAT_1:def 1;
reconsider y, z as Element of R by A1,A2,ZFMISC_1:87;
y <= z by A1,A2,RELAT_1:def 10;
then
A3: a in the InternalRel of R by A2,ORDERS_2:def 5;
y = z by A1,A2,RELAT_1:def 10;
then a in the InternalRel of R~ by A2,A3,RELAT_1:def 7;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem
for R being antisymmetric RelStr holds (the InternalRel of R) /\ the
InternalRel of (R~) c= id the carrier of R
proof
let R be antisymmetric RelStr;
let a be object;
assume
A1: a in (the InternalRel of R) /\ the InternalRel of R~;
then consider y, z being object such that
A2: a = [y,z] by RELAT_1:def 1;
A3: y in the carrier of R by A1,A2,ZFMISC_1:87;
reconsider y, z as Element of R by A1,A2,ZFMISC_1:87;
a in the InternalRel of R~ by A1,XBOOLE_0:def 4;
then [z,y] in the InternalRel of R by A2,RELAT_1:def 7;
then
A4: z <= y by ORDERS_2:def 5;
a in the InternalRel of R by A1,XBOOLE_0:def 4;
then y <= z by A2,ORDERS_2:def 5;
then y = z by A4,ORDERS_2:2;
hence thesis by A2,A3,RELAT_1:def 10;
end;
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;
coherence
proof
f.[a,b] is Element of L;
hence thesis;
end;
end;
theorem Th24:
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
proof
let R be upper-bounded Semilattice;
set f = inf_op R;
let X be Subset of [:R,R:] such that
A1: ex_inf_of f.:X,R and
A2: ex_inf_of X,[:R,R:];
thus ex_inf_of f.:X,R by A1;
A3: dom f = the carrier of [:R,R:] by FUNCT_2:def 1;
then
A4: dom f = [:the carrier of R,the carrier of R:] by YELLOW_3:def 2;
A5: for b being Element of R st b is_<=_than f.:X holds f.inf X >= b
proof
let b be Element of R such that
A6: b is_<=_than f.:X;
X is_>=_than [b,b]
proof
let c be Element of [:R,R:];
assume c in X;
then f.c in f.:X by A3,FUNCT_1:def 6;
then
A7: b <= f.c by A6;
consider s, t being object such that
A8: s in the carrier of R & t in the carrier of R and
A9: c = [s,t] by A3,A4,ZFMISC_1:def 2;
reconsider s, t as Element of R by A8;
A10: f.c = f.(s,t) by A9
.= s "/\" t by WAYBEL_2:def 4;
s "/\" t <= t by YELLOW_0:23;
then
A11: b <= t by A7,A10,ORDERS_2:3;
s "/\" t <= s by YELLOW_0:23;
then b <= s by A7,A10,ORDERS_2:3;
hence [b,b] <= c by A9,A11,YELLOW_3:11;
end;
then [b,b] <= inf X by A2,YELLOW_0:def 10;
then f.(b,b) <= f.inf X by WAYBEL_1:def 2;
then b "/\" b <= f.inf X by WAYBEL_2:def 4;
hence b <= f.inf X by YELLOW_0:25;
end;
inf X is_<=_than X by A2,YELLOW_0:def 10;
then f.inf X is_<=_than f.:X by YELLOW_2:13;
hence thesis by A1,A5,YELLOW_0:def 10;
end;
registration
let R be complete Semilattice;
cluster inf_op R -> infs-preserving;
coherence
proof
let X be Subset of [:R,R:] such that
A1: ex_inf_of X,[:R,R:];
thus ex_inf_of (inf_op R).:X,R by YELLOW_0:17;
then inf_op R preserves_inf_of X by Th24;
hence thesis by A1;
end;
end;
theorem Th25:
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
proof
let R be lower-bounded sup-Semilattice;
set f = sup_op R;
let X be Subset of [:R,R:] such that
A1: ex_sup_of f.:X,R and
A2: ex_sup_of X,[:R,R:];
thus ex_sup_of f.:X,R by A1;
A3: dom f = the carrier of [:R,R:] by FUNCT_2:def 1;
then
A4: dom f = [:the carrier of R,the carrier of R:] by YELLOW_3:def 2;
A5: for b being Element of R st b is_>=_than f.:X holds f.sup X <= b
proof
let b be Element of R such that
A6: b is_>=_than f.:X;
X is_<=_than [b,b]
proof
let c be Element of [:R,R:];
assume c in X;
then f.c in f.:X by A3,FUNCT_1:def 6;
then
A7: f.c <= b by A6;
consider s, t being object such that
A8: s in the carrier of R & t in the carrier of R and
A9: c = [s,t] by A3,A4,ZFMISC_1:def 2;
reconsider s, t as Element of R by A8;
A10: f.c = f.(s,t) by A9
.= s "\/" t by WAYBEL_2:def 5;
t <= s "\/" t by YELLOW_0:22;
then
A11: t <= b by A7,A10,ORDERS_2:3;
s <= s "\/" t by YELLOW_0:22;
then s <= b by A7,A10,ORDERS_2:3;
hence c <= [b,b] by A9,A11,YELLOW_3:11;
end;
then sup X <= [b,b] by A2,YELLOW_0:def 9;
then f.sup X <= f.(b,b) by WAYBEL_1:def 2;
then b <= b & f.sup X <= b "\/" b by WAYBEL_2:def 5;
hence thesis by YELLOW_0:24;
end;
X is_<=_than sup X by A2,YELLOW_0:def 9;
then f.:X is_<=_than f.sup X by YELLOW_2:14;
hence thesis by A1,A5,YELLOW_0:def 9;
end;
registration
let R be complete sup-Semilattice;
cluster sup_op R -> sups-preserving;
coherence
proof
let X be Subset of [:R,R:] such that
A1: ex_sup_of X,[:R,R:];
thus ex_sup_of (sup_op R).:X,R by YELLOW_0:17;
then sup_op R preserves_sup_of X by Th25;
hence thesis by A1;
end;
end;
theorem
for N being Semilattice, A being Subset of N st subrelstr A is
meet-inheriting holds A is filtered
proof
let N be Semilattice, A be Subset of N such that
A1: subrelstr A is meet-inheriting;
let x, y be Element of N such that
A2: x in A & y in A;
take x"/\"y;
A3: the carrier of subrelstr A = A by YELLOW_0:def 15;
ex_inf_of {x,y},N by YELLOW_0:21;
then inf {x,y} in the carrier of subrelstr A by A1,A2,A3;
hence x"/\"y in A by A3,YELLOW_0:40;
thus x"/\"y <= x & x"/\"y <= y by YELLOW_0:23;
end;
theorem
for N being sup-Semilattice, A being Subset of N st subrelstr A is
join-inheriting holds A is directed
proof
let N be sup-Semilattice, A be Subset of N such that
A1: subrelstr A is join-inheriting;
let x, y be Element of N such that
A2: x in A & y in A;
take x"\/"y;
A3: the carrier of subrelstr A = A by YELLOW_0:def 15;
ex_sup_of {x,y},N by YELLOW_0:20;
then sup {x,y} in the carrier of subrelstr A by A1,A2,A3;
hence x"\/"y in A by A3,YELLOW_0:41;
thus x <= x"\/"y & y <= x"\/"y by YELLOW_0:22;
end;
theorem
for N being transitive RelStr, A, J being Subset of N st A
is_coarser_than uparrow J holds uparrow A c= uparrow J
proof
let N be transitive RelStr, A, J be Subset of N such that
A1: A is_coarser_than uparrow J;
let w be object;
assume
A2: w in uparrow A;
then reconsider w1 = w as Element of N;
consider t being Element of N such that
A3: t <= w1 and
A4: t in A by A2,WAYBEL_0:def 16;
consider t1 being Element of N such that
A5: t1 in uparrow J and
A6: t1 <= t by A1,A4,YELLOW_4:def 2;
consider t2 being Element of N such that
A7: t2 <= t1 and
A8: t2 in J by A5,WAYBEL_0:def 16;
t2 <= t by A6,A7,ORDERS_2:3;
then t2 <= w1 by A3,ORDERS_2:3;
hence thesis by A8,WAYBEL_0:def 16;
end;
theorem
for N being transitive RelStr, A, J being Subset of N st A
is_finer_than downarrow J holds downarrow A c= downarrow J
proof
let N be transitive RelStr, A, J be Subset of N such that
A1: A is_finer_than downarrow J;
let w be object;
assume
A2: w in downarrow A;
then reconsider w1 = w as Element of N;
consider t being Element of N such that
A3: w1 <= t and
A4: t in A by A2,WAYBEL_0:def 15;
consider t1 being Element of N such that
A5: t1 in downarrow J and
A6: t <= t1 by A1,A4,YELLOW_4:def 1;
consider t2 being Element of N such that
A7: t1 <= t2 and
A8: t2 in J by A5,WAYBEL_0:def 15;
w1 <= t1 by A3,A6,ORDERS_2:3;
then w1 <= t2 by A7,ORDERS_2:3;
hence thesis by A8,WAYBEL_0:def 15;
end;
theorem
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
proof
let N be non empty reflexive RelStr, x be Element of N, X be Subset of N
such that
A1: x in X;
let a be object;
assume
A2: a in uparrow x;
then reconsider b = a as Element of N;
x <= b by A2,WAYBEL_0:18;
hence thesis by A1,WAYBEL_0:def 16;
end;
theorem
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
proof
let N be non empty reflexive RelStr, x be Element of N, X be Subset of N
such that
A1: x in X;
let a be object;
assume
A2: a in downarrow x;
then reconsider b = a as Element of N;
b <= x by A2,WAYBEL_0:17;
hence thesis by A1,WAYBEL_0:def 15;
end;
begin :: On the Hausdorff Spaces
reserve R, S, T for non empty TopSpace;
theorem Th32:
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
proof
let S, T be TopStruct, B be Basis of S;
A1: B c= the topology of S by TOPS_2:64;
assume
A2: the TopStruct of S = the TopStruct of T;
then the topology of T c= UniCl B by CANTOR_1:def 2;
hence thesis by A2,A1,CANTOR_1:def 2,TOPS_2:64;
end;
theorem Th33:
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
proof
let S, T be TopStruct, B be prebasis of S;
consider F being Basis of S such that
A1: F c= FinMeetCl B by CANTOR_1:def 4;
assume
A2: the TopStruct of S = the TopStruct of T;
then B c= the topology of T & F is Basis of T by Th32,TOPS_2:64;
hence thesis by A2,A1,CANTOR_1:def 4,TOPS_2:64;
end;
theorem Th34:
for J being Basis of T holds J is non empty
proof
let J be Basis of T;
assume J is empty;
then
A1: UniCl J = {{}} by YELLOW_9:16;
the topology of T c= UniCl J & the carrier of T in the topology of T by
CANTOR_1:def 2,PRE_TOPC:def 1;
hence contradiction by A1,TARSKI:def 1;
end;
registration
let T be non empty TopSpace;
cluster -> non empty for Basis of T;
coherence by Th34;
end;
theorem Th35:
for x being Point of T, J being Basis of x holds J is non empty
proof
let x be Point of T, J be Basis of x;
ex W being Subset of T st W in J & W c= [#]T by YELLOW_8:13;
hence thesis;
end;
registration
let T be non empty TopSpace, x be Point of T;
cluster -> non empty for Basis of x;
coherence by Th35;
end;
theorem
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
proof
let S1, T1, S2, T2 be TopSpace, f be Function of S1, S2, g be Function of T1
, T2 such that
A1: the TopStruct of S1 = the TopStruct of T1 and
A2: the TopStruct of S2 = the TopStruct of T2 and
A3: f = g and
A4: f is continuous;
now
let P2 be Subset of T2 such that
A5: P2 is closed;
reconsider P1 = P2 as Subset of S2 by A2;
P1 is closed by A2,A5,TOPS_3:79;
then f"P1 is closed by A4;
hence g"P2 is closed by A1,A3,TOPS_3:79;
end;
hence thesis;
end;
theorem Th37:
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
set f = pr1(the carrier of T,the carrier of T), g = pr2(the carrier of T,the
carrier of T);
A1: the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] by
BORSUK_1:def 2;
hereby
let a be object;
assume
A2: a in id the carrier of T;
then consider x, y being object such that
A3: x in the carrier of T and
A4: y in the carrier of T and
A5: a = [x,y] by ZFMISC_1:def 2;
A6: x = y by A2,A5,RELAT_1:def 10;
f.(x,y) = x by A3,A4,FUNCT_3:def 4
.= g.(x,y) by A3,A6,FUNCT_3:def 5;
hence a in {p where p is Point of [:T,T:]: f.p = g.p} by A1,A2,A5;
end;
let a be object;
assume a in {p where p is Point of [:T,T:]: f.p = g.p};
then consider p being Point of [:T,T:] such that
A7: a = p and
A8: f.p = g.p;
consider x, y being object such that
A9: x in the carrier of T and
A10: y in the carrier of T and
A11: p = [x,y] by A1,ZFMISC_1:def 2;
A12: f.(x,y) = g.(x,y) by A8,A11;
x = f.(x,y) by A9,A10,FUNCT_3:def 4
.= y by A9,A10,A12,FUNCT_3:def 5;
hence thesis by A7,A9,A11,RELAT_1:def 10;
end;
theorem Th38:
delta the carrier of T is continuous Function of T, [:T,T:]
proof
the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by
BORSUK_1:def 2;
then reconsider f = delta the carrier of T as Function of T, [:T,T:];
f is continuous
proof
let W be Point of T, G be a_neighborhood of f.W;
consider A being Subset-Family of [:T,T:] such that
A1: Int G = union A and
A2: for e being set st e in A ex X1, Y1 being Subset of T st e = [:X1,
Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
f.W in Int G by CONNSP_2:def 1;
then consider Z being set such that
A3: f.W in Z and
A4: Z in A by A1,TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A5: Z = [:X1,Y1:] and
A6: X1 is open & Y1 is open by A2,A4;
f.W = [W,W] by FUNCT_3:def 6;
then W in X1 & W in Y1 by A3,A5,ZFMISC_1:87;
then
A7: W in X1 /\ Y1 by XBOOLE_0:def 4;
X1 /\ Y1 is open by A6;
then W in Int (X1 /\ Y1) by A7,TOPS_1:23;
then reconsider H = X1 /\ Y1 as a_neighborhood of W by CONNSP_2:def 1;
A8: f.:H c= Int G
proof
let y be object;
assume y in f.:H;
then consider x being object such that
A9: x in dom f and
A10: x in H and
A11: y = f.x by FUNCT_1:def 6;
A12: x in X1 & x in Y1 by A10,XBOOLE_0:def 4;
y = [x,x] by A9,A11,FUNCT_3:def 6;
then y in Z by A5,A12,ZFMISC_1:87;
hence thesis by A1,A4,TARSKI:def 4;
end;
take H;
Int G c= G by TOPS_1:16;
hence thesis by A8;
end;
hence thesis;
end;
theorem Th39:
pr1(the carrier of S,the carrier of T) is continuous Function of [:S,T:], S
proof
set I = the carrier of S, J = the carrier of T;
A1: the carrier of [:S,T:] = [:I,J:] by BORSUK_1:def 2;
then reconsider f = pr1(I,J) as Function of [:S,T:], S;
f is continuous
proof
let w be Point of [:S,T:], G be a_neighborhood of f.w;
set H = [:Int G, [#]T:];
A2: Int H = [:Int Int G, Int [#]T:] by BORSUK_1:7
.= [:Int G, [#]T:] by TOPS_1:15;
consider x, y being object such that
A3: x in I and
A4: y in J and
A5: w = [x,y] by A1,ZFMISC_1:def 2;
f.w in Int G & f.(x,y) = x by A3,A4,CONNSP_2:def 1,FUNCT_3:def 4;
then w in Int H by A4,A5,A2,ZFMISC_1:def 2;
then reconsider H as a_neighborhood of w by CONNSP_2:def 1;
take H;
reconsider X = Int G as non empty Subset of S by CONNSP_2:def 1;
[:X,[#]T:] <> {};
then f.:H = Int G by EQREL_1:49;
hence thesis by TOPS_1:16;
end;
hence thesis;
end;
theorem Th40:
pr2(the carrier of S,the carrier of T) is continuous Function of [:S,T:], T
proof
set I = the carrier of S, J = the carrier of T;
A1: the carrier of [:S,T:] = [:I,J:] by BORSUK_1:def 2;
then reconsider f = pr2(I,J) as Function of [:S,T:], T;
f is continuous
proof
let w be Point of [:S,T:], G be a_neighborhood of f.w;
set H = [:[#]S,Int G:];
A2: Int H = [:Int [#]S,Int Int G:] by BORSUK_1:7
.= [:[#]S,Int G:] by TOPS_1:15;
consider x, y being object such that
A3: x in I and
A4: y in J and
A5: w = [x,y] by A1,ZFMISC_1:def 2;
f.w in Int G & f.(x,y) = y by A3,A4,CONNSP_2:def 1,FUNCT_3:def 5;
then w in Int H by A3,A5,A2,ZFMISC_1:def 2;
then reconsider H as a_neighborhood of w by CONNSP_2:def 1;
take H;
reconsider X = Int G as non empty Subset of T by CONNSP_2:def 1;
[:[#]S,X:] <> {};
then f.:H = Int G by EQREL_1:49;
hence thesis by TOPS_1:16;
end;
hence thesis;
end;
theorem Th41:
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:]
proof
let f be continuous Function of T, S, g be continuous Function of T, R;
A1: <:f,g:> = [:f,g:]*(delta the carrier of T) by FUNCT_3:78;
delta the carrier of T is continuous Function of T,[:T,T:] by Th38;
hence thesis by A1;
end;
theorem Th42:
<: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
pr1(the carrier of S,the carrier of T) is continuous Function of [:S,T:]
,S & pr2(the carrier of S,the carrier of T) is continuous Function of [:S,T:],T
by Th39,Th40;
hence thesis by Th41;
end;
theorem Th43:
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
let f be Function of [:S,T:], [:T,S:] such that
A1: f = <:pr2(the carrier of S,the carrier of T), pr1(the carrier of S,
the carrier of T):>;
thus dom f = [#][:S,T:] by FUNCT_2:def 1;
thus
A2: rng f = [:the carrier of T,the carrier of S:] by A1,Th4
.= [#][:T,S:] by BORSUK_1:def 2;
thus
f is one-to-one by A1;
thus f is continuous by A1,Th42;
f is onto by A2,FUNCT_2:def 3;
then f" = (f qua Function)" by A1,TOPS_2:def 4
.= <:pr2(the carrier of T,the carrier of S), pr1(the carrier of T,the
carrier of S):> by A1,Th8;
hence thesis by Th42;
end;
theorem
[:S,T:], [:T,S:] are_homeomorphic
proof
reconsider f = <:pr2(the carrier of S,the carrier of T), pr1(the carrier of
S,the carrier of T):> as Function of [:S,T:], [:T,S:] by Th42;
take f;
thus thesis by Th43;
end;
theorem Th45:
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
proof
let T be Hausdorff non empty TopSpace, f, g be continuous Function of S, T;
{p where p is Point of S: f.p <> g.p} c= the carrier of S
proof
let x be object;
assume x in {p where p is Point of S: f.p <> g.p};
then ex a being Point of S st x = a & f.a <> g.a;
hence thesis;
end;
then reconsider A = {p where p is Point of S: f.p <> g.p} as Subset of S;
A1: [#]T <> {};
thus for X being Subset of S st X = {p where p is Point of S: f.p <> g.p
} holds X is open
proof
let X be Subset of S such that
A2: X = {p where p is Point of S: f.p <> g.p};
for x being set holds x in X iff ex Q being Subset of S st Q is open &
Q c= X & x in Q
proof
let x be set;
hereby
assume x in X;
then consider p being Point of S such that
A3: x = p and
A4: f.p <> g.p by A2;
consider W, V being Subset of T such that
A5: W is open & V is open and
A6: f.p in W and
A7: g.p in V and
A8: W misses V by A4,PRE_TOPC:def 10;
dom g = the carrier of S by FUNCT_2:def 1;
then [x,g.p] in g by A3,FUNCT_1:def 2;
then
A9: x in g"V by A7,RELAT_1:def 14;
take Q = (f"W) /\ (g"V);
f"W is open & g"V is open by A1,A5,TOPS_2:43;
hence Q is open;
thus Q c= X
proof
let q be object;
assume
A10: q in Q;
then q in f"W by XBOOLE_0:def 4;
then consider yf being object such that
A11: [q,yf] in f and
A12: yf in W by RELAT_1:def 14;
q in g"V by A10,XBOOLE_0:def 4;
then consider yg being object such that
A13: [q,yg] in g & yg in V by RELAT_1:def 14;
A14: yg = g.q & not yg in W by A8,A13,FUNCT_1:1,XBOOLE_0:3;
yf = f.q by A11,FUNCT_1:1;
hence thesis by A2,A10,A12,A14;
end;
dom f = the carrier of S by FUNCT_2:def 1;
then [x,f.p] in f by A3,FUNCT_1:def 2;
then x in f"W by A6,RELAT_1:def 14;
hence x in Q by A9,XBOOLE_0:def 4;
end;
given Q being Subset of S such that
Q is open and
A15: Q c= X & x in Q;
thus thesis by A15;
end;
hence thesis by TOPS_1:25;
end;
then
A16: A is open;
let X be Subset of S such that
A17: X = {p where p is Point of S: f.p = g.p};
X` = A
proof
hereby
let x be object;
assume
A18: x in X`;
then not x in X by XBOOLE_0:def 5;
then f.x <> g.x by A17,A18;
hence x in A by A18;
end;
let x be object;
assume x in A;
then consider p being Point of S such that
A19: x = p and
A20: f.p <> g.p;
now
assume p in {t where t is Point of S: f.t = g.t};
then ex t being Point of S st p = t & f.t = g.t;
hence contradiction by A20;
end;
hence thesis by A17,A19,XBOOLE_0:def 5;
end;
hence thesis by A16;
end;
theorem
T is Hausdorff iff for A being Subset of [:T,T:] st A = id the carrier
of T holds A is closed
proof
reconsider f = pr1(the carrier of T,the carrier of T), g = pr2(the carrier
of T,the carrier of T) as continuous Function of [:T,T:],T by Th39,Th40;
reconsider A = id the carrier of T as Subset of [:T,T:] by BORSUK_1:def 2;
hereby
assume
A1: T is Hausdorff;
let A be Subset of [:T,T:];
assume A = id the carrier of T;
then A = {p where p is Point of [:T,T:]: f.p = g.p} by Th37;
hence A is closed by A1,Th45;
end;
assume
for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed;
then [#][:T,T:] = [:[#]T,[#]T:] & A is closed by BORSUK_1:def 2;
then [:[#]T,[#]T:] \ A is open;
then consider SF being Subset-Family of [:T,T:] such that
A2: [:[#]T,[#]T:] \ A = union SF and
A3: for e being set st e in SF ex X1, Y1 being Subset of T st e = [:X1,
Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
let p, q be Point of T;
assume not p = q;
then
the carrier of [:T,T:] = [:the carrier of T,the carrier of T:] & not [p
,q] in id [#]T by BORSUK_1:def 2,RELAT_1:def 10;
then [p,q] in [:[#]T,[#]T:] \ A by XBOOLE_0:def 5;
then consider XY being set such that
A4: [p,q] in XY and
A5: XY in SF by A2,TARSKI:def 4;
consider X1, Y1 being Subset of T such that
A6: XY = [:X1,Y1:] and
A7: X1 is open & Y1 is open by A3,A5;
take X1, Y1;
thus X1 is open & Y1 is open by A7;
thus p in X1 & q in Y1 by A4,A6,ZFMISC_1:87;
assume X1 /\ Y1 <> {};
then consider w being object such that
A8: w in X1 /\ Y1 by XBOOLE_0:def 1;
w in X1 & w in Y1 by A8,XBOOLE_0:def 4;
then [w,w] in XY by A6,ZFMISC_1:87;
then [w,w] in union SF by A5,TARSKI:def 4;
then not [w,w] in A by A2,XBOOLE_0:def 5;
hence contradiction by A8,RELAT_1:def 10;
end;
registration
let S, T be TopStruct;
cluster strict for Refinement of S, T;
existence
proof
set R = the Refinement of S, T;
set R1 = the TopStruct of R;
(the topology of S) \/ (the topology of T) is prebasis of R by
YELLOW_9:def 6;
then the carrier of R1 = (the carrier of S) \/ (the carrier of T) & (the
topology of S) \/ (the topology of T) is prebasis of R1 by Th33,YELLOW_9:def 6;
then reconsider R1 as Refinement of S, T by YELLOW_9:def 6;
take R1;
thus thesis;
end;
end;
registration
let S be non empty TopStruct, T be TopStruct;
cluster strict non empty for Refinement of S, T;
existence
proof
set R = the strict Refinement of S, T;
take R;
thus thesis;
end;
cluster strict non empty for Refinement of T, S;
existence
proof
set R = the strict Refinement of T, S;
take R;
thus thesis;
end;
end;
theorem
for R, S, T being TopStruct holds R is Refinement of S, T iff the
TopStruct of R is Refinement of S, T
proof
let R, S, T be TopStruct;
hereby
assume
A1: R is Refinement of S, T;
then reconsider R1 = R as TopSpace;
(the topology of S) \/ (the topology of T) is prebasis of R by A1,
YELLOW_9:def 6;
then
A2: (the topology of S) \/ (the topology of T) is prebasis of the TopStruct
of R1 by Th33;
the carrier of the TopStruct of R1 = (the carrier of S) \/ (the
carrier of T) by A1,YELLOW_9:def 6;
hence the TopStruct of R is Refinement of S, T by A2,YELLOW_9:def 6;
end;
assume
A3: the TopStruct of R is Refinement of S, T;
then reconsider R1 = R as TopSpace by TEX_2:7;
(the topology of S) \/ (the topology of T) is prebasis of the TopStruct
of R by A3,YELLOW_9:def 6;
then
A4: (the topology of S) \/ (the topology of T) is prebasis of R1 by Th33;
the carrier of R1 = (the carrier of S) \/ (the carrier of T) by A3,
YELLOW_9:def 6;
hence thesis by A4,YELLOW_9:def 6;
end;
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 Th48:
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
proof
assume
A1: the carrier of S1 = the carrier of S2 & the carrier of T1 = the
carrier of T2;
set Y = { [: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 };
A2: the carrier of [:S2,T2:] = [:the carrier of S2, the carrier of T2:] by
BORSUK_1:def 2;
A3: the carrier of [:S1,T1:] = [:the carrier of S1, the carrier of T1:] by
BORSUK_1:def 2;
then reconsider
BST = INTERSECTION(the topology of [:S1,T1:], the topology of [:
S2,T2:]) as Basis of R by A1,A2,YELLOW_9:60;
A4: the carrier of R = (the carrier of [:S1,T1:]) \/ the carrier of [:S2,T2
:] by YELLOW_9:def 6
.= [:the carrier of S1,the carrier of T1:] \/ [:the carrier of S2,the
carrier of T2:] by A3,BORSUK_1:def 2
.= [:the carrier of S1,the carrier of T1:] by A1;
Y c= bool the carrier of R
proof
let c be object;
assume c in Y;
then
ex U1 being Subset of S1, U2 being Subset of S2, V1 being Subset of T1
, V2 being Subset of T2 st c = [:U1,V1:] /\ [:U2,V2:] & U1 is open & U2 is open
& V1 is open & V2 is open;
hence thesis by A1,A2,A4;
end;
then reconsider C1 = Y as Subset-Family of R;
reconsider C1 as Subset-Family of R;
A5: the topology of [:S2,T2:] = { union A where A is Subset-Family of [:S2,
T2:]: A c= { [:X1,Y1:] where X1 is Subset of S2, Y1 is Subset of T2 : X1 in the
topology of S2 & Y1 in the topology of T2}} by BORSUK_1:def 2;
A6: the topology of [:S1,T1:] = { union A where A is Subset-Family of [:S1,
T1:]: A c= { [:X1,Y1:] where X1 is Subset of S1, Y1 is Subset of T1 : X1 in the
topology of S1 & Y1 in the topology of T1}} by BORSUK_1:def 2;
A7: for A being Subset of R st A is open for p being Point of R st p in A
ex a being Subset of R st a in C1 & p in a & a c= A
proof
let A be Subset of R such that
A8: A is open;
let p be Point of R;
assume p in A;
then consider X being Subset of R such that
A9: X in BST and
A10: p in X and
A11: X c= A by A8,YELLOW_9:31;
consider X1, X2 be set such that
A12: X1 in the topology of [:S1,T1:] and
A13: X2 in the topology of [:S2,T2:] and
A14: X = X1 /\ X2 by A9,SETFAM_1:def 5;
consider F1 being Subset-Family of [:S1,T1:] such that
A15: X1 = union F1 and
A16: F1 c= { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 :
K1 in the topology of S1 & L1 in the topology of T1 } by A6,A12;
p in X1 by A10,A14,XBOOLE_0:def 4;
then consider G1 being set such that
A17: p in G1 and
A18: G1 in F1 by A15,TARSKI:def 4;
A19: G1 in { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : K1
in the topology of S1 & L1 in the topology of T1 } by A16,A18;
consider F2 being Subset-Family of [:S2,T2:] such that
A20: X2 = union F2 and
A21: F2 c= { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 :
K2 in the topology of S2 & L2 in the topology of T2 } by A5,A13;
p in X2 by A10,A14,XBOOLE_0:def 4;
then consider G2 being set such that
A22: p in G2 and
A23: G2 in F2 by A20,TARSKI:def 4;
G2 in { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : K2
in the topology of S2 & L2 in the topology of T2 } by A21,A23;
then consider K2 being Subset of S2, L2 being Subset of T2 such that
A24: G2 = [:K2,L2:] and
A25: K2 in the topology of S2 & L2 in the topology of T2;
A26: [:K2,L2:] c= X2 by A20,A23,A24,ZFMISC_1:74;
A27: K2 is open & L2 is open by A25;
consider K1 being Subset of S1, L1 being Subset of T1 such that
A28: G1 = [:K1,L1:] and
A29: K1 in the topology of S1 & L1 in the topology of T1 by A19;
reconsider a = [:K1,L1:] /\ [:K2,L2:] as Subset of R by A1,A4,
BORSUK_1:def 2;
take a;
K1 is open & L1 is open by A29;
hence a in C1 by A27;
thus p in a by A17,A22,A28,A24,XBOOLE_0:def 4;
[:K1,L1:] c= X1 by A15,A18,A28,ZFMISC_1:74;
then a c= X by A14,A26,XBOOLE_1:27;
hence thesis by A11;
end;
Y c= the topology of R
proof
let c be object;
A30: BST c= the topology of R by TOPS_2:64;
assume c in Y;
then consider
U1 being Subset of S1, U2 being Subset of S2, V1 being Subset of
T1, V2 being Subset of T2 such that
A31: c = [:U1,V1:] /\ [:U2,V2:] and
A32: U1 is open and
A33: U2 is open and
A34: V1 is open and
A35: V2 is open;
[:U2,V2:] is open by A33,A35,BORSUK_1:6;
then
A36: [:U2,V2:] in the topology of [:S2,T2:];
[:U1,V1:] is open by A32,A34,BORSUK_1:6;
then [:U1,V1:] in the topology of [:S1,T1:];
then c in BST by A31,A36,SETFAM_1:def 5;
hence thesis by A30;
end;
hence thesis by A7,YELLOW_9:32;
end;
theorem Th49:
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
proof
assume that
A1: the carrier of S1 = the carrier of S2 and
A2: the carrier of T1 = the carrier of T2;
A3: the carrier of R1 = (the carrier of S1) \/ the carrier of S2 by
YELLOW_9:def 6
.= the carrier of S1 by A1;
set C = { [: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 };
reconsider BT = INTERSECTION(the topology of T1, the topology of T2) as
Basis of R2 by A2,YELLOW_9:60;
reconsider BS = INTERSECTION(the topology of S1, the topology of S2) as
Basis of R1 by A1,YELLOW_9:60;
reconsider Bpr = {[:a,b:] where a is Subset of R1, b is Subset of R2: a in
BS & b in BT} as Basis of [:R1,R2:] by YELLOW_9:40;
A4: C = Bpr
proof
hereby
let c be object;
assume c in C;
then consider
U1 being Subset of S1, U2 being Subset of S2, V1 being Subset
of T1, V2 being Subset of T2 such that
A5: c = [:U1,V1:] /\ [:U2,V2:] and
A6: U1 is open & U2 is open and
A7: V1 is open & V2 is open;
U1 in the topology of S1 & U2 in the topology of S2 by A6;
then
A8: U1 /\ U2 in BS by SETFAM_1:def 5;
V1 in the topology of T1 & V2 in the topology of T2 by A7;
then
A9: V1 /\ V2 in BT by SETFAM_1:def 5;
c = [:U1 /\ U2, V1 /\ V2:] by A5,ZFMISC_1:100;
hence c in Bpr by A8,A9;
end;
let c be object;
assume c in Bpr;
then consider a being Subset of R1, b being Subset of R2 such that
A10: c = [:a,b:] and
A11: a in BS and
A12: b in BT;
consider a1, a2 being set such that
A13: a1 in the topology of S1 and
A14: a2 in the topology of S2 and
A15: a = a1 /\ a2 by A11,SETFAM_1:def 5;
reconsider a2 as Subset of S2 by A14;
reconsider a1 as Subset of S1 by A13;
A16: a1 is open & a2 is open by A13,A14;
consider b1, b2 being set such that
A17: b1 in the topology of T1 and
A18: b2 in the topology of T2 and
A19: b = b1 /\ b2 by A12,SETFAM_1:def 5;
reconsider b2 as Subset of T2 by A18;
reconsider b1 as Subset of T1 by A17;
A20: b1 is open & b2 is open by A17,A18;
c = [:a1,b1:] /\ [:a2,b2:] by A10,A15,A19,ZFMISC_1:100;
hence thesis by A16,A20;
end;
A21: the carrier of R2 = (the carrier of T1) \/ the carrier of T2 by
YELLOW_9:def 6
.= the carrier of T1 by A2;
A22: the carrier of [:S1,T1:] = [:the carrier of S1, the carrier of T1:] by
BORSUK_1:def 2;
the carrier of R = (the carrier of [:S1,T1:]) \/ the carrier of [:S2,T2
:] by YELLOW_9:def 6
.= [:the carrier of S1,the carrier of T1:] \/ [:the carrier of S2,the
carrier of T2:] by A22,BORSUK_1:def 2
.= [:the carrier of S1,the carrier of T1:] by A1,A2;
hence
A23: the carrier of [:R1,R2:] = the carrier of R by A3,A21,BORSUK_1:def 2;
C is Basis of R by A1,A2,Th48;
hence thesis by A23,A4,YELLOW_9:25;
end;
theorem
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:]
proof
set R = the strict Refinement of [:S1,T1:], [:S2,T2:];
assume
A1: the carrier of S1 = the carrier of S2 & the carrier of T1 = the
carrier of T2;
then the carrier of [:R1,R2:] = the carrier of R by Th49;
hence thesis by A1,Th49;
end;