:: by Zbigniew Karno

::

:: Received May 22, 1992

:: Copyright (c) 1992-2012 Association of Mizar Users

begin

registration

let X be non empty TopSpace;

let X1, X2 be non empty SubSpace of X;

coherence

X1 union X2 is TopSpace-like ;

end;
let X1, X2 be non empty SubSpace of X;

coherence

X1 union X2 is TopSpace-like ;

definition

let A, B be non empty set ;

let A1, A2 be non empty Subset of A;

let f1 be Function of A1,B;

let f2 be Function of A2,B;

assume A1: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) ;

ex b_{1} being Function of (A1 \/ A2),B st

( b_{1} | A1 = f1 & b_{1} | A2 = f2 )

for b_{1}, b_{2} being Function of (A1 \/ A2),B st b_{1} | A1 = f1 & b_{1} | A2 = f2 & b_{2} | A1 = f1 & b_{2} | A2 = f2 holds

b_{1} = b_{2}

end;
let A1, A2 be non empty Subset of A;

let f1 be Function of A1,B;

let f2 be Function of A2,B;

assume A1: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) ;

func f1 union f2 -> Function of (A1 \/ A2),B means :Def1: :: TMAP_1:def 1

( it | A1 = f1 & it | A2 = f2 );

existence ( it | A1 = f1 & it | A2 = f2 );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines union TMAP_1:def 1 :

for A, B being non empty set

for A1, A2 being non empty Subset of A

for f1 being Function of A1,B

for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds

for b_{7} being Function of (A1 \/ A2),B holds

( b_{7} = f1 union f2 iff ( b_{7} | A1 = f1 & b_{7} | A2 = f2 ) );

for A, B being non empty set

for A1, A2 being non empty Subset of A

for f1 being Function of A1,B

for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds

for b

( b

theorem Th1: :: TMAP_1:1

for A, B being non empty set

for A1, A2 being non empty Subset of A st A1 misses A2 holds

for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

for A1, A2 being non empty Subset of A st A1 misses A2 holds

for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

proof end;

theorem Th2: :: TMAP_1:2

for A, B being non empty set

for A1, A2 being non empty Subset of A

for g being Function of (A1 \/ A2),B

for g1 being Function of A1,B

for g2 being Function of A2,B st g | A1 = g1 & g | A2 = g2 holds

g = g1 union g2

for A1, A2 being non empty Subset of A

for g being Function of (A1 \/ A2),B

for g1 being Function of A1,B

for g2 being Function of A2,B st g | A1 = g1 & g | A2 = g2 holds

g = g1 union g2

proof end;

theorem :: TMAP_1:3

for A, B being non empty set

for A1, A2 being non empty Subset of A

for f1 being Function of A1,B

for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds

f1 union f2 = f2 union f1

for A1, A2 being non empty Subset of A

for f1 being Function of A1,B

for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds

f1 union f2 = f2 union f1

proof end;

theorem :: TMAP_1:4

for A, B being non empty set

for A1, A2, A3, A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2 \/ A3 holds

for f1 being Function of A1,B

for f2 being Function of A2,B

for 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) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

for A1, A2, A3, A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2 \/ A3 holds

for f1 being Function of A1,B

for f2 being Function of A2,B

for 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) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

proof end;

theorem :: TMAP_1:5

for A, B being non empty set

for A1, A2 being non empty Subset of A

for f1 being Function of A1,B

for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds

( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) )

for A1, A2 being non empty Subset of A

for f1 being Function of A1,B

for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds

( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) )

proof end;

begin

theorem Th6: :: TMAP_1:6

for X being TopStruct

for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X

for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X

proof end;

theorem Th7: :: TMAP_1:7

for X being TopStruct

for X1, X2 being TopSpace st X1 = TopStruct(# the carrier of X2, the topology of X2 #) holds

( X1 is SubSpace of X iff X2 is SubSpace of X )

for X1, X2 being TopSpace st X1 = TopStruct(# the carrier of X2, the topology of X2 #) holds

( X1 is SubSpace of X iff X2 is SubSpace of X )

proof end;

theorem Th8: :: TMAP_1:8

for X, X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds

( X1 is closed SubSpace of X iff X2 is closed SubSpace of X )

( X1 is closed SubSpace of X iff X2 is closed SubSpace of X )

proof end;

theorem Th9: :: TMAP_1:9

for X, X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds

( X1 is open SubSpace of X iff X2 is open SubSpace of X )

( X1 is open SubSpace of X iff X2 is open SubSpace of X )

proof end;

theorem Th10: :: TMAP_1:10

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds

for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1

for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds

for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1

proof end;

theorem Th11: :: TMAP_1:11

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X

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 )

for X1, X2 being non empty SubSpace of X

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 )

proof end;

theorem Th12: :: TMAP_1:12

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

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 )

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

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 )

proof end;

theorem :: TMAP_1:13

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for F1 being Subset of X1

for F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds

ex H being Subset of (X1 union X2) st

( H is closed & x in H & H c= F1 \/ F2 )

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for F1 being Subset of X1

for F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds

ex H being Subset of (X1 union X2) st

( H is closed & x in H & H c= F1 \/ F2 )

proof end;

theorem Th14: :: TMAP_1:14

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for U1 being Subset of X1

for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds

ex V being Subset of (X1 union X2) st

( V is open & x in V & V c= U1 \/ U2 )

proof end;

theorem Th15: :: TMAP_1:15

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for x1 being Point of X1

for x2 being Point of X2 st x1 = x & x2 = x holds

for A1 being a_neighborhood of x1

for 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 )

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for x1 being Point of X1

for x2 being Point of X2 st x1 = x & x2 = x holds

for A1 being a_neighborhood of x1

for 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 )

proof end;

theorem Th16: :: TMAP_1:16

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for x1 being Point of X1

for x2 being Point of X2 st x1 = x & x2 = x holds

