:: by Yatsuka Nakamura

::

:: Received July 16, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

theorem Th1: :: JGRAPH_2:1

for T, T1, T2, S being non empty TopSpace

for f being Function of T1,S

for g being Function of T2,S

for F1, F2 being Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is continuous & g is continuous & ( for p being object st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) holds

ex h being Function of T,S st

( h = f +* g & h is continuous )

for f being Function of T1,S

for g being Function of T2,S

for F1, F2 being Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is continuous & g is continuous & ( for p being object st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) holds

ex h being Function of T,S st

( h = f +* g & h is continuous )

proof end;

theorem Th2: :: JGRAPH_2:2

for n being Element of NAT

for q2 being Point of (Euclid n)

for q being Point of (TOP-REAL n)

for r being Real st q = q2 holds

Ball (q2,r) = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }

for q2 being Point of (Euclid n)

for q being Point of (TOP-REAL n)

for r being Real st q = q2 holds

Ball (q2,r) = { q3 where q3 is Point of (TOP-REAL n) : |.(q - q3).| < r }

proof end;

theorem Th9: :: JGRAPH_2:9

for B being Subset of (TOP-REAL 2) st B = {(0. (TOP-REAL 2))} holds

( B ` <> {} & the carrier of (TOP-REAL 2) \ B <> {} )

( B ` <> {} & the carrier of (TOP-REAL 2) \ B <> {} )

proof end;

theorem Th10: :: JGRAPH_2:10

for X, Y being non empty TopSpace

for f being Function of X,Y holds

( f is continuous iff for p being Point of X

for V being Subset of Y st f . p in V & V is open holds

ex W being Subset of X st

( p in W & W is open & f .: W c= V ) )

for f being Function of X,Y holds

( f is continuous iff for p being Point of X

for V being Subset of Y st f . p in V & V is open holds

ex W being Subset of X st

( p in W & W is open & f .: W c= V ) )

proof end;

theorem Th11: :: JGRAPH_2:11

for p being Point of (TOP-REAL 2)

for G being Subset of (TOP-REAL 2) st G is open & p in G holds

ex r being Real st

( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1) - r < q `1 & q `1 < (p `1) + r & (p `2) - r < q `2 & q `2 < (p `2) + r ) } c= G )

for G being Subset of (TOP-REAL 2) st G is open & p in G holds

ex r being Real st

( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1) - r < q `1 & q `1 < (p `1) + r & (p `2) - r < q `2 & q `2 < (p `2) + r ) } c= G )

proof end;

theorem Th12: :: JGRAPH_2:12

for X, Y, Z being non empty TopSpace

for B being Subset of Y

for C being Subset of Z

for f being Function of X,Y

for h being Function of (Y | B),(Z | C) st f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} holds

ex g being Function of X,Z st

( g is continuous & g = h * f )

for B being Subset of Y

for C being Subset of Z

for f being Function of X,Y

for h being Function of (Y | B),(Z | C) st f is continuous & h is continuous & rng f c= B & B <> {} & C <> {} holds

ex g being Function of X,Z st

( g is continuous & g = h * f )

proof end;

definition

ex b_{1} being Function of (NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)) st

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b_{1} . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or b_{1} . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) )

for b_{1}, b_{2} being Function of (NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)) st ( for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b_{1} . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or b_{1} . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) ) ) & ( for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b_{2} . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or b_{2} . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) ) ) holds

b_{1} = b_{2}
end;

func Out_In_Sq -> Function of (NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)) means :Def1: :: JGRAPH_2:def 1

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies it . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or it . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) );

existence for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies it . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or it . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) );

ex b

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b

proof end;

uniqueness for b

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b

b

proof end;

:: deftheorem Def1 defines Out_In_Sq JGRAPH_2:def 1 :

for b_{1} being Function of (NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)) holds

( b_{1} = Out_In_Sq iff for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b_{1} . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or b_{1} . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) ) );

for b

