:: Properties of the Product of Compact Topological Spaces
:: by Adam Grabowski
::
:: Received February 13, 1999
:: Copyright (c) 1999-2026 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 PRE_TOPC, SUBSET_1, ZFMISC_1, XBOOLE_0, FUNCOP_1, ORDINAL2,
FUNCT_1, RELAT_1, STRUCT_0, TOPS_2, T_0TOPSP, RCOMP_1, MCART_1, PARTFUN1,
TARSKI, PBOOLE, BORSUK_1, TOPS_1, CONNSP_2, SETFAM_1, FINSET_1, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, FUNCT_1,
PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1,
STRUCT_0, PRE_TOPC, TOPS_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP,
FINSET_1, FUNCT_3, CONNSP_2;
constructors FUNCT_3, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, T_0TOPSP, FUNCOP_1,
BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC,
TOPS_1, BORSUK_1, COMPTS_1, BORSUK_2, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI, TOPS_2, T_0TOPSP, FUNCT_1, XBOOLE_0;
equalities BINOP_1, STRUCT_0;
expansions TARSKI, TOPS_2, COMPTS_1, T_0TOPSP, XBOOLE_0;
theorems BORSUK_1, FUNCOP_1, TOPS_2, FUNCT_2, FUNCT_1, PRE_TOPC, TARSKI,
TOPS_1, TOPMETR, ZFMISC_1, CONNSP_2, FUNCT_3, COMPTS_1, FINSET_1,
YELLOW12, TSEP_1, TOPGRP_1, XBOOLE_0, XBOOLE_1, SETFAM_1;
schemes PBOOLE, CLASSES1, XFAMILY;
begin :: Preliminaries
theorem
for S, T being TopSpace holds [#][:S, T:] = [:[#]S, [#]T:] by BORSUK_1:def 2;
theorem Th2:
for X, Y being non empty TopSpace, x being Point of X holds Y -->
x is continuous Function of Y, X|{x}
proof
let X, Y be non empty TopSpace, x be Point of X;
set Z = {x};
set f = Y --> x;
x in Z & the carrier of (X|Z) = Z by PRE_TOPC:8,TARSKI:def 1;
then reconsider g = f as Function of Y, X|Z by FUNCOP_1:45;
g is continuous by TOPMETR:6;
hence thesis;
end;
registration
let T be TopStruct;
cluster id T -> being_homeomorphism;
coherence by TOPGRP_1:20;
end;
Lm1: for S being TopStruct holds S, S are_homeomorphic
proof
let S be TopStruct;
take id S;
thus thesis;
end;
Lm2: for S, T being non empty TopStruct st S, T are_homeomorphic holds T, S
are_homeomorphic
proof
let S, T be non empty TopStruct;
assume S, T are_homeomorphic;
then consider f being Function of S, T such that
A1: f is being_homeomorphism;
f" is being_homeomorphism by A1,TOPS_2:56;
hence thesis;
end;
definition
let S, T be TopStruct;
redefine pred S, T are_homeomorphic; :: redefines are_homeomorphic (T_0TOPSP, definition)
reflexivity by Lm1;
end;
definition
let S, T be non empty TopStruct;
redefine pred S, T are_homeomorphic; :: redefines are_homeomorphic (T_0TOPSP, definition)
reflexivity by Lm1;
symmetry by Lm2;
end;
theorem
for S, T, V being non empty TopSpace st S, T are_homeomorphic & T, V
are_homeomorphic holds S, V are_homeomorphic
proof
let S, T, V be non empty TopSpace;
assume that
A1: S, T are_homeomorphic and
A2: T, V are_homeomorphic;
consider f being Function of S, T such that
A3: f is being_homeomorphism by A1;
consider g being Function of T, V such that
A4: g is being_homeomorphism by A2;
g * f is being_homeomorphism by A3,A4,TOPS_2:57;
hence thesis;
end;
begin :: On the projections and empty topological spaces
registration
let T be TopStruct, P be empty Subset of T;
cluster T | P -> empty;
coherence;
end;
registration
cluster empty -> compact for TopSpace;
coherence;
end;
theorem Th4:
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is
one-to-one
proof
let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | {
x}:], Y;
set Z = {x};
assume
A1: f = pr1(the carrier of Y, Z);
let z, y be object such that
A2: z in dom f and
A3: y in dom f and
A4: f.z = f.y;
A5: dom f = [:the carrier of Y, Z:] by A1,FUNCT_3:def 4;
then consider x1, x2 being object such that
A6: x1 in the carrier of Y and
A7: x2 in Z and
A8: z = [x1, x2] by A2,ZFMISC_1:def 2;
consider y1, y2 being object such that
A9: y1 in the carrier of Y and
A10: y2 in Z and
A11: y = [y1, y2] by A5,A3,ZFMISC_1:def 2;
A12: x2 = x by A7,TARSKI:def 1
.= y2 by A10,TARSKI:def 1;
x1 = f.(x1, x2) by A1,A6,A7,FUNCT_3:def 4
.= f.(y1, y2) by A4,A8,A11
.= y1 by A1,A9,A10,FUNCT_3:def 4;
hence thesis by A8,A11,A12;
end;
theorem Th5:
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is
one-to-one
proof
let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x},
Y:], Y;
set Z = {x};
assume
A1: f = pr2(Z, the carrier of Y);
let z, y be object such that
A2: z in dom f and
A3: y in dom f and
A4: f.z = f.y;
A5: dom f = [:Z, the carrier of Y:] by A1,FUNCT_3:def 5;
then consider x1, x2 being object such that
A6: x1 in Z and
A7: x2 in the carrier of Y and
A8: z = [x1,x2] by A2,ZFMISC_1:def 2;
consider y1, y2 being object such that
A9: y1 in Z and
A10: y2 in the carrier of Y and
A11: y = [y1,y2] by A5,A3,ZFMISC_1:def 2;
A12: x1 = x by A6,TARSKI:def 1
.= y1 by A9,TARSKI:def 1;
x2= f.(x1, x2) by A1,A6,A7,FUNCT_3:def 5
.= f.(y1, y2) by A4,A8,A11
.= y2 by A1,A9,A10,FUNCT_3:def 5;
hence thesis by A8,A11,A12;
end;
theorem Th6:
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f" = <:id
Y, Y --> x:>
proof
let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | {
x}:], Y;
set Z = {x};
set idZ = id Y;
A1: rng idZ c= the carrier of Y;
assume
A2: f = pr1(the carrier of Y, Z);
then
A3: rng f = the carrier of Y by FUNCT_3:44;
reconsider Z as non empty Subset of X;
reconsider idY = Y --> x as continuous Function of Y, (X|Z) by Th2;
reconsider KA = <:idZ, idY:> as continuous Function of Y, [:Y, (X|Z):] by
YELLOW12:41;
A4: [:the carrier of Y, Z:] c= rng KA
proof
let y be object;
assume y in [:the carrier of Y, Z:];
then consider y1, y2 being object such that
A5: y1 in the carrier of Y and
A6: y2 in {x} & y = [y1,y2] by ZFMISC_1:def 2;
A7: y = [y1, x] by A6,TARSKI:def 1;
A8: idY.y1 = ((the carrier of Y) --> x).y1 .= x by A5,FUNCOP_1:7;
A9: y1 in dom KA by A5,FUNCT_2:def 1;
then KA. y1 = [idZ.y1, idY.y1] by FUNCT_3:def 7
.= [y1, x] by A5,A8,FUNCT_1:18;
hence thesis by A7,A9,FUNCT_1:def 3;
end;
rng idY c= the carrier of (X|Z);
then
A10: rng idY c= Z by PRE_TOPC:8;
then rng KA c= [:rng idZ, rng idY:] & [:rng idZ, rng idY:] c= [:the carrier
of Y, Z:] by FUNCT_3:51,ZFMISC_1:96;
then rng KA c= [:the carrier of Y, Z:];
then
A11: rng KA = [:the carrier of Y, Z:] by A4
.= dom f by A2,FUNCT_3:def 4;
A12: f is one-to-one by A2,Th4;
A13: f is onto by A3,FUNCT_2:def 3;
dom idY = the carrier of Y by FUNCT_2:def 1
.= dom idZ by FUNCT_2:def 1;
then f*KA = id rng f by A2,A3,A10,A1,FUNCT_3:52;
then KA = (f qua Function)" by A12,A11,FUNCT_1:42;
hence thesis by A12,A13,TOPS_2:def 4;
end;
theorem Th7:
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f" = <:Y
--> x, id Y:>
proof
let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x},
Y:], Y;
set Z = {x};
set idY = id Y;
A1: rng idY c= the carrier of Y;
assume
A2: f = pr2(Z, the carrier of Y);
then
A3: rng f = the carrier of Y by FUNCT_3:46;
reconsider Z as non empty Subset of X;
reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2;
reconsider KA = <:idZ, idY:> as continuous Function of Y, [:(X|Z), Y:] by
YELLOW12:41;
A4: [:{x}, the carrier of Y:] c= rng KA
proof
let y be object;
assume y in [:{x}, the carrier of Y:];
then consider y1, y2 being object such that
A5: y1 in {x} and
A6: y2 in the carrier of Y and
A7: y = [y1,y2] by ZFMISC_1:def 2;
A8: y = [x, y2] by A5,A7,TARSKI:def 1;
A9: idZ.y2 = ((the carrier of Y) --> x).y2 .= x by A6,FUNCOP_1:7;
A10: y2 in dom KA by A6,FUNCT_2:def 1;
then KA. y2 = [idZ.y2, idY.y2] by FUNCT_3:def 7
.= [x, y2] by A6,A9,FUNCT_1:18;
hence thesis by A8,A10,FUNCT_1:def 3;
end;
rng idZ c= the carrier of (X|Z);
then
A11: rng idZ c= Z by PRE_TOPC:8;
then rng KA c= [:rng idZ, rng idY:] & [:rng idZ, rng idY:] c= [:{x},the
carrier of Y:] by FUNCT_3:51,ZFMISC_1:96;
then rng KA c= [:{x}, the carrier of Y:];
then
A12: rng KA = [:Z, the carrier of Y:] by A4
.= dom f by A2,FUNCT_3:def 5;
A13: f is one-to-one by A2,Th5;
A14: f is onto by A3,FUNCT_2:def 3;
dom idZ = the carrier of Y by FUNCT_2:def 1
.= dom idY by FUNCT_2:def 1;
then f*KA = id rng f by A2,A3,A11,A1,FUNCT_3:52;
then KA = (f qua Function)" by A13,A12,FUNCT_1:42;
hence thesis by A13,A14,TOPS_2:def 4;
end;
theorem
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:Y, X | {x}:], Y st f = pr1(the carrier of Y, {x}) holds f is
being_homeomorphism
proof
let X, Y be non empty TopSpace, x be Point of X, f be Function of [:Y, X | {
x}:], Y;
set Z = {x};
assume
A1: f = pr1(the carrier of Y, Z);
thus dom f = [#][:Y, (X|Z):] by FUNCT_2:def 1;
thus rng f = [#]Y by A1,FUNCT_3:44;
thus f is one-to-one by A1,Th4;
the carrier of (X|Z) = Z by PRE_TOPC:8;
hence f is continuous by A1,YELLOW12:39;
reconsider Z as non empty Subset of X;
reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2;
reconsider KA = <:id Y, idZ:> as continuous Function of Y, [:Y, (X|Z):] by
YELLOW12:41;
KA = f" by A1,Th6;
hence thesis;
end;
theorem Th9:
for X, Y being non empty TopSpace, x being Point of X, f being
Function of [:X | {x}, Y:], Y st f = pr2({x}, the carrier of Y) holds f is
being_homeomorphism
proof
let X, Y be non empty TopSpace, x be Point of X, f be Function of [:X | {x},
Y:], Y;
set Z = {x};
assume
A1: f = pr2(Z, the carrier of Y);
thus dom f = [#][:(X|Z), Y:] by FUNCT_2:def 1;
thus rng f = [#]Y by A1,FUNCT_3:46;
thus f is one-to-one by A1,Th5;
the carrier of (X|Z) = Z by PRE_TOPC:8;
hence f is continuous by A1,YELLOW12:40;
reconsider Z as non empty Subset of X;
reconsider idZ = Y --> x as continuous Function of Y, (X|Z) by Th2;
reconsider KA = <:idZ, id Y:> as continuous Function of Y, [:(X|Z), Y:] by
YELLOW12:41;
KA = f" by A1,Th7;
hence thesis;
end;
begin :: On the product of compact spaces
theorem
for X being non empty TopSpace, Y being compact non empty TopSpace, G
being open Subset of [:X, Y:], x being set st [:{x}, the carrier of Y:] c= G ex
f being ManySortedSet of the carrier of Y st
for i being object st i in the
carrier of Y ex G1 being Subset of X, H1 being Subset of Y st f.i = [G1,H1] & [
x, i] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G
proof
let X be non empty TopSpace, Y be compact non empty TopSpace, G be open
Subset of [:X, Y:], x be set;
set y = the Point of Y;
A1: the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] & [x,y]
in [:{x},the carrier of Y:] by BORSUK_1:def 2,ZFMISC_1:105;
defpred P[object,object] means
ex G1 be Subset of X, H1 be Subset of Y st $2 = [
G1,H1] & [x, $1] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G;
assume
A2: [:{x}, the carrier of Y:] c= G;
then [:{x}, the carrier of Y:] c= the carrier of [:X,Y:] by XBOOLE_1:1;
then reconsider x9 = x as Point of X by A1,ZFMISC_1:87;
A3: [:{x9}, the carrier of Y:] c= union Base-Appr G by A2,BORSUK_1:13;
A4: now
let y be set;
A5: x in {x9} by TARSKI:def 1;
assume y in the carrier of Y;
then [x,y] in [:{x9}, the carrier of Y:] by A5,ZFMISC_1:87;
then consider Z be set such that
A6: [x, y] in Z and
A7: Z in Base-Appr G by A3,TARSKI:def 4;
Base-Appr G = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y:
[:X1,Y1:] c= G & X1 is open & Y1 is open} by BORSUK_1:def 3;
then ex X1 be Subset of X, Y1 be Subset of Y st Z = [:X1, Y1:] & [:X1,Y1:]
c= G & X1 is open & Y1 is open by A7;
hence ex G1 be Subset of X, H1 be Subset of Y st [x, y] in [:G1, H1:] & [:
G1,H1:] c= G & G1 is open & H1 is open by A6;
end;
A8: for i be object st i in the carrier of Y ex j be object st P[i,j]
proof
let i be object;
assume i in the carrier of Y;
then consider G1 be Subset of X, H1 be Subset of Y such that
A9: [x, i] in [:G1, H1:] & [:G1, H1:] c= G & G1 is open & H1 is open by A4;
ex G2 be Subset of X, H2 be Subset of Y st [G1,H1] = [G2,H2] & [x, i]
in [:G2, H2:] & G2 is open & H2 is open & [:G2, H2:] c= G by A9;
hence thesis;
end;
ex f being ManySortedSet of the carrier of Y st for i be object st i in
the carrier of Y holds P[i,f.i] from PBOOLE:sch 3 (A8 );
hence thesis;
end;
theorem Th11:
for X being non empty TopSpace, Y being compact non empty
TopSpace, G being open Subset of [:Y, X:] holds for x being set st [:[#]Y, {x}
:] c= G holds ex R be open Subset of X st x in R & R c= { y where y is Point of
X: [:[#]Y, {y}:] c= G }
proof
let X be non empty TopSpace, Y be compact non empty TopSpace, G be open
Subset of [:Y, X:];
let x be set;
set y = the Point of Y;
A1: the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & [y,x]
in [:the carrier of Y,{x}:] by BORSUK_1:def 2,ZFMISC_1:106;
assume
A2: [:[#]Y, {x}:] c= G;
then [:[#]Y,{x}:] c= the carrier of [:Y,X:] by XBOOLE_1:1;
then reconsider x9 = x as Point of X by A1,ZFMISC_1:87;
Int G = G by TOPS_1:23;
then [#]Y is compact & G is a_neighborhood of [:[#]Y, {x9}:] by A2,COMPTS_1:1
,CONNSP_2:def 2;
then consider
W being a_neighborhood of [#]Y, V being a_neighborhood of x9 such
that
A3: [:W, V:] c= G by BORSUK_1:25;
take R = Int V;
Int W c= W & [#]Y c= Int W by CONNSP_2:def 2,TOPS_1:16;
then
A4: [#]Y c= W;
A5: Int V c= V by TOPS_1:16;
R c= { z where z is Point of X : [:[#]Y, {z}:] c= G }
proof
let r be object;
assume
A6: r in R;
then reconsider r9 = r as Point of X;
{r} c= V by A5,A6,ZFMISC_1:31;
then [:[#]Y, {r9}:] c= [:W, V:] by A4,ZFMISC_1:96;
then [:[#]Y, {r9}:] c= G by A3;
hence thesis;
end;
hence thesis by CONNSP_2:def 1;
end;
theorem Th12:
for X being non empty TopSpace, Y being compact non empty
TopSpace, G being open Subset of [:Y, X:] holds { x where x is Point of X : [:
[#]Y, {x}:] c= G } in the topology of X
proof
let X be non empty TopSpace, Y be compact non empty TopSpace, G be open
Subset of [:Y, X:];
set Q = { x where x is Point of X : [:[#]Y, {x}:] c= G };
Q c= the carrier of X
proof
let q be object;
assume q in Q;
then ex x9 being Point of X st q = x9 & [:[#]Y, {x9}:] c= G;
hence thesis;
end;
then reconsider Q as Subset of X;
defpred P[set] means ex y be set st y in Q & ex S be Subset of X st S = $1 &
S is open & y in S & S c= Q;
consider RR be set such that
A1: for x be set holds x in RR iff x in bool Q & P[x] from XFAMILY:sch
1;
RR c= bool Q
by A1;
then reconsider RR as Subset-Family of Q;
Q c= union RR
proof
let a be object;
assume a in Q;
then ex x9 being Point of X st a = x9 & [:[#]Y, {x9}:] c= G;
then consider R be open Subset of X such that
A2: a in R and
A3: R c= Q by Th11;
R in RR by A1,A2,A3;
hence thesis by A2,TARSKI:def 4;
end;
then
A4: union RR = Q;
bool Q c= bool the carrier of X by ZFMISC_1:67;
then reconsider RR as Subset-Family of X by XBOOLE_1:1;
RR c= the topology of X
proof
let x be object;
assume x in RR;
then ex y be set st y in Q & ex S be Subset of X st S = x & S is open & y
in S & S c= Q by A1;
hence thesis by PRE_TOPC:def 2;
end;
hence thesis by A4,PRE_TOPC:def 1;
end;
theorem Th13:
for X, Y being non empty TopSpace, x being Point of X holds [: X
| {x}, Y :], Y are_homeomorphic
proof
let X be non empty TopSpace, Y be non empty TopSpace, x be Point of X;
set Z = {x};
the carrier of [:(X|Z), Y:] = [:the carrier of (X|Z), the carrier of Y
:] by BORSUK_1:def 2
.= [:Z, the carrier of Y:] by PRE_TOPC:8;
then reconsider f= pr2(Z, the carrier of Y) as Function of [:X|Z, Y:], Y;
take f;
thus thesis by Th9;
end;
Lm3: for X being non empty TopSpace, Y being non empty TopSpace, x being Point
of X, Z being non empty Subset of X st Z = {x} holds [: Y, X | Z :], Y
are_homeomorphic
proof
let X be non empty TopSpace, Y be non empty TopSpace, x be Point of X, Z be
non empty Subset of X;
[: Y, X | Z :], [: X | Z, Y :] are_homeomorphic by YELLOW12:44;
then consider g being Function of [: Y, X | Z :], [: X | Z, Y :] such that
A1: g is being_homeomorphism;
assume Z = {x};
then [: X | Z, Y :], Y are_homeomorphic by Th13;
then consider f being Function of [: X | Z, Y :], Y such that
A2: f is being_homeomorphism;
reconsider gf = f * g as Function of [: Y, X | Z :], Y;
gf is being_homeomorphism by A2,A1,TOPS_2:57;
hence thesis;
end;
theorem Th14:
for S, T being non empty TopSpace st S, T are_homeomorphic & S
is compact holds T is compact
proof
let S, T be non empty TopSpace;
assume that
A1: S, T are_homeomorphic and
A2: S is compact;
consider f being Function of S, T such that
A3: f is being_homeomorphism by A1;
f is continuous & rng f = [#] T by A3;
hence thesis by A2,COMPTS_1:14;
end;
theorem Th15:
for X, Y being TopSpace, XV being SubSpace of X holds [:Y, XV:]
is SubSpace of [:Y, X:]
proof
let X, Y be TopSpace, XV be SubSpace of X;
set S = [:Y, XV:], T = [:Y, X:];
A1: the carrier of [:Y, XV:] = [:the carrier of Y, the carrier of XV:] by
BORSUK_1:def 2;
A2: the carrier of [:Y, X:] = [:the carrier of Y, the carrier of X:] & the
carrier of XV c= the carrier of X by BORSUK_1:1,def 2;
A3: for P being Subset of S holds P in the topology of S iff ex Q being
Subset of T st Q in the topology of T & P = Q /\ [#]S
proof
reconsider oS = [#]S as Subset of T by A1,A2,ZFMISC_1:96;
let P be Subset of S;
reconsider P9 = P as Subset of S;
hereby
assume P in the topology of S;
then P9 is open by PRE_TOPC:def 2;
then consider A being Subset-Family of S such that
A4: P9 = union A and
A5: for e be set st e in A ex X1 being Subset of Y, Y1 being Subset
of XV st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
set AA = {[:X1, Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1
being Subset of XV st Y1 = Y2 /\ [#](XV) & X1 is open & Y2 is open & [:X1, Y1:]
in A };
AA c= bool the carrier of T
proof
let a be object;
assume a in AA;
then
ex Xx1 being Subset of Y, Yy2 being Subset of X st a = [: Xx1, Yy2
:] & ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is
open & [:Xx1, Y1:] in A;
hence thesis;
end;
then reconsider AA as Subset-Family of T;
reconsider AA as Subset-Family of T;
A6: P c= union AA /\ [#]S
proof
let p be object;
assume p in P;
then consider A1 be set such that
A7: p in A1 and
A8: A1 in A by A4,TARSKI:def 4;
reconsider A1 as Subset of S by A8;
consider X2 being Subset of Y, Y2 being Subset of XV such that
A9: A1 = [:X2,Y2:] and
A10: X2 is open and
A11: Y2 is open by A5,A8;
Y2 in the topology of XV by A11,PRE_TOPC:def 2;
then consider Q1 being Subset of X such that
A12: Q1 in the topology of X and
A13: Y2 = Q1 /\ [#]XV by PRE_TOPC:def 4;
consider p1, p2 being object such that
A14: p1 in X2 and
A15: p2 in Y2 and
A16: p = [p1, p2] by A7,A9,ZFMISC_1:def 2;
reconsider Q1 as Subset of X;
set EX = [:X2, Q1:];
p2 in Q1 by A15,A13,XBOOLE_0:def 4;
then
A17: p in EX by A14,A16,ZFMISC_1:87;
Q1 is open by A12,PRE_TOPC:def 2;
then
EX in {[:Xx1, Yy2:] where Xx1 is Subset of Y, Yy2 is Subset of X:
ex Z1 being Subset of XV st Z1 = Yy2 /\ [#](XV) & Xx1 is open & Yy2 is open &
[:Xx1, Z1:] in A } by A8,A9,A10,A13;
then p in union AA by A17,TARSKI:def 4;
hence thesis by A7,A8,XBOOLE_0:def 4;
end;
AA c= the topology of T
proof
let t be object;
set A9 = { t };
assume t in AA;
then consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A18: t = [:Xx1, Yy2:] and
A19: ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open
& Yy2 is open & [:Xx1, Y1:] in A;
A9 c= bool the carrier of T
proof
let a be object;
assume a in A9;
then a = t by TARSKI:def 1;
hence thesis by A18;
end;
then reconsider A9 as Subset-Family of T;
A20: A9 c= { [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : X1
in the topology of Y & Y1 in the topology of X }
proof
let x be object;
assume x in A9;
then
A21: x = [:Xx1,Yy2:] by A18,TARSKI:def 1;
Xx1 in the topology of Y & Yy2 in the topology of X by A19,
PRE_TOPC:def 2;
hence thesis by A21;
end;
t = union A9;
then t in { union As where As is Subset-Family of T : As c= { [:X1,Y1
:] where X1 is Subset of Y, Y1 is Subset of X : X1 in the topology of Y & Y1 in
the topology of X}} by A20;
hence thesis by BORSUK_1:def 2;
end;
then
A22: union AA in the topology of T by PRE_TOPC:def 1;
union AA /\ [#]S c= P
proof
let h be object;
assume
A23: h in union AA /\ [#]S;
then h in union AA by XBOOLE_0:def 4;
then consider A2 being set such that
A24: h in A2 and
A25: A2 in AA by TARSKI:def 4;
consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A26: A2 = [:Xx1, Yy2:] and
A27: ex Y1 being Subset of XV st Y1 = Yy2 /\ [#](XV) & Xx1 is open
& Yy2 is open & [:Xx1, Y1:] in A by A25;
consider Yy1 being Subset of XV such that
A28: Yy1 = Yy2 /\ [#](XV) and
Xx1 is open and
Yy2 is open and
A29: [:Xx1, Yy1:] in A by A27;
consider p1, p2 being object such that
A30: p1 in Xx1 and
A31: p2 in Yy2 and
A32: h = [p1, p2] by A24,A26,ZFMISC_1:def 2;
p2 in the carrier of XV by A1,A23,A32,ZFMISC_1:87;
then p2 in Yy2 /\ [#]XV by A31,XBOOLE_0:def 4;
then h in [:Xx1, Yy1:] by A30,A32,A28,ZFMISC_1:87;
hence thesis by A4,A29,TARSKI:def 4;
end;
then P = union AA /\ [#]S by A6;
hence
ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by A22;
end;
given Q being Subset of T such that
A33: Q in the topology of T and
A34: P = Q /\ [#]S;
reconsider Q9 = Q as Subset of T;
Q9 is open by A33,PRE_TOPC:def 2;
then consider A being Subset-Family of T such that
A35: Q9 = union A and
A36: for e be set st e in A ex X1 being Subset of Y, Y1 being Subset
of X st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
reconsider A as Subset-Family of T;
reconsider AA = A | oS as Subset-Family of T|oS;
reconsider AA as Subset-Family of S by PRE_TOPC:8;
reconsider AA as Subset-Family of S;
A37: for e be set st e in AA ex X1 being Subset of Y, Y1 being Subset of
XV st e = [:X1,Y1:] & X1 is open & Y1 is open
proof
let e be set;
assume
A38: e in AA;
then reconsider e9 = e as Subset of T|oS;
consider R being Subset of T such that
A39: R in A and
A40: R /\ oS = e9 by A38,TOPS_2:def 3;
consider X1 being Subset of Y, Y1 being Subset of X such that
A41: R = [:X1,Y1:] and
A42: X1 is open and
A43: Y1 is open by A36,A39;
reconsider D2 = Y1 /\ [#]XV as Subset of XV;
Y1 in the topology of X by A43,PRE_TOPC:def 2;
then D2 in the topology of XV by PRE_TOPC:def 4;
then
A44: D2 is open by PRE_TOPC:def 2;
[#][:Y, XV:] = [:[#]Y, [#]XV:] by BORSUK_1:def 2;
then e9 = [:X1 /\ [#]Y, Y1 /\ [#](XV):] by A40,A41,ZFMISC_1:100;
hence thesis by A42,A44;
end;
A45: union A /\ oS c= union AA
proof
let s be object;
assume
A46: s in union A /\ oS;
then s in union A by XBOOLE_0:def 4;
then consider A1 being set such that
A47: s in A1 and
A48: A1 in A by TARSKI:def 4;
s in oS by A46,XBOOLE_0:def 4;
then
A49: s in A1 /\ oS by A47,XBOOLE_0:def 4;
reconsider A1 as Subset of T by A48;
A1 /\ oS in AA by A48,TOPS_2:31;
hence thesis by A49,TARSKI:def 4;
end;
union AA c= union A by TOPS_2:34;
then union AA c= union A /\ oS by XBOOLE_1:19;
then P = union AA by A34,A35,A45;
then P9 is open by A37,BORSUK_1:5;
hence thesis by PRE_TOPC:def 2;
end;
[#]S c= [#]T by A1,A2,ZFMISC_1:96;
hence thesis by A3,PRE_TOPC:def 4;
end;
Lm4: for X, Y being TopSpace, Z being Subset of [:Y, X:], V being Subset of X
st Z = [:[#]Y, V:] holds the TopStruct of [:Y, X | V:] = the TopStruct of [:Y,
X:] | Z
proof
let X, Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X;
reconsider A = [:Y, X | V:] as SubSpace of [:Y, X:] by Th15;
assume
A1: Z = [:[#]Y, V:];
the carrier of A = [:the carrier of Y, the carrier of (X|V):] by
BORSUK_1:def 2
.= Z by A1,PRE_TOPC:8
.= the carrier of ([:Y, X:]|Z) by PRE_TOPC:8;
then A is SubSpace of [:Y, X:] | Z & [:Y, X:] | Z is SubSpace of A by
TOPMETR:3;
hence thesis by TSEP_1:6;
end;
theorem Th16:
for X being non empty TopSpace, Y being compact non empty
TopSpace, x being Point of X, Z being Subset of [:Y, X:] st Z = [:[#]Y, {x}:]
holds Z is compact
proof
let X be non empty TopSpace, Y be compact non empty TopSpace, x be Point of
X, Z be Subset of [:Y, X:];
reconsider V = {x} as non empty Subset of X;
Y, [: Y, X | V :] are_homeomorphic by Lm3;
then
A1: [:Y, X | V:] is compact by Th14;
assume
A2: Z = [:[#]Y, {x}:];
then the TopStruct of [:Y, X | V:] = the TopStruct of ([:Y, X:] | Z) by Lm4;
hence thesis by A2,A1,COMPTS_1:3;
end;
registration
let X be non empty TopSpace, Y be compact non empty TopSpace,
x be Point of X;
cluster [:Y, X|{x}:] -> compact;
coherence
proof
Y, [: Y, X | {x} :] are_homeomorphic by Lm3;
hence thesis by Th14;
end;
end;
theorem
for X, Y being compact non empty TopSpace, R being Subset-Family of X
st R = { Q where Q is open Subset of X : [:[#]Y, Q:] c= union Base-Appr [#][:Y,
X:] } holds R is open & R is Cover of [#]X
proof
let X, Y be compact non empty TopSpace, R be Subset-Family of X;
assume
A1: R = { Q where Q is open Subset of X : [:[#]Y, Q:] c= union Base-Appr
[#][:Y, X:] };
now
let P be Subset of X;
assume P in R;
then ex E being open Subset of X st E = P & [:[#]Y, E:] c= union Base-Appr
[#][:Y, X:] by A1;
hence P is open;
end;
hence R is open;
[#]X c= union R
proof
let k be object;
assume k in [#]X;
then reconsider k9 = k as Point of X;
reconsider Z = [:[#]Y, {k9}:] as Subset of [:Y, X:];
Z c= [#][:Y, X:];
then Z c= union Base-Appr [#][:Y, X:] by BORSUK_1:13;
then
A2: Base-Appr [#][:Y, X:] is Cover of Z by SETFAM_1:def 11;
Z is compact by Th16;
then consider G being Subset-Family of [:Y, X:] such that
A3: G c= Base-Appr [#][:Y, X:] and
A4: G is Cover of Z and
G is finite by A2;
set uR = union G;
set Q = { x where x is Point of X : [:[#]Y, {x}:] c= uR };
Q c= the carrier of X
proof
let k be object;
assume k in Q;
then ex x1 being Point of X st k = x1 & [:[#]Y, {x1}:] c= uR;
hence thesis;
end;
then reconsider Q as Subset of X;
Z c= union G by A4,SETFAM_1:def 11;
then
A5: k9 in Q;
A6: [:[#]Y, Q:] c= union Base-Appr [#][:Y, X:]
proof
let z be object;
assume z in [:[#]Y, Q:];
then consider x1, x2 be object such that
A7: x1 in [#]Y and
A8: x2 in Q and
A9: z = [x1, x2] by ZFMISC_1:def 2;
consider x29 being Point of X such that
A10: x29 = x2 and
A11: [:[#]Y, {x29}:] c= uR by A8;
x2 in {x29} by A10,TARSKI:def 1;
then
A12: z in [:[#]Y, {x29}:] by A7,A9,ZFMISC_1:87;
uR c= union Base-Appr [#][:Y, X:] by A3,ZFMISC_1:77;
then [:[#]Y, {x29}:] c= union Base-Appr [#][:Y, X:] by A11;
hence thesis by A12;
end;
uR is open by A3,TOPS_2:11,19;
then Q in the topology of X by Th12;
then Q is open by PRE_TOPC:def 2;
then Q in R by A1,A6;
hence thesis by A5,TARSKI:def 4;
end;
hence thesis by SETFAM_1:def 11;
end;
theorem Th18:
for X, Y being compact non empty TopSpace, R being Subset-Family
of X, F being Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open &
R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st
FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } holds R is open & R is Cover
of X
proof
let X, Y be compact non empty TopSpace, R be Subset-Family of X, F be
Subset-Family of [:Y, X:];
assume that
A1: F is Cover of [:Y, X:] and
A2: F is open and
A3: R = { Q where Q is open Subset of X : ex FQ being Subset-Family of
[:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ };
now
let P be Subset of X;
assume P in R;
then
ex E being open Subset of X st E = P & ex FQ being Subset-Family of [:Y
, X:] st FQ c= F & FQ is finite & [: [#]Y, E:] c= union FQ by A3;
hence P is open;
end;
hence R is open;
A4: union F = [#] [:Y, X:] by A1,SETFAM_1:45;
[#]X c= union R
proof
let k be object;
assume k in [#]X;
then reconsider k9 = k as Point of X;
reconsider Z = [:[#]Y, {k9}:] as Subset of [:Y, X:];
F is Cover of Z & Z is compact by A4,Th16,SETFAM_1:def 11;
then consider G being Subset-Family of [:Y, X:] such that
A5: G c= F and
A6: G is Cover of Z and
A7: G is finite by A2;
set uR = union G;
set Q = { x where x is Point of X : [:[#]Y, {x}:] c= uR };
Q c= the carrier of X
proof
let k be object;
assume k in Q;
then ex x1 being Point of X st k = x1 & [:[#]Y, {x1}:] c= uR;
hence thesis;
end;
then reconsider Q as Subset of X;
Z c= union G by A6,SETFAM_1:def 11;
then
A8: k9 in Q;
A9: ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
[#]Y, Q:] c= union FQ
proof
take G;
[:[#]Y, Q:] c= union G
proof
let z be object;
assume z in [:[#]Y, Q:];
then consider x1, x2 be object such that
A10: x1 in [#]Y and
A11: x2 in Q and
A12: z = [x1, x2] by ZFMISC_1:def 2;
consider x29 being Point of X such that
A13: x29 = x2 and
A14: [:[#]Y, {x29}:] c= uR by A11;
x2 in {x29} by A13,TARSKI:def 1;
then z in [:[#]Y, {x29}:] by A10,A12,ZFMISC_1:87;
hence thesis by A14;
end;
hence thesis by A5,A7;
end;
uR is open by A2,A5,TOPS_2:11,19;
then Q in the topology of X by Th12;
then Q is open by PRE_TOPC:def 2;
then Q in R by A3,A9;
hence thesis by A8,TARSKI:def 4;
end;
hence thesis by SETFAM_1:def 11;
end;
theorem Th19:
for X, Y being compact non empty TopSpace, R being Subset-Family
of X, F being Subset-Family of [:Y, X:] st F is Cover of [:Y, X:] & F is open &
R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y, X:] st
FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } holds ex C being
Subset-Family of X st C c= R & C is finite & C is Cover of X
proof
let X, Y be compact non empty TopSpace, R be Subset-Family of X, F be
Subset-Family of [:Y, X:];
assume F is Cover of [:Y, X:] & F is open & R = { Q where Q is open Subset
of X : ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:[#]Y
, Q:] c= union FQ };
then R is open & R is Cover of X by Th18;
then
ex G being Subset-Family of X st G c= R & G is Cover of X & G is finite
by COMPTS_1:def 1;
hence thesis;
end;
theorem Th20:
for X, Y being compact non empty TopSpace, F being Subset-Family
of [:Y, X:] st F is Cover of [:Y, X:] & F is open ex G being Subset-Family of
[:Y, X:] st G c= F & G is Cover of [:Y, X:] & G is finite
proof
let X, Y be compact non empty TopSpace;
let F be Subset-Family of [:Y, X:];
set R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,
X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ };
R c= bool the carrier of X
proof
let s be object;
assume s in R;
then ex Q1 being open Subset of X st s = Q1 & ex FQ being Subset-Family of
[:Y, X:] st FQ c= F & FQ is finite & [: [#]Y, Q1:] c= union FQ;
hence thesis;
end;
then reconsider R as Subset-Family of X;
reconsider R as Subset-Family of X;
defpred P[object,object] means
ex D1 being set, FQ being Subset-Family of [:Y, X:] st
D1 = $1 & FQ c= F &
FQ is finite & [:[#]Y, D1:] c= union FQ & $2 = FQ;
deffunc F(set) = [:[#]Y, $1:];
assume F is Cover of [:Y, X:] & F is open;
then consider C being Subset-Family of X such that
A1: C c= R and
A2: C is finite and
A3: C is Cover of X by Th19;
set CX = { F(f) where f is Subset of X : f in C };
CX c= bool the carrier of [:Y, X:]
proof
let s be object;
assume s in CX;
then consider f1 being Subset of X such that
A4: s = F(f1) and
f1 in C;
[:[#]Y, f1:] c= the carrier of [:Y, X:];
hence thesis by A4;
end;
then reconsider CX as Subset-Family of [:Y, X:];
reconsider CX as Subset-Family of [:Y, X:];
A5: for e be object st e in C ex u be object st P[e,u]
proof
let e be object;
assume e in C;
then e in R by A1;
then ex Q1 being open Subset of X st Q1 = e & ex FQ being Subset-Family of
[:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q1:] c= union FQ;
hence thesis;
end;
consider t being Function such that
A6: dom t = C & for s being object st s in C holds P[s, t.s] from CLASSES1
:sch 1(A5);
set G = union rng t;
A7: union rng t c= F
proof
let k be object;
assume k in union rng t;
then consider K be set such that
A8: k in K and
A9: K in rng t by TARSKI:def 4;
consider x1 be object such that
A10: x1 in dom t & K = t.x1 by A9,FUNCT_1:def 3;
reconsider x1 as set by TARSKI:1;
P[x1, t.x1] by A6,A10;
then ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
[#]Y, x1:] c= union FQ & K = FQ by A10;
hence thesis by A8;
end;
G c= bool the carrier of [:Y, X:]
proof
let s be object;
assume s in G;
then s in F by A7;
hence thesis;
end;
then reconsider G as Subset-Family of [:Y, X:];
reconsider G as Subset-Family of [:Y, X:];
take G;
thus G c= F by A7;
union CX = [:[#]Y, union C:]
proof
hereby
let g be object;
assume g in union CX;
then consider GG being set such that
A11: g in GG and
A12: GG in CX by TARSKI:def 4;
consider FF being Subset of X such that
A13: GG = [:[#]Y, FF:] and
A14: FF in C by A12;
consider g1, g2 be object such that
A15: g1 in [#]Y and
A16: g2 in FF and
A17: g = [g1, g2] by A11,A13,ZFMISC_1:def 2;
g2 in union C by A14,A16,TARSKI:def 4;
hence g in [:[#]Y, union C:] by A15,A17,ZFMISC_1:87;
end;
let g be object;
assume g in [:[#]Y, union C:];
then consider g1, g2 be object such that
A18: g1 in [#]Y and
A19: g2 in union C and
A20: g = [g1, g2] by ZFMISC_1:def 2;
consider GG being set such that
A21: g2 in GG and
A22: GG in C by A19,TARSKI:def 4;
GG in { Q where Q is open Subset of X : ex FQ being Subset-Family of
[:Y, X:] st FQ c= F & FQ is finite & [:[#]Y, Q:] c= union FQ } by A1,A22;
then consider Q1 being open Subset of X such that
A23: GG = Q1 and
ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
[#]Y, Q1:] c= union FQ;
A24: [:[#]Y, Q1:] in CX by A22,A23;
g in [:[#]Y, Q1:] by A18,A20,A21,A23,ZFMISC_1:87;
hence thesis by A24,TARSKI:def 4;
end;
then
A25: union CX = [:[#]Y, [#]X:] by A3,SETFAM_1:45
.= [#][:Y, X:] by BORSUK_1:def 2;
[#][:Y, X:] c= union union rng t
proof
let d be object;
assume d in [#][:Y, X:];
then consider CC being set such that
A26: d in CC and
A27: CC in CX by A25,TARSKI:def 4;
consider Cc being Subset of X such that
A28: CC = [:[#]Y, Cc:] and
A29: Cc in C by A27;
Cc in R by A1,A29;
then consider Qq being open Subset of X such that
A30: Cc = Qq and
ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
[#]Y, Qq:] c= union FQ;
P[Cc, t.Cc] by A6,A29;
then consider FQ1 being Subset-Family of [:Y, X:] such that
FQ1 c= F and
FQ1 is finite and
A31: [:[#]Y, Qq:] c= union FQ1 and
A32: t.Qq = FQ1 by A30;
consider DC being set such that
A33: d in DC and
A34: DC in FQ1 by A26,A28,A30,A31,TARSKI:def 4;
FQ1 in rng t by A6,A29,A30,A32,FUNCT_1:def 3;
then DC in union rng t by A34,TARSKI:def 4;
hence thesis by A33,TARSKI:def 4;
end;
hence G is Cover of [:Y, X:] by SETFAM_1:def 11;
A35: for X1 be set st X1 in rng t holds X1 is finite
proof
let X1 be set;
assume X1 in rng t;
then consider x1 be object such that
A36: x1 in dom t and
A37: X1 = t.x1 by FUNCT_1:def 3;
reconsider x1 as set by TARSKI:1;
P[x1, t.x1] by A6,A36;
then ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite & [:
[#]Y, x1:] c= union FQ & t.x1 = FQ;
hence thesis by A37;
end;
rng t is finite by A2,A6,FINSET_1:8;
hence thesis by A35,FINSET_1:7;
end;
Lm5: for T1, T2 be compact non empty TopSpace holds [:T1, T2:] is compact
by Th20;
registration
let T1,T2 be compact TopSpace;
cluster [:T1, T2:] -> compact;
coherence
proof
per cases;
suppose
T1 is non empty & T2 is non empty;
hence thesis by Lm5;
end;
suppose
T1 is empty & T2 is empty;
hence thesis;
end;
suppose
T1 is empty & T2 is non empty;
hence thesis;
end;
suppose
T1 is non empty & T2 is empty;
hence thesis;
end;
end;
end;
Lm6: for X, Y being TopSpace, XV being SubSpace of X holds [:XV, Y:] is
SubSpace of [:X, Y:]
proof
let X, Y be TopSpace, XV be SubSpace of X;
set S = [:XV, Y:], T = [:X, Y:];
A1: the carrier of S = [:the carrier of XV, the carrier of Y:] by
BORSUK_1:def 2;
A2: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] & the
carrier of XV c= the carrier of X by BORSUK_1:1,def 2;
A3: for P being Subset of S holds P in the topology of S iff ex Q being
Subset of T st Q in the topology of T & P = Q /\ [#]S
proof
reconsider oS = [#]S as Subset of T by A1,A2,ZFMISC_1:96;
let P be Subset of S;
reconsider P9 = P as Subset of S;
hereby
assume P in the topology of S;
then P9 is open by PRE_TOPC:def 2;
then consider A being Subset-Family of S such that
A4: P9 = union A and
A5: for e be set st e in A ex X1 being Subset of XV, Y1 being Subset
of Y st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
set AA = {[:X1, Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1
being Subset of XV st Y1 = X1 /\ [#](XV) & X1 is open & Y2 is open & [:Y1, Y2:]
in A };
AA c= bool the carrier of T
proof
let a be object;
assume a in AA;
then
ex Xx1 being Subset of X, Yy2 being Subset of Y st a = [: Xx1, Yy2
:] & ex Y1 being Subset of XV st Y1 = Xx1 /\ [#](XV) & Xx1 is open & Yy2 is
open & [:Y1, Yy2:] in A;
hence thesis;
end;
then reconsider AA as Subset-Family of T;
reconsider AA as Subset-Family of T;
A6: P c= union AA /\ [#]S
proof
let p be object;
assume p in P;
then consider A1 be set such that
A7: p in A1 and
A8: A1 in A by A4,TARSKI:def 4;
reconsider A1 as Subset of S by A8;
consider X2 being Subset of XV, Y2 being Subset of Y such that
A9: A1 = [:X2,Y2:] and
A10: X2 is open and
A11: Y2 is open by A5,A8;
X2 in the topology of XV by A10,PRE_TOPC:def 2;
then consider Q1 being Subset of X such that
A12: Q1 in the topology of X and
A13: X2 = Q1 /\ [#]XV by PRE_TOPC:def 4;
consider p1, p2 being object such that
A14: p1 in X2 and
A15: p2 in Y2 & p = [p1, p2] by A7,A9,ZFMISC_1:def 2;
reconsider Q1 as Subset of X;
set EX = [:Q1, Y2:];
p1 in Q1 by A14,A13,XBOOLE_0:def 4;
then
A16: p in EX by A15,ZFMISC_1:87;
Q1 is open by A12,PRE_TOPC:def 2;
then
EX in {[:Xx1, Yy2:] where Xx1 is Subset of X, Yy2 is Subset of Y:
ex Z1 being Subset of XV st Z1 = Xx1 /\ [#](XV) & Xx1 is open & Yy2 is open &
[:Z1, Yy2:] in A } by A8,A9,A11,A13;
then p in union AA by A16,TARSKI:def 4;
hence thesis by A7,A8,XBOOLE_0:def 4;
end;
AA c= the topology of T
proof
let t be object;
set A9 = { t };
assume t in AA;
then consider Xx1 being Subset of X, Yy2 being Subset of Y such that
A17: t = [:Xx1, Yy2:] and
A18: ex Y1 being Subset of XV st Y1 = Xx1 /\ [#](XV) & Xx1 is open
& Yy2 is open & [:Y1, Yy2:] in A;
A9 c= bool the carrier of T
proof
let a be object;
assume a in A9;
then a = t by TARSKI:def 1;
hence thesis by A17;
end;
then reconsider A9 as Subset-Family of T;
A19: A9 c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : X1
in the topology of X & Y1 in the topology of Y }
proof
let x be object;
assume x in A9;
then
A20: x = [:Xx1,Yy2:] by A17,TARSKI:def 1;
Xx1 in the topology of X & Yy2 in the topology of Y by A18,
PRE_TOPC:def 2;
hence thesis by A20;
end;
t = union A9;
then t in { union As where As is Subset-Family of T : As c= { [:X1,Y1
:] where X1 is Subset of X, Y1 is Subset of Y : X1 in the topology of X & Y1 in
the topology of Y}} by A19;
hence thesis by BORSUK_1:def 2;
end;
then
A21: union AA in the topology of T by PRE_TOPC:def 1;
union AA /\ [#]S c= P
proof
let h be object;
assume
A22: h in union AA /\ [#]S;
then h in union AA by XBOOLE_0:def 4;
then consider A2 being set such that
A23: h in A2 and
A24: A2 in AA by TARSKI:def 4;
consider Xx1 being Subset of X, Yy2 being Subset of Y such that
A25: A2 = [:Xx1, Yy2:] and
A26: ex Y1 being Subset of XV st Y1 = Xx1 /\ [#]XV & Xx1 is open &
Yy2 is open & [:Y1, Yy2:] in A by A24;
consider Yy1 being Subset of XV such that
A27: Yy1 = Xx1 /\ [#]XV and
Xx1 is open and
Yy2 is open and
A28: [:Yy1, Yy2:] in A by A26;
consider p1, p2 being object such that
A29: p1 in Xx1 and
A30: p2 in Yy2 and
A31: h = [p1, p2] by A23,A25,ZFMISC_1:def 2;
p1 in the carrier of XV by A1,A22,A31,ZFMISC_1:87;
then p1 in Xx1 /\ [#](XV) by A29,XBOOLE_0:def 4;
then h in [:Yy1, Yy2:] by A30,A31,A27,ZFMISC_1:87;
hence thesis by A4,A28,TARSKI:def 4;
end;
then P = union AA /\ [#]S by A6;
hence
ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by A21;
end;
given Q being Subset of T such that
A32: Q in the topology of T and
A33: P = Q /\ [#]S;
reconsider Q9 = Q as Subset of T;
Q9 is open by A32,PRE_TOPC:def 2;
then consider A being Subset-Family of T such that
A34: Q9 = union A and
A35: for e be set st e in A ex X1 being Subset of X, Y1 being Subset
of Y st e = [:X1,Y1:] & X1 is open & Y1 is open by BORSUK_1:5;
reconsider A as Subset-Family of T;
reconsider AA = A | oS as Subset-Family of T|oS;
reconsider AA as Subset-Family of S by PRE_TOPC:8;
reconsider AA as Subset-Family of S;
A36: for e be set st e in AA ex X1 being Subset of XV, Y1 being Subset of
Y st e = [:X1,Y1:] & X1 is open & Y1 is open
proof
let e be set;
assume
A37: e in AA;
then reconsider e9 = e as Subset of T|oS;
consider R being Subset of T such that
A38: R in A and
A39: R /\ oS = e9 by A37,TOPS_2:def 3;
consider X1 being Subset of X, Y1 being Subset of Y such that
A40: R = [:X1,Y1:] and
A41: X1 is open and
A42: Y1 is open by A35,A38;
reconsider D2 = X1 /\ [#](XV) as Subset of XV;
X1 in the topology of X by A41,PRE_TOPC:def 2;
then D2 in the topology of XV by PRE_TOPC:def 4;
then
A43: D2 is open by PRE_TOPC:def 2;
[#][:XV, Y:] = [:[#]XV, [#]Y:] by BORSUK_1:def 2;
then e9 = [:X1 /\ [#]XV, Y1 /\ [#]Y:] by A39,A40,ZFMISC_1:100;
hence thesis by A42,A43;
end;
A44: union A /\ oS c= union AA
proof
let s be object;
assume
A45: s in union A /\ oS;
then s in union A by XBOOLE_0:def 4;
then consider A1 being set such that
A46: s in A1 and
A47: A1 in A by TARSKI:def 4;
s in oS by A45,XBOOLE_0:def 4;
then
A48: s in A1 /\ oS by A46,XBOOLE_0:def 4;
reconsider A1 as Subset of T by A47;
A1 /\ oS in AA by A47,TOPS_2:31;
hence thesis by A48,TARSKI:def 4;
end;
union AA c= union A by TOPS_2:34;
then union AA c= union A /\ oS by XBOOLE_1:19;
then P = union AA by A33,A34,A44;
then P9 is open by A36,BORSUK_1:5;
hence thesis by PRE_TOPC:def 2;
end;
[#]S c= [#]T by A1,A2,ZFMISC_1:96;
hence thesis by A3,PRE_TOPC:def 4;
end;
theorem Th21:
for X, Y being TopSpace, XV being SubSpace of X, YV being
SubSpace of Y holds [:XV, YV:] is SubSpace of [:X, Y:]
proof
let X, Y be TopSpace, XV be SubSpace of X, YV be SubSpace of Y;
[:XV, Y:] is SubSpace of [:X, Y:] & [:XV, YV:] is SubSpace of [:XV, Y:]
by Lm6,Th15;
hence thesis by TSEP_1:7;
end;
theorem Th22:
for X, Y being TopSpace, Z being Subset of [:Y, X:], V being
Subset of X, W being Subset of Y st Z = [:W, V:] holds the TopStruct of [:Y | W
, X | V:] = the TopStruct of [:Y, X:] | Z
proof
let X, Y be TopSpace, Z be Subset of [:Y, X:], V be Subset of X, W be Subset
of Y;
reconsider A = [:Y | W, X | V:] as SubSpace of [:Y, X:] by Th21;
assume
A1: Z = [:W, V:];
the carrier of A = [:the carrier of (Y|W), the carrier of (X|V):] by
BORSUK_1:def 2
.= [:the carrier of (Y|W), V:] by PRE_TOPC:8
.= Z by A1,PRE_TOPC:8
.= the carrier of ([:Y, X:]|Z) by PRE_TOPC:8;
then A is SubSpace of [:Y, X:] | Z & [:Y, X:] | Z is SubSpace of A by
TOPMETR:3;
hence thesis by TSEP_1:6;
end;
registration
let T be TopSpace;
cluster empty for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
registration
let T be TopSpace, P be compact Subset of T;
cluster T | P -> compact;
coherence
proof
per cases;
suppose
P is non empty;
hence thesis by COMPTS_1:3;
end;
suppose
P is empty;
hence thesis;
end;
end;
end;
theorem
for T1, T2 being TopSpace, S1 being Subset of T1, S2 being Subset of
T2 st S1 is compact & S2 is compact holds [:S1, S2:] is compact Subset of [:T1,
T2:]
proof
let T1, T2 be TopSpace, S1 be Subset of T1, S2 be Subset of T2;
assume that
A1: S1 is compact and
A2: S2 is compact;
per cases;
suppose
A3: S1 is non empty & S2 is non empty;
then (ex x be object st x in S1 )& ex y be object st y in S2;
then reconsider T1, T2 as non empty TopSpace;
reconsider S2 as compact non empty Subset of T2 by A2,A3;
reconsider S1 as compact non empty Subset of T1 by A1,A3;
reconsider X = [:S1, S2:] as Subset of [:T1, T2:];
the TopStruct of [:T1|S1, T2|S2:] = the TopStruct of ([:T1, T2:] | X)
by Th22;
hence thesis by COMPTS_1:3;
end;
suppose
S1 is empty & S2 is non empty;
then reconsider S1 as empty Subset of T1;
[:S1, S2:] = {}([:T1, T2:]);
hence thesis;
end;
suppose
S1 is non empty & S2 is empty;
then reconsider S2 as empty Subset of T2;
[:S1, S2:] = {}([:T1, T2:]);
hence thesis;
end;
suppose
S1 is empty & S2 is empty;
then reconsider S2 as empty Subset of T2;
[:S1, S2:] = {}([:T1, T2:]);
hence thesis;
end;
end;