for A1 being a_neighborhood of x1

for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for x1 being Point of X1

for x2 being Point of X2 st x1 = x & x2 = x holds

for A1 being a_neighborhood of x1

for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2

proof end;

theorem Th17: :: TMAP_1:17

for X being non empty TopSpace

for X0, X1 being non empty SubSpace of X st X0 is SubSpace of X1 holds

( X0 meets X1 & X1 meets X0 )

for X0, X1 being non empty SubSpace of X st X0 is SubSpace of X1 holds

( X0 meets X1 & X1 meets X0 )

proof end;

theorem Th18: :: TMAP_1:18

for X being non empty TopSpace

for X0, X1, X2 being non empty SubSpace of X st X0 is SubSpace of X1 & ( X0 meets X2 or X2 meets X0 ) holds

( X1 meets X2 & X2 meets X1 )

for X0, X1, X2 being non empty SubSpace of X st X0 is SubSpace of X1 & ( X0 meets X2 or X2 meets X0 ) holds

( X1 meets X2 & X2 meets X1 )

proof end;

theorem Th19: :: TMAP_1:19

for X being non empty TopSpace

for X0, X1, X2 being non empty SubSpace of X st X0 is SubSpace of X1 & ( X1 misses X2 or X2 misses X1 ) holds

( X0 misses X2 & X2 misses X0 )

for X0, X1, X2 being non empty SubSpace of X st X0 is SubSpace of X1 & ( X1 misses X2 or X2 misses X1 ) holds

( X0 misses X2 & X2 misses X0 )

proof end;

theorem :: TMAP_1:20

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds X0 union X0 = TopStruct(# the carrier of X0, the topology of X0 #)

for X0 being non empty SubSpace of X holds X0 union X0 = TopStruct(# the carrier of X0, the topology of X0 #)

proof end;

theorem :: TMAP_1:21

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #)

for X0 being non empty SubSpace of X holds X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #)

proof end;

theorem Th22: :: TMAP_1:22

for X being non empty TopSpace

for Y1, X1, Y2, X2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds

Y1 union Y2 is SubSpace of X1 union X2

for Y1, X1, Y2, X2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds

Y1 union Y2 is SubSpace of X1 union X2

proof end;

theorem :: TMAP_1:23

for X being non empty TopSpace

for Y1, Y2, X1, X2 being non empty SubSpace of X st Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds

Y1 meet Y2 is SubSpace of X1 meet X2

for Y1, Y2, X1, X2 being non empty SubSpace of X st Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds

Y1 meet Y2 is SubSpace of X1 meet X2

proof end;

theorem Th24: :: TMAP_1:24

for X being non empty TopSpace

for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X0 holds

X1 union X2 is SubSpace of X0

for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X0 holds

X1 union X2 is SubSpace of X0

proof end;

theorem :: TMAP_1:25

for X being non empty TopSpace

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 holds

X1 meet X2 is SubSpace of X0

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 holds

X1 meet X2 is SubSpace of X0

proof end;

theorem Th26: :: TMAP_1:26

for X being non empty TopSpace

for X1, X0, X2 being non empty SubSpace of X holds

( ( ( 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 ) ) )

for X1, X0, X2 being non empty SubSpace of X holds

( ( ( 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 ) ) )

proof end;

theorem Th27: :: TMAP_1:27

for X being non empty TopSpace

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( 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 ) )

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( 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 ) )

proof end;

theorem Th28: :: TMAP_1:28

for X being non empty TopSpace

for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & ( X0 misses X2 or X2 misses X0 ) holds

( X0 meet (X1 union X2) = TopStruct(# the carrier of X1, the topology of X1 #) & X0 meet (X2 union X1) = TopStruct(# the carrier of X1, the topology of X1 #) )

for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & ( X0 misses X2 or X2 misses X0 ) holds

( X0 meet (X1 union X2) = TopStruct(# the carrier of X1, the topology of X1 #) & X0 meet (X2 union X1) = TopStruct(# the carrier of X1, the topology of X1 #) )

proof end;

theorem Th29: :: TMAP_1:29

for X being non empty TopSpace

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( 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 ) ) )

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( 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 ) ) )

proof end;

theorem Th30: :: TMAP_1:30

for X being non empty TopSpace

for X1, Y1, X2, Y2 being non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) holds

( Y1 misses X2 & Y2 misses X1 )

for X1, Y1, X2, Y2 being non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) holds

( Y1 misses X2 & Y2 misses X1 )

proof end;

theorem Th31: :: TMAP_1:31

for X being non empty TopSpace

for X1, X2, Y1, Y2 being non empty SubSpace of X st 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 holds

( Y1 meets X1 union X2 & Y2 meets X1 union X2 )

for X1, X2, Y1, Y2 being non empty SubSpace of X st 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 holds

( Y1 meets X1 union X2 & Y2 meets X1 union X2 )

proof end;

theorem Th32: :: TMAP_1:32

for X being non empty TopSpace

for X1, X2, Y1, Y2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & TopStruct(# the carrier of X, the topology 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 holds

( Y1 meets X1 union X2 & Y2 meets X1 union X2 )

for X1, X2, Y1, Y2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & TopStruct(# the carrier of X, the topology 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 holds

( Y1 meets X1 union X2 & Y2 meets X1 union X2 )

proof end;

theorem Th33: :: TMAP_1:33

for X being non empty TopSpace

for X1, X2, Y1, Y2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is not SubSpace of Y1 union Y2 & TopStruct(# the carrier of X, the topology 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 holds

( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 )

for X1, X2, Y1, Y2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is not SubSpace of Y1 union Y2 & TopStruct(# the carrier of X, the topology 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 holds

( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 )

proof end;

theorem Th34: :: TMAP_1:34

for X being non empty TopSpace

for X1, X2, X0 being non empty SubSpace of X holds

( ( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 ) & ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 ) & ( not X0 meets X1 union X2 or X0 meets X1 or X0 meets X2 ) & ( ( X0 meets X1 or X0 meets X2 ) implies X0 meets X1 union X2 ) )

for X1, X2, X0 being non empty SubSpace of X holds

( ( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 ) & ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 ) & ( not X0 meets X1 union X2 or X0 meets X1 or X0 meets X2 ) & ( ( X0 meets X1 or X0 meets X2 ) implies X0 meets X1 union X2 ) )

proof end;

theorem :: TMAP_1:35

for X being non empty TopSpace

for X1, X2, X0 being non empty SubSpace of X holds

( ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) ) & ( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 ) & ( X0 misses X1 union X2 implies ( X0 misses X1 & X0 misses X2 ) ) & ( X0 misses X1 & X0 misses X2 implies X0 misses X1 union X2 ) )