( b

( ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies b

theorem Th13: :: JGRAPH_2:13

for p being Point of (TOP-REAL 2) holds

( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) )

( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) )

proof end;

theorem Th14: :: JGRAPH_2:14

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) )

( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) )

proof end;

theorem Th15: :: JGRAPH_2:15

for D being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | D) st K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds

rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

for K0 being Subset of ((TOP-REAL 2) | D) st K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds

rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

proof end;

theorem Th16: :: JGRAPH_2:16

for D being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | D) st K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds

rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

for K0 being Subset of ((TOP-REAL 2) | D) st K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds

rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)

proof end;

Lm1: 0. (TOP-REAL 2) = 0.REAL 2

by EUCLID:66;

theorem Th17: :: JGRAPH_2:17

for K0a being set

for D being non empty Subset of (TOP-REAL 2) st K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } & D ` = {(0. (TOP-REAL 2))} holds

( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )

for D being non empty Subset of (TOP-REAL 2) st K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } & D ` = {(0. (TOP-REAL 2))} holds

( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )

proof end;

theorem Th18: :: JGRAPH_2:18

for K0a being set

for D being non empty Subset of (TOP-REAL 2) st K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } & D ` = {(0. (TOP-REAL 2))} holds

( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )

for D being non empty Subset of (TOP-REAL 2) st K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } & D ` = {(0. (TOP-REAL 2))} holds

( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )

proof end;

theorem Th19: :: JGRAPH_2:19

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 + r2 ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 + r2 ) & g is continuous )

proof end;

theorem :: JGRAPH_2:20

for X being non empty TopSpace

for a being Real ex g being Function of X,R^1 st

( ( for p being Point of X holds g . p = a ) & g is continuous )

for a being Real ex g being Function of X,R^1 st

( ( for p being Point of X holds g . p = a ) & g is continuous )

proof end;

theorem Th21: :: JGRAPH_2:21

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 - r2 ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 - r2 ) & g is continuous )

proof end;

theorem Th22: :: JGRAPH_2:22

for X being non empty TopSpace

for f1 being Function of X,R^1 st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 * r1 ) & g is continuous )

for f1 being Function of X,R^1 st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 * r1 ) & g is continuous )

proof end;

theorem Th23: :: JGRAPH_2:23

for X being non empty TopSpace

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = a * r1 ) & g is continuous )

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = a * r1 ) & g is continuous )

proof end;

theorem Th24: :: JGRAPH_2:24

for X being non empty TopSpace

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 + a ) & g is continuous )

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 + a ) & g is continuous )

proof end;

theorem Th25: :: JGRAPH_2:25

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * r2 ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * r2 ) & g is continuous )

proof end;

theorem Th26: :: JGRAPH_2:26

for X being non empty TopSpace

for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X holds f1 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = 1 / r1 ) & g is continuous )

for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X holds f1 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = 1 / r1 ) & g is continuous )

proof end;

theorem Th27: :: JGRAPH_2:27

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 / r2 ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 / r2 ) & g is continuous )

proof end;

theorem Th28: :: JGRAPH_2:28

for X being non empty TopSpace

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = (r1 / r2) / r2 ) & g is continuous )

for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = (r1 / r2) / r2 ) & g is continuous )

proof end;

theorem Th29: :: JGRAPH_2:29

for K0 being Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K0),R^1 st ( for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj1 . p ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K0),R^1 st ( for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj1 . p ) holds

f is continuous

proof end;

theorem Th30: :: JGRAPH_2:30

for K0 being Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K0),R^1 st ( for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj2 . p ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K0),R^1 st ( for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj2 . p ) holds

f is continuous

proof end;

theorem Th31: :: JGRAPH_2:31

for K1 being non empty Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = 1 / (p `1) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = 1 / (p `1) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

proof end;

theorem Th32: :: JGRAPH_2:32

for K1 being non empty Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = 1 / (p `2) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = 1 / (p `2) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

proof end;

theorem Th33: :: JGRAPH_2:33

