:: by Artur Korni{\l}owicz

::

:: Received February 21, 1999

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

begin

theorem Th2: :: TOPREAL7:2

for a, b, c, d, e, f being Real st a <= b + c & d <= e + f holds

max (a,d) <= (max (b,e)) + (max (c,f))

max (a,d) <= (max (b,e)) + (max (c,f))

proof end;

theorem Th4: :: TOPREAL7:4

for i being Nat

for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds

i - (len f) in dom g

for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds

i - (len f) in dom g

proof end;

theorem Th5: :: TOPREAL7:5

for f, g, h, k being FinSequence st f ^ g = h ^ k & len f = len h & len g = len k holds

( f = h & g = k )

( f = h & g = k )

proof end;

theorem Th6: :: TOPREAL7:6

for f, g being FinSequence of REAL st ( len f = len g or dom f = dom g ) holds

( len (f + g) = len f & dom (f + g) = dom f )

( len (f + g) = len f & dom (f + g) = dom f )

proof end;

theorem Th7: :: TOPREAL7:7

for f, g being FinSequence of REAL st ( len f = len g or dom f = dom g ) holds

( len (f - g) = len f & dom (f - g) = dom f )

( len (f - g) = len f & dom (f - g) = dom f )

proof end;

theorem :: TOPREAL7:12

for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds

sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k))

sqr ((f ^ g) + (h ^ k)) = (sqr (f + h)) ^ (sqr (g + k))

proof end;

theorem :: TOPREAL7:13

for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds

abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k))

abs ((f ^ g) + (h ^ k)) = (abs (f + h)) ^ (abs (g + k))

proof end;

theorem :: TOPREAL7:14

for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds

sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k))

sqr ((f ^ g) - (h ^ k)) = (sqr (f - h)) ^ (sqr (g - k))

proof end;

theorem Th15: :: TOPREAL7:15

for f, h, g, k being FinSequence of REAL st len f = len h & len g = len k holds

abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k))

abs ((f ^ g) - (h ^ k)) = (abs (f - h)) ^ (abs (g - k))

proof end;

theorem Th16: :: TOPREAL7:16

for n being Element of NAT

for f being FinSequence of REAL st len f = n holds

f in the carrier of (Euclid n) by TOPREAL3:45;

for f being FinSequence of REAL st len f = n holds

f in the carrier of (Euclid n) by TOPREAL3:45;

theorem :: TOPREAL7:17

for n being Element of NAT

for f being FinSequence of REAL st len f = n holds

f in the carrier of (TOP-REAL n) by TOPREAL3:46;

for f being FinSequence of REAL st len f = n holds

f in the carrier of (TOP-REAL n) by TOPREAL3:46;

definition

let M, N be non empty MetrStruct ;

ex b_{1} being strict MetrStruct st

( the carrier of b_{1} = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b_{1} ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of b_{1} . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) )

for b_{1}, b_{2} being strict MetrStruct st the carrier of b_{1} = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b_{1} ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of b_{1} . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) & the carrier of b_{2} = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b_{2} ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of b_{2} . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) holds

b_{1} = b_{2}

end;
func max-Prod2 (M,N) -> strict MetrStruct means :Def1: :: TOPREAL7:def 1

( the carrier of it = [: the carrier of M, the carrier of N:] & ( for x, y being Point of it ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of it . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) );

existence ( the carrier of it = [: the carrier of M, the carrier of N:] & ( for x, y being Point of it ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of it . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) );

ex b

( the carrier of b

( x = [x1,x2] & y = [y1,y2] & the distance of b

proof end;

uniqueness for b

( x = [x1,x2] & y = [y1,y2] & the distance of b

( x = [x1,x2] & y = [y1,y2] & the distance of b

b

proof end;

:: deftheorem Def1 defines max-Prod2 TOPREAL7:def 1 :

for M, N being non empty MetrStruct

for b_{3} being strict MetrStruct holds

( b_{3} = max-Prod2 (M,N) iff ( the carrier of b_{3} = [: the carrier of M, the carrier of N:] & ( for x, y being Point of b_{3} ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of b_{3} . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) ) );

for M, N being non empty MetrStruct

for b

( b

( x = [x1,x2] & y = [y1,y2] & the distance of b

registration
end;

definition

let M, N be non empty MetrStruct ;

let x be Point of M;

let y be Point of N;

:: original: [

redefine func [x,y] -> Element of (max-Prod2 (M,N));

coherence

[x,y] is Element of (max-Prod2 (M,N))

end;
let x be Point of M;

let y be Point of N;

:: original: [

redefine func [x,y] -> Element of (max-Prod2 (M,N));

coherence

[x,y] is Element of (max-Prod2 (M,N))

proof end;

definition

let M, N be non empty MetrStruct ;

let x be Point of (max-Prod2 (M,N));

:: original: `1

redefine func x `1 -> Element of M;

coherence

x `1 is Element of M

redefine func x `2 -> Element of N;

coherence

x `2 is Element of N

end;
let x be Point of (max-Prod2 (M,N));

:: original: `1

redefine func x `1 -> Element of M;

coherence

x `1 is Element of M

proof end;

:: original: `2redefine func x `2 -> Element of N;

coherence

x `2 is Element of N

proof end;

theorem Th18: :: TOPREAL7:18

for M, N being non empty MetrStruct

for m1, m2 being Point of M

for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))

for m1, m2 being Point of M

for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))

proof end;

theorem :: TOPREAL7:19

for M, N being non empty MetrStruct

for m, n being Point of (max-Prod2 (M,N)) holds dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2))))

for m, n being Point of (max-Prod2 (M,N)) holds dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2))))

proof end;

registration
end;

Lm1: for M, N being non empty MetrSpace holds max-Prod2 (M,N) is discerning

proof end;

registration
end;

registration
end;

theorem Th23: :: TOPREAL7:23

for M, N being non empty MetrSpace holds [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 (M,N))

proof end;

theorem :: TOPREAL7:24

for M, N being non empty MetrSpace st the carrier of M = the carrier of N & ( for m being Point of M

for n being Point of N

for r being Real st r > 0 & m = n holds

ex r1 being Real st

( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M

for n being Point of N

for r being Real st r > 0 & m = n holds

ex r1 being Real st

( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) holds

TopSpaceMetr M = TopSpaceMetr N

for n being Point of N

for r being Real st r > 0 & m = n holds

ex r1 being Real st

( r1 > 0 & Ball (n,r1) c= Ball (m,r) ) ) & ( for m being Point of M

for n being Point of N

for r being Real st r > 0 & m = n holds

ex r1 being Real st

( r1 > 0 & Ball (m,r1) c= Ball (n,r) ) ) holds

TopSpaceMetr M = TopSpaceMetr N

proof end;

Lm2: for i, j being Element of NAT ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st

( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) )

proof end;

theorem :: TOPREAL7:25

for i, j being Element of NAT holds [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], TopSpaceMetr (Euclid (i + j)) are_homeomorphic

proof end;

theorem :: TOPREAL7:26

for i, j being Element of NAT ex f being Function of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):],(TopSpaceMetr (Euclid (i + j))) st

( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) ) by Lm2;

( f is being_homeomorphism & ( for fi, fj being FinSequence st [fi,fj] in dom f holds

f . (fi,fj) = fi ^ fj ) ) by Lm2;