for X1, X2, X0 being non empty SubSpace of X holds

( ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) ) & ( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 ) & ( X0 misses X1 union X2 implies ( X0 misses X1 & X0 misses X2 ) ) & ( X0 misses X1 & X0 misses X2 implies X0 misses X1 union X2 ) )

proof end;

theorem :: TMAP_1:36

for X being non empty TopSpace

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( X1 meet X2 meets X0 implies ( X1 meets X0 & X2 meets X0 ) ) & ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) ) )

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( X1 meet X2 meets X0 implies ( X1 meets X0 & X2 meets X0 ) ) & ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) ) )

proof end;

theorem :: TMAP_1:37

for X being non empty TopSpace

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( ( 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 ) )

for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds

( ( ( 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 ) )

proof end;

theorem Th38: :: TMAP_1:38

for X being non empty TopSpace

for X1 being non empty SubSpace of X

for X0 being non empty closed SubSpace of X st X0 meets X1 holds

X0 meet X1 is closed SubSpace of X1

for X1 being non empty SubSpace of X

for X0 being non empty closed SubSpace of X st X0 meets X1 holds

X0 meet X1 is closed SubSpace of X1

proof end;

theorem Th39: :: TMAP_1:39

for X being non empty TopSpace

for X1 being non empty SubSpace of X

for X0 being non empty open SubSpace of X st X0 meets X1 holds

X0 meet X1 is open SubSpace of X1

for X1 being non empty SubSpace of X

for X0 being non empty open SubSpace of X st X0 meets X1 holds

X0 meet X1 is open SubSpace of X1

proof end;

theorem :: TMAP_1:40

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for X0 being non empty closed SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds

( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 )

for X1, X2 being non empty SubSpace of X

for X0 being non empty closed SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds

( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 )

proof end;

theorem Th41: :: TMAP_1:41

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for X0 being non empty open SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds

( X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1 )

for X1, X2 being non empty SubSpace of X

for X0 being non empty open SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds

( X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1 )

proof end;

begin

definition

let X, Y be non empty TopSpace;

let f be Function of X,Y;

let x be Point of X;

end;
let f be Function of X,Y;

let x be Point of X;

pred f is_continuous_at x means :Def2: :: TMAP_1:def 2

for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G;

for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G;

:: deftheorem Def2 defines is_continuous_at TMAP_1:def 2 :

for X, Y being non empty TopSpace

for f being Function of X,Y

for x being Point of X holds

( f is_continuous_at x iff for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G );

for X, Y being non empty TopSpace

for f being Function of X,Y

for x being Point of X holds

( f is_continuous_at x iff for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G );

notation

let X, Y be non empty TopSpace;

let f be Function of X,Y;

let x be Point of X;

antonym f is_not_continuous_at x for f is_continuous_at x;

end;
let f be Function of X,Y;

let x be Point of X;

antonym f is_not_continuous_at x for f is_continuous_at x;

theorem Th42: :: TMAP_1:42

for Y, X being non empty TopSpace

for f being Function of X,Y

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 )

for f being Function of X,Y

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 )

proof end;

theorem Th43: :: TMAP_1:43

for X, Y being non empty TopSpace

for f being Function of X,Y

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 holds

ex H being Subset of X st

( H is open & x in H & f .: H c= G ) )

for f being Function of X,Y

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 holds

ex H being Subset of X st

( H is open & x in H & f .: H c= G ) )

proof end;

theorem Th44: :: TMAP_1:44

for Y, X being non empty TopSpace

for f being Function of X,Y holds

( f is continuous iff for x being Point of X holds f is_continuous_at x )

for f being Function of X,Y holds

( f is continuous iff for x being Point of X holds f is_continuous_at x )

proof end;

theorem Th45: :: 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 holds

for f being Function of X,Y

for g being Function of X,Z st f = g holds

for x being Point of X st f is_continuous_at x holds

g is_continuous_at x

for f being Function of X,Y

for g being Function of X,Z st f = g holds

for x being Point of X st f is_continuous_at x holds

g is_continuous_at x

proof end;

theorem Th46: :: 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 holds

for f being Function of X,Z

for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

for f being Function of X,Z

for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

proof end;

theorem Th47: :: TMAP_1:47

for Z, X, Y being non empty TopSpace

for f being Function of X,Y

for g being Function of Y,Z

for x being Point of X

for y being Point of Y st y = f . x & f is_continuous_at x & g is_continuous_at y holds

g * f is_continuous_at x

for f being Function of X,Y

for g being Function of Y,Z

for x being Point of X

for y being Point of Y st y = f . x & f is_continuous_at x & g is_continuous_at y holds

g * f is_continuous_at x

proof end;

theorem :: TMAP_1:48

for Z, Y, X being non empty TopSpace

for f being Function of X,Y

for g being Function of Y,Z

for y being Point of Y st f is continuous & g is_continuous_at y holds

for x being Point of X st x in f " {y} holds

g * f is_continuous_at x

for f being Function of X,Y

for g being Function of Y,Z

for y being Point of Y st f is continuous & g is_continuous_at y holds

for x being Point of X st x in f " {y} holds

g * f is_continuous_at x

proof end;

