:: by Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received October 18, 2004

:: Copyright (c) 2004-2017 Association of Mizar Users

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;

let s be positive Real;

coherence

not ].r,(r + s).[ is empty

not [.r,(r + s).[ is empty

not ].r,(r + s).] is empty

not [.r,(r + s).] is empty

not ].(r - s),r.[ is empty

not [.(r - s),r.[ is empty

not ].(r - s),r.] is empty

not [.(r - s),r.] is empty

end;
let s be positive Real;

coherence

not ].r,(r + s).[ is empty

proof end;

coherence not [.r,(r + s).[ is empty

proof end;

coherence not ].r,(r + s).] is empty

proof end;

coherence not [.r,(r + s).] is empty

proof end;

coherence not ].(r - s),r.[ is empty

proof end;

coherence not [.(r - s),r.[ is empty

proof end;

coherence not ].(r - s),r.] is empty

proof end;

coherence not [.(r - s),r.] is empty

proof end;

registration

let r be non positive Real;

let s be positive Real;

coherence

not ].r,s.[ is empty

not [.r,s.[ is empty by XXREAL_1:3;

coherence

not ].r,s.] is empty by XXREAL_1:2;

coherence

not [.r,s.] is empty by XXREAL_1:1;

end;
let s be positive Real;

coherence

not ].r,s.[ is empty

proof end;

coherence not [.r,s.[ is empty by XXREAL_1:3;

coherence

not ].r,s.] is empty by XXREAL_1:2;

coherence

not [.r,s.] is empty by XXREAL_1:1;

registration

let r be negative Real;

let s be non negative Real;

coherence

not ].r,s.[ is empty

not [.r,s.[ is empty by XXREAL_1:3;

coherence

not ].r,s.] is empty by XXREAL_1:2;

coherence

not [.r,s.] is empty by XXREAL_1:1;

end;
let s be non negative Real;

coherence

not ].r,s.[ is empty

proof end;

coherence not [.r,s.[ is empty by XXREAL_1:3;

coherence

not ].r,s.] is empty by XXREAL_1:2;

coherence

not [.r,s.] is empty by XXREAL_1:1;

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

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 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 )

for f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds

( f . x in X & f . y in Y )

proof end;

registration

existence

ex b_{1} being TopSpace st

( b_{1} is constituted-FinSeqs & not b_{1} is empty & b_{1} is strict )

end;
ex b

( b

proof end;

registration

let T be constituted-FinSeqs TopSpace;

coherence

for b_{1} being SubSpace of T holds b_{1} is constituted-FinSeqs

end;
coherence

for b

proof 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

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 end;

registration

coherence

for b_{1} being TopSpace st b_{1} is empty holds

( b_{1} is discrete & b_{1} is anti-discrete )

end;
for b

( b

proof end;

registration

let X be discrete TopSpace;

let Y be TopSpace;

for b_{1} being Function of X,Y holds b_{1} is continuous
by TEX_2:62;

end;
let Y be TopSpace;

cluster Function-like quasi_total -> continuous for Element of bool [: the carrier of X, the carrier of Y:];

coherence for b

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

for Y being TopStruct

for f being Function of X,Y st f is empty holds

f is continuous

proof end;

registration

let X be TopSpace;

let Y be TopStruct ;

for b_{1} being Function of X,Y st b_{1} is empty holds

b_{1} is continuous
by Th6;

end;
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 b

b

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

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 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

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 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

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 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

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 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

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 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

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 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 )

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 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 )

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 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 )

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 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

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 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

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 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

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 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

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 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

for g being Function of REAL,REAL st f = g & g is continuous holds

f is continuous

proof end;

theorem :: TOPREALA:23

for a, b, r, s being Real st a <= r & s <= b holds

[.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))

[.r,s.] is closed Subset of (Closed-Interval-TSpace (a,b))

proof end;

theorem :: TOPREALA:24

for a, b, r, s being Real st a <= r & s <= b holds

].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b))

].r,s.[ is open Subset of (Closed-Interval-TSpace (a,b))

proof end;

theorem :: TOPREALA:25

for a, b, r being Real st a <= b & a <= r holds

].r,b.] is open Subset of (Closed-Interval-TSpace (a,b))

].r,b.] is open Subset of (Closed-Interval-TSpace (a,b))

proof end;

theorem :: TOPREALA:26

for a, b, r being Real st a <= b & r <= b holds

[.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b))

[.a,r.[ is open Subset of (Closed-Interval-TSpace (a,b))

proof end;

theorem Th27: :: TOPREALA:27

for a, b, r, s being Real st a <= b & r <= s holds

the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:]

the carrier of [:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):] = [:[.a,b.],[.r,s.]:]

proof end;

theorem Th30: :: TOPREALA:30

for a, b, r, s being Real holds closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.]))

proof end;

definition

let a, b, c, d be Real;

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)) is SubSpace of TOP-REAL 2 ;

end;
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));

(TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)) is SubSpace of TOP-REAL 2 ;

:: deftheorem defines Trectangle TOPREALA:def 1 :

for a, b, c, d being Real holds Trectangle (a,b,c,d) = (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d));

for a, b, c, d being Real holds Trectangle (a,b,c,d) = (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d));

registration

let a, c be non positive Real;

let b, d be non negative Real;

coherence

not Trectangle (a,b,c,d) is empty by Th32;

end;
let b, d be non negative Real;

coherence

not Trectangle (a,b,c,d) is empty by Th32;

definition

ex b_{1} being Function of [:R^1,R^1:],(TOP-REAL 2) st

for x, y being Real holds b_{1} . [x,y] = <*x,y*>
by BORSUK_6:20;

uniqueness

for b_{1}, b_{2} being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being Real holds b_{1} . [x,y] = <*x,y*> ) & ( for x, y being Real holds b_{2} . [x,y] = <*x,y*> ) holds

b_{1} = b_{2}
end;

func R2Homeomorphism -> Function of [:R^1,R^1:],(TOP-REAL 2) means :Def2: :: TOPREALA:def 2

for x, y being Real holds it . [x,y] = <*x,y*>;

existence for x, y being Real holds it . [x,y] = <*x,y*>;

ex b

for x, y being Real holds b

uniqueness

for b

b

proof end;

:: deftheorem Def2 defines R2Homeomorphism TOPREALA:def 2 :

for b_{1} being Function of [:R^1,R^1:],(TOP-REAL 2) holds

( b_{1} = R2Homeomorphism iff for x, y being Real holds b_{1} . [x,y] = <*x,y*> );

for b

( b

theorem Th35: :: TOPREALA:35

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))

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 end;

theorem Th36: :: TOPREALA:36

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

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 end;

theorem :: TOPREALA:37

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

[:(Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (r,s)):], Trectangle (a,b,r,s) are_homeomorphic

proof end;

theorem Th38: :: TOPREALA:38

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))

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 end;

theorem :: TOPREALA:39

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))

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 end;

theorem :: TOPREALA:40

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))

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 end;