environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, XBOOLE_0, METRIC_1, REAL_1, XXREAL_0, ARYTM_3, RELAT_1, TARSKI, ORDINAL4, NAT_1, ARYTM_1, FUNCT_1, FINSEQ_2, RVSUM_1, COMPLEX1, EUCLID, SQUARE_1, STRUCT_0, ZFMISC_1, PRE_TOPC, MCART_1, CARD_1, RELAT_2, PCOMPS_1, SETFAM_1, BORSUK_1, RCOMP_1, T_0TOPSP, CARD_3, ORDINAL2, TOPREAL7, TOPS_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, XCMPLX_0, COMPLEX1, BINOP_1, MCART_1, ORDINAL1, NUMBERS, XXREAL_0, DOMAIN_1, XREAL_0, REAL_1, SQUARE_1, NAT_1, FINSEQ_1, RVSUM_1, STRUCT_0, PRE_TOPC, TOPS_2, PCOMPS_1, BORSUK_1, METRIC_1, EUCLID, FINSEQ_2, T_0TOPSP;
definitions TARSKI, FUNCT_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_2, T_0TOPSP, XBOOLE_0;
theorems BINOP_1, BORSUK_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2, INT_1, MCART_1, METRIC_1, NAT_1, PCOMPS_1, RVSUM_1, SQUARE_1, TARSKI, TBSP_1, TOPMETR, TOPREAL3, TOPREAL6, TOPS_2, ZFMISC_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, CARD_1, XTUPLE_0, XREAL_0;
schemes BINOP_1;
registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, INT_1, VALUED_0, FINSEQ_2, RELAT_1, NAT_1, XTUPLE_0;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, TOPS_2, BORSUK_1, T_0TOPSP, GOBOARD1, RVSUM_1, BINOP_2, PCOMPS_1, XTUPLE_0, BINOP_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, METRIC_1, XBOOLE_0, EUCLID, BINOP_1;
expansions TARSKI, METRIC_1, PRE_TOPC;
definition
let M,
N be non
empty MetrStruct ;
func max-Prod2 (
M,
N)
-> strict MetrStruct means :
Def1:
( 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))) ) ) )
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
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))) ) ) ) );
Lm1:
for M, N being non empty MetrSpace holds max-Prod2 (M,N) is discerning
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 ) )