theorem :: TMAP_1:49

for Y, Z, X being non empty TopSpace

for f being Function of X,Y

for g being Function of Y,Z

for x being Point of X st f is_continuous_at x & g is continuous holds

g * f is_continuous_at x

for f being Function of X,Y

for g being Function of Y,Z

for x being Point of X st f is_continuous_at x & g is continuous holds

g * f is_continuous_at x

proof end;

theorem :: TMAP_1:50

for X, Y being non empty TopSpace

for f being Function of X,Y holds

( f is continuous Function of X,Y iff for x being Point of X holds f is_continuous_at x ) by Th44;

for f being Function of X,Y holds

( f is continuous Function of X,Y iff for x being Point of X holds f is_continuous_at x ) by Th44;

theorem Th51: :: 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 holds

for f being continuous Function of X,Y holds f is continuous Function of X,Z

for f being continuous Function of X,Y holds f is continuous Function of X,Z

proof end;

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 holds

for f being continuous Function of Y,Z holds f is continuous Function of X,Z

for f being continuous Function of Y,Z holds f is continuous Function of X,Z

proof end;

Lm1: for A being set holds {} is Function of A,{}

proof end;

definition

let S, T be 1-sorted ;

let f be Function of S,T;

let R be 1-sorted ;

assume A1: the carrier of R c= the carrier of S ;

coherence

f | the carrier of R is Function of R,T

end;
let f be Function of S,T;

let R be 1-sorted ;

assume A1: the carrier of R c= the carrier of S ;

coherence

f | the carrier of R is Function of R,T

proof end;

:: deftheorem Def3 defines | TMAP_1:def 3 :

for S, T being 1-sorted

for f being Function of S,T

for R being 1-sorted st the carrier of R c= the carrier of S holds

f | R = f | the carrier of R;

for S, T being 1-sorted

for f being Function of S,T

for R being 1-sorted st the carrier of R c= the carrier of S holds

f | R = f | the carrier of R;

definition

let X, Y be non empty TopSpace;

let f be Function of X,Y;

let X0 be SubSpace of X;

compatibility

for b_{1} being Function of X0,Y holds

( b_{1} = f | X0 iff b_{1} = f | the carrier of X0 )

end;
let f be Function of X,Y;

let X0 be SubSpace of X;

compatibility

for b

( b

proof end;

:: deftheorem defines | TMAP_1:def 4 :

for X, Y being non empty TopSpace

for f being Function of X,Y

for X0 being SubSpace of X holds f | X0 = f | the carrier of X0;

for X, Y being non empty TopSpace

for f being Function of X,Y

for X0 being SubSpace of X holds f | X0 = f | the carrier of X0;

theorem Th53: :: TMAP_1:53

for Y, X being non empty TopSpace

for X0 being non empty SubSpace of X

for f being Function of X,Y

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

for X0 being non empty SubSpace of X

for f being Function of X,Y

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

proof end;

theorem Th54: :: TMAP_1:54

for Y, X being non empty TopSpace

for X0 being non empty SubSpace of X

for f being Function of X,Y st TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) holds

f = f | X0

for X0 being non empty SubSpace of X

for f being Function of X,Y st TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) holds

f = f | X0

proof end;

theorem :: TMAP_1:55

theorem :: TMAP_1:56

theorem Th57: :: TMAP_1:57

for Y, X being non empty TopSpace

for X0 being non empty SubSpace of X

for g being Function of X0,Y ex h being Function of X,Y st h | X0 = g

for X0 being non empty SubSpace of X

for g being Function of X0,Y ex h being Function of X,Y st h | X0 = g

proof end;

theorem Th58: :: TMAP_1:58

for Y, X being non empty TopSpace

for f being Function of X,Y

for X0 being non empty SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

for f being Function of X,Y

for X0 being non empty SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

proof end;

::Characterizations of Continuity at the Point by Local one.

theorem Th59: :: TMAP_1:59

for Y, X being non empty TopSpace

for f being Function of X,Y

for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for 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 )

for f being Function of X,Y

for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for 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 )

proof end;

theorem Th60: :: TMAP_1:60

for Y, X being non empty TopSpace

for f being Function of X,Y

for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for 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 )

for f being Function of X,Y

for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for 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 )

proof end;

theorem :: TMAP_1:61

for Y, X being non empty TopSpace

for f being Function of X,Y

for X0 being non empty open SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

for f being Function of X,Y

for X0 being non empty open SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

proof end;

registration

let X, Y be non empty TopSpace;

let f be continuous Function of X,Y;

let X0 be non empty SubSpace of X;

coherence

f | X0 is continuous

end;
let f be continuous Function of X,Y;

let X0 be non empty SubSpace of X;

coherence

f | X0 is continuous

proof end;

theorem Th62: :: TMAP_1:62

for X, Y, Z being non empty TopSpace

for X0 being non empty SubSpace of X

for f being Function of X,Y

for g being Function of Y,Z holds (g * f) | X0 = g * (f | X0)

for X0 being non empty SubSpace of X

for f being Function of X,Y

for g being Function of Y,Z holds (g * f) | X0 = g * (f | X0)

proof end;

theorem Th63: :: TMAP_1:63

for X, Y, Z being non empty TopSpace

for X0 being non empty SubSpace of X

for g being Function of Y,Z

for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

for X0 being non empty SubSpace of X

for g being Function of Y,Z

for f being Function of X,Y st g is continuous & f | X0 is continuous holds

(g * f) | X0 is continuous

proof end;

theorem :: TMAP_1:64

for X, Y, Z being non empty TopSpace

for X0 being non empty SubSpace of X

for g being continuous Function of Y,Z

for 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 by Th63;

for X0 being non empty SubSpace of X

for g being continuous Function of Y,Z

for 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 by Th63;

::(Definition of the restriction mapping - special case.)

definition

let X, Y be non empty TopSpace;

let X0, X1 be SubSpace of X;

