:: Continuity of Mappings over the Union of Subspaces :: by Zbigniew Karno :: :: Received May 22, 1992 :: Copyright (c) 1992-2018 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, PRE_TOPC, TARSKI, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4, STRUCT_0, RCOMP_1, SETFAM_1, CONNSP_2, ORDINAL2, FUNCOP_1, FUNCT_3, ZFMISC_1, TSEP_1, CONNSP_1, TMAP_1, PARTFUN1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, CONNSP_1, CONNSP_2, BORSUK_1, TSEP_1; constructors SETFAM_1, FUNCT_4, CONNSP_1, BORSUK_1, TSEP_1, FUNCOP_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC, BORSUK_1, TSEP_1, RELSET_1, PARTFUN1, TOPS_1; requirements BOOLE, SUBSET; begin :: 1. Set-Theoretic Preliminaries. registration let X be non empty TopSpace; let X1, X2 be non empty SubSpace of X; cluster X1 union X2 -> TopSpace-like; end; definition let A,B be non empty set; let A1,A2 be non empty Subset of A; let f1 be Function of A1,B, f2 be Function of A2,B; func f1 union f2 -> Function of A1 \/ A2,B equals :: TMAP_1:def 1 f1 +* f2; end; theorem :: TMAP_1:1 for A, B be non empty set, A1, A2 being non empty Subset of A st A1 misses A2 for f1 being Function of A1,B, f2 being Function of A2,B holds f1|(A1 /\ A2) = f2|(A1 /\ A2) & (f1 union f2)|A1 = f1 & (f1 union f2)|A2 = f2; reserve A, B for non empty set, A1, A2, A3 for non empty Subset of A; theorem :: TMAP_1:2 for g being Function of A1 \/ A2,B, g1 being Function of A1,B, g2 being Function of A2,B st g|A1 = g1 & g|A2 = g2 holds g = g1 union g2; theorem :: TMAP_1:3 for f1 being Function of A1,B, f2 being Function of A2,B st f1|(A1 /\ A2) = f2|(A1 /\ A2) holds f1 union f2 = f2 union f1; theorem :: TMAP_1:4 for A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2 \/ A3 for f1 being Function of A1,B, f2 being Function of A2,B, f3 being Function of A3,B st f1|(A1 /\ A2) = f2|(A1 /\ A2) & f2|(A2 /\ A3) = f3|(A2 /\ A3) & f1|(A1 /\ A3) = f3|(A1 /\ A3) for f12 being Function of A12,B, f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds f12 union f3 = f1 union f23; theorem :: TMAP_1:5 for f1 being Function of A1,B, f2 being Function of A2,B st f1|(A1 /\ A2) = f2|(A1 /\ A2) holds (A1 is Subset of A2 iff f1 union f2 = f2) & (A2 is Subset of A1 iff f1 union f2 = f1); begin :: 2. Selected Properties of Subspaces of Topological Spaces. reserve X for TopSpace; theorem :: TMAP_1:6 for X being TopStruct, X0 being SubSpace of X holds the TopStruct of X0 is strict SubSpace of X; theorem :: TMAP_1:7 for X being TopStruct for X1,X2 being TopSpace st X1 = the TopStruct of X2 holds X1 is SubSpace of X iff X2 is SubSpace of X; theorem :: TMAP_1:8 for X1,X2 being TopSpace st X2 = the TopStruct of X1 holds X1 is closed SubSpace of X iff X2 is closed SubSpace of X; theorem :: TMAP_1:9 for X1,X2 being TopSpace st X2 = the TopStruct of X1 holds X1 is open SubSpace of X iff X2 is open SubSpace of X; reserve X for non empty TopSpace; reserve X1, X2 for non empty SubSpace of X; theorem :: TMAP_1:10 X1 is SubSpace of X2 implies for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1; theorem :: TMAP_1:11 for x being Point of X1 union X2 holds (ex x1 being Point of X1 st x1 = x) or ex x2 being Point of X2 st x2 = x; theorem :: TMAP_1:12 X1 meets X2 implies for x being Point of X1 meet X2 holds (ex x1 being Point of X1 st x1 = x) & ex x2 being Point of X2 st x2 = x; theorem :: TMAP_1:13 for x being Point of X1 union X2 for F1 being Subset of X1, F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 ex H being Subset of X1 union X2 st H is closed & x in H & H c= F1 \/ F2; theorem :: TMAP_1:14 for x being Point of X1 union X2 for U1 being Subset of X1, U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 ex V being Subset of X1 union X2 st V is open & x in V & V c= U1 \/ U2; theorem :: TMAP_1:15 for x being Point of X1 union X2 for x1 being Point of X1, x2 being Point of X2 st x1 = x & x2 = x for A1 being a_neighborhood of x1, A2 being a_neighborhood of x2 ex V being Subset of X1 union X2 st V is open & x in V & V c= A1 \/ A2; theorem :: TMAP_1:16 for x being Point of X1 union X2 for x1 being Point of X1, x2 being Point of X2 st x1 = x & x2 = x for A1 being a_neighborhood of x1, A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2; reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X; theorem :: TMAP_1:17 X0 is SubSpace of X1 implies X0 meets X1 & X1 meets X0; theorem :: TMAP_1:18 X0 is SubSpace of X1 & (X0 meets X2 or X2 meets X0) implies X1 meets X2 & X2 meets X1; theorem :: TMAP_1:19 X0 is SubSpace of X1 & (X1 misses X2 or X2 misses X1) implies X0 misses X2 & X2 misses X0; theorem :: TMAP_1:20 X0 union X0 = the TopStruct of X0; theorem :: TMAP_1:21 X0 meet X0 = the TopStruct of X0; theorem :: TMAP_1:22 Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies Y1 union Y2 is SubSpace of X1 union X2; theorem :: TMAP_1:23 Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 implies Y1 meet Y2 is SubSpace of X1 meet X2; theorem :: TMAP_1:24 X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 union X2 is SubSpace of X0; theorem :: TMAP_1:25 X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0; theorem :: TMAP_1:26 ((X1 misses X0 or X0 misses X1) & (X2 meets X0 or X0 meets X2) implies (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) & ((X1 meets X0 or X0 meets X1) & (X2 misses X0 or X0 misses X2) implies (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1); theorem :: TMAP_1:27 X1 meets X2 implies (X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2) & (X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0); theorem :: TMAP_1:28 X1 is SubSpace of X0 & (X0 misses X2 or X2 misses X0) implies X0 meet (X1 union X2) = the TopStruct of X1 & X0 meet (X2 union X1) = the TopStruct of X1; theorem :: TMAP_1:29 X1 meets X2 implies (X1 is SubSpace of X0 implies (X0 meet X2) meets X1 & (X2 meet X0) meets X1) & (X2 is SubSpace of X0 implies (X1 meet X0) meets X2 & (X0 meet X1) meets X2); theorem :: TMAP_1:30 X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2) implies Y1 misses X2 & Y2 misses X1; theorem :: TMAP_1:31 X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is SubSpace of Y1 union Y2 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 implies Y1 meets X1 union X2 & Y2 meets X1 union X2; theorem :: TMAP_1:32 X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & the TopStruct of X = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2 ) is SubSpace of X1 meet X2 implies Y1 meets X1 union X2 & Y2 meets X1 union X2 ; theorem :: TMAP_1:33 X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & not X1 union X2 is SubSpace of Y1 union Y2 & the TopStruct of X = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2 implies Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2; theorem :: TMAP_1:34 ((X1 union X2) meets X0 iff X1 meets X0 or X2 meets X0) & (X0 meets (X1 union X2) iff X0 meets X1 or X0 meets X2); theorem :: TMAP_1:35 ((X1 union X2) misses X0 iff X1 misses X0 & X2 misses X0) & (X0 misses (X1 union X2) iff X0 misses X1 & X0 misses X2); theorem :: TMAP_1:36 X1 meets X2 implies ((X1 meet X2) meets X0 implies X1 meets X0 & X2 meets X0) & (X0 meets (X1 meet X2) implies X0 meets X1 & X0 meets X2); theorem :: TMAP_1:37 X1 meets X2 implies (X1 misses X0 or X2 misses X0 implies (X1 meet X2) misses X0) & (X0 misses X1 or X0 misses X2 implies X0 misses (X1 meet X2)); theorem :: TMAP_1:38 for X0 being closed non empty SubSpace of X holds X0 meets X1 implies X0 meet X1 is closed SubSpace of X1; theorem :: TMAP_1:39 for X0 being open non empty SubSpace of X holds X0 meets X1 implies X0 meet X1 is open SubSpace of X1; theorem :: TMAP_1:40 for X0 being closed non empty SubSpace of X holds X1 is SubSpace of X0 & X0 misses X2 implies X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1; theorem :: TMAP_1:41 for X0 being open non empty SubSpace of X holds X1 is SubSpace of X0 & X0 misses X2 implies X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1; begin :: 3. Continuity of Mappings. definition let X, Y be non empty TopSpace, f be Function of X,Y, x be Point of X; pred f is_continuous_at x means :: TMAP_1:def 2 for G being a_neighborhood of f.x ex H being a_neighborhood of x st f.:H c= G; end; notation let X, Y be non empty TopSpace, f be Function of X,Y, x be Point of X; antonym f is_not_continuous_at x for f is_continuous_at x; end; reserve X, Y for non empty TopSpace; reserve f for Function of X,Y; theorem :: TMAP_1:42 for x being Point of X holds f is_continuous_at x iff for G being a_neighborhood of f.x holds f"G is a_neighborhood of x; theorem :: TMAP_1:43 for x being Point of X holds f is_continuous_at x iff for G being Subset of Y st G is open & f.x in G ex H being Subset of X st H is open & x in H & f.:H c= G; theorem :: TMAP_1:44 f is continuous iff for x being Point of X holds f is_continuous_at x; theorem :: TMAP_1:45 for X,Y,Z being non empty TopSpace st the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y for f being Function of X ,Y, g being Function of X,Z st f = g holds for x being Point of X holds f is_continuous_at x implies g is_continuous_at x; theorem :: TMAP_1:46 for X,Y,Z being non empty TopSpace st the carrier of X = the carrier of Y & the topology of Y c= the topology of X for f being Function of X ,Z, g being Function of Y,Z st f = g holds for x being Point of X, y being Point of Y st x = y holds g is_continuous_at y implies f is_continuous_at x; reserve X,Y,Z for non empty TopSpace; reserve f for Function of X,Y, g for Function of Y,Z; theorem :: TMAP_1:47 for x being Point of X, y being Point of Y st y = f.x holds f is_continuous_at x & g is_continuous_at y implies g*f is_continuous_at x; theorem :: TMAP_1:48 for y being Point of Y holds f is continuous & g is_continuous_at y implies for x being Point of X st x in f"{y} holds g*f is_continuous_at x; theorem :: TMAP_1:49 for x being Point of X holds f is_continuous_at x & g is continuous implies g*f is_continuous_at x; theorem :: TMAP_1:50 f is continuous Function of X,Y iff for x being Point of X holds f is_continuous_at x; theorem :: TMAP_1:51 for X,Y,Z being non empty TopSpace st the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y for f being continuous Function of X,Y holds f is continuous Function of X,Z; theorem :: TMAP_1:52 for X,Y,Z being non empty TopSpace st the carrier of X = the carrier of Y & the topology of Y c= the topology of X for f being continuous Function of Y,Z holds f is continuous Function of X,Z; definition let S,T be 1-sorted; let f be Function of S,T; let R be 1-sorted such that the carrier of R c= the carrier of S; func f|R -> Function of R,T equals :: TMAP_1:def 3 f | the carrier of R; end; definition let X, Y be non empty TopSpace, f be Function of X,Y; let X0 be SubSpace of X; redefine func f | X0 equals :: TMAP_1:def 4 f | the carrier of X0; end; reserve X, Y for non empty TopSpace, X0 for non empty SubSpace of X; reserve f for Function of X,Y; theorem :: TMAP_1:53 for f0 being Function of X0,Y st for x being Point of X st x in the carrier of X0 holds f.x = f0.x holds f|X0 = f0; theorem :: TMAP_1:54 the TopStruct of X0 = the TopStruct of X implies f = f|X0; theorem :: TMAP_1:55 for A being Subset of X st A c= the carrier of X0 holds f.:A = (f|X0) .:A; theorem :: TMAP_1:56 for B being Subset of Y st f"B c= the carrier of X0 holds f"B = (f|X0) "B; theorem :: TMAP_1:57 for g being Function of X0,Y ex h being Function of X,Y st h|X0 = g; reserve f for Function of X,Y, X0 for non empty SubSpace of X; theorem :: TMAP_1:58 for x being Point of X, x0 being Point of X0 st x = x0 holds f is_continuous_at x implies f|X0 is_continuous_at x0; ::Characterizations of Continuity at the Point by Local one. theorem :: TMAP_1:59 for A being Subset of X, x being Point of X, x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds f is_continuous_at x iff f|X0 is_continuous_at x0; theorem :: TMAP_1:60 for A being Subset of X, x being Point of X, x0 being Point of X0 st A is open & x in A & A c= the carrier of X0 & x = x0 holds f is_continuous_at x iff f|X0 is_continuous_at x0; theorem :: TMAP_1:61 for X0 being open non empty SubSpace of X, x being Point of X, x0 being Point of X0 st x = x0 holds f is_continuous_at x iff f|X0 is_continuous_at x0; registration let X,Y; let f be continuous Function of X,Y, X0 be non empty SubSpace of X; cluster f|X0 -> continuous; end; theorem :: TMAP_1:62 for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X, f being Function of X,Y, g being Function of Y,Z holds (g*f)|X0 = g*(f|X0 ); theorem :: TMAP_1:63 for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X, g being Function of Y,Z, f being Function of X,Y st g is continuous & f| X0 is continuous holds (g*f)|X0 is continuous; theorem :: TMAP_1:64 for X,Y,Z being non empty TopSpace, X0 being non empty SubSpace of X, g being continuous Function of Y,Z, f being Function of X,Y st f|X0 is continuous Function of X0,Y holds (g*f)|X0 is continuous Function of X0,Z; ::(Definition of the restriction mapping - special case.) definition let X,Y be non empty TopSpace, X0, X1 be SubSpace of X, g be Function of X0, Y; assume X1 is SubSpace of X0; func g|X1 -> Function of X1,Y equals :: TMAP_1:def 5 g | the carrier of X1; end; reserve X, Y for non empty TopSpace, X0, X1 for non empty SubSpace of X; reserve f for Function of X,Y, g for Function of X0,Y; theorem :: TMAP_1:65 X1 is SubSpace of X0 implies for x0 being Point of X0 st x0 in the carrier of X1 holds g.x0 = (g|X1).x0; theorem :: TMAP_1:66 X1 is SubSpace of X0 implies for g1 being Function of X1,Y st for x0 being Point of X0 st x0 in the carrier of X1 holds g.x0 = g1.x0 holds g|X1 = g1 ; theorem :: TMAP_1:67 g = g|X0; theorem :: TMAP_1:68 X1 is SubSpace of X0 implies for A being Subset of X0 st A c= the carrier of X1 holds g.:A = (g|X1).:A; theorem :: TMAP_1:69 X1 is SubSpace of X0 implies for B being Subset of Y st g"B c= the carrier of X1 holds g"B = (g|X1)"B; theorem :: TMAP_1:70 for g being Function of X0,Y st g = f|X0 holds X1 is SubSpace of X0 implies g|X1 = f|X1; theorem :: TMAP_1:71 X1 is SubSpace of X0 implies (f|X0)|X1 = f|X1; theorem :: TMAP_1:72 for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 for g being Function of X0,Y holds (g|X1)|X2 = g| X2; theorem :: TMAP_1:73 for f being Function of X,Y, f0 being Function of X1,Y, g being Function of X0,Y holds X0 = X & f = g implies (g|X1 = f0 iff f|X1 = f0) ; reserve X0, X1, X2 for non empty SubSpace of X; reserve f for Function of X,Y, g for Function of X0,Y; theorem :: TMAP_1:74 for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds X1 is SubSpace of X0 & g is_continuous_at x0 implies g|X1 is_continuous_at x1 ; theorem :: TMAP_1:75 X1 is SubSpace of X0 implies for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds f|X0 is_continuous_at x0 implies f|X1 is_continuous_at x1; ::Characterizations of Continuity at the Point by Local one. theorem :: TMAP_1:76 X1 is SubSpace of X0 implies for A being Subset of X0, x0 being Point of X0, x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1; theorem :: TMAP_1:77 X1 is SubSpace of X0 implies for A being Subset of X0, x0 being Point of X0, x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1; theorem :: TMAP_1:78 X1 is SubSpace of X0 implies for A being Subset of X, x0 being Point of X0, x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1; theorem :: TMAP_1:79 X1 is open SubSpace of X0 implies for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds g is_continuous_at x0 iff g|X1 is_continuous_at x1; theorem :: TMAP_1:80 X1 is open SubSpace of X & X1 is SubSpace of X0 implies for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds g is_continuous_at x0 iff g| X1 is_continuous_at x1; theorem :: TMAP_1:81 the TopStruct of X1 = X0 implies for x0 being Point of X0, x1 being Point of X1 st x0 = x1 holds g|X1 is_continuous_at x1 implies g is_continuous_at x0; theorem :: TMAP_1:82 for g being continuous Function of X0,Y holds X1 is SubSpace of X0 implies g|X1 is continuous Function of X1,Y; theorem :: TMAP_1:83 X1 is SubSpace of X0 & X2 is SubSpace of X1 implies for g being Function of X0,Y holds g|X1 is continuous Function of X1,Y implies g|X2 is continuous Function of X2,Y; registration let X; cluster id X -> continuous; end; ::(Definition of the inclusion mapping.) definition let X be non empty TopSpace, X0 be SubSpace of X; func incl X0 -> Function of X0,X equals :: TMAP_1:def 6 (id X)|X0; end; notation let X be non empty TopSpace, X0 be SubSpace of X; synonym X0 incl X for incl X0; end; theorem :: TMAP_1:84 for X0 being non empty SubSpace of X, x being Point of X st x in the carrier of X0 holds (incl X0).x = x; theorem :: TMAP_1:85 for X0 being non empty SubSpace of X, f0 being Function of X0,X st for x being Point of X st x in the carrier of X0 holds x = f0.x holds incl X0 = f0; theorem :: TMAP_1:86 for X0 being non empty SubSpace of X, f being Function of X,Y holds f| X0 = f*(incl X0); theorem :: TMAP_1:87 for X0 being non empty SubSpace of X holds incl X0 is continuous Function of X0,X; begin :: 4. A Modification of the Topology of Topological Spaces. reserve X for non empty TopSpace, H, G for Subset of X; definition let X; let A be Subset of X; func A-extension_of_the_topology_of X -> Subset-Family of X equals :: TMAP_1:def 7 {H \/ (G /\ A) : H in the topology of X & G in the topology of X}; end; theorem :: TMAP_1:88 for A being Subset of X holds the topology of X c= A -extension_of_the_topology_of X; theorem :: TMAP_1:89 for A being Subset of X holds {G /\ A where G is Subset of X : G in the topology of X} c= A-extension_of_the_topology_of X; theorem :: TMAP_1:90 for A being Subset of X holds for C, D being Subset of X st C in the topology of X & D in {G /\ A where G is Subset of X : G in the topology of X} holds C \/ D in A-extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X; theorem :: TMAP_1:91 for A being Subset of X holds A in A -extension_of_the_topology_of X; theorem :: TMAP_1:92 for A being Subset of X holds A in the topology of X iff the topology of X = A-extension_of_the_topology_of X; definition let X be non empty TopSpace, A be Subset of X; func X modified_with_respect_to A -> strict TopSpace equals :: TMAP_1:def 8 TopStruct(#the carrier of X, A-extension_of_the_topology_of X#); end; registration let X be non empty TopSpace, A be Subset of X; cluster X modified_with_respect_to A -> non empty; end; reserve A for Subset of X; theorem :: TMAP_1:93 the carrier of (X modified_with_respect_to A) = the carrier of X & the topology of (X modified_with_respect_to A) = A-extension_of_the_topology_of X; theorem :: TMAP_1:94 for B being Subset of X modified_with_respect_to A st B = A holds B is open; theorem :: TMAP_1:95 for A being Subset of X holds A is open iff the TopStruct of X = X modified_with_respect_to A; definition let X be non empty TopSpace, A be Subset of X; func modid(X,A) -> Function of X,X modified_with_respect_to A equals :: TMAP_1:def 9 id (the carrier of X); end; theorem :: TMAP_1:96 for x being Point of X st not x in A holds modid(X,A) is_continuous_at x; theorem :: TMAP_1:97 for X0 being non empty SubSpace of X st the carrier of X0 misses A for x0 being Point of X0 holds (modid(X,A))|X0 is_continuous_at x0; theorem :: TMAP_1:98 for X0 being non empty SubSpace of X st the carrier of X0 = A for x0 being Point of X0 holds (modid(X,A))|X0 is_continuous_at x0; theorem :: TMAP_1:99 for X0 being non empty SubSpace of X st the carrier of X0 misses A holds (modid(X,A))|X0 is continuous Function of X0,X modified_with_respect_to A; theorem :: TMAP_1:100 for X0 being non empty SubSpace of X st the carrier of X0 = A holds (modid(X,A))|X0 is continuous Function of X0,X modified_with_respect_to A ; theorem :: TMAP_1:101 for A being Subset of X holds A is open iff modid(X,A) is continuous Function of X,X modified_with_respect_to A; definition let X be non empty TopSpace, X0 be SubSpace of X; func X modified_with_respect_to X0 -> strict TopSpace means :: TMAP_1:def 10 for A being Subset of X st A = the carrier of X0 holds it = X modified_with_respect_to A; end; registration let X be non empty TopSpace, X0 be SubSpace of X; cluster X modified_with_respect_to X0 -> non empty; end; reserve X0 for non empty SubSpace of X; theorem :: TMAP_1:102 the carrier of (X modified_with_respect_to X0) = the carrier of X & for A being Subset of X st A = the carrier of X0 holds the topology of (X modified_with_respect_to X0) = A-extension_of_the_topology_of X; theorem :: TMAP_1:103 for Y0 being SubSpace of X modified_with_respect_to X0 st the carrier of Y0 = the carrier of X0 holds Y0 is open SubSpace of X modified_with_respect_to X0; theorem :: TMAP_1:104 X0 is open SubSpace of X iff the TopStruct of X = X modified_with_respect_to X0; definition let X be non empty TopSpace, X0 be SubSpace of X; func modid(X,X0) -> Function of X,X modified_with_respect_to X0 means :: TMAP_1:def 11 for A being Subset of X st A = the carrier of X0 holds it = modid(X,A); end; theorem :: TMAP_1:105 modid(X,X0) = id X; theorem :: TMAP_1:106 for X0, X1 being non empty SubSpace of X st X0 misses X1 for x1 being Point of X1 holds (modid(X,X0))|X1 is_continuous_at x1; theorem :: TMAP_1:107 for X0 being non empty SubSpace of X for x0 being Point of X0 holds (modid(X,X0))|X0 is_continuous_at x0; theorem :: TMAP_1:108 for X0, X1 being non empty SubSpace of X st X0 misses X1 holds (modid( X,X0))|X1 is continuous Function of X1,X modified_with_respect_to X0; theorem :: TMAP_1:109 for X0 being non empty SubSpace of X holds (modid(X,X0))|X0 is continuous Function of X0,X modified_with_respect_to X0; theorem :: TMAP_1:110 for X0 being SubSpace of X holds X0 is open SubSpace of X iff modid(X, X0) is continuous Function of X,X modified_with_respect_to X0; begin :: 5. Continuity of Mappings over the Union of Subspaces. reserve X, Y for non empty TopSpace; ::Continuity at the Point of Mappings over the Union of Subspaces. theorem :: TMAP_1:111 for X1, X2 being non empty SubSpace of X, g being Function of X1 union X2,Y for x1 being Point of X1, x2 being Point of X2, x being Point of X1 union X2 st x = x1 & x = x2 holds g is_continuous_at x iff g|X1 is_continuous_at x1 & g|X2 is_continuous_at x2; theorem :: TMAP_1:112 for f being Function of X,Y, X1, X2 being non empty SubSpace of X for x being Point of X1 union X2, x1 being Point of X1, x2 being Point of X2 st x = x1 & x = x2 holds f|(X1 union X2) is_continuous_at x iff f|X1 is_continuous_at x1 & f|X2 is_continuous_at x2; theorem :: TMAP_1:113 for f being Function of X,Y, X1, X2 being non empty SubSpace of X st X = X1 union X2 for x being Point of X, x1 being Point of X1, x2 being Point of X2 st x = x1 & x = x2 holds f is_continuous_at x iff f|X1 is_continuous_at x1 & f|X2 is_continuous_at x2; reserve X1, X2 for non empty SubSpace of X; ::Continuity of Mappings over the Union of Subspaces. theorem :: TMAP_1:114 X1,X2 are_weakly_separated implies for g being Function of X1 union X2,Y holds g is continuous Function of X1 union X2,Y iff g|X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y; theorem :: TMAP_1:115 for X1, X2 being closed non empty SubSpace of X for g being Function of X1 union X2,Y holds g is continuous Function of X1 union X2,Y iff g |X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y; theorem :: TMAP_1:116 for X1, X2 being open non empty SubSpace of X for g being Function of X1 union X2,Y holds g is continuous Function of X1 union X2,Y iff g |X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y; theorem :: TMAP_1:117 X1,X2 are_weakly_separated implies for f being Function of X,Y holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y; theorem :: TMAP_1:118 for f being Function of X,Y, X1, X2 being closed non empty SubSpace of X holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y; theorem :: TMAP_1:119 for f being Function of X,Y, X1, X2 being open non empty SubSpace of X holds f|(X1 union X2) is continuous Function of X1 union X2,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y; theorem :: TMAP_1:120 for f being Function of X,Y, X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated holds f is continuous Function of X,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y; theorem :: TMAP_1:121 for f being Function of X,Y, X1, X2 being closed non empty SubSpace of X st X = X1 union X2 holds f is continuous Function of X,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y; theorem :: TMAP_1:122 for f being Function of X,Y, X1, X2 being open non empty SubSpace of X st X = X1 union X2 holds f is continuous Function of X,Y iff f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y; ::Some Characterizations of Separated Subspaces of Topological Spaces. theorem :: TMAP_1:123 X1,X2 are_separated iff X1 misses X2 & for Y being non empty TopSpace, g being Function of X1 union X2,Y st g|X1 is continuous Function of X1,Y & g|X2 is continuous Function of X2,Y holds g is continuous Function of X1 union X2,Y; theorem :: TMAP_1:124 X1,X2 are_separated iff X1 misses X2 & for Y being non empty TopSpace, f being Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y holds f|(X1 union X2) is continuous Function of X1 union X2,Y; theorem :: TMAP_1:125 for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds X1, X2 are_separated iff X1 misses X2 & for Y being non empty TopSpace, f being Function of X,Y st f|X1 is continuous Function of X1,Y & f|X2 is continuous Function of X2,Y holds f is continuous Function of X,Y; begin :: 6. The Union of Continuous Mappings. definition let X,Y be non empty TopSpace, X1, X2 be non empty SubSpace of X; let f1 be Function of X1,Y, f2 be Function of X2,Y; assume X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2); func f1 union f2 -> Function of X1 union X2,Y means :: TMAP_1:def 12 it|X1 = f1 & it| X2 = f2; end; reserve X, Y for non empty TopSpace; theorem :: TMAP_1:126 for X1, X2 being non empty SubSpace of X for g being Function of X1 union X2,Y holds g = (g|X1) union (g|X2); theorem :: TMAP_1:127 for X1, X2 being non empty SubSpace of X st X = X1 union X2 for g being Function of X,Y holds g = (g|X1) union (g|X2); theorem :: TMAP_1:128 for X1, X2 being non empty SubSpace of X st X1 meets X2 for f1 being Function of X1,Y, f2 being Function of X2,Y holds (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 iff f1|(X1 meet X2) = f2|(X1 meet X2); theorem :: TMAP_1:129 for X1, X2 being non empty SubSpace of X, f1 being Function of X1,Y, f2 being Function of X2,Y st f1|(X1 meet X2) = f2|(X1 meet X2) holds (X1 is SubSpace of X2 iff f1 union f2 = f2) & (X2 is SubSpace of X1 iff f1 union f2 = f1); theorem :: TMAP_1:130 for X1, X2 being non empty SubSpace of X, f1 being Function of X1,Y, f2 being Function of X2,Y st X1 misses X2 or f1|(X1 meet X2) = f2|(X1 meet X2) holds f1 union f2 = f2 union f1; theorem :: TMAP_1:131 for X1, X2, X3 being non empty SubSpace of X, f1 being Function of X1, Y, f2 being Function of X2,Y, f3 being Function of X3,Y st (X1 misses X2 or f1| (X1 meet X2) = f2|(X1 meet X2)) & (X1 misses X3 or f1|(X1 meet X3) = f3|(X1 meet X3)) & (X2 misses X3 or f2|(X2 meet X3) = f3|(X2 meet X3)) holds (f1 union f2) union f3 = f1 union (f2 union f3); ::Continuity of the Union of Continuous Mappings. ::(Theorems presented below are suitable also in the case X = X1 union X2.) theorem :: TMAP_1:132 for X1, X2 being non empty SubSpace of X st X1 meets X2 for f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|(X1 meet X2) = f2|(X1 meet X2) holds X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of X1 union X2,Y; theorem :: TMAP_1:133 for X1, X2 being non empty SubSpace of X st X1 misses X2 for f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of X1 union X2,Y; theorem :: TMAP_1:134 for X1, X2 being closed non empty SubSpace of X st X1 meets X2 for f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|( X1 meet X2) = f2|(X1 meet X2) holds f1 union f2 is continuous Function of X1 union X2,Y; theorem :: TMAP_1:135 for X1, X2 being open non empty SubSpace of X st X1 meets X2 for f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y st f1|( X1 meet X2) = f2|(X1 meet X2) holds f1 union f2 is continuous Function of X1 union X2,Y; theorem :: TMAP_1:136 for X1, X2 being closed non empty SubSpace of X st X1 misses X2 for f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of X1 union X2,Y; theorem :: TMAP_1:137 for X1, X2 being open non empty SubSpace of X st X1 misses X2 for f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of X1 union X2,Y; ::A Characterization of Separated Subspaces by means of Continuity of the Union ::of Continuous continuous mappings defined on the Subspaces. theorem :: TMAP_1:138 for X1, X2 being non empty SubSpace of X holds X1,X2 are_separated iff X1 misses X2 & for Y being non empty TopSpace, f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of X1 union X2,Y; ::Continuity of the Union of Continuous Mappings (a special case). theorem :: TMAP_1:139 for X1, X2 being non empty SubSpace of X st X = X1 union X2 for f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y st (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of X,Y; theorem :: TMAP_1:140 for X1, X2 being closed non empty SubSpace of X, f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y st X = X1 union X2 & (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds f1 union f2 is continuous Function of X,Y; theorem :: TMAP_1:141 for X1, X2 being open non empty SubSpace of X, f1 being continuous Function of X1,Y, f2 being continuous Function of X2,Y st X = X1 union X2 & (f1 union f2)|X1 = f1 & (f1 union f2)|X2 = f2 holds f1 union f2 is continuous Function of X,Y; theorem :: TMAP_1:142 for A,B be non empty set for A1,A2 be non empty Subset of A for f1 be Function of A1,B, f2 be Function of A2,B st f1|(A1 /\ A2) = f2|(A1 /\ A2) holds (f1 union f2)|A1 = f1 & (f1 union f2)|A2 = f2;