for K1 being non empty Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = ((p `2) / (p `1)) / (p `1) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = ((p `2) / (p `1)) / (p `1) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `1 <> 0 ) holds

f is continuous

proof end;

theorem Th34: :: JGRAPH_2:34

for K1 being non empty Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = ((p `1) / (p `2)) / (p `2) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K1),R^1 st ( for p being Point of (TOP-REAL 2) st p in the carrier of ((TOP-REAL 2) | K1) holds

f . p = ((p `1) / (p `2)) / (p `2) ) & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds

q `2 <> 0 ) holds

f is continuous

proof end;

theorem Th35: :: JGRAPH_2:35

for K0, B0 being Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0)

for f1, f2 being Function of ((TOP-REAL 2) | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being Real st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds

f . |[x,y]| = |[r,s]| ) holds

f is continuous

for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0)

for f1, f2 being Function of ((TOP-REAL 2) | K0),R^1 st f1 is continuous & f2 is continuous & K0 <> {} & B0 <> {} & ( for x, y, r, s being Real st |[x,y]| in K0 & r = f1 . |[x,y]| & s = f2 . |[x,y]| holds

f . |[x,y]| = |[r,s]| ) holds

f is continuous

proof end;

theorem Th36: :: JGRAPH_2:36

for K0, B0 being Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

theorem Th37: :: JGRAPH_2:37

for K0, B0 being Subset of (TOP-REAL 2)

for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

