:: Some Properties of Rectangles on the Plane
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received October 18, 2004
:: Copyright (c) 2004-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors 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;
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;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_2, PRE_TOPC, T_0TOPSP, TMAP_1, STRUCT_0,
RCOMP_1, FCONT_1, MONOID_0, PARTFUN2;
equalities XBOOLE_0, TMAP_1, STRUCT_0, RCOMP_1, EUCLID;
expansions TARSKI, XBOOLE_0, FUNCT_2, T_0TOPSP, FCONT_1;
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;
begin :: Subsets of REAL
set R = the carrier of R^1;
Lm1: the carrier of [:R^1,R^1:] = [:R,R:] by BORSUK_1:def 2;
reserve i for Integer,
a, b, r, s for Real;
registration
let r be Real, s be positive Real;
cluster ].r,r+s.[ -> non empty;
coherence
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 thesis by XXREAL_1:4;
end;
cluster [.r,r+s.[ -> non empty;
coherence
proof
r+0 < r+s by XREAL_1:6;
hence thesis by XXREAL_1:3;
end;
cluster ].r,r+s.] -> non empty;
coherence
proof
r+0 < r+s by XREAL_1:6;
hence thesis by XXREAL_1:2;
end;
cluster [.r,r+s.] -> non empty;
coherence
proof
r+0 < r+s by XREAL_1:6;
hence thesis by XXREAL_1:1;
end;
cluster ].r-s,r.[ -> non empty;
coherence
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 thesis by XXREAL_1:4;
end;
cluster [.r-s,r.[ -> non empty;
coherence
proof
r-s < r-0 by XREAL_1:15;
hence thesis by XXREAL_1:3;
end;
cluster ].r-s,r.] -> non empty;
coherence
proof
r-s < r-0 by XREAL_1:15;
hence thesis by XXREAL_1:32;
end;
cluster [.r-s,r.] -> non empty;
coherence
proof
r-s < r-0 by XREAL_1:15;
hence thesis by XXREAL_1:1;
end;
end;
registration
let r be non positive Real, s be positive Real;
cluster ].r,s.[ -> non empty;
coherence
proof
r < (r+s)/2 & (r+s)/2 < s by XREAL_1:226;
hence thesis by XXREAL_1:4;
end;
cluster [.r,s.[ -> non empty;
coherence by XXREAL_1:3;
cluster ].r,s.] -> non empty;
coherence by XXREAL_1:2;
cluster [.r,s.] -> non empty;
coherence by XXREAL_1:1;
end;
registration
let r be negative Real, s be non negative Real;
cluster ].r,s.[ -> non empty;
coherence
proof
r < (r+s)/2 & (r+s)/2 < s by XREAL_1:226;
hence thesis by XXREAL_1:4;
end;
cluster [.r,s.[ -> non empty;
coherence by XXREAL_1:3;
cluster ].r,s.] -> non empty;
coherence by XXREAL_1:2;
cluster [.r,s.] -> non empty;
coherence by XXREAL_1:1;
end;
begin :: Functions
theorem
for f being Function, 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, x, X be set;
assume
A1: x in dom f;
assume f.x in f.:X;
then
A2: ex a being object st a in dom f & a in X & f.x = f.a by FUNCT_1:def 6;
assume f is one-to-one;
hence thesis by A1,A2,FUNCT_1:def 4;
end;
theorem
for f being FinSequence, i being Nat st i+1 in dom f holds
i in dom f or i = 0
proof
let f be FinSequence;
let i be Nat;
assume
A1: i+1 in dom f;
then 1 <= i+1 by FINSEQ_3:25;
then
A2: 1 < i+1 or 1+0 = i+1 by XXREAL_0:1;
per cases by A2,NAT_1:13;
suppose
i = 0;
hence thesis;
end;
suppose
A3: 1 <= i;
i+1 <= len f by A1,FINSEQ_3:25;
then i <= len f by NAT_1:13;
hence thesis by A3,FINSEQ_3:25;
end;
end;
theorem Th3:
for x, y, X, Y being set, 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, f be Function such that
A1: x <> y and
A2: f in product ((x,y) --> (X,Y));
set g = (x,y) --> (X,Y);
A3: dom g = {x,y} by FUNCT_4:62;
then y in dom g by TARSKI:def 2;
then
A4: f.y in g.y by A2,CARD_3:9;
x in dom g by A3,TARSKI:def 2;
then f.x in g.x by A2,CARD_3:9;
hence thesis by A1,A4,FUNCT_4:63;
end;
theorem Th4:
for a, b being object holds <*a,b*> = (1,2) --> (a,b)
proof
let a, b be object;
set f = (1,2) --> (a,b);
set g = <*a,b*>;
A1: dom f = {1,2} by FUNCT_4:62;
A2: now
let x be object;
assume
A3: x in dom f;
per cases by A1,A3,TARSKI:def 2;
suppose
A4: x = 1;
hence f.x = a by FUNCT_4:63
.= g.x by A4,FINSEQ_1:44;
end;
suppose
A5: x = 2;
hence f.x = b by FUNCT_4:63
.= g.x by A5,FINSEQ_1:44;
end;
end;
dom g = {1,2} by FINSEQ_1:2,89;
hence thesis by A2,FUNCT_1:2,FUNCT_4:62;
end;
begin :: General topology
registration
cluster constituted-FinSeqs non empty strict for TopSpace;
existence
proof
take T=TopSpaceMetr Euclid 1;
thus for a being Element of T holds a is FinSequence
proof
let a be Element of T;
T = the TopStruct of TOP-REAL 1 by EUCLID:def 8;
hence a is FinSequence;
end;
thus thesis;
end;
end;
registration
let T be constituted-FinSeqs TopSpace;
cluster -> constituted-FinSeqs for SubSpace of T;
coherence
proof
let X be SubSpace of T;
let p be Element of X;
A1: the carrier of X is Subset of T by TSEP_1:1;
per cases;
suppose
the carrier of X is non empty;
then p in the carrier of X;
then reconsider p as Point of T by A1;
p is FinSequence;
hence thesis;
end;
suppose
the carrier of X is empty;
hence thesis;
end;
end;
end;
theorem Th5:
for T being non empty TopSpace, Z being non empty SubSpace of T,
t being Point of T, z being Point of Z, N being open a_neighborhood of t, 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, Z be non empty SubSpace of T, t be Point of T,
z be Point of Z, N be open a_neighborhood of t, M be Subset of Z such that
A1: t = z and
A2: M = N /\ [#]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 thesis by A2,CONNSP_2:def 1,TOPS_2:24;
end;
registration
cluster empty -> discrete anti-discrete for TopSpace;
coherence
proof
let T be TopSpace;
assume T is empty;
then the carrier of T = {};
then bool the carrier of T = {{}, the carrier of T} by ENUMSET1:29
,ZFMISC_1:1;
hence thesis by TDLAT_3:14;
end;
end;
registration
let X be discrete TopSpace, Y be TopSpace;
cluster -> continuous for Function of X,Y;
coherence by TEX_2:62;
end;
theorem Th6:
for X being TopSpace, Y being TopStruct, f being Function of X,Y
st f is empty holds f is continuous
proof
let X be TopSpace, Y be TopStruct, f be Function of X,Y such that
A1: f is empty;
let P being Subset of Y;
assume P is closed;
f"P = {}X by A1;
hence thesis;
end;
registration
let X be TopSpace, Y be TopStruct;
cluster empty -> continuous for Function of X,Y;
coherence by Th6;
end;
theorem
for X being TopStruct, Y being non empty TopStruct, Z being non empty
SubSpace of Y, f being Function of X,Z holds f is Function of X,Y
proof
let X be TopStruct, Y be non empty TopStruct, Z be non empty SubSpace of Y;
let f be Function of X,Z;
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 thesis by A1,FUNCT_2:2;
end;
theorem
for S, T being non empty TopSpace, X being Subset of S, Y being Subset
of T, f being continuous Function of S,T, g being Function of S|X,T|Y st g = f|
X holds g is continuous
proof
let S, T be non empty TopSpace, X be Subset of S, Y be Subset of T, f be
continuous Function of S,T, g be Function of S|X,T|Y such that
A1: g = f|X;
set h = f|X;
A2: the carrier of S|X = X & rng h c= the carrier of T by PRE_TOPC:8;
dom f = the carrier of S by FUNCT_2:def 1;
then dom h = X by RELAT_1:62;
then reconsider h as Function of S|X,T by A2,FUNCT_2:2;
h is continuous by TOPMETR:7;
hence thesis by A1,TOPMETR:6;
end;
theorem
for S, T being non empty TopSpace, Z being non empty SubSpace of T, f
being Function of S,T, g being Function of S,Z st f = g & f is open holds g is
open
proof
let S, T be non empty TopSpace, Z be non empty SubSpace of T, f be Function
of S,T, g be Function of S,Z such that
A1: f = g and
A2: f is open;
for p being Point of S, 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, P be open a_neighborhood of 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 as a_neighborhood of g.p by A1,Th5;
take R2;
R2 c= R by XBOOLE_1:17;
hence thesis by A1,A3;
end;
hence thesis by TOPGRP_1:23;
end;
theorem
for S, T being non empty TopSpace, S1 being Subset of S, T1 being
Subset of T, f being Function of S,T, g being Function of S|S1,T|T1 st g = f|S1
& g is onto & f is open one-to-one holds g is open
proof
let S, T be non empty TopSpace, S1 be Subset of S, T1 be Subset of T, f be
Function of S,T, g be Function of S|S1,T|T1 such 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;
let A be Subset of S|S1;
A5: [#](T|T1)= T1 by PRE_TOPC:def 5;
assume 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;
let y be object;
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;
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 object 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 thesis by A14,A15,FUNCT_1:def 6;
end;
f.:C is open by A3,A6;
hence thesis by A5,A9,TOPS_2:24;
end;
theorem
for X, Y, Z being non empty TopSpace, f being Function of X,Y, 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, f be Function of X,Y, g be Function of Y,
Z such that
A1: f is open and
A2: g is open;
let A be Subset of X;
assume A is open;
then
A3: f.:A is open by A1;
(g*f).:A = g.:(f.:A) by RELAT_1:126;
hence thesis by A2,A3;
end;
theorem
for X, Y being TopSpace, Z being open SubSpace of Y, f being Function
of X, Y, g being Function of X, Z st f = g & g is open holds f is open
proof
let X, Y be TopSpace, Z be open SubSpace of Y, f be Function of X, Y, g be
Function of X, Z such that
A1: f = g and
A2: g is open;
let A be Subset of X;
assume A is open;
then g.:A is open by A2;
hence thesis by A1,TSEP_1:17;
end;
theorem Th13:
for S, T being non empty TopSpace, f being Function of S,T st f
is one-to-one onto holds f is continuous iff f" is open
proof
let S, T be non empty TopSpace, f be Function of S,T such that
A1: f is one-to-one;
assume f is onto;
then
A2: f qua Function" = f" by A1,TOPS_2:def 4;
A3: [#]T <> {};
thus f is continuous implies f" is open
proof
assume
A4: f is continuous;
let A be Subset of T;
assume A is open;
then f"A is open by A3,A4,TOPS_2:43;
hence thesis by A1,A2,FUNCT_1:85;
end;
assume
A5: f" is open;
now
let A be Subset of T;
assume A is open;
then f".:A is open by A5;
hence f"A is open by A1,A2,FUNCT_1:85;
end;
hence thesis by A3,TOPS_2:43;
end;
theorem
for S, T being non empty TopSpace, f being Function of S,T st f is
one-to-one onto holds f is open iff f" is continuous
proof
let S, T be non empty TopSpace, f be Function of S,T such that
A1: f is one-to-one;
assume f is onto;
then
A2: rng f = [#]T;
then rng (f") = [#]S by A1,TOPS_2:49;
then
A3: f" is onto;
f" is one-to-one & f"" = f by A1,A2,TOPS_2:50,51;
hence thesis by A3,Th13;
end;
theorem
for S being TopSpace, T being non empty TopSpace holds S,T
are_homeomorphic iff the TopStruct of S, the TopStruct of T are_homeomorphic
proof
let S be TopSpace, T be non empty TopSpace;
set SS = the TopStruct of S;
set TT = the TopStruct of T;
A1: [#]S = [#]SS & [#]T = [#]TT;
thus S,T are_homeomorphic implies the TopStruct of S, the TopStruct of T
are_homeomorphic
proof
given f being Function of S,T such that
A2: f is being_homeomorphism;
reconsider g = f as Function of SS,TT;
A3: now
let P be Subset of SS;
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;
end;
take g;
dom f = [#]S & rng f = [#]T by A2,TOPS_2:60;
hence thesis by A1,A2,A3,TOPS_2:60;
end;
given f being Function of SS,TT such that
A4: f is being_homeomorphism;
reconsider g = f as Function of S,T;
A5: now
let P be Subset of S;
reconsider R = P as Subset of SS;
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;
end;
take g;
dom f = [#]SS & rng f = [#]TT by A4,TOPS_2:60;
hence thesis by A1,A4,A5,TOPS_2:60;
end;
theorem
for S, T being non empty TopSpace, f being Function of S,T st f is
one-to-one onto continuous open holds f is being_homeomorphism
proof
let S, T be non empty TopSpace, f be Function of S,T such that
A1: f is one-to-one and
A2: f is onto and
A3: f is continuous and
A4: f is open;
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;
thus P is open implies f.:P is open by A4;
assume f.:P is open;
then f"(f.:P) is open by A3,A5,TOPS_2:43;
hence thesis by A1,A6,FUNCT_1:94;
end;
dom f = [#]S & rng f = [#]T by A2,FUNCT_2:def 1;
hence thesis by A1,A7,TOPGRP_1:25;
end;
begin :: R^1
theorem
for f being PartFunc of REAL,REAL st f = REAL --> r holds f|REAL is
continuous
proof
let f be PartFunc of REAL,REAL such that
A1: f = REAL --> r;
f|REAL is constant
proof
reconsider r as Element of REAL by XREAL_0:def 1;
take r;
let c be Element of REAL;
assume c in dom(f|REAL);
thus (f|REAL).c = f.c
.= r by A1,FUNCOP_1:7;
end;
hence thesis;
end;
theorem
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;
set X1 = dom f1, X2 = dom f2;
assume that
A1: dom f = X1 \/ X2 and
A2: X1 is open and
A3: X2 is open and
A4: f1|X1 is continuous and
A5: f2|X2 is continuous and
A6: for z being set st z in X1 holds f.z = f1.z and
A7: for z being set st z in X2 holds f.z = f2.z;
A8: dom f /\ X1 = X1 by A1,XBOOLE_1:7,28;
A9: dom (f|X2) = dom f /\ X2 by RELAT_1:61;
let x be Real;
assume x in dom(f|dom f);
then
A10: x in dom f;
A11: (f|(X1 \/ X2)).x = f.x by A1;
A12: dom f /\ X2 = X2 by A1,XBOOLE_1:7,28;
A13: dom (f|X1) = dom f /\ X1 by RELAT_1:61;
per cases by A1,A10,XBOOLE_0:def 3;
suppose
A14: x in X1;
then
A15: (f|(X1 \/ X2)).x = f1.x by A6,A11
.= (f1|X1).x;
for N1 being Neighbourhood of (f|(X1 \/ X2)).x ex N being
Neighbourhood of x st for x1 being Real st x1 in dom (f|(X1 \/ X2)) & x1
in N holds (f|(X1 \/ X2)).x1 in N1
proof
let N1 be Neighbourhood of (f|(X1 \/ X2)).x;
consider N2 being Neighbourhood of x such that
A16: N2 c= X1 by A2,A14,RCOMP_1:18;
x in dom(f1|X1) by A14;
then f1|X1 is_continuous_in x by A4;
then consider N being Neighbourhood of x such that
A17: for x1 being Real st x1 in dom (f1|X1) & x1 in N holds (
f1|X1).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;
let x1 be Real such that
A20: x1 in dom (f|(X1 \/ X2)) and
A21: x1 in N3;
per cases;
suppose
A22: x1 in dom (f|X1);
A23: dom (f|X1) = X1 /\ X1 by A1,A13,XBOOLE_1:7,28
.= dom (f1|X1);
A24: x1 in X1 by A13,A22,XBOOLE_0:def 4;
(f|(X1 \/ X2)).x1 = f.x1 by A20,FUNCT_1:47
.= f1.x1 by A6,A24
.= (f1|X1).x1;
hence thesis by A17,A18,A21,A22,A23;
end;
suppose
A25: not x1 in dom (f|X1);
x1 in N2 by A19,A21;
hence thesis by A13,A8,A16,A25;
end;
end;
hence thesis by A1,FCONT_1:4;
end;
suppose
A26: x in X2;
then
A27: (f|(X1 \/ X2)).x = f2.x by A7,A11
.= (f2|X2).x;
for N1 being Neighbourhood of (f|(X1 \/ X2)).x ex N being
Neighbourhood of x st for x1 being Real st x1 in dom (f|(X1 \/ X2)) & x1
in N holds (f|(X1 \/ X2)).x1 in N1
proof
let N1 be Neighbourhood of (f|(X1 \/ X2)).x;
consider N2 being Neighbourhood of x such that
A28: N2 c= X2 by A3,A26,RCOMP_1:18;
x in dom(f2|X2) by A26;
then f2|X2 is_continuous_in x by A5;
then consider N being Neighbourhood of x such that
A29: for x1 being Real st x1 in dom (f2|X2) & x1 in N holds (
f2|X2).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;
let x1 be Real such that
A32: x1 in dom (f|(X1 \/ X2)) and
A33: x1 in N3;
per cases;
suppose
A34: x1 in dom (f|X2);
A35: dom (f|X2) = X2 /\ X2 by A1,A9,XBOOLE_1:7,28
.= dom (f2|X2);
A36: x1 in X2 by A9,A34,XBOOLE_0:def 4;
(f|(X1 \/ X2)).x1 = f.x1 by A32,FUNCT_1:47
.= f2.x1 by A7,A36
.= (f2|X2).x1;
hence thesis by A29,A30,A33,A34,A35;
end;
suppose
A37: not x1 in dom (f|X2);
x1 in N2 by A31,A33;
hence thesis by A9,A12,A28,A37;
end;
end;
hence thesis by A1,FCONT_1:4;
end;
end;
theorem Th19:
for x being Point of R^1, N being Subset of REAL, M being Subset
of R^1 st M = N holds N is Neighbourhood of x implies M is a_neighborhood of x
proof
let x be Point of R^1, N be Subset of REAL, M be Subset of R^1 such that
A1: M = N;
given r such that
A2: 0 < r and
A3: N = ].x-r,x+r.[;
M is open by A1,A3,JORDAN6:35;
hence thesis by A1,A2,A3,CONNSP_2:3,TOPREAL6:15;
end;
theorem Th20:
for x being Point of R^1, M being a_neighborhood of x ex N being
Neighbourhood of x st N c= M
proof
let x be Point of R^1, M be a_neighborhood of x;
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;
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;
thus thesis by A2,A5;
end;
theorem Th21:
for f being Function of R^1,R^1, g being PartFunc of REAL,REAL,
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, g be PartFunc of REAL,REAL, x be Point of R^1
such that
A1: f = g and
A2: g is_continuous_in x;
let G be a_neighborhood of f.x;
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;
thus thesis by A1,A3,A4;
end;
theorem
for f being Function of R^1,R^1, 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, g be Function of REAL,REAL such that
A1: f = g and
A2: g is continuous;
for x being Point of R^1 holds f is_continuous_at x
proof
let x be Point of R^1;
dom f = REAL by A1,FUNCT_2:def 1;
then x in dom g by A1;
then g is_continuous_in x by A2;
hence thesis by A1,Th21;
end;
hence thesis by TMAP_1:44;
end;
theorem
a <= r & s <= b implies [.r,s.] is closed Subset of
Closed-Interval-TSpace(a,b)
proof
set T = Closed-Interval-TSpace(a,b);
set A = [.r,s.];
assume that
A1: a <= r and
A2: s <= b;
per cases;
suppose
r > s;
then A = {}T by XXREAL_1:29;
hence thesis;
end;
suppose
r <= s;
then a <= s by A1,XXREAL_0:2;
then the carrier of T = [.a,b.] by A2,TOPMETR:18,XXREAL_0:2;
then reconsider A as Subset of T by A1,A2,XXREAL_1:34;
reconsider C = A as Subset of R^1 by TOPMETR:17;
C is closed & C /\ [#]T = A by TREAL_1:1,XBOOLE_1:28;
hence thesis by PRE_TOPC:13;
end;
end;
theorem
a <= r & s <= b implies ].r,s.[ is open Subset of Closed-Interval-TSpace(a,b)
proof
set T = Closed-Interval-TSpace(a,b);
set A = ].r,s.[;
assume that
A1: a <= r and
A2: s <= b;
per cases;
suppose
r >= s;
then A = {}T by XXREAL_1:28;
hence thesis;
end;
suppose
r < s;
then a < s by A1,XXREAL_0:2;
then the carrier of T = [.a,b.] by A2,TOPMETR:18,XXREAL_0:2;
then reconsider A as Subset of T by A1,A2,XXREAL_1:37;
reconsider C = A as Subset of R^1 by TOPMETR:17;
C is open & C /\ [#]T = A by JORDAN6:35,XBOOLE_1:28;
hence thesis by TOPS_2:24;
end;
end;
theorem
a <= b & a <= r implies ].r,b.] is open Subset of Closed-Interval-TSpace(a,b)
proof
set T = Closed-Interval-TSpace(a,b);
assume that
A1: a <= b and
A2: a <= r;
A3: the carrier of T = [.a,b.] by A1,TOPMETR:18;
then reconsider A = ].r,b.] as Subset of T by A2,XXREAL_1:36;
reconsider C = ].r,b+1.[ as Subset of R^1 by TOPMETR:17;
A4: C /\ [#]T c= A
proof
let x be object;
assume
A5: x in C /\ [#]T;
then
A6: x in C by XBOOLE_0:def 4;
then reconsider x as Real;
A7: r < x by A6,XXREAL_1:4;
x <= b by A3,A5,XXREAL_1:1;
hence thesis by A7;
end;
b+0 < b+1 by XREAL_1:6;
then A c= C by XXREAL_1:49;
then A c= C /\ [#]T by XBOOLE_1:19;
then C is open & C /\ [#]T = A by A4,JORDAN6:35;
hence thesis by TOPS_2:24;
end;
theorem
a <= b & r <= b implies [.a,r.[ is open Subset of Closed-Interval-TSpace(a,b)
proof
set T = Closed-Interval-TSpace(a,b);
assume that
A1: a <= b and
A2: r <= b;
A3: the carrier of T = [.a,b.] by A1,TOPMETR:18;
then reconsider A = [.a,r.[ as Subset of T by A2,XXREAL_1:35;
reconsider C = ].a-1,r.[ as Subset of R^1 by TOPMETR:17;
A4: C /\ [#]T c= A
proof
let x be object;
assume
A5: x in C /\ [#]T;
then
A6: x in C by XBOOLE_0:def 4;
then reconsider x as Real;
A7: x < r by A6,XXREAL_1:4;
a <= x by A3,A5,XXREAL_1:1;
hence thesis by A7;
end;
a-1 < a-0 by XREAL_1:15;
then A c= C by XXREAL_1:48;
then A c= C/\[#]T by XBOOLE_1:19;
then C is open & C /\ [#]T = A by A4,JORDAN6:35;
hence thesis by TOPS_2:24;
end;
theorem Th27:
a <= b & r <= s implies the carrier of [:Closed-Interval-TSpace(
a,b),Closed-Interval-TSpace(r,s):] = [: [.a,b.], [.r,s.] :]
proof
set C1 = Closed-Interval-TSpace(a,b);
set C2 = Closed-Interval-TSpace(r,s);
assume a <= b & r <= s;
then the carrier of C1 = [.a,b.] & the carrier of C2 = [.r,s.] by TOPMETR:18;
hence thesis by BORSUK_1:def 2;
end;
begin :: TOP-REAL 2
theorem
|[a,b]| = (1,2) --> (a,b) by Th4;
theorem
|[a,b]|.1 = a & |[a,b]|.2 = b
proof
thus |[a,b]|.1 = ((1,2) --> (a,b)).1 by Th4
.= a by FUNCT_4:63;
thus |[a,b]|.2 = ((1,2) --> (a,b)).2 by Th4
.= b by FUNCT_4:63;
end;
theorem Th30:
closed_inside_of_rectangle(a,b,r,s) = product ((1,2)-->([.a,b.], [.r,s.]))
proof
set A = [.a,b.], B = [.r,s.];
set f = (1,2)-->(A,B);
set R = closed_inside_of_rectangle(a,b,r,s);
A1: R = {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 R c= product f
proof
let x be object;
assume x in R;
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 & p`2 in B by A3;
hence thesis by A2,A4,HILBERT3:11;
end;
let x be object;
assume
A5: x in product f;
then consider g being Function such that
A6: x = g and
A7: dom g = dom f and
for y being object st y in dom f holds g.y in f.y by CARD_3:def 5;
A8: g.2 in B by A5,A6,Th3;
A9: g.1 in A by A5,A6,Th3;
then reconsider g1 = g.1, g2 = g.2 as Real by A8;
A10: dom f = {1,2} by FUNCT_4:62;
then reconsider g as FinSequence by A7,FINSEQ_1:2,def 2;
A11: len g = 2 by A7,A10,FINSEQ_1:2,def 3;
|[g1,g2]| = (1,2) --> (g1,g2) by Th4;
then reconsider 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 thesis by A1,A6,A12;
end;
theorem Th31:
a <= b & r <= s implies |[a,r]| in closed_inside_of_rectangle(a, b,r,s)
proof
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} & o`1 = a by EUCLID:52
,JGRAPH_6:def 2;
A2: o`2 = r by EUCLID:52;
assume a <= b & r <= s;
hence thesis by A1,A2;
end;
definition
let a, b, c, d be Real;
func Trectangle(a,b,c,d) -> SubSpace of TOP-REAL 2 equals
(TOP-REAL 2) |
closed_inside_of_rectangle(a,b,c,d);
coherence;
end;
theorem Th32:
a <= b & r <= s implies Trectangle(a,b,r,s) is non empty
proof
assume a <= b & r <= s;
then |[a,r]| in closed_inside_of_rectangle(a,b,r,s) by Th31;
hence the carrier of Trectangle(a,b,r,s) is non empty;
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 by Th32;
end;
definition
func R2Homeomorphism -> Function of [:R^1,R^1:], TOP-REAL 2 means
:Def2:
for x, y being Real holds it. [x,y] = <*x,y*>;
existence
by BORSUK_6:20;
uniqueness
proof
let f, g be Function of [:R^1,R^1:], TOP-REAL 2 such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> and
A2: for x, y being Real holds g. [x,y] = <*x,y*>;
let a be Point of [:R^1,R^1:];
consider x, y being Element of R such that
A3: a = [x,y] by Lm1,DOMAIN_1:1;
thus f.a = <*x,y*> by A1,A3
.= g.a by A2,A3;
end;
end;
theorem Th33:
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 thesis by TOPREAL6:75;
end;
theorem Th34:
R2Homeomorphism is being_homeomorphism
proof
for x, y being Real holds R2Homeomorphism. [x,y] = <*x,y*> by Def2;
hence thesis by TOPREAL6:76;
end;
theorem Th35:
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)
proof
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 [:C1,C2:];
assume a <= b & r <= s;
then
A1: the carrier of [:C1,C2:] = [: [.a,b.], [.r,s.] :] by Th27;
dom R2Homeomorphism = [:R,R:] by Lm1,FUNCT_2:def 1;
then
A2: dom h = the carrier of [:C1,C2:] by A1,RELAT_1:62,TOPMETR:17,ZFMISC_1:96;
rng h c= the carrier of TR
proof
let y be object;
A3: the carrier of TR = 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 h;
then consider x being object such that
A4: x in dom h and
A5: h.x = y by FUNCT_1:def 3;
reconsider x as Point of [:R^1,R^1:] by A4;
dom h c= [:R,R:] by A1,A2,TOPMETR:17,ZFMISC_1:96;
then consider x1, x2 being Element of R 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: h.x = R2Homeomorphism.x by A4,FUNCT_1:47;
then reconsider p = h.x as Point of TOP-REAL 2;
A9: h.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 thesis by A5,A3,A10;
end;
hence thesis by A2,FUNCT_2:2;
end;
theorem Th36:
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
proof
assume
A1: a <= b & r <= s;
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]|;
p`1 = a & p`2 = r by EUCLID:52;
then p in closed_inside_of_rectangle(a,b,r,s) by A1,A2;
then reconsider T0 = TR 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 [:C1,C2:], TR such that
A3: h = R2Homeomorphism | the carrier of [:C1,C2:];
reconsider S0 = [:C1,C2:] 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 TR = 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;
let y be object;
A6: the carrier of [:C1,C2:] = [:[.a,b.],[.r,s.]:] & dom g = the carrier
of S0 by A1,Th27,FUNCT_2:def 1;
assume y in the carrier of T0;
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 thesis by A9,FUNCT_1:def 3;
end;
g = R2Homeomorphism|S0 by A3;
hence thesis by A5,Th34,JORDAN16:9;
end;
theorem
a <= b & r <= s implies [:Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s) are_homeomorphic
proof
set C1 = Closed-Interval-TSpace(a,b);
set C2 = Closed-Interval-TSpace(r,s);
assume
A1: a <= b & r <= s;
then reconsider
h = R2Homeomorphism | the carrier of [:C1,C2:] as Function of [:
C1,C2:], Trectangle(a,b,r,s) by Th35;
take h;
thus thesis by A1,Th36;
end;
theorem Th38:
a <= b & r <= s implies for A being Subset of
Closed-Interval-TSpace(a,b), B being Subset of Closed-Interval-TSpace(r,s)
holds product ((1,2)-->(A,B)) is Subset of Trectangle(a,b,r,s)
proof
set T = Closed-Interval-TSpace(a,b);
set S = Closed-Interval-TSpace(r,s);
assume a <= b & r <= s;
then
A1: the carrier of T = [.a,b.] & the carrier of S = [.r,s.] by TOPMETR:18;
let A be Subset of T;
let B be Subset of 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 thesis by PRE_TOPC:8;
end;
theorem
a <= b & r <= s implies for A being open Subset of
Closed-Interval-TSpace(a,b), 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
set T = Closed-Interval-TSpace(a,b);
set S = Closed-Interval-TSpace(r,s);
assume
A1: 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 T, B be open Subset of 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 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 T 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 & Trectangle(a,b,r,s) is non empty by A1,Th32,Th36;
hence thesis by A5,A2,TOPGRP_1:25;
end;
theorem
a <= b & r <= s implies for A being closed Subset of
Closed-Interval-TSpace(a,b), 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
set T = Closed-Interval-TSpace(a,b);
set S = Closed-Interval-TSpace(r,s);
assume
A1: 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 T, B be closed Subset of 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 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 T 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 & Trectangle(a,b,r,s) is non empty by A1,Th32,Th36;
hence thesis by A5,A2,TOPS_2:58;
end;