:: Some Properties of Rectangles on the Plane
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received October 18, 2004
:: Copyright (c) 2004-2021 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;

cluster K149(r,(r + s)) -> non empty ;

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

proof end;

cluster K147(r,(r + s)) -> non empty ;

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

proof end;

cluster K148(r,(r + s)) -> non empty ;

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

proof end;

cluster K146(r,(r + s)) -> non empty ;

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

proof end;

cluster K149((r - s),r) -> non empty ;

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

proof end;

cluster K147((r - s),r) -> non empty ;

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

proof end;

cluster K148((r - s),r) -> non empty ;

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

proof end;

cluster K146((r - s),r) -> non empty ;

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

proof end;

end;

registration

let r be non positive Real;
let s be positive Real;

cluster K149(r,s) -> non empty ;

coherence
not ].r,s.[ is empty

proof end;

cluster K147(r,s) -> non empty ;

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

cluster K148(r,s) -> non empty ;

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

cluster K146(r,s) -> non empty ;

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

end;

registration

let r be negative Real;
let s be non negative Real;

cluster K149(r,s) -> non empty ;

coherence
not ].r,s.[ is empty

proof end;

cluster K147(r,s) -> non empty ;

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

cluster K148(r,s) -> non empty ;

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

cluster K146(r,s) -> non empty ;

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

end;

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

theorem Th4: :: TOPREALA:4

for a, b being object holds <*a,b*> = (1,2) --> (a,b)

proof end;

registration

cluster non empty strict TopSpace-like constituted-FinSeqs for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is constituted-FinSeqs & not b₁ is empty & b₁ is strict )

proof end;

end;

registration

let T be constituted-FinSeqs TopSpace;

cluster -> constituted-FinSeqs for SubSpace of T;

coherence
for b₁ being SubSpace of T holds b₁ is constituted-FinSeqs

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

registration

cluster empty TopSpace-like -> discrete anti-discrete for TopStruct ;

coherence
for b₁ being TopSpace st b₁ is empty holds
( b₁ is discrete & b₁ is anti-discrete )

proof 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 b₁ being Function of X,Y holds b₁ 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 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 b₁ being Function of X,Y st b₁ is empty holds
b₁ 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 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 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 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 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 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 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 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 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 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 end;

theorem :: TOPREALA:17

for r being Real
for f being PartFunc of REAL,REAL st f = REAL --> r holds
f | REAL is continuous

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

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

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

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

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

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

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.]:]

proof end;

theorem :: TOPREALA:28

for a, b being Real holds |[a,b]| = (1,2) --> (a,b) by Th4;

theorem :: TOPREALA:29

for a, b being Real holds
( |[a,b]| . 1 = a & |[a,b]| . 2 = b )

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;

theorem Th31: :: TOPREALA:31

for a, b, r, s being Real st a <= b & r <= s holds
|[a,r]| in closed_inside_of_rectangle (a,b,r,s)

proof end;

definition

let a, b, c, d be Real;

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 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 st a <= b & r <= s holds
not Trectangle (a,b,r,s) is empty

proof end;

registration

let a, c be non positive Real;
let b, d be non negative Real;

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 holds it . [x,y] = <*x,y*>;

existence
ex b₁ being Function of [:R^1,R^1:],(TOP-REAL 2) st
for x, y being Real holds b₁ . [x,y] = <*x,y*> by BORSUK_6:20;
uniqueness
for b₁, b₂ being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being Real holds b₁ . [x,y] = <*x,y*> ) & ( for x, y being Real holds b₂ . [x,y] = <*x,y*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines R2Homeomorphism TOPREALA:def 2 :
for b₁ being Function of [:R^1,R^1:],(TOP-REAL 2) holds
( b₁ = R2Homeomorphism iff for x, y being Real holds b₁ . [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 end;

theorem Th34: :: TOPREALA:34

R2Homeomorphism is being_homeomorphism

proof end;

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

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

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

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

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

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

proof end;