let g be Function of X0,Y;

assume A1: X1 is SubSpace of X0 ;

coherence

g | the carrier of X1 is Function of X1,Y

end;
let X0, X1 be SubSpace of X;

let g be Function of X0,Y;

assume A1: X1 is SubSpace of X0 ;

coherence

g | the carrier of X1 is Function of X1,Y

proof end;

:: deftheorem Def5 defines | TMAP_1:def 5 :

for X, Y being non empty TopSpace

for X0, X1 being SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

g | X1 = g | the carrier of X1;

for X, Y being non empty TopSpace

for X0, X1 being SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

g | X1 = g | the carrier of X1;

theorem Th65: :: TMAP_1:65

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = (g | X1) . x0

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for x0 being Point of X0 st x0 in the carrier of X1 holds

g . x0 = (g | X1) . x0

proof end;

theorem :: TMAP_1:66

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

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

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

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

proof end;

theorem Th67: :: TMAP_1:67

for X, Y being non empty TopSpace

for X0 being non empty SubSpace of X

for g being Function of X0,Y holds g = g | X0

for X0 being non empty SubSpace of X

for g being Function of X0,Y holds g = g | X0

proof end;

theorem Th68: :: TMAP_1:68

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X0 st A c= the carrier of X1 holds

g .: A = (g | X1) .: A

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X0 st A c= the carrier of X1 holds

g .: A = (g | X1) .: A

proof end;

theorem :: TMAP_1:69

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for B being Subset of Y st g " B c= the carrier of X1 holds

g " B = (g | X1) " B

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for B being Subset of Y st g " B c= the carrier of X1 holds

g " B = (g | X1) " B

proof end;

theorem Th70: :: TMAP_1:70

for X, Y being non empty TopSpace

for X0, X1 being non empty SubSpace of X

for f being Function of X,Y

for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds

g | X1 = f | X1

for X0, X1 being non empty SubSpace of X

for f being Function of X,Y

for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds

g | X1 = f | X1

proof end;

theorem Th71: :: TMAP_1:71

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for f being Function of X,Y st X1 is SubSpace of X0 holds

(f | X0) | X1 = f | X1

for X1, X0 being non empty SubSpace of X

for f being Function of X,Y st X1 is SubSpace of X0 holds

(f | X0) | X1 = f | X1

proof end;

theorem Th72: :: TMAP_1:72

for X, Y being non empty TopSpace

for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds

for g being Function of X0,Y holds (g | X1) | X2 = g | X2

for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds

for g being Function of X0,Y holds (g | X1) | X2 = g | X2

proof end;

theorem :: TMAP_1:73

theorem Th74: :: TMAP_1:74

for X, Y being non empty TopSpace

for X0, X1 being non empty SubSpace of X

for g being Function of X0,Y

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 holds

g | X1 is_continuous_at x1

for X0, X1 being non empty SubSpace of X

for g being Function of X0,Y

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 holds

g | X1 is_continuous_at x1

proof end;

theorem Th75: :: TMAP_1:75

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for f being Function of X,Y st X1 is SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

for X1, X0 being non empty SubSpace of X

for f being Function of X,Y st X1 is SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds

f | X1 is_continuous_at x1

proof end;

::Characterizations of Continuity at the Point by Local one.

theorem Th76: :: TMAP_1:76

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X0

for x0 being Point of X0

for 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 )

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X0

for x0 being Point of X0

for 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 )

proof end;

theorem Th77: :: TMAP_1:77

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X0

for x0 being Point of X0

for 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 )

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X0

for x0 being Point of X0

for 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 )

proof end;

theorem :: TMAP_1:78

for Y, X being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X

for x0 being Point of X0

for 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 )

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is SubSpace of X0 holds

for A being Subset of X

for x0 being Point of X0

for 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 )

proof end;

theorem Th79: :: TMAP_1:79

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is open SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is open SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

proof end;

theorem :: TMAP_1:80

for Y, X being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is open SubSpace of X & X1 is SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st X1 is open SubSpace of X & X1 is SubSpace of X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 holds

( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )

proof end;

theorem Th81: :: TMAP_1:81

for X, Y being non empty TopSpace

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st TopStruct(# the carrier of X1, the topology of X1 #) = X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & g | X1 is_continuous_at x1 holds

g is_continuous_at x0

for X1, X0 being non empty SubSpace of X

for g being Function of X0,Y st TopStruct(# the carrier of X1, the topology of X1 #) = X0 holds

for x0 being Point of X0

for x1 being Point of X1 st x0 = x1 & g | X1 is_continuous_at x1 holds

g is_continuous_at x0

proof end;

theorem Th82: :: TMAP_1:82

for X, Y being non empty TopSpace

for X0, X1 being non empty SubSpace of X

for g being continuous Function of X0,Y st X1 is SubSpace of X0 holds

g | X1 is continuous Function of X1,Y

for X0, X1 being non empty SubSpace of X

for g being continuous Function of X0,Y st X1 is SubSpace of X0 holds

g | X1 is continuous Function of X1,Y

proof end;

theorem Th83: :: TMAP_1:83

for X, Y being non empty TopSpace

for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds

for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y

for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds

for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds

g | X2 is continuous Function of X2,Y

proof end;

registration
end;

::(Definition of the inclusion mapping.)

definition

let X be non empty TopSpace;

let X0 be SubSpace of X;

coherence

(id X) | X0 is Function of X0,X ;

correctness

;

end;
let X0 be SubSpace of X;

coherence

(id X) | X0 is Function of X0,X ;

correctness

;

:: deftheorem defines incl TMAP_1:def 6 :

for X being non empty TopSpace

for X0 being SubSpace of X holds incl X0 = (id X) | X0;

for X being non empty TopSpace

for X0 being SubSpace of X holds incl X0 = (id X) | X0;

theorem :: TMAP_1:84

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for x being Point of X st x in the carrier of X0 holds

(incl X0) . x = x

for X0 being non empty SubSpace of X

for x being Point of X st x in the carrier of X0 holds

(incl X0) . x = x

proof end;

theorem :: TMAP_1:85

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for 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

for X0 being non empty SubSpace of X

for 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

proof end;

theorem :: TMAP_1:86

for X, Y being non empty TopSpace

for X0 being non empty SubSpace of X

for f being Function of X,Y holds f | X0 = f * (incl X0)

for X0 being non empty SubSpace of X

for f being Function of X,Y holds f | X0 = f * (incl X0)

proof end;

theorem :: TMAP_1:87

begin

definition

let X be non empty TopSpace;

let A be Subset of X;

{ (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } is Subset-Family of X

end;
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)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;

coherence { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;

{ (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } is Subset-Family of X

proof end;

:: deftheorem defines -extension_of_the_topology_of TMAP_1:def 7 :

for X being non empty TopSpace

for A being Subset of X holds A -extension_of_the_topology_of X = { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;

for X being non empty TopSpace

for A being Subset of X holds A -extension_of_the_topology_of X = { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;

theorem Th88: :: TMAP_1:88

for X being non empty TopSpace

for A being Subset of X holds the topology of X c= A -extension_of_the_topology_of X

for A being Subset of X holds the topology of X c= A -extension_of_the_topology_of X

proof end;

theorem Th89: :: TMAP_1:89

for X being non empty TopSpace

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

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

proof end;

theorem Th90: :: TMAP_1:90

for X being non empty TopSpace

for A, 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 )

for A, 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 )

proof end;

theorem Th92: :: TMAP_1:92

for X being non empty TopSpace

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 )

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 )

proof end;

definition

let X be non empty TopSpace;

let A be Subset of X;

TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) is strict TopSpace

end;
let 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) #);