for f being Function of ((TOP-REAL 2) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds

f is continuous

proof end;

Lm2: now :: thesis: for p01, p02, px1, px2 being Real st (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) holds

(p01 - p02) / 2 <= px1 - px2

(p01 - p02) / 2 <= px1 - px2

let p01, p02, px1, px2 be Real; :: thesis: ( (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) implies (p01 - p02) / 2 <= px1 - px2 )

set r0 = (p01 - p02) / 4;

assume (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) ; :: thesis: (p01 - p02) / 2 <= px1 - px2

then (p01 - p02) - (px1 - px2) <= ((p01 - p02) / 4) + ((p01 - p02) / 4) ;

then p01 - p02 <= (px1 - px2) + (((p01 - p02) / 4) + ((p01 - p02) / 4)) by XREAL_1:20;

then (p01 - p02) - ((p01 - p02) / 2) <= px1 - px2 by XREAL_1:20;

hence (p01 - p02) / 2 <= px1 - px2 ; :: thesis: verum

end;
set r0 = (p01 - p02) / 4;

assume (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) ; :: thesis: (p01 - p02) / 2 <= px1 - px2

then (p01 - p02) - (px1 - px2) <= ((p01 - p02) / 4) + ((p01 - p02) / 4) ;

then p01 - p02 <= (px1 - px2) + (((p01 - p02) / 4) + ((p01 - p02) / 4)) by XREAL_1:20;

then (p01 - p02) - ((p01 - p02) / 2) <= px1 - px2 by XREAL_1:20;

hence (p01 - p02) / 2 <= px1 - px2 ; :: thesis: verum

scheme :: JGRAPH_2:sch 3

ClosedSubset{ F_{1}( Point of (TOP-REAL 2)) -> Real, F_{2}( Point of (TOP-REAL 2)) -> Real } :

provided

ClosedSubset{ F

provided

A1:
for p, q being Point of (TOP-REAL 2) holds

( F_{1}((p - q)) = F_{1}(p) - F_{1}(q) & F_{2}((p - q)) = F_{2}(p) - F_{2}(q) )
and

A2: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (F_{1}((p - q)) ^2) + (F_{2}((p - q)) ^2)

( F

A2: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (F

proof end;

deffunc H

deffunc H

Lm3: for p, q being Point of (TOP-REAL 2) holds

( H

by TOPREAL3:3;

Lm4: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H

by JGRAPH_1:29;

Lm5: { p7 where p7 is Point of (TOP-REAL 2) : H

from JGRAPH_2:sch 3(Lm3, Lm4);

Lm6: for p, q being Point of (TOP-REAL 2) holds

( H

by TOPREAL3:3;

Lm7: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H

by JGRAPH_1:29;

Lm8: { p7 where p7 is Point of (TOP-REAL 2) : H

from JGRAPH_2:sch 3(Lm6, Lm7);

deffunc H

deffunc H

Lm9: now :: thesis: for p, q being Point of (TOP-REAL 2) holds

( H_{3}(p - q) = H_{3}(p) - H_{3}(q) & H_{2}(p - q) = H_{2}(p) - H_{2}(q) )

( H

let p, q be Point of (TOP-REAL 2); :: thesis: ( H_{3}(p - q) = H_{3}(p) - H_{3}(q) & H_{2}(p - q) = H_{2}(p) - H_{2}(q) )

thus H_{3}(p - q) =
- ((p `1) - (q `1))
by TOPREAL3:3

.= H_{3}(p) - H_{3}(q)
; :: thesis: H_{2}(p - q) = H_{2}(p) - H_{2}(q)

thus H_{2}(p - q) = H_{2}(p) - H_{2}(q)
by TOPREAL3:3; :: thesis: verum

end;
thus H

.= H

thus H

Lm10: now :: thesis: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H_{3}(p - q) ^2) + (H_{2}(p - q) ^2)

let p, q be Point of (TOP-REAL 2); :: thesis: |.(p - q).| ^2 = (H_{3}(p - q) ^2) + (H_{2}(p - q) ^2)

H_{3}(p - q) ^2 = H_{1}(p - q) ^2
;

hence |.(p - q).| ^2 = (H_{3}(p - q) ^2) + (H_{2}(p - q) ^2)
by JGRAPH_1:29; :: thesis: verum

end;
H

hence |.(p - q).| ^2 = (H

Lm11: { p7 where p7 is Point of (TOP-REAL 2) : H

from JGRAPH_2:sch 3(Lm9, Lm10);

Lm12: now :: thesis: for p, q being Point of (TOP-REAL 2) holds

( H_{2}(p - q) = H_{2}(p) - H_{2}(q) & H_{3}(p - q) = H_{3}(p) - H_{3}(q) )

( H

let p, q be Point of (TOP-REAL 2); :: thesis: ( H_{2}(p - q) = H_{2}(p) - H_{2}(q) & H_{3}(p - q) = H_{3}(p) - H_{3}(q) )

thus H_{2}(p - q) = H_{2}(p) - H_{2}(q)
by TOPREAL3:3; :: thesis: H_{3}(p - q) = H_{3}(p) - H_{3}(q)

thus H_{3}(p - q) =
- ((p `1) - (q `1))
by TOPREAL3:3

.= H_{3}(p) - H_{3}(q)
; :: thesis: verum

end;
thus H

thus H

.= H

Lm13: now :: thesis: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H_{2}(p - q) ^2) + (H_{3}(p - q) ^2)

let p, q be Point of (TOP-REAL 2); :: thesis: |.(p - q).| ^2 = (H_{2}(p - q) ^2) + (H_{3}(p - q) ^2)

(- ((p - q) `1)) ^2 = ((p - q) `1) ^2 ;

hence |.(p - q).| ^2 = (H_{2}(p - q) ^2) + (H_{3}(p - q) ^2)
by JGRAPH_1:29; :: thesis: verum

end;
(- ((p - q) `1)) ^2 = ((p - q) `1) ^2 ;

hence |.(p - q).| ^2 = (H

Lm14: { p7 where p7 is Point of (TOP-REAL 2) : H

from JGRAPH_2:sch 3(Lm12, Lm13);

Lm15: now :: thesis: for p, q being Point of (TOP-REAL 2) holds

( H_{4}(p - q) = H_{4}(p) - H_{4}(q) & H_{1}(p - q) = H_{1}(p) - H_{1}(q) )

( H

let p, q be Point of (TOP-REAL 2); :: thesis: ( H_{4}(p - q) = H_{4}(p) - H_{4}(q) & H_{1}(p - q) = H_{1}(p) - H_{1}(q) )

thus H_{4}(p - q) =
- ((p `2) - (q `2))
by TOPREAL3:3

.= H_{4}(p) - H_{4}(q)
; :: thesis: H_{1}(p - q) = H_{1}(p) - H_{1}(q)

thus H_{1}(p - q) = H_{1}(p) - H_{1}(q)
by TOPREAL3:3; :: thesis: verum

end;
thus H

.= H

thus H

Lm16: now :: thesis: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H_{4}(p - q) ^2) + (H_{1}(p - q) ^2)

let p, q be Point of (TOP-REAL 2); :: thesis: |.(p - q).| ^2 = (H_{4}(p - q) ^2) + (H_{1}(p - q) ^2)

(- ((p - q) `2)) ^2 = ((p - q) `2) ^2 ;

hence |.(p - q).| ^2 = (H_{4}(p - q) ^2) + (H_{1}(p - q) ^2)
by JGRAPH_1:29; :: thesis: verum

end;
(- ((p - q) `2)) ^2 = ((p - q) `2) ^2 ;

hence |.(p - q).| ^2 = (H

Lm17: { p7 where p7 is Point of (TOP-REAL 2) : H

from JGRAPH_2:sch 3(Lm15, Lm16);

Lm18: now :: thesis: for p, q being Point of (TOP-REAL 2) holds

( H_{1}(p - q) = H_{1}(p) - H_{1}(q) & H_{4}(p - q) = H_{4}(p) - H_{4}(q) )

( H

let p, q be Point of (TOP-REAL 2); :: thesis: ( H_{1}(p - q) = H_{1}(p) - H_{1}(q) & H_{4}(p - q) = H_{4}(p) - H_{4}(q) )

thus H_{1}(p - q) = H_{1}(p) - H_{1}(q)
by TOPREAL3:3; :: thesis: H_{4}(p - q) = H_{4}(p) - H_{4}(q)

thus H_{4}(p - q) =
- ((p `2) - (q `2))
by TOPREAL3:3

.= H_{4}(p) - H_{4}(q)
; :: thesis: verum

end;
thus H

thus H

.= H

Lm19: now :: thesis: for p, q being Point of (TOP-REAL 2) holds |.(p - q).| ^2 = (H_{1}(p - q) ^2) + (H_{4}(p - q) ^2)

let p, q be Point of (TOP-REAL 2); :: thesis: |.(p - q).| ^2 = (H_{1}(p - q) ^2) + (H_{4}(p - q) ^2)

H_{4}(p - q) ^2 = H_{2}(p - q) ^2
;

hence |.(p - q).| ^2 = (H_{1}(p - q) ^2) + (H_{4}(p - q) ^2)
by JGRAPH_1:29; :: thesis: verum

end;
H

hence |.(p - q).| ^2 = (H

Lm20: { p7 where p7 is Point of (TOP-REAL 2) : H

from JGRAPH_2:sch 3(Lm18, Lm19);

theorem Th38: :: JGRAPH_2:38

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for f being Function of (((TOP-REAL 2) | B0) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds

( f is continuous & K0 is closed )

for K0 being Subset of ((TOP-REAL 2) | B0)

for f being Function of (((TOP-REAL 2) | B0) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds

( f is continuous & K0 is closed )

proof end;

theorem Th39: :: JGRAPH_2:39

for B0 being Subset of (TOP-REAL 2)

for K0 being Subset of ((TOP-REAL 2) | B0)

for f being Function of (((TOP-REAL 2) | B0) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds

( f is continuous & K0 is closed )

for K0 being Subset of ((TOP-REAL 2) | B0)

for f being Function of (((TOP-REAL 2) | B0) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } holds

( f is continuous & K0 is closed )

proof end;

theorem Th40: :: JGRAPH_2:40

for D being non empty Subset of (TOP-REAL 2) st D ` = {(0. (TOP-REAL 2))} holds

ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = Out_In_Sq & h is continuous )

ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st

( h = Out_In_Sq & h is continuous )

proof end;

theorem Th41: :: JGRAPH_2:41

for B, K0, Kb being Subset of (TOP-REAL 2) st B = {(0. (TOP-REAL 2))} & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } holds

ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st

( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds

not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds

f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds

f . s = s ) )

ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st

( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds

not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds

f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds

f . s = s ) )

proof end;

theorem Th42: :: JGRAPH_2:42

for f, g being Function of I[01],(TOP-REAL 2)

for K0 being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & (f . O) `1 = - 1 & (f . I) `1 = 1 & - 1 <= (f . O) `2 & (f . O) `2 <= 1 & - 1 <= (f . I) `2 & (f . I) `2 <= 1 & (g . O) `2 = - 1 & (g . I) `2 = 1 & - 1 <= (g . O) `1 & (g . O) `1 <= 1 & - 1 <= (g . I) `1 & (g . I) `1 <= 1 & rng f misses K0 & rng g misses K0 holds

rng f meets rng g

for K0 being Subset of (TOP-REAL 2)

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & (f . O) `1 = - 1 & (f . I) `1 = 1 & - 1 <= (f . O) `2 & (f . O) `2 <= 1 & - 1 <= (f . I) `2 & (f . I) `2 <= 1 & (g . O) `2 = - 1 & (g . I) `2 = 1 & - 1 <= (g . O) `1 & (g . O) `1 <= 1 & - 1 <= (g . I) `1 & (g . I) `1 <= 1 & rng f misses K0 & rng g misses K0 holds

rng f meets rng g

proof end;

theorem Th43: :: JGRAPH_2:43

for A, B, C, D being Real

for f being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for t being Point of (TOP-REAL 2) holds f . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ) holds

f is continuous

for f being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for t being Point of (TOP-REAL 2) holds f . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ) holds

f is continuous

proof end;

definition

let A, B, C, D be Real;

ex b_{1} being Function of (TOP-REAL 2),(TOP-REAL 2) st

for t being Point of (TOP-REAL 2) holds b_{1} . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]|

for b_{1}, b_{2} being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for t being Point of (TOP-REAL 2) holds b_{1} . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ) & ( for t being Point of (TOP-REAL 2) holds b_{2} . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| ) holds

b_{1} = b_{2}

end;
func AffineMap (A,B,C,D) -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def2: :: JGRAPH_2:def 2

for t being Point of (TOP-REAL 2) holds it . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]|;

existence for t being Point of (TOP-REAL 2) holds it . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]|;

ex b

for t being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines AffineMap JGRAPH_2:def 2 :

for A, B, C, D being Real

for b_{5} being Function of (TOP-REAL 2),(TOP-REAL 2) holds

( b_{5} = AffineMap (A,B,C,D) iff for t being Point of (TOP-REAL 2) holds b_{5} . t = |[((A * (t `1)) + B),((C * (t `2)) + D)]| );

for A, B, C, D being Real

for b

( b

theorem :: JGRAPH_2:45

for f, g being Function of I[01],(TOP-REAL 2)

for a, b, c, d being Real

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds

( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds

( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) holds

rng f meets rng g

for a, b, c, d being Real

for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & (f . O) `1 = a & (f . I) `1 = b & c <= (f . O) `2 & (f . O) `2 <= d & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & (g . I) `2 = d & a <= (g . O) `1 & (g . O) `1 <= b & a <= (g . I) `1 & (g . I) `1 <= b & a < b & c < d & ( for r being Point of I[01] holds

( not a < (f . r) `1 or not (f . r) `1 < b or not c < (f . r) `2 or not (f . r) `2 < d ) ) & ( for r being Point of I[01] holds

( not a < (g . r) `1 or not (g . r) `1 < b or not c < (g . r) `2 or not (g . r) `2 < d ) ) holds

rng f meets rng g

proof end;

theorem :: JGRAPH_2:46

theorem :: JGRAPH_2:47

theorem :: JGRAPH_2:48