environ
vocabularies HIDDEN, ARYTM_1, ARYTM_3, CARD_1, COMPLEX1, CONVEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_4, MEMBERED, METRIC_1, NAT_1, NUMBERS, ORDINAL2, PCOMPS_1, PRE_TOPC, RCOMP_1, REAL_1, RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPMETR, TOPS_1, TOPS_2, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_2, FUNCT_2, EUCLID_9, TOPREALC, FINSEQ_1, XXREAL_1, FINSEQ_2, CARD_3, PARTFUN3, SQUARE_1, FUNCT_6, XCMPLX_0, PARTFUN1, FINSET_1, ZFMISC_1, VALUED_0, SETFAM_1, T_0TOPSP, BROUWER, ORDINAL4, TIETZE_2, FUNCT_3;
notations HIDDEN, TARSKI, XBOOLE_0, FINSET_1, SETFAM_1, VALUED_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, RVSUM_1, XCMPLX_0, MEMBERED, FUNCOP_1, FINSEQ_1, FINSEQ_2, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, TOPMETR, FUNCT_7, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL9, PARTFUN3, TOPS_2, COMPTS_1, TBSP_1, XXREAL_2, EUCLID_9, CARD_3, SQUARE_1, FUNCT_6, TOPREALC, METRIZTS, ZFMISC_1, RCOMP_1, BORSUK_1, T_0TOPSP, BINOP_1, FUNCT_3, NAT_1, BORSUK_2, BROUWER, TMAP_1;
definitions TARSKI, XBOOLE_0, CONVEX1;
theorems ABSVALUE, BORSUK_1, BROUWER, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_2, GOBOARD6, JORDAN2C, MEMBERED, ORDINAL1, PRE_TOPC, RELAT_1, SUBSET_1, TARSKI, TBSP_1, TOPMETR, TOPREAL9, TOPREALC, TOPS_1, TOPS_2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, XXREAL_2, ZFMISC_1, EUCLID_9, FINSEQ_2, TIETZE, CARD_1, CARD_3, FINSEQ_1, PARTFUN3, XXREAL_1, FINSEQ_3, VALUED_1, PARTFUN1, FUNCT_7, TOPREAL7, JORDAN6, SETFAM_1, BROUWER2, FUNCT_6, METRIZTS, T_0TOPSP, FUNCTOR0, FUNCT_3, TOPGRP_1, BORSUK_2, SIMPLEX2, JORDAN24, BORSUK_3, NAT_1, JORDAN, TMAP_1;
schemes FINSEQ_1;
registrations BORSUK_1, EUCLID, EUCLID_9, FUNCOP_1, FINSEQ_1, FUNCT_1, FUNCT_2, MEMBERED, NAT_1, PCOMPS_1, PRE_TOPC, RELAT_1, PARTFUN3, RVSUM_1, SIMPLEX2, STRUCT_0, SUBSET_1, TOPGRP_1, TOPMETR, TOPS_1, VALUED_0, VALUED_2, XBOOLE_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, TBSP_1, MONOID_0, JORDAN2B, FINSEQ_2, XXREAL_2, COMPTS_1, CARD_1, TOPREAL1, RLAFFIN3, XCMPLX_0, TOPREAL9, FUNCT_3, FUNCT_6, NUMBERS, BORSUK_2, TMAP_1, TOPREALC;
constructors HIDDEN, COMPLEX1, TBSP_1, MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1, FUNCSDOM, PARTFUN3, TOPREALC, SEQ_4, EUCLID_9, SQUARE_1, FUNCT_6, METRIZTS, BORSUK_3, BORSUK_2, BROUWER, TMAP_1;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
equalities BINOP_1, FUNCOP_1, TARSKI, XBOOLE_0, STRUCT_0, FINSEQ_2, CONVEX1, XCMPLX_0, TOPREAL9, XXREAL_0, ORDINAL1, CARD_1;
expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, STRUCT_0, FINSEQ_2, CONVEX1, XCMPLX_0, TOPREAL9, XXREAL_0;
theorem Th15:
for
n,
m being
Nat for
pn being
Point of
(TOP-REAL n) for
pm being
Point of
(TOP-REAL m) for
r,
s being
Real st
r > 0 &
s > 0 holds
ex
h being
Function of
[:((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r)))),((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))):],
((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st
(
h is
being_homeomorphism &
h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] = OpenHypercube (
(0. (TOP-REAL (n + m))),1) )
theorem Th16:
for
n,
m being
Nat for
T1,
T2 being non
empty TopSpace for
pn being
Point of
(TOP-REAL n) for
pm being
Point of
(TOP-REAL m) for
r,
s being
Real st
r > 0 &
s > 0 holds
for
f being
Function of
T1,
((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r)))) for
g being
Function of
T2,
((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))) st
f is
being_homeomorphism &
g is
being_homeomorphism holds
ex
h being
Function of
[:T1,T2:],
((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st
(
h is
being_homeomorphism & ( for
t1 being
Point of
T1 for
t2 being
Point of
T2 holds
( (
f . t1 in OpenHypercube (
pn,
r) &
g . t2 in OpenHypercube (
pm,
s) ) iff
h . (
t1,
t2)
in OpenHypercube (
(0. (TOP-REAL (n + m))),1) ) ) )
Lm1:
for n being Nat
for p being Point of (TOP-REAL n)
for r being Real st r > 0 holds
( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )
theorem Th18:
for
n,
m being
Nat for
pn being
Point of
(TOP-REAL n) for
pm being
Point of
(TOP-REAL m) for
r,
s being
Real st
r > 0 &
s > 0 holds
ex
h being
Function of
[:(Tdisk (pn,r)),(Tdisk (pm,s)):],
(Tdisk ((0. (TOP-REAL (n + m))),1)) st
(
h is
being_homeomorphism &
h .: [:(Ball (pn,r)),(Ball (pm,s)):] = Ball (
(0. (TOP-REAL (n + m))),1) )
theorem
for
n,
m being
Nat for
r,
s being
Real for
T1,
T2 being non
empty TopSpace for
pn being
Point of
(TOP-REAL n) for
pm being
Point of
(TOP-REAL m) st
r > 0 &
s > 0 &
T1,
(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic &
T2,
(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds
[:T1,T2:],
(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic
Lm2:
for n being Nat
for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds
for e being Point of (Euclid n) st e in V holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= V )
::