coherence TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #);

TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) is strict TopSpace

proof end;

:: deftheorem defines modified_with_respect_to TMAP_1:def 8 :

for X being non empty TopSpace

for A being Subset of X holds X modified_with_respect_to A = TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #);

for X being non empty TopSpace

for A being Subset of X holds X modified_with_respect_to A = TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #);

registration

let X be non empty TopSpace;

let A be Subset of X;

coherence

not X modified_with_respect_to A is empty ;

end;
let A be Subset of X;

coherence

not X modified_with_respect_to A is empty ;

theorem :: TMAP_1:93

for X being non empty TopSpace

for A being Subset of X holds

( 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 ) ;

for A being Subset of X holds

( 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 Th94: :: TMAP_1:94

for X being non empty TopSpace

for A being Subset of X

for B being Subset of (X modified_with_respect_to A) st B = A holds

B is open

for A being Subset of X

for B being Subset of (X modified_with_respect_to A) st B = A holds

B is open

proof end;

theorem Th95: :: TMAP_1:95

for X being non empty TopSpace

for A being Subset of X holds

( A is open iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A )

for A being Subset of X holds

( A is open iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A )

proof end;

definition

let X be non empty TopSpace;

let A be Subset of X;

id the carrier of X is Function of X,(X modified_with_respect_to A) ;

end;
let 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;

coherence id the carrier of X;

id the carrier of X is Function of X,(X modified_with_respect_to A) ;

:: deftheorem defines modid TMAP_1:def 9 :

for X being non empty TopSpace

for A being Subset of X holds modid (X,A) = id the carrier of X;

for X being non empty TopSpace

for A being Subset of X holds modid (X,A) = id the carrier of X;

theorem Th96: :: TMAP_1:96

for X being non empty TopSpace

for A being Subset of X

for x being Point of X st not x in A holds

modid (X,A) is_continuous_at x

for A being Subset of X

for x being Point of X st not x in A holds

modid (X,A) is_continuous_at x

proof end;

theorem Th97: :: TMAP_1:97

for X being non empty TopSpace

for A being Subset of X

for X0 being non empty SubSpace of X st the carrier of X0 misses A holds

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

for A being Subset of X

for X0 being non empty SubSpace of X st the carrier of X0 misses A holds

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

proof end;

theorem Th98: :: TMAP_1:98

for X being non empty TopSpace

for A being Subset of X

for X0 being non empty SubSpace of X st the carrier of X0 = A holds

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

for A being Subset of X

for X0 being non empty SubSpace of X st the carrier of X0 = A holds

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

proof end;

theorem Th99: :: TMAP_1:99

for X being non empty TopSpace

for A being Subset of X

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)

for A being Subset of X

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)

proof end;

theorem Th100: :: TMAP_1:100

for X being non empty TopSpace

for A being Subset of X

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)

for A being Subset of X

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)

proof end;

theorem Th101: :: TMAP_1:101

for X being non empty TopSpace

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) )

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) )

proof end;

definition

let X be non empty TopSpace;

let X0 be SubSpace of X;

ex b_{1} being strict TopSpace st

for A being Subset of X st A = the carrier of X0 holds

b_{1} = X modified_with_respect_to A

for b_{1}, b_{2} being strict TopSpace st ( for A being Subset of X st A = the carrier of X0 holds

b_{1} = X modified_with_respect_to A ) & ( for A being Subset of X st A = the carrier of X0 holds

b_{2} = X modified_with_respect_to A ) holds

b_{1} = b_{2}

end;
let X0 be SubSpace of X;

func X modified_with_respect_to X0 -> strict TopSpace means :Def10: :: TMAP_1:def 10

for A being Subset of X st A = the carrier of X0 holds

it = X modified_with_respect_to A;

existence for A being Subset of X st A = the carrier of X0 holds

it = X modified_with_respect_to A;

ex b

for A being Subset of X st A = the carrier of X0 holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines modified_with_respect_to TMAP_1:def 10 :

for X being non empty TopSpace

for X0 being SubSpace of X

for b_{3} being strict TopSpace holds

( b_{3} = X modified_with_respect_to X0 iff for A being Subset of X st A = the carrier of X0 holds

b_{3} = X modified_with_respect_to A );

