:: Continuity of Mappings over the Union of Subspaces
:: by Zbigniew Karno
::
:: Received May 22, 1992
:: Copyright (c) 1992 Association of Mizar Users

begin

registration

let X be non empty TopSpace;
let X1, X2 be non empty SubSpace of X;
cluster X1 union X2 -> TopSpace-like ;
coherence
X1 union X2 is 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;
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
ex b₁ being Function of (A1 \/ A2),B st
( b₁ | A1 = f1 & b₁ | A2 = f2 )

proof end;

uniqueness
for b₁, b₂ being Function of (A1 \/ A2),B st b₁ | A1 = f1 & b₁ | A2 = f2 & b₂ | A1 = f1 & b₂ | A2 = f2 holds
b₁ = b₂

proof end;

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₇ being Function of (A1 \/ A2),B holds
( b₇ = f1 union f2 iff ( b₇ | A1 = f1 & b₇ | A2 = f2 ) );

theorem :: TMAP_1:1

canceled;

theorem :: TMAP_1:2

canceled;

theorem :: TMAP_1:3

canceled;

theorem :: TMAP_1:4

canceled;

theorem :: TMAP_1:5

canceled;

theorem Th6: :: TMAP_1:6

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 )

proof end;

theorem Th7: :: TMAP_1:7

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

proof end;

theorem :: TMAP_1:8

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

proof end;

theorem :: TMAP_1:9

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

proof end;

theorem :: TMAP_1:10

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

proof end;

begin

theorem Th11: :: TMAP_1:11

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

proof end;

theorem Th12: :: TMAP_1:12

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 )

proof end;

theorem Th13: :: TMAP_1:13

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 )

proof end;

theorem Th14: :: TMAP_1:14

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 )

proof end;

theorem Th15: :: TMAP_1:15

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

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) holds
( ex x1 being Point of X1 st x1 = x or ex x2 being Point of X2 st x2 = x )

proof end;

theorem Th17: :: TMAP_1:17

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 )

proof end;

theorem :: TMAP_1:18

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 )

proof end;

theorem Th19: :: TMAP_1:19

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 )

proof end;

theorem Th20: :: TMAP_1:20

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 )

proof end;

theorem Th21: :: TMAP_1:21

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

proof end;

theorem Th22: :: TMAP_1:22

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 )

proof end;

theorem Th23: :: TMAP_1:23

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 )

proof end;

theorem Th24: :: TMAP_1:24

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 )

proof end;

theorem :: TMAP_1:25

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

proof end;

theorem :: TMAP_1:26

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

proof end;

theorem Th27: :: TMAP_1:27

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

proof end;

theorem :: TMAP_1:28

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

proof end;

theorem Th29: :: TMAP_1:29

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

proof end;

theorem :: TMAP_1:30

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

proof end;

theorem Th31: :: TMAP_1:31

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

proof end;

theorem Th32: :: TMAP_1:32

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

proof end;

theorem Th33: :: TMAP_1:33

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

proof end;

theorem Th34: :: TMAP_1:34

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

proof end;

theorem Th35: :: TMAP_1:35

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 )

proof end;

theorem Th36: :: TMAP_1:36

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 )

proof end;

theorem Th37: :: TMAP_1:37

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 )

proof end;

theorem Th38: :: TMAP_1:38

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 )

proof end;

theorem Th39: :: TMAP_1:39

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

proof end;

theorem :: TMAP_1:40

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

proof end;

theorem :: TMAP_1:41

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

proof end;

theorem :: TMAP_1:42

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

proof end;

theorem Th43: :: TMAP_1:43

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

proof end;

theorem Th44: :: TMAP_1:44

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

proof end;

theorem :: TMAP_1:45

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 )

proof end;

theorem Th46: :: TMAP_1:46

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 )

proof end;

begin

definition

let X, Y be non empty TopSpace;
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;

end;

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

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;

theorem Th47: :: TMAP_1:47

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 )

proof end;

theorem Th48: :: TMAP_1:48

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

proof end;

theorem Th49: :: TMAP_1:49

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 )

proof end;

theorem Th50: :: TMAP_1:50

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

