:: Properties of the Product of Compact Topological Spaces :: by Adam Grabowski :: :: Received February 13, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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; begin :: Preliminaries theorem :: BORSUK_3:1 for S, T being TopSpace holds [#][:S, T:] = [:[#]S, [#]T:]; theorem :: BORSUK_3:2 for X, Y being non empty TopSpace, x being Point of X holds Y --> x is continuous Function of Y, X|{x}; registration let T be TopStruct; cluster id T -> being_homeomorphism; end; definition let S, T be TopStruct; redefine pred S, T are_homeomorphic; reflexivity; end; definition let S, T be non empty TopStruct; redefine pred S, T are_homeomorphic; reflexivity; symmetry; end; theorem :: BORSUK_3:3 for S, T, V being non empty TopSpace st S, T are_homeomorphic & T, V are_homeomorphic holds S, V are_homeomorphic; begin :: On the projections and empty topological spaces registration let T be TopStruct, P be empty Subset of T; cluster T | P -> empty; end; registration cluster empty -> compact for TopSpace; end; theorem :: BORSUK_3:4 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; theorem :: BORSUK_3:5 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; theorem :: BORSUK_3:6 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:>; theorem :: BORSUK_3:7 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:>; theorem :: BORSUK_3:8 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; theorem :: BORSUK_3:9 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; begin :: On the product of compact spaces theorem :: BORSUK_3:10 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; theorem :: BORSUK_3:11 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 }; theorem :: BORSUK_3:12 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; theorem :: BORSUK_3:13 for X, Y being non empty TopSpace, x being Point of X holds [: X | {x}, Y :], Y are_homeomorphic; theorem :: BORSUK_3:14 for S, T being non empty TopSpace st S, T are_homeomorphic & S is compact holds T is compact; theorem :: BORSUK_3:15 for X, Y being TopSpace, XV being SubSpace of X holds [:Y, XV:] is SubSpace of [:Y, X:]; theorem :: BORSUK_3:16 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; registration let X be non empty TopSpace, Y be compact non empty TopSpace, x be Point of X; cluster [:Y, X|{x}:] -> compact; end; theorem :: BORSUK_3:17 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; theorem :: BORSUK_3:18 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; theorem :: BORSUK_3:19 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; theorem :: BORSUK_3:20 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; registration let T1,T2 be compact TopSpace; cluster [:T1, T2:] -> compact; end; theorem :: BORSUK_3:21 for X, Y being TopSpace, XV being SubSpace of X, YV being SubSpace of Y holds [:XV, YV:] is SubSpace of [:X, Y:]; theorem :: BORSUK_3:22 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; registration let T be TopSpace; cluster empty for Subset of T; end; registration let T be TopSpace, P be compact Subset of T; cluster T | P -> compact; end; theorem :: BORSUK_3:23 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:];