:: TOPREAL7 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: TOPREAL7:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real st max a,b <= a holds
max a,b = a
proof end;

theorem Th2: :: TOPREAL7:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being Real holds max (a + c),(b + d) <= (max a,b) + (max c,d)
proof end;

theorem Th3: :: TOPREAL7:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: TOPREAL7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence holds dom g c= dom (f ^ g)
proof end;

theorem Th5: :: TOPREAL7:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th6: :: TOPREAL7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th7: :: TOPREAL7:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th8: :: TOPREAL7:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th9: :: TOPREAL7:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds
( len f = len (sqr f) & dom f = dom (sqr f) )
proof end;

theorem Th10: :: TOPREAL7:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds
( len f = len (abs f) & dom f = dom (abs f) )
proof end;

theorem Th11: :: TOPREAL7:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of REAL holds sqr (f ^ g) = (sqr f) ^ (sqr g)
proof end;

theorem :: TOPREAL7:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of REAL holds abs (f ^ g) = (abs f) ^ (abs g)
proof end;

theorem :: TOPREAL7:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem :: TOPREAL7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem :: TOPREAL7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem Th16: :: TOPREAL7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem Th17: :: TOPREAL7:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being FinSequence of REAL st len f = n holds
f in the carrier of (Euclid n)
proof end;

theorem :: TOPREAL7:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being FinSequence of REAL st len f = n holds
f in the carrier of (TOP-REAL n)
proof end;

theorem Th19: :: TOPREAL7:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being FinSequence st f in the carrier of (Euclid n) holds
len f = n by FINSEQ_2:109;

definition
let M, N be non empty MetrStruct ;
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
ex b1 being strict MetrStruct st
( the carrier of b1 = [:the carrier of M,the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b1 . x,y = max (the distance of M . x1,y1),(the distance of N . x2,y2) ) ) )
proof end;
uniqueness
for b1, b2 being strict MetrStruct st the carrier of b1 = [:the carrier of M,the carrier of N:] & ( for x, y being Point of b1 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b1 . x,y = max (the distance of M . x1,y1),(the distance of N . x2,y2) ) ) & the carrier of b2 = [:the carrier of M,the carrier of N:] & ( for x, y being Point of b2 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b2 . x,y = max (the distance of M . x1,y1),(the distance of N . x2,y2) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines max-Prod2 TOPREAL7:def 1 :
for M, N being non empty MetrStruct
for b3 being strict MetrStruct holds
( b3 = max-Prod2 M,N iff ( the carrier of b3 = [:the carrier of M,the carrier of N:] & ( for x, y being Point of b3 ex x1, y1 being Point of M ex x2, y2 being Point of N st
( x = [x1,x2] & y = [y1,y2] & the distance of b3 . x,y = max (the distance of M . x1,y1),(the distance of N . x2,y2) ) ) ) );

registration
let M, N be non empty MetrStruct ;
cluster max-Prod2 M,N -> non empty strict ;
coherence
not max-Prod2 M,N is empty
proof end;
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)
proof end;
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
proof end;
:: original: `2
redefine func x `2 -> Element of N;
coherence
x `2 is Element of N
proof end;
end;

theorem Th20: :: TOPREAL7:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: TOPREAL7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ))
proof end;

theorem Th22: :: TOPREAL7:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M, N being non empty Reflexive MetrStruct holds max-Prod2 M,N is Reflexive
proof end;

registration
let M, N be non empty Reflexive MetrStruct ;
cluster max-Prod2 M,N -> non empty strict Reflexive ;
coherence
max-Prod2 M,N is Reflexive
by Th22;
end;

Lm1: for M, N being non empty MetrSpace holds max-Prod2 M,N is discerning
proof end;

theorem Th23: :: TOPREAL7:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M, N being non empty symmetric MetrStruct holds max-Prod2 M,N is symmetric
proof end;

registration
let M, N be non empty symmetric MetrStruct ;
cluster max-Prod2 M,N -> non empty strict symmetric ;
coherence
max-Prod2 M,N is symmetric
by Th23;
end;

theorem Th24: :: TOPREAL7:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M, N being non empty triangle MetrStruct holds max-Prod2 M,N is triangle
proof end;

registration
let M, N be non empty triangle MetrStruct ;
cluster max-Prod2 M,N -> non empty strict triangle ;
coherence
max-Prod2 M,N is triangle
by Th24;
end;

registration
let M, N be non empty MetrSpace;
cluster max-Prod2 M,N -> non empty strict Reflexive discerning symmetric triangle ;
coherence
max-Prod2 M,N is discerning
by Lm1;
end;

theorem Th25: :: TOPREAL7:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M, N being non empty MetrSpace holds [:(TopSpaceMetr M),(TopSpaceMetr N):] = TopSpaceMetr (max-Prod2 M,N)
proof end;

theorem :: TOPREAL7:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: TOPREAL7:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat holds [:(TOP-REAL i),(TOP-REAL j):], TOP-REAL (i + j) are_homeomorphic
proof end;