proof end;

theorem Th51: :: TMAP_1:51

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

proof end;

theorem Th52: :: TMAP_1:52

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

proof end;

theorem :: TMAP_1:53

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

proof end;

theorem :: TMAP_1:54

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

proof end;

theorem :: TMAP_1:55

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 Th49;

theorem Th56: :: TMAP_1:56

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

proof end;

theorem :: TMAP_1:57

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

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 ;
func f | R -> Function of R,T equals :Def3: :: TMAP_1:def 3
f | the carrier of R;
coherence
f | the carrier of R is Function of R,T

proof end;

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;

definition

let X, Y be non empty TopSpace;
let 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;
compatibility
for b₁ being Function of X0,Y holds
( b₁ = f | X0 iff b₁ = f | the carrier of X0 )

proof end;

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;

theorem :: TMAP_1:58

canceled;

theorem Th59: :: TMAP_1:59

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

proof end;

theorem Th60: :: TMAP_1:60

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

proof end;

theorem :: TMAP_1:61

for Y, X being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for A being Subset of X st A c= the carrier of X0 holds
f .: A = (f | X0) .: A by FUNCT_2:174;

theorem :: TMAP_1:62

for X, Y being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for B being Subset of Y st f " B c= the carrier of X0 holds
f " B = (f | X0) " B by FUNCT_2:175;

theorem Th63: :: TMAP_1:63

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

proof end;

theorem Th64: :: TMAP_1:64

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

proof end;

theorem Th65: :: TMAP_1:65

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 )

proof end;

theorem Th66: :: TMAP_1:66

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 )

proof end;

theorem :: TMAP_1:67

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 )

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;
cluster f | X0 -> continuous ;
coherence
f | X0 is continuous

proof end;

end;

theorem :: TMAP_1:68

canceled;

theorem Th69: :: TMAP_1:69

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)

proof end;

theorem Th70: :: TMAP_1:70

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

proof end;

theorem :: TMAP_1:71

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 Th70;

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 ;
func g | X1 -> Function of X1,Y equals :Def5: :: TMAP_1:def 5
g | the carrier of X1;
coherence
g | the carrier of X1 is Function of X1,Y

proof end;

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;

theorem Th72: :: TMAP_1:72

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

proof end;

theorem :: TMAP_1:73

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

proof end;

theorem Th74: :: TMAP_1:74

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

proof end;

theorem Th75: :: TMAP_1:75

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

proof end;

theorem :: 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 B being Subset of Y st g " B c= the carrier of X1 holds
g " B = (g | X1) " B

proof end;

theorem Th77: :: TMAP_1:77

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

proof end;

theorem Th78: :: TMAP_1:78

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

proof end;

theorem Th79: :: TMAP_1:79

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

proof end;

theorem :: TMAP_1:80

for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for f being Function of X,Y
for f0 being Function of X1,Y
for g being Function of X0,Y st X0 = X & f = g holds
( g | X1 = f0 iff f | X1 = f0 ) by Def5;

theorem Th81: :: TMAP_1:81

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

proof end;

theorem Th82: :: TMAP_1:82

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

proof end;

theorem Th83: :: TMAP_1:83

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 )

proof end;

theorem Th84: :: TMAP_1:84

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 )

proof end;

theorem :: TMAP_1:85

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 )

proof end;

theorem Th86: :: TMAP_1:86

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 )

proof end;

theorem :: TMAP_1:87

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 )

proof end;

theorem Th88: :: TMAP_1:88

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

proof end;

theorem Th89: :: TMAP_1:89

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

proof end;

theorem Th90: :: TMAP_1:90

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

proof end;

theorem :: TMAP_1:91

canceled;

theorem :: TMAP_1:92

canceled;

theorem :: TMAP_1:93

canceled;

registration

let X be non empty TopSpace;
cluster id X -> continuous ;
coherence
id X is continuous

proof end;

end;

definition

let X be non empty TopSpace;
let X0 be SubSpace of X;
canceled;
func incl X0 -> Function of X0,X equals :: TMAP_1:def 7
(id X) | X0;
coherence
(id X) | X0 is Function of X0,X ;
correctness
;

