:: TOPREALA semantic presentation begin 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; registration let r be real number ; let s be real positive number ; clusterK148(r,(r + s)) -> non empty ; coherence not ].r,(r + s).[ is empty proof r + 0 < r + s by XREAL_1:6; then ( r < (r + (r + s)) / 2 & (r + (r + s)) / 2 < r + s ) by XREAL_1:226; hence not ].r,(r + s).[ is empty by XXREAL_1:4; ::_thesis: verum end; clusterK146(r,(r + s)) -> non empty ; coherence not [.r,(r + s).[ is empty proof r + 0 < r + s by XREAL_1:6; hence not [.r,(r + s).[ is empty by XXREAL_1:3; ::_thesis: verum end; clusterK147(r,(r + s)) -> non empty ; coherence not ].r,(r + s).] is empty proof r + 0 < r + s by XREAL_1:6; hence not ].r,(r + s).] is empty by XXREAL_1:2; ::_thesis: verum end; clusterK145(r,(r + s)) -> non empty ; coherence not [.r,(r + s).] is empty proof r + 0 < r + s by XREAL_1:6; hence not [.r,(r + s).] is empty by XXREAL_1:1; ::_thesis: verum end; clusterK148((r - s),r) -> non empty ; coherence not ].(r - s),r.[ is empty proof r - s < r - 0 by XREAL_1:15; then ( r - s < ((r - s) + r) / 2 & ((r - s) + r) / 2 < r ) by XREAL_1:226; hence not ].(r - s),r.[ is empty by XXREAL_1:4; ::_thesis: verum end; clusterK146((r - s),r) -> non empty ; coherence not [.(r - s),r.[ is empty proof r - s < r - 0 by XREAL_1:15; hence not [.(r - s),r.[ is empty by XXREAL_1:3; ::_thesis: verum end; clusterK147((r - s),r) -> non empty ; coherence not ].(r - s),r.] is empty proof r - s < r - 0 by XREAL_1:15; hence not ].(r - s),r.] is empty by XXREAL_1:32; ::_thesis: verum end; clusterK145((r - s),r) -> non empty ; coherence not [.(r - s),r.] is empty proof r - s < r - 0 by XREAL_1:15; hence not [.(r - s),r.] is empty by XXREAL_1:1; ::_thesis: verum end; end; registration let r be real non positive number ; let s be real positive number ; clusterK148(r,s) -> non empty ; coherence not ].r,s.[ is empty proof ( r < (r + s) / 2 & (r + s) / 2 < s ) by XREAL_1:226; hence not ].r,s.[ is empty by XXREAL_1:4; ::_thesis: verum end; clusterK146(r,s) -> non empty ; coherence not [.r,s.[ is empty by XXREAL_1:3; clusterK147(r,s) -> non empty ; coherence not ].r,s.] is empty by XXREAL_1:2; clusterK145(r,s) -> non empty ; coherence not [.r,s.] is empty by XXREAL_1:1; end; registration let r be real negative number ; let s be real non negative number ; clusterK148(r,s) -> non empty ; coherence not ].r,s.[ is empty proof ( r < (r + s) / 2 & (r + s) / 2 < s ) by XREAL_1:226; hence not ].r,s.[ is empty by XXREAL_1:4; ::_thesis: verum end; clusterK146(r,s) -> non empty ; coherence not [.r,s.[ is empty by XXREAL_1:3; clusterK147(r,s) -> non empty ; coherence not ].r,s.] is empty by XXREAL_1:2; clusterK145(r,s) -> non empty ; coherence not [.r,s.] is empty by XXREAL_1:1; end; begin theorem :: TOPREALA:1 for f being Function for x, X being set st x in dom f & f . x in f .: X & f is one-to-one holds x in X proof let f be Function; ::_thesis: for x, X being set st x in dom f & f . x in f .: X & f is one-to-one holds x in X let x, X be set ; ::_thesis: ( x in dom f & f . x in f .: X & f is one-to-one implies x in X ) assume A1: x in dom f ; ::_thesis: ( not f . x in f .: X or not f is one-to-one or x in X ) assume f . x in f .: X ; ::_thesis: ( not f is one-to-one or x in X ) then A2: ex a being set st ( a in dom f & a in X & f . x = f . a ) by FUNCT_1:def_6; assume f is one-to-one ; ::_thesis: x in X hence x in X by A1, A2, FUNCT_1:def_4; ::_thesis: verum end; theorem :: TOPREALA:2 for f being FinSequence for i being Nat holds ( not i + 1 in dom f or i in dom f or i = 0 ) proof let f be FinSequence; ::_thesis: for i being Nat holds ( not i + 1 in dom f or i in dom f or i = 0 ) let i be Nat; ::_thesis: ( not i + 1 in dom f or i in dom f or i = 0 ) assume A1: i + 1 in dom f ; ::_thesis: ( i in dom f or i = 0 ) then 1 <= i + 1 by FINSEQ_3:25; then A2: ( 1 < i + 1 or 1 + 0 = i + 1 ) by XXREAL_0:1; percases ( i = 0 or 1 <= i ) by A2, NAT_1:13; suppose i = 0 ; ::_thesis: ( i in dom f or i = 0 ) hence ( i in dom f or i = 0 ) ; ::_thesis: verum end; supposeA3: 1 <= i ; ::_thesis: ( i in dom f or i = 0 ) i + 1 <= len f by A1, FINSEQ_3:25; then i <= len f by NAT_1:13; hence ( i in dom f or i = 0 ) by A3, FINSEQ_3:25; ::_thesis: verum end; end; end; theorem Th3: :: TOPREALA:3 for x, y, X, Y being set for f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds ( f . x in X & f . y in Y ) proof let x, y, X, Y be set ; ::_thesis: for f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds ( f . x in X & f . y in Y ) let f be Function; ::_thesis: ( x <> y & f in product ((x,y) --> (X,Y)) implies ( f . x in X & f . y in Y ) ) assume that A1: x <> y and A2: f in product ((x,y) --> (X,Y)) ; ::_thesis: ( f . x in X & f . y in Y ) set g = (x,y) --> (X,Y); A3: dom ((x,y) --> (X,Y)) = {x,y} by FUNCT_4:62; then y in dom ((x,y) --> (X,Y)) by TARSKI:def_2; then A4: f . y in ((x,y) --> (X,Y)) . y by A2, CARD_3:9; x in dom ((x,y) --> (X,Y)) by A3, TARSKI:def_2; then f . x in ((x,y) --> (X,Y)) . x by A2, CARD_3:9; hence ( f . x in X & f . y in Y ) by A1, A4, FUNCT_4:63; ::_thesis: verum end; theorem Th4: :: TOPREALA:4 for a, b being set holds <*a,b*> = (1,2) --> (a,b) proof let a, b be set ; ::_thesis: <*a,b*> = (1,2) --> (a,b) set f = (1,2) --> (a,b); set g = <*a,b*>; A1: dom ((1,2) --> (a,b)) = {1,2} by FUNCT_4:62; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_((1,2)_-->_(a,b))_holds_ ((1,2)_-->_(a,b))_._x_=_<*a,b*>_._x let x be set ; ::_thesis: ( x in dom ((1,2) --> (a,b)) implies ((1,2) --> (a,b)) . b1 = <*a,b*> . b1 ) assume A3: x in dom ((1,2) --> (a,b)) ; ::_thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1 percases ( x = 1 or x = 2 ) by A1, A3, TARSKI:def_2; supposeA4: x = 1 ; ::_thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1 hence ((1,2) --> (a,b)) . x = a by FUNCT_4:63 .= <*a,b*> . x by A4, FINSEQ_1:44 ; ::_thesis: verum end; supposeA5: x = 2 ; ::_thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1 hence ((1,2) --> (a,b)) . x = b by FUNCT_4:63 .= <*a,b*> . x by A5, FINSEQ_1:44 ; ::_thesis: verum end; end; end; dom <*a,b*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; hence <*a,b*> = (1,2) --> (a,b) by A2, FUNCT_1:2, FUNCT_4:62; ::_thesis: verum end; begin registration cluster non empty strict TopSpace-like constituted-FinSeqs for TopStruct ; existence ex b1 being TopSpace st ( b1 is constituted-FinSeqs & not b1 is empty & b1 is strict ) proof take T = TopSpaceMetr (Euclid 1); ::_thesis: ( T is constituted-FinSeqs & not T is empty & T is strict ) thus for a being Element of T holds a is FinSequence :: according to MONOID_0:def_2 ::_thesis: ( not T is empty & T is strict ) proof let a be Element of T; ::_thesis: a is FinSequence T = TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) by EUCLID:def_8; hence a is FinSequence ; ::_thesis: verum end; thus ( not T is empty & T is strict ) ; ::_thesis: verum end; end; registration let T be constituted-FinSeqs TopSpace; cluster -> constituted-FinSeqs for SubSpace of T; coherence for b1 being SubSpace of T holds b1 is constituted-FinSeqs proof let X be SubSpace of T; ::_thesis: X is constituted-FinSeqs let p be Element of X; :: according to MONOID_0:def_2 ::_thesis: p is set A1: the carrier of X is Subset of T by TSEP_1:1; percases ( not the carrier of X is empty or the carrier of X is empty ) ; suppose not the carrier of X is empty ; ::_thesis: p is set then p in the carrier of X ; then reconsider p = p as Point of T by A1; p is FinSequence ; hence p is set ; ::_thesis: verum end; suppose the carrier of X is empty ; ::_thesis: p is set hence p is set ; ::_thesis: verum end; end; end; end; theorem Th5: :: TOPREALA:5 for T being non empty TopSpace for Z being non empty SubSpace of T for t being Point of T for z being Point of Z for N being open a_neighborhood of t for M being Subset of Z st t = z & M = N /\ ([#] Z) holds M is open a_neighborhood of z proof let T be non empty TopSpace; ::_thesis: for Z being non empty SubSpace of T for t being Point of T for z being Point of Z for N being open a_neighborhood of t for M being Subset of Z st t = z & M = N /\ ([#] Z) holds M is open a_neighborhood of z let Z be non empty SubSpace of T; ::_thesis: for t being Point of T for z being Point of Z for N being open a_neighborhood of t for M being Subset of Z st t = z & M = N /\ ([#] Z) holds M is open a_neighborhood of z let t be Point of T; ::_thesis: for z being Point of Z for N being open a_neighborhood of t for M being Subset of Z st t = z & M = N /\ ([#] Z) holds M is open a_neighborhood of z let z be Point of Z; ::_thesis: for N being open a_neighborhood of t for M being Subset of Z st t = z & M = N /\ ([#] Z) holds M is open a_neighborhood of z let N be open a_neighborhood of t; ::_thesis: for M being Subset of Z st t = z & M = N /\ ([#] Z) holds M is open a_neighborhood of z let M be Subset of Z; ::_thesis: ( t = z & M = N /\ ([#] Z) implies M is open a_neighborhood of z ) assume that A1: t = z and A2: M = N /\ ([#] Z) ; ::_thesis: M is open a_neighborhood of z M is open by A2, TOPS_2:24; then A3: Int M = M by TOPS_1:23; ( t in Int N & Int N c= N ) by CONNSP_2:def_1, TOPS_1:16; then z in Int M by A1, A2, A3, XBOOLE_0:def_4; hence M is open a_neighborhood of z by A2, CONNSP_2:def_1, TOPS_2:24; ::_thesis: verum end; registration cluster empty TopSpace-like -> discrete anti-discrete for TopStruct ; coherence for b1 being TopSpace st b1 is empty holds ( b1 is discrete & b1 is anti-discrete ) proof let T be TopSpace; ::_thesis: ( T is empty implies ( T is discrete & T is anti-discrete ) ) assume T is empty ; ::_thesis: ( T is discrete & T is anti-discrete ) then the carrier of T = {} ; then bool the carrier of T = {{}, the carrier of T} by ENUMSET1:29, ZFMISC_1:1; hence ( T is discrete & T is anti-discrete ) by TDLAT_3:14; ::_thesis: verum end; end; registration let X be discrete TopSpace; let Y be TopSpace; cluster Function-like quasi_total -> continuous for Element of bool [: the carrier of X, the carrier of Y:]; coherence for b1 being Function of X,Y holds b1 is continuous by TEX_2:62; end; theorem Th6: :: TOPREALA:6 for X being TopSpace for Y being TopStruct for f being Function of X,Y st f is empty holds f is continuous proof let X be TopSpace; ::_thesis: for Y being TopStruct for f being Function of X,Y st f is empty holds f is continuous let Y be TopStruct ; ::_thesis: for f being Function of X,Y st f is empty holds f is continuous let f be Function of X,Y; ::_thesis: ( f is empty implies f is continuous ) assume A1: f is empty ; ::_thesis: f is continuous let P be Subset of Y; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or f " P is closed ) assume P is closed ; ::_thesis: f " P is closed f " P = {} X by A1; hence f " P is closed ; ::_thesis: verum end; registration let X be TopSpace; let Y be TopStruct ; cluster Function-like empty quasi_total -> continuous for Element of bool [: the carrier of X, the carrier of Y:]; coherence for b1 being Function of X,Y st b1 is empty holds b1 is continuous by Th6; end; theorem :: TOPREALA:7 for X being TopStruct for Y being non empty TopStruct for Z being non empty SubSpace of Y for f being Function of X,Z holds f is Function of X,Y proof let X be TopStruct ; ::_thesis: for Y being non empty TopStruct for Z being non empty SubSpace of Y for f being Function of X,Z holds f is Function of X,Y let Y be non empty TopStruct ; ::_thesis: for Z being non empty SubSpace of Y for f being Function of X,Z holds f is Function of X,Y let Z be non empty SubSpace of Y; ::_thesis: for f being Function of X,Z holds f is Function of X,Y let f be Function of X,Z; ::_thesis: f is Function of X,Y the carrier of Z is Subset of Y by TSEP_1:1; then A1: rng f c= the carrier of Y by XBOOLE_1:1; dom f = the carrier of X by FUNCT_2:def_1; hence f is Function of X,Y by A1, FUNCT_2:2; ::_thesis: verum end; theorem :: TOPREALA:8 for S, T being non empty TopSpace for X being Subset of S for Y being Subset of T for f being continuous Function of S,T for g being Function of (S | X),(T | Y) st g = f | X holds g is continuous proof let S, T be non empty TopSpace; ::_thesis: for X being Subset of S for Y being Subset of T for f being continuous Function of S,T for g being Function of (S | X),(T | Y) st g = f | X holds g is continuous let X be Subset of S; ::_thesis: for Y being Subset of T for f being continuous Function of S,T for g being Function of (S | X),(T | Y) st g = f | X holds g is continuous let Y be Subset of T; ::_thesis: for f being continuous Function of S,T for g being Function of (S | X),(T | Y) st g = f | X holds g is continuous let f be continuous Function of S,T; ::_thesis: for g being Function of (S | X),(T | Y) st g = f | X holds g is continuous let g be Function of (S | X),(T | Y); ::_thesis: ( g = f | X implies g is continuous ) assume A1: g = f | X ; ::_thesis: g is continuous set h = f | X; A2: ( the carrier of (S | X) = X & rng (f | X) c= the carrier of T ) by PRE_TOPC:8; dom f = the carrier of S by FUNCT_2:def_1; then dom (f | X) = X by RELAT_1:62; then reconsider h = f | X as Function of (S | X),T by A2, FUNCT_2:2; h is continuous by TOPMETR:7; hence g is continuous by A1, TOPMETR:6; ::_thesis: verum end; theorem :: TOPREALA:9 for S, T being non empty TopSpace for Z being non empty SubSpace of T for f being Function of S,T for g being Function of S,Z st f = g & f is open holds g is open proof let S, T be non empty TopSpace; ::_thesis: for Z being non empty SubSpace of T for f being Function of S,T for g being Function of S,Z st f = g & f is open holds g is open let Z be non empty SubSpace of T; ::_thesis: for f being Function of S,T for g being Function of S,Z st f = g & f is open holds g is open let f be Function of S,T; ::_thesis: for g being Function of S,Z st f = g & f is open holds g is open let g be Function of S,Z; ::_thesis: ( f = g & f is open implies g is open ) assume that A1: f = g and A2: f is open ; ::_thesis: g is open for p being Point of S for P being open a_neighborhood of p ex R being a_neighborhood of g . p st R c= g .: P proof let p be Point of S; ::_thesis: for P being open a_neighborhood of p ex R being a_neighborhood of g . p st R c= g .: P let P be open a_neighborhood of p; ::_thesis: ex R being a_neighborhood of g . p st R c= g .: P consider R being open a_neighborhood of f . p such that A3: R c= f .: P by A2, TOPGRP_1:22; reconsider R2 = R /\ ([#] Z) as Subset of Z ; reconsider R2 = R2 as a_neighborhood of g . p by A1, Th5; take R2 ; ::_thesis: R2 c= g .: P R2 c= R by XBOOLE_1:17; hence R2 c= g .: P by A1, A3, XBOOLE_1:1; ::_thesis: verum end; hence g is open by TOPGRP_1:23; ::_thesis: verum end; theorem :: TOPREALA:10 for S, T being non empty TopSpace for S1 being Subset of S for T1 being Subset of T for f being Function of S,T for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds g is open proof let S, T be non empty TopSpace; ::_thesis: for S1 being Subset of S for T1 being Subset of T for f being Function of S,T for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds g is open let S1 be Subset of S; ::_thesis: for T1 being Subset of T for f being Function of S,T for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds g is open let T1 be Subset of T; ::_thesis: for f being Function of S,T for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds g is open let f be Function of S,T; ::_thesis: for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds g is open let g be Function of (S | S1),(T | T1); ::_thesis: ( g = f | S1 & g is onto & f is open & f is one-to-one implies g is open ) assume that A1: g = f | S1 and A2: rng g = the carrier of (T | T1) and A3: f is open and A4: f is one-to-one ; :: according to FUNCT_2:def_3 ::_thesis: g is open let A be Subset of (S | S1); :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or g .: A is open ) A5: [#] (T | T1) = T1 by PRE_TOPC:def_5; assume A is open ; ::_thesis: g .: A is open then consider C being Subset of S such that A6: C is open and A7: C /\ ([#] (S | S1)) = A by TOPS_2:24; A8: ( [#] (S | S1) = S1 & g .: (C /\ S1) c= (g .: C) /\ (g .: S1) ) by PRE_TOPC:def_5, RELAT_1:121; A9: g .: A = (f .: C) /\ T1 proof g .: C c= f .: C by A1, RELAT_1:128; then (g .: C) /\ (g .: S1) c= (f .: C) /\ T1 by A5, XBOOLE_1:27; hence g .: A c= (f .: C) /\ T1 by A7, A8, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: (f .: C) /\ T1 c= g .: A let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (f .: C) /\ T1 or y in g .: A ) A10: ( dom g c= dom f & dom f = the carrier of S ) by A1, FUNCT_2:def_1, RELAT_1:60; assume A11: y in (f .: C) /\ T1 ; ::_thesis: y in g .: A then y in f .: C by XBOOLE_0:def_4; then consider x being Element of S such that A12: x in C and A13: y = f . x by FUNCT_2:65; y in T1 by A11, XBOOLE_0:def_4; then consider a being set such that A14: a in dom g and A15: g . a = y by A2, A5, FUNCT_1:def_3; f . a = g . a by A1, A14, FUNCT_1:47; then a = x by A4, A13, A14, A15, A10, FUNCT_1:def_4; then a in A by A7, A12, A14, XBOOLE_0:def_4; hence y in g .: A by A14, A15, FUNCT_1:def_6; ::_thesis: verum end; f .: C is open by A3, A6, T_0TOPSP:def_2; hence g .: A is open by A5, A9, TOPS_2:24; ::_thesis: verum end; theorem :: TOPREALA:11 for X, Y, Z being non empty TopSpace for f being Function of X,Y for g being Function of Y,Z st f is open & g is open holds g * f is open proof let X, Y, Z be non empty TopSpace; ::_thesis: for f being Function of X,Y for g being Function of Y,Z st f is open & g is open holds g * f is open let f be Function of X,Y; ::_thesis: for g being Function of Y,Z st f is open & g is open holds g * f is open let g be Function of Y,Z; ::_thesis: ( f is open & g is open implies g * f is open ) assume that A1: f is open and A2: g is open ; ::_thesis: g * f is open let A be Subset of X; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or (g * f) .: A is open ) assume A is open ; ::_thesis: (g * f) .: A is open then A3: f .: A is open by A1, T_0TOPSP:def_2; (g * f) .: A = g .: (f .: A) by RELAT_1:126; hence (g * f) .: A is open by A2, A3, T_0TOPSP:def_2; ::_thesis: verum end; theorem :: TOPREALA:12 for X, Y being TopSpace for Z being open SubSpace of Y for f being Function of X,Y for g being Function of X,Z st f = g & g is open holds f is open proof let X, Y be TopSpace; ::_thesis: for Z being open SubSpace of Y for f being Function of X,Y for g being Function of X,Z st f = g & g is open holds f is open let Z be open SubSpace of Y; ::_thesis: for f being Function of X,Y for g being Function of X,Z st f = g & g is open holds f is open let f be Function of X,Y; ::_thesis: for g being Function of X,Z st f = g & g is open holds f is open let g be Function of X,Z; ::_thesis: ( f = g & g is open implies f is open ) assume that A1: f = g and A2: g is open ; ::_thesis: f is open let A be Subset of X; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open ) assume A is open ; ::_thesis: f .: A is open then g .: A is open by A2, T_0TOPSP:def_2; hence f .: A is open by A1, TSEP_1:17; ::_thesis: verum end; theorem Th13: :: TOPREALA:13 for S, T being non empty TopSpace for f being Function of S,T st f is one-to-one & f is onto holds ( f is continuous iff f " is open ) proof let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto holds ( f is continuous iff f " is open ) let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto implies ( f is continuous iff f " is open ) ) assume A1: f is one-to-one ; ::_thesis: ( not f is onto or ( f is continuous iff f " is open ) ) assume f is onto ; ::_thesis: ( f is continuous iff f " is open ) then A2: f " = f " by A1, TOPS_2:def_4; A3: [#] T <> {} ; thus ( f is continuous implies f " is open ) ::_thesis: ( f " is open implies f is continuous ) proof assume A4: f is continuous ; ::_thesis: f " is open let A be Subset of T; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or (f ") .: A is open ) assume A is open ; ::_thesis: (f ") .: A is open then f " A is open by A3, A4, TOPS_2:43; hence (f ") .: A is open by A1, A2, FUNCT_1:85; ::_thesis: verum end; assume A5: f " is open ; ::_thesis: f is continuous now__::_thesis:_for_A_being_Subset_of_T_st_A_is_open_holds_ f_"_A_is_open let A be Subset of T; ::_thesis: ( A is open implies f " A is open ) assume A is open ; ::_thesis: f " A is open then (f ") .: A is open by A5, T_0TOPSP:def_2; hence f " A is open by A1, A2, FUNCT_1:85; ::_thesis: verum end; hence f is continuous by A3, TOPS_2:43; ::_thesis: verum end; theorem :: TOPREALA:14 for S, T being non empty TopSpace for f being Function of S,T st f is one-to-one & f is onto holds ( f is open iff f " is continuous ) proof let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto holds ( f is open iff f " is continuous ) let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto implies ( f is open iff f " is continuous ) ) assume A1: f is one-to-one ; ::_thesis: ( not f is onto or ( f is open iff f " is continuous ) ) assume f is onto ; ::_thesis: ( f is open iff f " is continuous ) then A2: rng f = [#] T by FUNCT_2:def_3; then rng (f ") = [#] S by A1, TOPS_2:49; then A3: f " is onto by FUNCT_2:def_3; ( f " is one-to-one & (f ") " = f ) by A1, A2, TOPS_2:50, TOPS_2:51; hence ( f is open iff f " is continuous ) by A3, Th13; ::_thesis: verum end; theorem :: TOPREALA:15 for S being TopSpace for T being non empty TopSpace holds ( S,T are_homeomorphic iff TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic ) proof let S be TopSpace; ::_thesis: for T being non empty TopSpace holds ( S,T are_homeomorphic iff TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic ) let T be non empty TopSpace; ::_thesis: ( S,T are_homeomorphic iff TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic ) set SS = TopStruct(# the carrier of S, the topology of S #); set TT = TopStruct(# the carrier of T, the topology of T #); A1: ( [#] S = [#] TopStruct(# the carrier of S, the topology of S #) & [#] T = [#] TopStruct(# the carrier of T, the topology of T #) ) ; thus ( S,T are_homeomorphic implies TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic ) ::_thesis: ( TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic implies S,T are_homeomorphic ) proof given f being Function of S,T such that A2: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: TopStruct(# the carrier of S, the topology of S #), TopStruct(# the carrier of T, the topology of T #) are_homeomorphic reconsider g = f as Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) ; A3: now__::_thesis:_for_P_being_Subset_of_TopStruct(#_the_carrier_of_S,_the_topology_of_S_#)_holds_g_.:_(Cl_P)_=_Cl_(g_.:_P) let P be Subset of TopStruct(# the carrier of S, the topology of S #); ::_thesis: g .: (Cl P) = Cl (g .: P) reconsider R = P as Subset of S ; thus g .: (Cl P) = f .: (Cl R) by TOPS_3:80 .= Cl (f .: R) by A2, TOPS_2:60 .= Cl (g .: P) by TOPS_3:80 ; ::_thesis: verum end; take g ; :: according to T_0TOPSP:def_1 ::_thesis: g is being_homeomorphism ( dom f = [#] S & rng f = [#] T ) by A2, TOPS_2:60; hence g is being_homeomorphism by A1, A2, A3, TOPS_2:60; ::_thesis: verum end; given f being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) such that A4: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: S,T are_homeomorphic reconsider g = f as Function of S,T ; A5: now__::_thesis:_for_P_being_Subset_of_S_holds_g_.:_(Cl_P)_=_Cl_(g_.:_P) let P be Subset of S; ::_thesis: g .: (Cl P) = Cl (g .: P) reconsider R = P as Subset of TopStruct(# the carrier of S, the topology of S #) ; thus g .: (Cl P) = f .: (Cl R) by TOPS_3:80 .= Cl (f .: R) by A4, TOPS_2:60 .= Cl (g .: P) by TOPS_3:80 ; ::_thesis: verum end; take g ; :: according to T_0TOPSP:def_1 ::_thesis: g is being_homeomorphism ( dom f = [#] TopStruct(# the carrier of S, the topology of S #) & rng f = [#] TopStruct(# the carrier of T, the topology of T #) ) by A4, TOPS_2:60; hence g is being_homeomorphism by A1, A4, A5, TOPS_2:60; ::_thesis: verum end; theorem :: TOPREALA:16 for S, T being non empty TopSpace for f being Function of S,T st f is one-to-one & f is onto & f is continuous & f is open holds f is being_homeomorphism proof let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto & f is continuous & f is open holds f is being_homeomorphism let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto & f is continuous & f is open implies f is being_homeomorphism ) assume that A1: f is one-to-one and A2: f is onto and A3: f is continuous and A4: f is open ; ::_thesis: f is being_homeomorphism A5: [#] T <> {} ; A6: dom f = the carrier of S by FUNCT_2:def_1; A7: for P being Subset of S holds ( P is open iff f .: P is open ) proof let P be Subset of S; ::_thesis: ( P is open iff f .: P is open ) thus ( P is open implies f .: P is open ) by A4, T_0TOPSP:def_2; ::_thesis: ( f .: P is open implies P is open ) assume f .: P is open ; ::_thesis: P is open then f " (f .: P) is open by A3, A5, TOPS_2:43; hence P is open by A1, A6, FUNCT_1:94; ::_thesis: verum end; ( dom f = [#] S & rng f = [#] T ) by A2, FUNCT_2:def_1, FUNCT_2:def_3; hence f is being_homeomorphism by A1, A7, TOPGRP_1:25; ::_thesis: verum end; begin theorem :: TOPREALA:17 for r being real number for f being PartFunc of REAL,REAL st f = REAL --> r holds f | REAL is continuous proof let r be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f = REAL --> r holds f | REAL is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( f = REAL --> r implies f | REAL is continuous ) assume A1: f = REAL --> r ; ::_thesis: f | REAL is continuous f | REAL is constant proof reconsider r = r as Real by XREAL_0:def_1; take r ; :: according to PARTFUN2:def_1 ::_thesis: for b1 being Element of REAL holds ( not b1 in dom (f | REAL) or (f | REAL) . b1 = r ) let c be Element of REAL ; ::_thesis: ( not c in dom (f | REAL) or (f | REAL) . c = r ) assume c in dom (f | REAL) ; ::_thesis: (f | REAL) . c = r thus (f | REAL) . c = f . c .= r by A1, FUNCOP_1:7 ; ::_thesis: verum end; hence f | REAL is continuous ; ::_thesis: verum end; theorem :: TOPREALA:18 for f, f1, f2 being PartFunc of REAL,REAL st dom f = (dom f1) \/ (dom f2) & dom f1 is open & dom f2 is open & f1 | (dom f1) is continuous & f2 | (dom f2) is continuous & ( for z being set st z in dom f1 holds f . z = f1 . z ) & ( for z being set st z in dom f2 holds f . z = f2 . z ) holds f | (dom f) is continuous proof let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f = (dom f1) \/ (dom f2) & dom f1 is open & dom f2 is open & f1 | (dom f1) is continuous & f2 | (dom f2) is continuous & ( for z being set st z in dom f1 holds f . z = f1 . z ) & ( for z being set st z in dom f2 holds f . z = f2 . z ) implies f | (dom f) is continuous ) set X1 = dom f1; set X2 = dom f2; assume that A1: dom f = (dom f1) \/ (dom f2) and A2: dom f1 is open and A3: dom f2 is open and A4: f1 | (dom f1) is continuous and A5: f2 | (dom f2) is continuous and A6: for z being set st z in dom f1 holds f . z = f1 . z and A7: for z being set st z in dom f2 holds f . z = f2 . z ; ::_thesis: f | (dom f) is continuous A8: (dom f) /\ (dom f1) = dom f1 by A1, XBOOLE_1:7, XBOOLE_1:28; A9: dom (f | (dom f2)) = (dom f) /\ (dom f2) by RELAT_1:61; let x be real number ; :: according to FCONT_1:def_2 ::_thesis: ( not x in dom (f | (dom f)) or f | (dom f) is_continuous_in x ) assume x in dom (f | (dom f)) ; ::_thesis: f | (dom f) is_continuous_in x then A10: x in dom f ; then A11: (f | ((dom f1) \/ (dom f2))) . x = f . x by A1, FUNCT_1:49; A12: (dom f) /\ (dom f2) = dom f2 by A1, XBOOLE_1:7, XBOOLE_1:28; A13: dom (f | (dom f1)) = (dom f) /\ (dom f1) by RELAT_1:61; percases ( x in dom f1 or x in dom f2 ) by A1, A10, XBOOLE_0:def_3; supposeA14: x in dom f1 ; ::_thesis: f | (dom f) is_continuous_in x then A15: (f | ((dom f1) \/ (dom f2))) . x = f1 . x by A6, A11 .= (f1 | (dom f1)) . x ; for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds (f | ((dom f1) \/ (dom f2))) . x1 in N1 proof let N1 be Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x; ::_thesis: ex N being Neighbourhood of x st for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds (f | ((dom f1) \/ (dom f2))) . x1 in N1 consider N2 being Neighbourhood of x such that A16: N2 c= dom f1 by A2, A14, RCOMP_1:18; x in dom (f1 | (dom f1)) by A14; then f1 | (dom f1) is_continuous_in x by A4, FCONT_1:def_2; then consider N being Neighbourhood of x such that A17: for x1 being real number st x1 in dom (f1 | (dom f1)) & x1 in N holds (f1 | (dom f1)) . x1 in N1 by A15, FCONT_1:4; consider N3 being Neighbourhood of x such that A18: N3 c= N and A19: N3 c= N2 by RCOMP_1:17; take N3 ; ::_thesis: for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 holds (f | ((dom f1) \/ (dom f2))) . x1 in N1 let x1 be real number ; ::_thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 ) assume that A20: x1 in dom (f | ((dom f1) \/ (dom f2))) and A21: x1 in N3 ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1 percases ( x1 in dom (f | (dom f1)) or not x1 in dom (f | (dom f1)) ) ; supposeA22: x1 in dom (f | (dom f1)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1 A23: dom (f | (dom f1)) = (dom f1) /\ (dom f1) by A1, A13, XBOOLE_1:7, XBOOLE_1:28 .= dom (f1 | (dom f1)) ; A24: x1 in dom f1 by A13, A22, XBOOLE_0:def_4; (f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A20, FUNCT_1:47 .= f1 . x1 by A6, A24 .= (f1 | (dom f1)) . x1 ; hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A17, A18, A21, A22, A23; ::_thesis: verum end; supposeA25: not x1 in dom (f | (dom f1)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1 x1 in N2 by A19, A21; hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A13, A8, A16, A25; ::_thesis: verum end; end; end; hence f | (dom f) is_continuous_in x by A1, FCONT_1:4; ::_thesis: verum end; supposeA26: x in dom f2 ; ::_thesis: f | (dom f) is_continuous_in x then A27: (f | ((dom f1) \/ (dom f2))) . x = f2 . x by A7, A11 .= (f2 | (dom f2)) . x ; for N1 being Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x ex N being Neighbourhood of x st for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds (f | ((dom f1) \/ (dom f2))) . x1 in N1 proof let N1 be Neighbourhood of (f | ((dom f1) \/ (dom f2))) . x; ::_thesis: ex N being Neighbourhood of x st for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N holds (f | ((dom f1) \/ (dom f2))) . x1 in N1 consider N2 being Neighbourhood of x such that A28: N2 c= dom f2 by A3, A26, RCOMP_1:18; x in dom (f2 | (dom f2)) by A26; then f2 | (dom f2) is_continuous_in x by A5, FCONT_1:def_2; then consider N being Neighbourhood of x such that A29: for x1 being real number st x1 in dom (f2 | (dom f2)) & x1 in N holds (f2 | (dom f2)) . x1 in N1 by A27, FCONT_1:4; consider N3 being Neighbourhood of x such that A30: N3 c= N and A31: N3 c= N2 by RCOMP_1:17; take N3 ; ::_thesis: for x1 being real number st x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 holds (f | ((dom f1) \/ (dom f2))) . x1 in N1 let x1 be real number ; ::_thesis: ( x1 in dom (f | ((dom f1) \/ (dom f2))) & x1 in N3 implies (f | ((dom f1) \/ (dom f2))) . x1 in N1 ) assume that A32: x1 in dom (f | ((dom f1) \/ (dom f2))) and A33: x1 in N3 ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1 percases ( x1 in dom (f | (dom f2)) or not x1 in dom (f | (dom f2)) ) ; supposeA34: x1 in dom (f | (dom f2)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1 A35: dom (f | (dom f2)) = (dom f2) /\ (dom f2) by A1, A9, XBOOLE_1:7, XBOOLE_1:28 .= dom (f2 | (dom f2)) ; A36: x1 in dom f2 by A9, A34, XBOOLE_0:def_4; (f | ((dom f1) \/ (dom f2))) . x1 = f . x1 by A32, FUNCT_1:47 .= f2 . x1 by A7, A36 .= (f2 | (dom f2)) . x1 ; hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A29, A30, A33, A34, A35; ::_thesis: verum end; supposeA37: not x1 in dom (f | (dom f2)) ; ::_thesis: (f | ((dom f1) \/ (dom f2))) . x1 in N1 x1 in N2 by A31, A33; hence (f | ((dom f1) \/ (dom f2))) . x1 in N1 by A9, A12, A28, A37; ::_thesis: verum end; end; end; hence f | (dom f) is_continuous_in x by A1, FCONT_1:4; ::_thesis: verum end; end; end; theorem Th19: :: TOPREALA:19 for x being Point of R^1 for N being Subset of REAL for M being Subset of R^1 st M = N & N is Neighbourhood of x holds M is a_neighborhood of x proof let x be Point of R^1; ::_thesis: for N being Subset of REAL for M being Subset of R^1 st M = N & N is Neighbourhood of x holds M is a_neighborhood of x let N be Subset of REAL; ::_thesis: for M being Subset of R^1 st M = N & N is Neighbourhood of x holds M is a_neighborhood of x let M be Subset of R^1; ::_thesis: ( M = N & N is Neighbourhood of x implies M is a_neighborhood of x ) assume A1: M = N ; ::_thesis: ( not N is Neighbourhood of x or M is a_neighborhood of x ) given r being real number such that A2: 0 < r and A3: N = ].(x - r),(x + r).[ ; :: according to RCOMP_1:def_6 ::_thesis: M is a_neighborhood of x M is open by A1, A3, JORDAN6:35; hence M is a_neighborhood of x by A1, A2, A3, CONNSP_2:3, TOPREAL6:15; ::_thesis: verum end; theorem Th20: :: TOPREALA:20 for x being Point of R^1 for M being a_neighborhood of x ex N being Neighbourhood of x st N c= M proof let x be Point of R^1; ::_thesis: for M being a_neighborhood of x ex N being Neighbourhood of x st N c= M let M be a_neighborhood of x; ::_thesis: ex N being Neighbourhood of x st N c= M consider V being Subset of R^1 such that A1: V is open and A2: V c= M and A3: x in V by CONNSP_2:6; x is Real by XREAL_0:def_1; then consider r being Real such that A4: r > 0 and A5: ].(x - r),(x + r).[ c= V by A1, A3, FRECHET:8; reconsider N = ].(x - r),(x + r).[ as Neighbourhood of x by A4, RCOMP_1:def_6; take N ; ::_thesis: N c= M thus N c= M by A2, A5, XBOOLE_1:1; ::_thesis: verum end; theorem Th21: :: TOPREALA:21 for f being Function of R^1,R^1 for g being PartFunc of REAL,REAL for x being Point of R^1 st f = g & g is_continuous_in x holds f is_continuous_at x proof let f be Function of R^1,R^1; ::_thesis: for g being PartFunc of REAL,REAL for x being Point of R^1 st f = g & g is_continuous_in x holds f is_continuous_at x let g be PartFunc of REAL,REAL; ::_thesis: for x being Point of R^1 st f = g & g is_continuous_in x holds f is_continuous_at x let x be Point of R^1; ::_thesis: ( f = g & g is_continuous_in x implies f is_continuous_at x ) assume that A1: f = g and A2: g is_continuous_in x ; ::_thesis: f is_continuous_at x let G be a_neighborhood of f . x; :: according to TMAP_1:def_2 ::_thesis: ex b1 being a_neighborhood of x st f .: b1 c= G consider Z being Neighbourhood of g . x such that A3: Z c= G by A1, Th20; consider N being Neighbourhood of x such that A4: g .: N c= Z by A2, FCONT_1:5; reconsider H = N as a_neighborhood of x by Th19, TOPMETR:17; take H ; ::_thesis: f .: H c= G thus f .: H c= G by A1, A3, A4, XBOOLE_1:1; ::_thesis: verum end; theorem :: TOPREALA:22 for f being Function of R^1,R^1 for g being Function of REAL,REAL st f = g & g is continuous holds f is continuous proof let f be Function of R^1,R^1; ::_thesis: for g being Function of REAL,REAL st f = g & g is continuous holds f is continuous let g be Function of REAL,REAL; ::_thesis: ( f = g & g is continuous implies f is continuous ) assume that A1: f = g and A2: g is continuous ; ::_thesis: f is continuous for x being Point of R^1 holds f is_continuous_at x proof let x be Point of R^1; ::_thesis: f is_continuous_at x dom f = REAL by A1, FUNCT_2:def_1; then x in dom g by A1, XREAL_0:def_1; then g is_continuous_in x by A2, FCONT_1:def_2; hence f is_continuous_at x by A1, Th21; ::_thesis: verum end; hence f is continuous by TMAP_1:44; ::_thesis: verum end; theorem :: TOPREALA:23 for a, r, s, b being real number st a <= r & s <= b holds [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) proof let a, r, s, b be real number ; ::_thesis: ( a <= r & s <= b implies [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) ) set T = Closed-Interval-TSpace (a,b); set A = [.r,s.]; assume that A1: a <= r and A2: s <= b ; ::_thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) percases ( r > s or r <= s ) ; suppose r > s ; ::_thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) then [.r,s.] = {} (Closed-Interval-TSpace (a,b)) by XXREAL_1:29; hence [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) ; ::_thesis: verum end; suppose r <= s ; ::_thesis: [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) then a <= s by A1, XXREAL_0:2; then the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A2, TOPMETR:18, XXREAL_0:2; then reconsider A = [.r,s.] as Subset of (Closed-Interval-TSpace (a,b)) by A1, A2, XXREAL_1:34; reconsider C = A as Subset of R^1 by TOPMETR:17; ( C is closed & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by TREAL_1:1, XBOOLE_1:28; hence [.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b)) by PRE_TOPC:13; ::_thesis: verum end; end; end; theorem :: TOPREALA:24 for a, r, s, b being real number st a <= r & s <= b holds ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) proof let a, r, s, b be real number ; ::_thesis: ( a <= r & s <= b implies ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) ) set T = Closed-Interval-TSpace (a,b); set A = ].r,s.[; assume that A1: a <= r and A2: s <= b ; ::_thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) percases ( r >= s or r < s ) ; suppose r >= s ; ::_thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) then ].r,s.[ = {} (Closed-Interval-TSpace (a,b)) by XXREAL_1:28; hence ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) ; ::_thesis: verum end; suppose r < s ; ::_thesis: ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) then a < s by A1, XXREAL_0:2; then the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A2, TOPMETR:18, XXREAL_0:2; then reconsider A = ].r,s.[ as Subset of (Closed-Interval-TSpace (a,b)) by A1, A2, XXREAL_1:37; reconsider C = A as Subset of R^1 by TOPMETR:17; ( C is open & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by JORDAN6:35, XBOOLE_1:28; hence ].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; ::_thesis: verum end; end; end; theorem :: TOPREALA:25 for a, b, r being real number st a <= b & a <= r holds ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b)) proof let a, b, r be real number ; ::_thesis: ( a <= b & a <= r implies ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b)) ) set T = Closed-Interval-TSpace (a,b); assume that A1: a <= b and A2: a <= r ; ::_thesis: ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b)) A3: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18; then reconsider A = ].r,b.] as Subset of (Closed-Interval-TSpace (a,b)) by A2, XXREAL_1:36; reconsider C = ].r,(b + 1).[ as Subset of R^1 by TOPMETR:17; A4: C /\ ([#] (Closed-Interval-TSpace (a,b))) c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C /\ ([#] (Closed-Interval-TSpace (a,b))) or x in A ) assume A5: x in C /\ ([#] (Closed-Interval-TSpace (a,b))) ; ::_thesis: x in A then A6: x in C by XBOOLE_0:def_4; then reconsider x = x as Real ; A7: r < x by A6, XXREAL_1:4; x <= b by A3, A5, XXREAL_1:1; hence x in A by A7; ::_thesis: verum end; b + 0 < b + 1 by XREAL_1:6; then A c= C by XXREAL_1:49; then A c= C /\ ([#] (Closed-Interval-TSpace (a,b))) by XBOOLE_1:19; then ( C is open & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by A4, JORDAN6:35, XBOOLE_0:def_10; hence ].r,b.] is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; ::_thesis: verum end; theorem :: TOPREALA:26 for a, b, r being real number st a <= b & r <= b holds [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b)) proof let a, b, r be real number ; ::_thesis: ( a <= b & r <= b implies [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b)) ) set T = Closed-Interval-TSpace (a,b); assume that A1: a <= b and A2: r <= b ; ::_thesis: [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b)) A3: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18; then reconsider A = [.a,r.[ as Subset of (Closed-Interval-TSpace (a,b)) by A2, XXREAL_1:35; reconsider C = ].(a - 1),r.[ as Subset of R^1 by TOPMETR:17; A4: C /\ ([#] (Closed-Interval-TSpace (a,b))) c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C /\ ([#] (Closed-Interval-TSpace (a,b))) or x in A ) assume A5: x in C /\ ([#] (Closed-Interval-TSpace (a,b))) ; ::_thesis: x in A then A6: x in C by XBOOLE_0:def_4; then reconsider x = x as Real ; A7: x < r by A6, XXREAL_1:4; a <= x by A3, A5, XXREAL_1:1; hence x in A by A7; ::_thesis: verum end; a - 1 < a - 0 by XREAL_1:15; then A c= C by XXREAL_1:48; then A c= C /\ ([#] (Closed-Interval-TSpace (a,b))) by XBOOLE_1:19; then ( C is open & C /\ ([#] (Closed-Interval-TSpace (a,b))) = A ) by A4, JORDAN6:35, XBOOLE_0:def_10; hence [.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b)) by TOPS_2:24; ::_thesis: verum end; theorem Th27: :: TOPREALA:27 for a, b, r, s being real number st a <= b & r <= s holds the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] ) set C1 = Closed-Interval-TSpace (a,b); set C2 = Closed-Interval-TSpace (r,s); assume ( a <= b & r <= s ) ; ::_thesis: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] then ( the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] & the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] ) by TOPMETR:18; hence the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] by BORSUK_1:def_2; ::_thesis: verum end; begin theorem :: TOPREALA:28 for a, b being real number holds |[a,b]| = (1,2) --> (a,b) by Th4; theorem :: TOPREALA:29 for a, b being real number holds ( |[a,b]| . 1 = a & |[a,b]| . 2 = b ) proof let a, b be real number ; ::_thesis: ( |[a,b]| . 1 = a & |[a,b]| . 2 = b ) thus |[a,b]| . 1 = ((1,2) --> (a,b)) . 1 by Th4 .= a by FUNCT_4:63 ; ::_thesis: |[a,b]| . 2 = b thus |[a,b]| . 2 = ((1,2) --> (a,b)) . 2 by Th4 .= b by FUNCT_4:63 ; ::_thesis: verum end; theorem Th30: :: TOPREALA:30 for a, b, r, s being real number holds closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.])) proof let a, b, r, s be real number ; ::_thesis: closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.])) set A = [.a,b.]; set B = [.r,s.]; set f = (1,2) --> ([.a,b.],[.r,s.]); set R = closed_inside_of_rectangle (a,b,r,s); A1: closed_inside_of_rectangle (a,b,r,s) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) } by JGRAPH_6:def_2; thus closed_inside_of_rectangle (a,b,r,s) c= product ((1,2) --> ([.a,b.],[.r,s.])) :: according to XBOOLE_0:def_10 ::_thesis: product ((1,2) --> ([.a,b.],[.r,s.])) c= closed_inside_of_rectangle (a,b,r,s) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in closed_inside_of_rectangle (a,b,r,s) or x in product ((1,2) --> ([.a,b.],[.r,s.])) ) assume x in closed_inside_of_rectangle (a,b,r,s) ; ::_thesis: x in product ((1,2) --> ([.a,b.],[.r,s.])) then consider p being Point of (TOP-REAL 2) such that A2: x = p and A3: ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) by A1; |[(p `1),(p `2)]| = (1,2) --> ((p `1),(p `2)) by Th4; then A4: p = (1,2) --> ((p `1),(p `2)) by EUCLID:53; ( p `1 in [.a,b.] & p `2 in [.r,s.] ) by A3; hence x in product ((1,2) --> ([.a,b.],[.r,s.])) by A2, A4, HILBERT3:11; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product ((1,2) --> ([.a,b.],[.r,s.])) or x in closed_inside_of_rectangle (a,b,r,s) ) assume A5: x in product ((1,2) --> ([.a,b.],[.r,s.])) ; ::_thesis: x in closed_inside_of_rectangle (a,b,r,s) then consider g being Function such that A6: x = g and A7: dom g = dom ((1,2) --> ([.a,b.],[.r,s.])) and for y being set st y in dom ((1,2) --> ([.a,b.],[.r,s.])) holds g . y in ((1,2) --> ([.a,b.],[.r,s.])) . y by CARD_3:def_5; A8: g . 2 in [.r,s.] by A5, A6, Th3; A9: g . 1 in [.a,b.] by A5, A6, Th3; then reconsider g1 = g . 1, g2 = g . 2 as Real by A8; A10: dom ((1,2) --> ([.a,b.],[.r,s.])) = {1,2} by FUNCT_4:62; then reconsider g = g as FinSequence by A7, FINSEQ_1:2, FINSEQ_1:def_2; A11: len g = 2 by A7, A10, FINSEQ_1:2, FINSEQ_1:def_3; |[g1,g2]| = (1,2) --> (g1,g2) by Th4; then reconsider g = g as Point of (TOP-REAL 2) by A11, FINSEQ_1:44; A12: ( r <= g `2 & g `2 <= s ) by A8, XXREAL_1:1; ( a <= g `1 & g `1 <= b ) by A9, XXREAL_1:1; hence x in closed_inside_of_rectangle (a,b,r,s) by A1, A6, A12; ::_thesis: verum end; theorem Th31: :: TOPREALA:31 for a, b, r, s being real number st a <= b & r <= s holds |[a,r]| in closed_inside_of_rectangle (a,b,r,s) proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies |[a,r]| in closed_inside_of_rectangle (a,b,r,s) ) set o = |[a,r]|; A1: ( closed_inside_of_rectangle (a,b,r,s) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) } & |[a,r]| `1 = a ) by EUCLID:52, JGRAPH_6:def_2; A2: |[a,r]| `2 = r by EUCLID:52; assume ( a <= b & r <= s ) ; ::_thesis: |[a,r]| in closed_inside_of_rectangle (a,b,r,s) hence |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by A1, A2; ::_thesis: verum end; definition let a, b, c, d be real number ; func Trectangle (a,b,c,d) -> SubSpace of TOP-REAL 2 equals :: TOPREALA:def 1 (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)); coherence (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)) is SubSpace of TOP-REAL 2 ; end; :: deftheorem defines Trectangle TOPREALA:def_1_:_ for a, b, c, d being real number holds Trectangle (a,b,c,d) = (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)); theorem Th32: :: TOPREALA:32 for a, b, r, s being real number st a <= b & r <= s holds not Trectangle (a,b,r,s) is empty proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies not Trectangle (a,b,r,s) is empty ) assume ( a <= b & r <= s ) ; ::_thesis: not Trectangle (a,b,r,s) is empty then |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by Th31; hence not the carrier of (Trectangle (a,b,r,s)) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; registration let a, c be real non positive number ; let b, d be real non negative number ; cluster Trectangle (a,b,c,d) -> non empty ; coherence not Trectangle (a,b,c,d) is empty by Th32; end; definition func R2Homeomorphism -> Function of [:R^1,R^1:],(TOP-REAL 2) means :Def2: :: TOPREALA:def 2 for x, y being real number holds it . [x,y] = <*x,y*>; existence ex b1 being Function of [:R^1,R^1:],(TOP-REAL 2) st for x, y being real number holds b1 . [x,y] = <*x,y*> proof consider f being Function of [:R^1,R^1:],(TOP-REAL 2) such that A1: for x, y being Real holds f . [x,y] = <*x,y*> by BORSUK_6:20; take f ; ::_thesis: for x, y being real number holds f . [x,y] = <*x,y*> let x, y be real number ; ::_thesis: f . [x,y] = <*x,y*> ( x is Real & y is Real ) by XREAL_0:def_1; hence f . [x,y] = <*x,y*> by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being real number holds b1 . [x,y] = <*x,y*> ) & ( for x, y being real number holds b2 . [x,y] = <*x,y*> ) holds b1 = b2 proof let f, g be Function of [:R^1,R^1:],(TOP-REAL 2); ::_thesis: ( ( for x, y being real number holds f . [x,y] = <*x,y*> ) & ( for x, y being real number holds g . [x,y] = <*x,y*> ) implies f = g ) assume that A2: for x, y being real number holds f . [x,y] = <*x,y*> and A3: for x, y being real number holds g . [x,y] = <*x,y*> ; ::_thesis: f = g let a be Point of [:R^1,R^1:]; :: according to FUNCT_2:def_8 ::_thesis: f . a = g . a consider x, y being Element of the carrier of R^1 such that A4: a = [x,y] by Lm1, DOMAIN_1:1; thus f . a = <*x,y*> by A2, A4 .= g . a by A3, A4 ; ::_thesis: verum end; end; :: deftheorem Def2 defines R2Homeomorphism TOPREALA:def_2_:_ for b1 being Function of [:R^1,R^1:],(TOP-REAL 2) holds ( b1 = R2Homeomorphism iff for x, y being real number holds b1 . [x,y] = <*x,y*> ); theorem Th33: :: TOPREALA:33 for A, B being Subset of REAL holds R2Homeomorphism .: [:A,B:] = product ((1,2) --> (A,B)) proof for x, y being Real holds R2Homeomorphism . [x,y] = <*x,y*> by Def2; hence for A, B being Subset of REAL holds R2Homeomorphism .: [:A,B:] = product ((1,2) --> (A,B)) by TOPREAL6:75; ::_thesis: verum end; theorem Th34: :: TOPREALA:34 R2Homeomorphism is being_homeomorphism proof for x, y being Real holds R2Homeomorphism . [x,y] = <*x,y*> by Def2; hence R2Homeomorphism is being_homeomorphism by TOPREAL6:76; ::_thesis: verum end; theorem Th35: :: TOPREALA:35 for a, b, r, s being real number 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)) proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies 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)) ) set C1 = Closed-Interval-TSpace (a,b); set C2 = Closed-Interval-TSpace (r,s); set TR = Trectangle (a,b,r,s); set h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]; assume ( a <= b & r <= s ) ; ::_thesis: 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)) then A1: the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] by Th27; dom R2Homeomorphism = [: the carrier of R^1, the carrier of R^1:] by Lm1, FUNCT_2:def_1; then A2: dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) = the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] by A1, RELAT_1:62, TOPMETR:17, ZFMISC_1:96; rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) c= the carrier of (Trectangle (a,b,r,s)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) or y in the carrier of (Trectangle (a,b,r,s)) ) A3: ( the carrier of (Trectangle (a,b,r,s)) = closed_inside_of_rectangle (a,b,r,s) & closed_inside_of_rectangle (a,b,r,s) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) } ) by JGRAPH_6:def_2, PRE_TOPC:8; assume y in rng (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) ; ::_thesis: y in the carrier of (Trectangle (a,b,r,s)) then consider x being set such that A4: x in dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) and A5: (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x = y by FUNCT_1:def_3; reconsider x = x as Point of [:R^1,R^1:] by A4; dom (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) c= [: the carrier of R^1, the carrier of R^1:] by A1, A2, TOPMETR:17, ZFMISC_1:96; then consider x1, x2 being Element of the carrier of R^1 such that A6: x = [x1,x2] by A4, DOMAIN_1:1; A7: x2 in [.r,s.] by A1, A2, A4, A6, ZFMISC_1:87; A8: (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x = R2Homeomorphism . x by A4, FUNCT_1:47; then reconsider p = (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x as Point of (TOP-REAL 2) ; A9: (R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):]) . x = <*x1,x2*> by A8, A6, Def2; then x2 = p `2 by FINSEQ_1:44; then A10: ( r <= p `2 & p `2 <= s ) by A7, XXREAL_1:1; A11: x1 in [.a,b.] by A1, A2, A4, A6, ZFMISC_1:87; x1 = p `1 by A9, FINSEQ_1:44; then ( a <= p `1 & p `1 <= b ) by A11, XXREAL_1:1; hence y in the carrier of (Trectangle (a,b,r,s)) by A5, A3, A10; ::_thesis: verum end; hence 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)) by A2, FUNCT_2:2; ::_thesis: verum end; theorem Th36: :: TOPREALA:36 for a, b, r, s being real number 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 proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies 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 ) assume A1: ( a <= b & r <= s ) ; ::_thesis: 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 set TR = Trectangle (a,b,r,s); A2: closed_inside_of_rectangle (a,b,r,s) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) } by JGRAPH_6:def_2; set p = |[a,r]|; ( |[a,r]| `1 = a & |[a,r]| `2 = r ) by EUCLID:52; then |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by A1, A2; then reconsider T0 = Trectangle (a,b,r,s) as non empty SubSpace of TOP-REAL 2 ; set C2 = Closed-Interval-TSpace (r,s); set C1 = Closed-Interval-TSpace (a,b); let h be Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)); ::_thesis: ( h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] implies h is being_homeomorphism ) assume A3: h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] ; ::_thesis: h is being_homeomorphism reconsider S0 = [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as non empty SubSpace of [:R^1,R^1:] by BORSUK_3:21; reconsider g = h as Function of S0,T0 ; A4: the carrier of (Trectangle (a,b,r,s)) = closed_inside_of_rectangle (a,b,r,s) by PRE_TOPC:8; A5: g is onto proof thus rng g c= the carrier of T0 ; :: according to XBOOLE_0:def_10,FUNCT_2:def_3 ::_thesis: the carrier of T0 c= rng g let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of T0 or y in rng g ) A6: ( the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:] & dom g = the carrier of S0 ) by A1, Th27, FUNCT_2:def_1; assume y in the carrier of T0 ; ::_thesis: y in rng g then consider p being Point of (TOP-REAL 2) such that A7: y = p and A8: ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) by A2, A4; ( p `1 in [.a,b.] & p `2 in [.r,s.] ) by A8; then A9: [(p `1),(p `2)] in dom g by A6, ZFMISC_1:def_2; then g . [(p `1),(p `2)] = R2Homeomorphism . [(p `1),(p `2)] by A3, FUNCT_1:49 .= |[(p `1),(p `2)]| by Def2 .= y by A7, EUCLID:53 ; hence y in rng g by A9, FUNCT_1:def_3; ::_thesis: verum end; g = R2Homeomorphism | S0 by A3; hence h is being_homeomorphism by A5, Th34, JORDAN16:9; ::_thesis: verum end; theorem :: TOPREALA:37 for a, b, r, s being real number st a <= b & r <= s holds [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], Trectangle (a,b,r,s) are_homeomorphic proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], Trectangle (a,b,r,s) are_homeomorphic ) set C1 = Closed-Interval-TSpace (a,b); set C2 = Closed-Interval-TSpace (r,s); assume A1: ( a <= b & r <= s ) ; ::_thesis: [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], Trectangle (a,b,r,s) are_homeomorphic then reconsider h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) by Th35; take h ; :: according to T_0TOPSP:def_1 ::_thesis: h is being_homeomorphism thus h is being_homeomorphism by A1, Th36; ::_thesis: verum end; theorem Th38: :: TOPREALA:38 for a, b, r, s being real number 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)) proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies 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)) ) set T = Closed-Interval-TSpace (a,b); set S = Closed-Interval-TSpace (r,s); assume ( a <= b & r <= s ) ; ::_thesis: 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)) then A1: ( the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] & the carrier of (Closed-Interval-TSpace (r,s)) = [.r,s.] ) by TOPMETR:18; let A be Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for B being Subset of (Closed-Interval-TSpace (r,s)) holds product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s)) let B be Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s)) closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.])) by Th30; then product ((1,2) --> (A,B)) c= closed_inside_of_rectangle (a,b,r,s) by A1, TOPREAL6:21; hence product ((1,2) --> (A,B)) is Subset of (Trectangle (a,b,r,s)) by PRE_TOPC:8; ::_thesis: verum end; theorem :: TOPREALA:39 for a, b, r, s being real number 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)) proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies 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)) ) set T = Closed-Interval-TSpace (a,b); set S = Closed-Interval-TSpace (r,s); assume A1: ( a <= b & r <= s ) ; ::_thesis: 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)) then reconsider h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) by Th35; let A be open Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: 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)) let B be open Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s)) reconsider P = product ((1,2) --> (A,B)) as Subset of (Trectangle (a,b,r,s)) by A1, Th38; A2: [:A,B:] is open by BORSUK_1:6; the carrier of (Closed-Interval-TSpace (r,s)) is Subset of R^1 by TSEP_1:1; then A3: B is Subset of REAL by TOPMETR:17, XBOOLE_1:1; the carrier of (Closed-Interval-TSpace (a,b)) is Subset of R^1 by TSEP_1:1; then A4: A is Subset of REAL by TOPMETR:17, XBOOLE_1:1; A5: h .: [:A,B:] = R2Homeomorphism .: [:A,B:] by RELAT_1:129 .= P by A4, A3, Th33 ; ( h is being_homeomorphism & not Trectangle (a,b,r,s) is empty ) by A1, Th32, Th36; hence product ((1,2) --> (A,B)) is open Subset of (Trectangle (a,b,r,s)) by A5, A2, TOPGRP_1:25; ::_thesis: verum end; theorem :: TOPREALA:40 for a, b, r, s being real number 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)) proof let a, b, r, s be real number ; ::_thesis: ( a <= b & r <= s implies 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)) ) set T = Closed-Interval-TSpace (a,b); set S = Closed-Interval-TSpace (r,s); assume A1: ( a <= b & r <= s ) ; ::_thesis: 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)) then reconsider h = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] as Function of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):],(Trectangle (a,b,r,s)) by Th35; let A be closed Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: 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)) let B be closed Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s)) reconsider P = product ((1,2) --> (A,B)) as Subset of (Trectangle (a,b,r,s)) by A1, Th38; A2: [:A,B:] is closed by TOPALG_3:15; the carrier of (Closed-Interval-TSpace (r,s)) is Subset of R^1 by TSEP_1:1; then A3: B is Subset of REAL by TOPMETR:17, XBOOLE_1:1; the carrier of (Closed-Interval-TSpace (a,b)) is Subset of R^1 by TSEP_1:1; then A4: A is Subset of REAL by TOPMETR:17, XBOOLE_1:1; A5: h .: [:A,B:] = R2Homeomorphism .: [:A,B:] by RELAT_1:129 .= P by A4, A3, Th33 ; ( h is being_homeomorphism & not Trectangle (a,b,r,s) is empty ) by A1, Th32, Th36; hence product ((1,2) --> (A,B)) is closed Subset of (Trectangle (a,b,r,s)) by A5, A2, TOPS_2:58; ::_thesis: verum end;