for X being non empty TopSpace

for X0 being SubSpace of X

for b

( b

b

registration

let X be non empty TopSpace;

let X0 be SubSpace of X;

coherence

not X modified_with_respect_to X0 is empty

end;
let X0 be SubSpace of X;

coherence

not X modified_with_respect_to X0 is empty

proof end;

theorem Th102: :: TMAP_1:102

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds

( 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 ) )

for X0 being non empty SubSpace of X holds

( 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 ) )

proof end;

theorem :: TMAP_1:103

for X being non empty TopSpace

for X0 being non empty SubSpace of X

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

for X0 being non empty SubSpace of X

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

proof end;

theorem :: TMAP_1:104

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds

( X0 is open SubSpace of X iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 )

for X0 being non empty SubSpace of X holds

( X0 is open SubSpace of X iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 )

proof end;

definition

let X be non empty TopSpace;

let X0 be SubSpace of X;

ex b_{1} being Function of X,(X modified_with_respect_to X0) st

for A being Subset of X st A = the carrier of X0 holds

b_{1} = modid (X,A)

for b_{1}, b_{2} being Function of X,(X modified_with_respect_to X0) st ( for A being Subset of X st A = the carrier of X0 holds

b_{1} = modid (X,A) ) & ( for A being Subset of X st A = the carrier of X0 holds

b_{2} = modid (X,A) ) holds

b_{1} = b_{2}

end;
let X0 be SubSpace of X;

func modid (X,X0) -> Function of X,(X modified_with_respect_to X0) means :Def11: :: TMAP_1:def 11

for A being Subset of X st A = the carrier of X0 holds

it = modid (X,A);

existence for A being Subset of X st A = the carrier of X0 holds

it = modid (X,A);

ex b

for A being Subset of X st A = the carrier of X0 holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def11 defines modid TMAP_1:def 11 :

for X being non empty TopSpace

for X0 being SubSpace of X

for b_{3} being Function of X,(X modified_with_respect_to X0) holds

( b_{3} = modid (X,X0) iff for A being Subset of X st A = the carrier of X0 holds

b_{3} = modid (X,A) );

for X being non empty TopSpace

for X0 being SubSpace of X

for b

( b

b

theorem Th106: :: TMAP_1:106

for X being non empty TopSpace

for X0, X1 being non empty SubSpace of X st X0 misses X1 holds

for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1

for X0, X1 being non empty SubSpace of X st X0 misses X1 holds

for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1

proof end;

theorem Th107: :: TMAP_1:107

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for x0 being Point of X0 holds (modid (X,X0)) | X0 is_continuous_at x0

for X0 being non empty SubSpace of X

for x0 being Point of X0 holds (modid (X,X0)) | X0 is_continuous_at x0

proof end;

theorem :: TMAP_1:108

for X being non empty TopSpace

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)

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)

proof end;

theorem :: TMAP_1:109

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0)

for X0 being non empty SubSpace of X holds (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0)

proof end;

theorem :: TMAP_1:110

for X being non empty TopSpace

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) )

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) )

proof end;

begin

::Continuity at the Point of Mappings over the Union of Subspaces.

theorem Th111: :: TMAP_1:111

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for g being Function of (X1 union X2),Y

for x1 being Point of X1

for x2 being Point of X2

for 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 ) )

for X1, X2 being non empty SubSpace of X

for g being Function of (X1 union X2),Y

for x1 being Point of X1

for x2 being Point of X2

for 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 ) )

proof end;

theorem :: TMAP_1:112

for X, Y being non empty TopSpace

for f being Function of X,Y

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for x1 being Point of X1

for 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 ) )

for f being Function of X,Y

for X1, X2 being non empty SubSpace of X

for x being Point of (X1 union X2)

for x1 being Point of X1

for 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 ) )

proof end;

theorem :: TMAP_1:113

for X, Y being non empty TopSpace

for f being Function of X,Y

for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds

for x being Point of X

for x1 being Point of X1

for 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 ) )

for f being Function of X,Y

for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds

for x being Point of X

for x1 being Point of X1

for 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 ) )

proof end;

::Continuity of Mappings over the Union of Subspaces.

theorem Th114: :: TMAP_1:114

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds

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 ) )

for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds

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 ) )

proof end;

theorem Th115: :: TMAP_1:115

for X, Y being non empty TopSpace

for X1, X2 being non empty closed 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 ) )

for X1, X2 being non empty closed 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 ) )

proof end;

theorem Th116: :: TMAP_1:116

for X, Y being non empty TopSpace

for X1, X2 being non empty open 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 ) )

for X1, X2 being non empty open 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 ) )

proof end;

theorem Th117: :: TMAP_1:117

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds

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 ) )

for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds

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 ) )

proof end;

theorem :: TMAP_1:118

for X, Y being non empty TopSpace

for f being Function of X,Y

for X1, X2 being non empty closed 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 ) )

for f being Function of X,Y

for X1, X2 being non empty closed 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 ) )

proof end;

theorem :: TMAP_1:119

for X, Y being non empty TopSpace

for f being Function of X,Y

for X1, X2 being non empty open 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 ) )

for f being Function of X,Y

for X1, X2 being non empty open 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 ) )

proof end;

theorem Th120: :: TMAP_1:120

for X, Y being non empty TopSpace

for f being Function of X,Y

for 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 ) )

for f being Function of X,Y

for 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 ) )

proof end;

theorem Th121: :: TMAP_1:121

for X, Y being non empty TopSpace

for f being Function of X,Y

for X1, X2 being non empty closed 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 ) )

for f being Function of X,Y

for X1, X2 being non empty closed 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 ) )

proof end;

theorem Th122: :: TMAP_1:122

for X, Y being non empty TopSpace

for f being Function of X,Y

for X1, X2 being non empty open 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 ) )

for f being Function of X,Y