end;

:: deftheorem TMAP_1:def 6 :
canceled;

:: deftheorem defines incl TMAP_1:def 7 :
for X being non empty TopSpace
for X0 being SubSpace of X holds incl X0 = (id X) | X0;

notation

let X be non empty TopSpace;
let X0 be SubSpace of X;
synonym X0 incl X for incl X0;

end;

theorem :: TMAP_1:94

canceled;

theorem :: TMAP_1:95

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

proof end;

theorem :: TMAP_1:96

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

proof end;

theorem :: TMAP_1:97

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)

proof end;

theorem :: TMAP_1:98

for X being non empty TopSpace
for X0 being non empty SubSpace of X holds incl X0 is continuous Function of X0,X ;

begin

definition

let X be non empty TopSpace;
let A be Subset of X;
func A -extension_of_the_topology_of X -> Subset-Family of X equals :: TMAP_1:def 8
{ (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 ) } is Subset-Family of X

proof end;

end;

:: deftheorem defines -extension_of_the_topology_of TMAP_1:def 8 :
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 Th99: :: TMAP_1:99

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

proof end;

theorem Th100: :: TMAP_1:100

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

proof end;

theorem Th101: :: TMAP_1:101

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 )

proof end;

theorem Th102: :: TMAP_1:102

for X being non empty TopSpace
for A being Subset of X holds A in A -extension_of_the_topology_of X

proof end;

theorem Th103: :: TMAP_1:103

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 )

proof end;

definition

let X be non empty TopSpace;
let A be Subset of X;
func X modified_with_respect_to A -> strict TopSpace equals :: TMAP_1:def 9
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) #) is strict TopSpace

proof end;

end;

:: deftheorem defines modified_with_respect_to TMAP_1:def 9 :
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;
cluster X modified_with_respect_to A -> non empty strict ;
coherence
not X modified_with_respect_to A is empty ;

end;

theorem :: TMAP_1:104

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

theorem Th105: :: TMAP_1:105

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

proof end;

theorem Th106: :: TMAP_1:106

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 )

proof end;

definition

let X be non empty TopSpace;
let A be Subset of X;
func modid (X,A) -> Function of X,(X modified_with_respect_to A) equals :: TMAP_1:def 10
id the carrier of X;
coherence
id the carrier of X is Function of X,(X modified_with_respect_to A) ;

end;

:: deftheorem defines modid TMAP_1:def 10 :
for X being non empty TopSpace
for A being Subset of X holds modid (X,A) = id the carrier of X;

theorem :: TMAP_1:107

canceled;

theorem Th108: :: TMAP_1:108

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

proof end;

theorem Th109: :: TMAP_1:109

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

proof end;

theorem Th110: :: TMAP_1:110

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

proof end;

theorem Th111: :: TMAP_1:111

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)

proof end;

theorem Th112: :: TMAP_1:112

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)

proof end;

theorem Th113: :: TMAP_1:113

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

proof end;

definition

let X be non empty TopSpace;
let X0 be SubSpace of X;
func X modified_with_respect_to X0 -> strict TopSpace means :Def11: :: TMAP_1:def 11
for A being Subset of X st A = the carrier of X0 holds
it = X modified_with_respect_to A;
existence
ex b₁ being strict TopSpace st
for A being Subset of X st A = the carrier of X0 holds
b₁ = X modified_with_respect_to A

proof end;

uniqueness
for b₁, b₂ being strict TopSpace st ( for A being Subset of X st A = the carrier of X0 holds
b₁ = X modified_with_respect_to A ) & ( for A being Subset of X st A = the carrier of X0 holds
b₂ = X modified_with_respect_to A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines modified_with_respect_to TMAP_1:def 11 :
for X being non empty TopSpace
for X0 being SubSpace of X
for b₃ being strict TopSpace holds
( b₃ = X modified_with_respect_to X0 iff for A being Subset of X st A = the carrier of X0 holds
b₃ = X modified_with_respect_to A );

registration

let X be non empty TopSpace;
let X0 be SubSpace of X;
cluster X modified_with_respect_to X0 -> non empty strict ;
coherence
not X modified_with_respect_to X0 is empty

proof end;

end;

theorem Th114: :: TMAP_1:114

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

proof end;

theorem :: TMAP_1:115

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

proof end;

theorem :: TMAP_1:116

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 )

