environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, TOPMETR, ZFMISC_1, INT_1, ARYTM_3, ARYTM_1, XXREAL_0, XXREAL_1, XBOOLE_0, CARD_1, FUNCT_1, RELAT_1, FINSEQ_1, CARD_3, FUNCOP_1, MONOID_0, PRE_TOPC, PCOMPS_1, EUCLID, SUBSET_1, RCOMP_1, CONNSP_2, TOPS_1, TARSKI, NATTRA_1, TDLAT_3, ORDINAL2, FUNCT_2, T_0TOPSP, TOPS_2, PARTFUN1, REAL_1, FCONT_1, TMAP_1, JGRAPH_6, MCART_1, TOPREALA, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, FUNCOP_1, INT_1, CARD_3, FINSEQ_1, FUNCT_4, MONOID_0, RCOMP_1, FCONT_1, STRUCT_0, PRE_TOPC, PCOMPS_1, TOPS_1, BORSUK_1, TSEP_1, TOPS_2, TDLAT_3, CONNSP_2, T_0TOPSP, TMAP_1, TOPMETR, EUCLID, JGRAPH_6;
definitions TARSKI, XBOOLE_0, FUNCT_2, PRE_TOPC, T_0TOPSP, TMAP_1, STRUCT_0, RCOMP_1, FCONT_1, MONOID_0, PARTFUN2;
theorems PRE_TOPC, XREAL_0, FUNCT_2, BORSUK_1, EUCLID, TOPS_2, BORSUK_3, FUNCT_1, TOPMETR, RELAT_1, FUNCOP_1, TOPREAL6, JORDAN16, BORSUK_6, TARSKI, ZFMISC_1, FUNCT_4, TSEP_1, HILBERT3, FINSEQ_1, TMAP_1, XBOOLE_1, JORDAN6, TOPS_3, FCONT_1, CONNSP_2, FRECHET, XBOOLE_0, FINSEQ_3, NAT_1, RCOMP_1, TEX_2, DOMAIN_1, TOPS_1, TOPGRP_1, TREAL_1, CARD_3, JGRAPH_6, TDLAT_3, ENUMSET1, TOPALG_3, XREAL_1, XXREAL_0, XXREAL_1;
schemes ;
registrations RELSET_1, FUNCT_2, FUNCT_4, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, MONOID_0, EUCLID, TOPMETR, TOPGRP_1, VALUED_0, FCONT_1, PCOMPS_1, FUNCT_1, RELAT_1, ORDINAL1;
constructors HIDDEN, FUNCT_4, REAL_1, CARD_3, RCOMP_1, FINSEQ_4, FCONT_1, TOPS_1, TOPS_2, TDLAT_3, TMAP_1, T_0TOPSP, MONOID_0, BORSUK_4, JGRAPH_6, FUNCSDOM, PCOMPS_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLE_0, TMAP_1, STRUCT_0, RCOMP_1, EUCLID;
expansions TARSKI, XBOOLE_0, FUNCT_2, T_0TOPSP, FCONT_1;
set R = the carrier of R^1;
Lm1:
the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:]
by BORSUK_1:def 2;
theorem Th30:
for
a,
b,
r,
s being
Real holds
closed_inside_of_rectangle (
a,
b,
r,
s)
= product ((1,2) --> ([.a,b.],[.r,s.]))
definition
existence
ex b1 being Function of [:R^1,R^1:],(TOP-REAL 2) st
for x, y being Real holds b1 . [x,y] = <*x,y*>
by BORSUK_6:20;
uniqueness
for b1, b2 being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being Real holds b1 . [x,y] = <*x,y*> ) & ( for x, y being Real holds b2 . [x,y] = <*x,y*> ) holds
b1 = b2
end;
theorem Th35:
for
a,
b,
r,
s being
Real st
a <= b &
r <= s holds
R2Homeomorphism | the
carrier of
[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] is
Function of
[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],
(Trectangle (a,b,r,s))
theorem Th36:
for
a,
b,
r,
s being
Real st
a <= b &
r <= s holds
for
h being
Function of
[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],
(Trectangle (a,b,r,s)) st
h = R2Homeomorphism | the
carrier of
[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] holds
h is
being_homeomorphism
theorem
for
a,
b,
r,
s being
Real st
a <= b &
r <= s holds
[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],
Trectangle (
a,
b,
r,
s)
are_homeomorphic
theorem Th38:
for
a,
b,
r,
s being
Real st
a <= b &
r <= s holds
for
A being
Subset of
(Closed-Interval-TSpace (a,b)) for
B being
Subset of
(Closed-Interval-TSpace (r,s)) holds
product ((1,2) --> (A,B)) is
Subset of
(Trectangle (a,b,r,s))
theorem
for
a,
b,
r,
s being
Real st
a <= b &
r <= s holds
for
A being
open Subset of
(Closed-Interval-TSpace (a,b)) for
B being
open Subset of
(Closed-Interval-TSpace (r,s)) holds
product ((1,2) --> (A,B)) is
open Subset of
(Trectangle (a,b,r,s))
theorem
for
a,
b,
r,
s being
Real st
a <= b &
r <= s holds
for
A being
closed Subset of
(Closed-Interval-TSpace (a,b)) for
B being
closed Subset of
(Closed-Interval-TSpace (r,s)) holds
product ((1,2) --> (A,B)) is
closed Subset of
(Trectangle (a,b,r,s))