for X1, X2 being non empty open 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 ) )

proof end;

::Some Characterizations of Separated Subspaces of Topological Spaces.

theorem Th123: :: TMAP_1:123

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X holds

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for 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 ) ) )

for X1, X2 being non empty SubSpace of X holds

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for 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 ) ) )

proof end;

theorem Th124: :: TMAP_1:124

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X holds

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for 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 ) ) )

for X1, X2 being non empty SubSpace of X holds

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for 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 ) ) )

proof end;

theorem :: TMAP_1:125

for X being non empty TopSpace

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

for 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 ) ) )

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

for 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 ) ) )

proof end;

begin

definition

let X, Y be non empty TopSpace;

let X1, X2 be non empty SubSpace of X;

let f1 be Function of X1,Y;

let f2 be Function of X2,Y;

assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ;

ex b_{1} being Function of (X1 union X2),Y st

( b_{1} | X1 = f1 & b_{1} | X2 = f2 )

for b_{1}, b_{2} being Function of (X1 union X2),Y st b_{1} | X1 = f1 & b_{1} | X2 = f2 & b_{2} | X1 = f1 & b_{2} | X2 = f2 holds

b_{1} = b_{2}

end;
let X1, X2 be non empty SubSpace of X;

let f1 be Function of X1,Y;

let f2 be Function of X2,Y;

assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ;

func f1 union f2 -> Function of (X1 union X2),Y means :Def12: :: TMAP_1:def 12

( it | X1 = f1 & it | X2 = f2 );

existence ( it | X1 = f1 & it | X2 = f2 );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines union TMAP_1:def 12 :

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for f1 being Function of X1,Y

for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds

for b_{7} being Function of (X1 union X2),Y holds

( b_{7} = f1 union f2 iff ( b_{7} | X1 = f1 & b_{7} | X2 = f2 ) );

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for f1 being Function of X1,Y

for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds

for b

( b

theorem Th126: :: TMAP_1:126

for X, Y being non empty TopSpace

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)

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)

proof end;

theorem :: TMAP_1:127

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds

for g being Function of X,Y holds g = (g | X1) union (g | X2)

for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds

for g being Function of X,Y holds g = (g | X1) union (g | X2)

proof end;

theorem Th128: :: TMAP_1:128

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

for f1 being Function of X1,Y

for 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) )

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

for f1 being Function of X1,Y

for 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) )

proof end;

theorem :: TMAP_1:129

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for f1 being Function of X1,Y

for f2 being Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds

( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) )

for X1, X2 being non empty SubSpace of X

for f1 being Function of X1,Y

for f2 being Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds

( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) )

proof end;

theorem :: TMAP_1:130

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X

for f1 being Function of X1,Y

for 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

for X1, X2 being non empty SubSpace of X

for f1 being Function of X1,Y

for 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

proof end;

theorem :: TMAP_1:131

for X, Y being non empty TopSpace

for X1, X2, X3 being non empty SubSpace of X

for f1 being Function of X1,Y

for f2 being Function of X2,Y

for 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)

for X1, X2, X3 being non empty SubSpace of X

for f1 being Function of X1,Y

for f2 being Function of X2,Y

for 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)

proof end;

::Continuity of the Union of Continuous Mappings.

::(Theorems presented below are suitable also in the case X = X1 union X2.)

::(Theorems presented below are suitable also in the case X = X1 union X2.)

theorem :: TMAP_1:132

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of (X1 union X2),Y

for X1, X2 being non empty SubSpace of X st X1 meets X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of (X1 union X2),Y

proof end;

theorem Th133: :: TMAP_1:133

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1 misses X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of (X1 union X2),Y

for X1, X2 being non empty SubSpace of X st X1 misses X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of (X1 union X2),Y

proof end;

theorem :: TMAP_1:134

for X, Y being non empty TopSpace

for X1, X2 being non empty closed SubSpace of X st X1 meets X2 holds

for f1 being continuous Function of X1,Y

for 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

for X1, X2 being non empty closed SubSpace of X st X1 meets X2 holds

for f1 being continuous Function of X1,Y

for 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

proof end;

theorem :: TMAP_1:135

for X, Y being non empty TopSpace

for X1, X2 being non empty open SubSpace of X st X1 meets X2 holds

for f1 being continuous Function of X1,Y

for 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

for X1, X2 being non empty open SubSpace of X st X1 meets X2 holds

for f1 being continuous Function of X1,Y

for 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

proof end;

theorem :: TMAP_1:136

for X, Y being non empty TopSpace

for X1, X2 being non empty closed SubSpace of X st X1 misses X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y

for X1, X2 being non empty closed SubSpace of X st X1 misses X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y

proof end;

theorem :: TMAP_1:137

for X, Y being non empty TopSpace

for X1, X2 being non empty open SubSpace of X st X1 misses X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y

for X1, X2 being non empty open SubSpace of X st X1 misses X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y

proof end;

::A Characterization of Separated Subspaces by means of Continuity of the Union

::of Continuous continuous mappings defined on the Subspaces.

::of Continuous continuous mappings defined on the Subspaces.

theorem :: TMAP_1:138

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X holds

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) )

for X1, X2 being non empty SubSpace of X holds

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) )

proof end;

::Continuity of the Union of Continuous Mappings (a special case).

theorem :: TMAP_1:139

for X, Y being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

proof end;

theorem :: TMAP_1:140

for X, Y being non empty TopSpace

for X1, X2 being non empty closed SubSpace of X

for f1 being continuous Function of X1,Y

for 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

for X1, X2 being non empty closed SubSpace of X

for f1 being continuous Function of X1,Y

for 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

proof end;

theorem :: TMAP_1:141

for X, Y being non empty TopSpace

for X1, X2 being non empty open SubSpace of X

for f1 being continuous Function of X1,Y

for 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

for X1, X2 being non empty open SubSpace of X

for f1 being continuous Function of X1,Y

for 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

proof end;