proof end;

definition

let X be non empty TopSpace;
let X0 be SubSpace of X;
func modid (X,X0) -> Function of X,(X modified_with_respect_to X0) means :Def12: :: TMAP_1:def 12
for A being Subset of X st A = the carrier of X0 holds
it = modid (X,A);
existence
ex b₁ 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₁ = modid (X,A)

proof end;

uniqueness
for b₁, b₂ 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₁ = modid (X,A) ) & ( for A being Subset of X st A = the carrier of X0 holds
b₂ = modid (X,A) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines modid TMAP_1:def 12 :
for X being non empty TopSpace
for X0 being SubSpace of X
for b₃ being Function of X,(X modified_with_respect_to X0) holds
( b₃ = modid (X,X0) iff for A being Subset of X st A = the carrier of X0 holds
b₃ = modid (X,A) );

theorem :: TMAP_1:117

for X being non empty TopSpace
for X0 being non empty SubSpace of X holds modid (X,X0) = id X

proof end;

theorem Th118: :: TMAP_1:118

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

proof end;

theorem Th119: :: TMAP_1:119

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

proof end;

theorem :: TMAP_1:120

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)

proof end;

theorem :: TMAP_1:121

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)

proof end;

theorem :: TMAP_1:122

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

proof end;

begin

theorem Th123: :: TMAP_1:123

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

proof end;

theorem :: TMAP_1:124

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

proof end;

theorem :: TMAP_1:125

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

proof end;

theorem Th126: :: TMAP_1:126

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

proof end;

theorem Th127: :: TMAP_1:127

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

proof end;

theorem Th128: :: TMAP_1:128

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

proof end;

theorem Th129: :: TMAP_1:129

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

proof end;

theorem :: TMAP_1:130

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

proof end;

theorem :: TMAP_1:131

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

proof end;

theorem Th132: :: TMAP_1:132

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

proof end;

theorem Th133: :: TMAP_1:133

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

proof end;

theorem Th134: :: TMAP_1:134

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

proof end;

theorem Th135: :: TMAP_1:135

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

proof end;

theorem Th136: :: TMAP_1:136

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

proof end;

theorem :: TMAP_1:137

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

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) ) ;
func f1 union f2 -> Function of (X1 union X2),Y means :Def13: :: TMAP_1:def 13
( it | X1 = f1 & it | X2 = f2 );
existence
ex b₁ being Function of (X1 union X2),Y st
( b₁ | X1 = f1 & b₁ | X2 = f2 )

proof end;

uniqueness
for b₁, b₂ being Function of (X1 union X2),Y st b₁ | X1 = f1 & b₁ | X2 = f2 & b₂ | X1 = f1 & b₂ | X2 = f2 holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines union TMAP_1:def 13 :
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₇ being Function of (X1 union X2),Y holds
( b₇ = f1 union f2 iff ( b₇ | X1 = f1 & b₇ | X2 = f2 ) );

theorem Th138: :: TMAP_1:138

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)

proof end;

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 g being Function of X,Y holds g = (g | X1) union (g | X2)

proof end;

theorem Th140: :: TMAP_1:140

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

proof end;

theorem :: TMAP_1:141

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

proof end;

theorem :: TMAP_1:142

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

proof end;

theorem :: TMAP_1:143

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)

proof end;

theorem :: TMAP_1:144

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

proof end;

theorem Th145: :: TMAP_1:145

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

proof end;

theorem :: TMAP_1:146

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

proof end;

theorem :: TMAP_1:147

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

proof end;

theorem :: TMAP_1:148

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

proof end;

theorem :: TMAP_1:149

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

proof end;

theorem :: TMAP_1:150

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

proof end;

theorem :: TMAP_1:151

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

proof end;

theorem :: TMAP_1:152

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

proof end;

theorem :: TMAP_1:153

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

proof end;