:: Some Properties of Real Maps
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997-2026 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, SUBSET_1, PRE_TOPC, EUCLID, TOPREAL1, RCOMP_1, FUNCT_1,
BORSUK_1, RELAT_1, TOPS_2, CARD_1, XBOOLE_0, ORDINAL2, STRUCT_0,
METRIC_1, ARYTM_1, ARYTM_3, SUPINF_2, RLTOPSP1, REAL_1, XXREAL_1, TARSKI,
XXREAL_0, PCOMPS_1, CONNSP_2, TOPMETR, TOPS_1, COMPLEX1, BORSUK_2,
GRAPH_1, PARTFUN1, TMAP_1, FCONT_1, VALUED_0, SEQ_4, XXREAL_2, FUNCT_2,
PSCOMP_1, FINSET_1, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, XXREAL_2, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
FINSET_1, PARTFUN1, FUNCT_2, FCONT_1, RFUNCT_2, SEQ_4, MEASURE6, TOPMETR,
BINOP_1, TOPS_1, METRIC_1, CONNSP_2, STRUCT_0, TOPREAL1, PRE_TOPC,
TOPS_2, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, TMAP_1, PSCOMP_1, PCOMPS_1,
WEIERSTR, BORSUK_2, RCOMP_1;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, FCONT_1, TOPS_1,
TOPS_2, COMPTS_1, TMAP_1, TOPREAL1, WEIERSTR, BORSUK_2, RVSUM_1, CONVEX1,
BINOP_2, PSCOMP_1, MEASURE6, BINOP_1;
registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
RCOMP_1, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR,
TOPREAL1, PSCOMP_1, BORSUK_2, VALUED_0, COMPTS_1, XXREAL_2, RLTOPSP1,
FCONT_1, FUNCT_2, FUNCT_1, SUBSET_1, FINSET_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, BORSUK_2, XBOOLE_0, XXREAL_2, PRE_TOPC, PSCOMP_1;
equalities STRUCT_0, RLTOPSP1, SUBSET_1, RLVECT_1;
expansions TARSKI, BORSUK_2, XBOOLE_0, XXREAL_2, PRE_TOPC;
theorems BORSUK_1, COMPTS_1, CONNSP_2, EUCLID, FCONT_1, FCONT_2, FUNCT_1,
FUNCT_2, GOBOARD7, GOBOARD9, METRIC_1, PARTFUN2, PCOMPS_1, PRE_TOPC,
RCOMP_1, RELAT_1, RFUNCT_2, SEQ_4, TARSKI, TBSP_1, TMAP_1, TOPMETR,
TOPREAL1, TOPS_2, TOPS_1, WEIERSTR, TOPREAL3, RELSET_1, XREAL_0,
XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, XXREAL_2,
XXREAL_1, MEMBERED, MEASURE6, HEINE, RLVECT_1;
schemes CLASSES1;
begin :: Preliminaries
theorem Th1:
for n being Nat, p, q being Point of TOP-REAL n, P
being Subset of TOP-REAL n st P is_an_arc_of p, q holds P is compact
proof
let n be Nat;
let p, q be Point of TOP-REAL n;
let P be Subset of TOP-REAL n;
assume P is_an_arc_of p, q;
then consider f be Function of I[01], (TOP-REAL n)|P such that
A1: f is being_homeomorphism and
f.0 = p and
f.1 = q by TOPREAL1:def 1;
per cases;
suppose
P <> {};
then reconsider P9 = P as non empty Subset of TOP-REAL n;
f is continuous & rng f = [#] ((TOP-REAL n)|P9) by A1,TOPS_2:def 5;
then (TOP-REAL n)|P9 is compact by COMPTS_1:14;
hence thesis by COMPTS_1:3;
end;
suppose
P = {}TOP-REAL n;
hence thesis;
end;
end;
Lm1: for n being Nat holds the carrier of Euclid n = REAL n & the
carrier of TOP-REAL n = REAL n
proof
let n be Nat;
Euclid n = MetrStruct(#REAL n, Pitag_dist n#) by EUCLID:def 7;
hence thesis by EUCLID:67;
end;
theorem Th2:
for n being Nat, p1, p2 being Point of TOP-REAL n, r1,
r2 being Real st (1-r1)*p1+r1*p2 = (1-r2)*p1+r2*p2 holds r1 = r2 or p1 =
p2
proof
let n be Nat, p1, p2 be Point of TOP-REAL n, r1, r2 be Real;
assume
A1: (1-r1)*p1+r1*p2 = (1-r2)*p1+r2*p2;
A2: 1*p1+(-r1*p1+r1*p2) = 1*p1+-r1*p1+r1*p2 by RLVECT_1:def 3
.= 1*p1-r1*p1+r1*p2
.= (1-r2)*p1+r2*p2 by A1,RLVECT_1:35
.= 1*p1-r2*p1+r2*p2 by RLVECT_1:35
.= 1*p1+-r2*p1+r2*p2
.= 1*p1+(-r2*p1+r2*p2) by RLVECT_1:def 3;
A3: (r2-r1)*p1+r1*p2 = r2*p1-r1*p1+r1*p2 by RLVECT_1:35
.= r2*p1+-r1*p1+r1*p2
.= r2*p1+(-r1*p1+r1*p2) by RLVECT_1:def 3
.= r2*p1+(-r2*p1+r2*p2) by A2,GOBOARD7:4
.= r2*p1+-r2*p1+r2*p2 by RLVECT_1:def 3
.= 0.TOP-REAL n + r2*p2 by RLVECT_1:5
.= r2*p2 by RLVECT_1:4;
(r2-r1)*p1 = (r2-r1)*p1 + 0.TOP-REAL n by RLVECT_1:4
.= (r2-r1)*p1+(r1*p2 - r1*p2) by RLVECT_1:5
.= r2*p2 - r1*p2 by A3,RLVECT_1:def 3
.= (r2-r1)*p2 by RLVECT_1:35;
then r2-r1=0 or p1 = p2 by RLVECT_1:36;
hence thesis;
end;
theorem Th3:
for n being Nat for p1,p2 being Point of TOP-REAL n st
p1 <> p2 ex f being Function of I[01], (TOP-REAL n) | LSeg(p1,p2) st (for x
being Real st x in [.0,1.] holds f.x = (1-x)*p1 + x*p2) & f is
being_homeomorphism & f.0 = p1 & f.1 = p2
proof
let n be Nat;
let p1, p2 be Point of TOP-REAL n;
reconsider p19 = p1, p29 = p2 as Element of REAL n by Lm1;
set P = LSeg(p1,p2);
reconsider PP = P as Subset of Euclid n by TOPREAL3:8;
reconsider PP as non empty Subset of Euclid n;
defpred P[object,object] means
for x being Real st x = $1 holds $2 = (1-x)*p1 + x* p2;
A1: for a being object st a in [.0,1.] ex u being object st P[a,u]
proof
let a be object;
assume a in [.0,1.];
then reconsider x = a as Real;
take (1-x)*p1 + x*p2;
thus thesis;
end;
consider f being Function such that
A2: dom f = [.0,1.] and
A3: for a being object st a in [.0,1.] holds P[a,f.a] from CLASSES1:sch 1(
A1);
rng f c= the carrier of (TOP-REAL n)|P
proof
let y be object;
assume y in rng f;
then consider x being object such that
A4: x in dom f and
A5: y = f.x by FUNCT_1:def 3;
x in { r where r is Real: 0 <= r & r <= 1 } by A2,A4,RCOMP_1:def 1;
then consider r being Real such that
A6: r = x and
A7: 0 <= r & r <= 1;
y = (1-r)*p1 + r*p2 by A2,A3,A4,A5,A6;
then y in P by A7;
then y in [#]((TOP-REAL n)|P) by PRE_TOPC:def 5;
hence thesis;
end;
then reconsider f as Function of I[01], (TOP-REAL n)|P by A2,BORSUK_1:40
,FUNCT_2:def 1,RELSET_1:4;
assume
A8: p1 <> p2;
now
let x1,x2 be object;
assume that
A9: x1 in dom f and
A10: x2 in dom f and
A11: f.x1 = f.x2;
x2 in {r where r is Real : 0 <= r & r <= 1} by A2,A10,RCOMP_1:def 1;
then consider r2 being Real such that
A12: r2 = x2 and
0 <= r2 and
r2 <= 1;
A13: f.x2 = (1-r2)*p1 + r2*p2 by A2,A3,A10,A12;
x1 in {r where r is Real: 0 <= r & r <= 1} by A2,A9,RCOMP_1:def 1;
then consider r1 being Real such that
A14: r1 = x1 and
0 <= r1 and
r1 <= 1;
f.x1 = (1-r1)*p1 + r1*p2 by A2,A3,A9,A14;
hence x1 = x2 by A8,A11,A14,A12,A13,Th2;
end;
then
A15: f is one-to-one by FUNCT_1:def 4;
A16: (TOP-REAL n)|P = TopSpaceMetr((Euclid n)|PP) by EUCLID:63;
for W being Point of I[01], G being a_neighborhood of f.W ex H being
a_neighborhood of W st f.:H c= G
proof
reconsider p11=p1, p22=p2 as Point of Euclid n by TOPREAL3:8;
let W be Point of I[01], G be a_neighborhood of f.W;
reconsider W9 = W as Point of Closed-Interval-MSpace(0,1) by BORSUK_1:40
,TOPMETR:10;
reconsider W1 = W as Real;
f.W in Int G by CONNSP_2:def 1;
then consider Q being Subset of (TOP-REAL n)|P such that
A17: Q is open and
A18: Q c= G and
A19: f.W in Q by TOPS_1:22;
[#]((TOP-REAL n)|P) = P by PRE_TOPC:def 5;
then reconsider Y = f.W as Point of (Euclid n)|PP by TOPMETR:def 2;
consider r being Real such that
A20: r > 0 and
A21: Ball(Y,r) c= Q by A16,A17,A19,TOPMETR:15;
reconsider r as Element of REAL by XREAL_0:def 1;
set delta = r/(Pitag_dist n).(p19,p29);
reconsider H = Ball(W9,delta) as Subset of I[01] by BORSUK_1:40,TOPMETR:10;
Closed-Interval-TSpace(0,1) = TopSpaceMetr(Closed-Interval-MSpace(0,1
)) by TOPMETR:def 7;
then
A22: H is open by TOPMETR:14,20;
P = the carrier of (Euclid n)|PP by TOPMETR:def 2;
then reconsider WW9 = Y as Point of Euclid n by TARSKI:def 3;
Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
then
A23: (Pitag_dist n).(p19,p29) = dist(p11,p22) by METRIC_1:def 1;
A24: dist(p11,p22) >= 0 & dist(p11,p22) <> 0 by A8,METRIC_1:2,5;
then W in H by A20,A23,TBSP_1:11,XREAL_1:139;
then W in Int H by A22,TOPS_1:23;
then reconsider H as a_neighborhood of W by CONNSP_2:def 1;
take H;
A25: delta > 0 by A20,A23,A24,XREAL_1:139;
f.:H c= Ball(Y,r)
proof
reconsider WW1 = WW9 as Element of REAL n by Lm1;
let a be object;
A26: [#] ((TOP-REAL n)|P) = P by PRE_TOPC:def 5;
assume a in f.:H;
then consider u being object such that
A27: u in dom f and
A28: u in H and
A29: a = f.u by FUNCT_1:def 6;
reconsider u1 = u as Real by A27;
A30: f.W = (1-W1)*p1 + W1*p2 by A3,BORSUK_1:40;
reconsider u9 = u as Point of Closed-Interval-MSpace(0,1) by A28;
reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR:8;
A31: dist(W9,u9) = (the distance of Closed-Interval-MSpace(0,1)).(W9,u9)
by METRIC_1:def 1
.= (the distance of RealSpace).(W99,u99) by TOPMETR:def 1
.= dist(W99,u99) by METRIC_1:def 1;
dist(W9,u9) < delta by A28,METRIC_1:11;
then |.W1-u1.| < delta by A31,TOPMETR:11;
then |.-(u1-W1).| < delta;
then
A32: |.u1-W1.| < delta by COMPLEX1:52;
A33: delta <> 0 by A20,A23,A24,XREAL_1:139;
then (Pitag_dist n).(p19,p29) = r/delta by XCMPLX_1:54;
then
A34: |.p19 - p29.| = r/delta by EUCLID:def 6;
f.u in rng f by A27,FUNCT_1:def 3;
then reconsider aa = a as Point of (Euclid n)|PP by A29,A26,TOPMETR:def 2
;
P = the carrier of (Euclid n)|PP by TOPMETR:def 2;
then reconsider aa9 = aa as Point of Euclid n by TARSKI:def 3;
reconsider aa1 = aa9 as Element of REAL n by Lm1;
aa1 = ((1-u1)*p1 + u1*p2) by A2,A3,A27,A29;
then WW1 - aa1 = (1-W1)*p1 + W1*p2 - ((1-u1)*p1 + u1*p2) by A30
.= W1*p2 + (1-W1)*p1 - (1-u1)*p1 - u1*p2 by RLVECT_1:27
.= W1*p2 + ((1-W1)*p1 - (1-u1)*p1) - u1*p2 by RLVECT_1:def 3
.= W1*p2 + ((1-W1)-(1-u1))*p1 - u1*p2 by RLVECT_1:35
.= (u1-W1)*p1 + (W1*p2 - u1*p2) by RLVECT_1:def 3
.= (u1-W1)*p1 + (W1-u1)*p2 by RLVECT_1:35
.= (u1-W1)*p1 + (-(u1-W1))*p2
.= (u1-W1)*p1 + -(u1-W1)*p2 by RLVECT_1:79
.= (u1-W1)*p1 - (u1-W1)*p2
.= (u1-W1)*(p1 - p2) by RLVECT_1:34
.= (u1-W1)*(p19 - p29);
then
A35: |. WW1 -aa1 .| = |.u1-W1.|*|.p19 - p29.| by EUCLID:11;
r/delta > 0 by A20,A25,XREAL_1:139;
then |. WW1 - aa1.| < delta*(r/delta) by A35,A32,A34,XREAL_1:68;
then Euclid n = MetrStruct(#REAL n,Pitag_dist n#) & |. WW1 - aa1 .| < r
by A33,EUCLID:def 7,XCMPLX_1:87;
then (the distance of Euclid n).(WW9,aa9) < r by EUCLID:def 6;
then (the distance of (Euclid n)|PP).(Y,aa) < r by TOPMETR:def 1;
then dist(Y,aa) < r by METRIC_1:def 1;
hence thesis by METRIC_1:11;
end;
then f.:H c= Q by A21;
hence thesis by A18;
end;
then
A36: f is continuous by BORSUK_1:def 1;
take f;
thus for x being Real st x in [.0,1.]
holds f.x = (1-x)*p1 + x*p2 by A3;
[#]((TOP-REAL n)|P) c= rng f
proof
let a be object;
assume a in [#]((TOP-REAL n)|P);
then a in { (1-l)*p1 + l*p2 where l is Real: 0 <= l & l <= 1 }
by PRE_TOPC:def 5;
then consider lambda be Real such that
A37: a = (1-lambda)*p1 + lambda*p2 and
A38: 0 <= lambda & lambda <= 1;
lambda in { r where r is Real : 0 <= r & r <= 1} by A38;
then
A39: lambda in dom f by A2,RCOMP_1:def 1;
then a = f.lambda by A2,A3,A37;
hence thesis by A39,FUNCT_1:def 3;
end;
then [#]I[01] = [.0,1.] & rng f = [#]((TOP-REAL n)|P) by BORSUK_1:40;
hence f is being_homeomorphism by A15,A36,COMPTS_1:17;
0 in [.0,1.] by XXREAL_1:1;
hence f.0 = (1-0)*p1 + 0 * p2 by A3
.= p1 + 0 * p2 by RLVECT_1:def 8
.= p1 + 0.TOP-REAL n by RLVECT_1:10
.= p1 by RLVECT_1:4;
1 in [.0,1.] by XXREAL_1:1;
hence f.1 = (1-1)*p1 + 1*p2 by A3
.= 0.TOP-REAL n + 1*p2 by RLVECT_1:10
.= 1*p2 by RLVECT_1:4
.= p2 by RLVECT_1:def 8;
end;
Lm2: for n being Nat holds TOP-REAL n is pathwise_connected
proof
let n be Nat;
set T = TOP-REAL n;
let a, b be Point of T;
set L = LSeg (a, b);
per cases;
suppose
a <> b;
then consider f being Function of I[01], T | L such that
for x being Real st x in [.0,1.] holds f.x = (1-x)*a + x*b and
A1: f is being_homeomorphism and
A2: f.0 = a & f.1 = b by Th3;
rng f c= [#](T|L);
then rng f c= L by PRE_TOPC:def 5;
then dom f = the carrier of I[01] & rng f c= the carrier of T by
FUNCT_2:def 1,XBOOLE_1:1;
then reconsider g = f as Function of I[01], T by RELSET_1:4;
f is continuous by A1,TOPS_2:def 5;
then g is continuous by PRE_TOPC:26;
hence thesis by A2;
end;
suppose a = b;
hence a,b are_connected;
end;
end;
registration
let n be Nat;
cluster TOP-REAL n -> pathwise_connected;
coherence by Lm2;
end;
registration
let n be Nat;
cluster compact non empty strict for SubSpace of TOP-REAL n;
existence
proof
set A = the compact non empty Subset of TOP-REAL n;
reconsider T = (TOP-REAL n) | A as non empty SubSpace of TOP-REAL n;
T is compact;
hence thesis;
end;
end;
theorem
for a, b being Point of TOP-REAL 2, f being Path of a, b, P being non
empty compact SubSpace of TOP-REAL 2, g being Function of I[01], P st f is
one-to-one & g = f & [#]P = rng f holds g is being_homeomorphism
by COMPTS_1:17,PRE_TOPC:27;
Lm3: for X being Subset of REAL holds X is open implies X in Family_open_set
RealSpace
proof
let X be Subset of REAL;
reconsider V = X as Subset of RealSpace by METRIC_1:def 13;
assume
A1: X is open;
for x be Element of RealSpace st x in X
ex r be Real st r>0 & Ball (x,r) c= X
proof
let x be Element of RealSpace;
reconsider r = x as Element of REAL by METRIC_1:def 13;
assume x in X;
then consider N be Neighbourhood of r such that
A2: N c= X by A1,RCOMP_1:18;
consider g be Real such that
A3: 0<g and
A4: N = ].r-g,r+g.[ by RCOMP_1:def 6;
reconsider g as Element of REAL by XREAL_0:def 1;
A5: N c= Ball(x,g)
proof
reconsider r9 = r as Element of RealSpace;
let a be object;
assume
A6: a in N;
then reconsider a9 = a as Element of REAL;
reconsider a1 = a9, r1 = r9 as Element of REAL;
a9 is Element of REAL;
then reconsider a99 = a as Element of RealSpace by METRIC_1:def 13;
|.a9-r.| < g by A4,A6,RCOMP_1:1;
then real_dist.(a9,r) < g by METRIC_1:def 12;
then dist(r9,a99) = real_dist.(r,a9) & real_dist.(r1,a1) < g by
METRIC_1:9,def 1,def 13;
hence thesis by METRIC_1:11;
end;
Ball(x,g) c= N
proof
let a be object;
assume a in Ball(x,g);
then a in {q where q is Element of RealSpace : dist(x,q)<g } by
METRIC_1:17;
then consider q be Element of RealSpace such that
A7: q = a and
A8: dist(x,q) < g;
reconsider a9 = a as Real by A7;
reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def 13;
real_dist.(q1,x1) < g by A8,METRIC_1:def 1,def 13;
then |.a9-r.| < g by A7,METRIC_1:def 12;
hence thesis by A4,RCOMP_1:1;
end;
then N = Ball(x,g) by A5;
hence thesis by A2,A3;
end;
then V in Family_open_set RealSpace by PCOMPS_1:def 4;
hence thesis;
end;
Lm4: for X being Subset of REAL holds X in Family_open_set RealSpace implies X
is open
proof
let X be Subset of REAL;
assume
A1: X in Family_open_set RealSpace;
for r be Element of REAL st r in X holds ex N be Neighbourhood of r st N c= X
proof
let r be Element of REAL;
assume
A2: r in X;
reconsider r as Element of REAL;
reconsider x = r as Element of RealSpace by METRIC_1:def 13;
ex N be Neighbourhood of r st N c= X
proof
consider r1 be Real such that
A3: r1 > 0 and
A4: Ball(x,r1) c= X by A1,A2,PCOMPS_1:def 4;
reconsider N1 = Ball (x, r1) as Subset of REAL by METRIC_1:def 13;
ex g be Real st 0<g & Ball(x,r1) = ].r-g,r+g.[
proof
take g = r1;
A5: ].r-g,r+g.[ c= N1
proof
let a be object;
assume
A6: a in ].r-g,r+g.[;
then reconsider a9 = a as Element of REAL;
a9 is Element of REAL;
then reconsider a99 = a, r9 = r as Element of RealSpace by
METRIC_1:def 13;
reconsider a1 = a9, r1 = r9 as Element of REAL;
|.a9-r.| < g by A6,RCOMP_1:1;
then real_dist.(a9,r) < g by METRIC_1:def 12;
then dist(r9,a99) = real_dist.(r,a9) & real_dist.(r1,a1) < g by
METRIC_1:9,def 1,def 13;
hence thesis by METRIC_1:11;
end;
N1 c= ].r-g,r+g.[
proof
let a be object;
assume a in N1;
then a in {q where q is Element of RealSpace : dist(x,q)<g } by
METRIC_1:17;
then consider q be Element of RealSpace such that
A7: q = a and
A8: dist(x,q) < g;
reconsider a9 = a as Real by A7;
reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def 13;
real_dist.(q1,x1) < g by A8,METRIC_1:def 1,def 13;
then |.a9-r.| < g by A7,METRIC_1:def 12;
hence thesis by RCOMP_1:1;
end;
hence thesis by A3,A5;
end;
then reconsider N = N1 as Neighbourhood of r by RCOMP_1:def 6;
take N;
thus thesis by A4;
end;
hence thesis;
end;
hence thesis by RCOMP_1:20;
end;
begin
:: Equivalence of analytical and topological definitions of continuity
theorem Th5:
for X being Subset of REAL holds X in Family_open_set RealSpace iff X
is open by Lm3,Lm4;
theorem Th6:
for f being Function of R^1, R^1, x being Point of R^1 for g
being PartFunc of REAL, REAL, x1 being Real
st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1
proof
let f be Function of R^1, R^1, x be Point of R^1;
let g be PartFunc of REAL, REAL, x1 be Real;
assume that
A1: f is_continuous_at x and
A2: f = g and
A3: x = x1;
for N1 being Neighbourhood of g.x1 ex N being Neighbourhood of x1 st g.:
N c= N1
proof
reconsider fx = f.x as Point of R^1;
let N1 be Neighbourhood of g.x1;
reconsider N19 = N1 as Subset of R^1 by TOPMETR:17;
reconsider N2 = N1 as Subset of RealSpace by TOPMETR:12,17,def 6;
N2 in Family_open_set RealSpace by Lm3;
then N2 in the topology of TopSpaceMetr RealSpace by TOPMETR:12;
then N19 is open by TOPMETR:def 6;
then reconsider G = N19 as a_neighborhood of fx by A2,A3,CONNSP_2:3
,RCOMP_1:16;
consider H being a_neighborhood of x such that
A4: f.:H c= G by A1,TMAP_1:def 2;
consider V being Subset of R^1 such that
A5: V is open and
A6: V c= H and
A7: x in V by CONNSP_2:6;
reconsider V1 = V as Subset of REAL by TOPMETR:17;
V in the topology of R^1 by A5;
then V in Family_open_set RealSpace by TOPMETR:12,def 6;
then V1 is open by Lm4;
then consider N being Neighbourhood of x1 such that
A8: N c= V1 by A3,A7,RCOMP_1:18;
N c= H by A6,A8;
then g.:N c= g.:H by RELAT_1:123;
hence thesis by A2,A4,XBOOLE_1:1;
end;
hence thesis by FCONT_1:5;
end;
theorem Th7:
for f being continuous Function of R^1, R^1, g being PartFunc of
REAL, REAL st f = g holds g is continuous
proof
let f be continuous Function of R^1, R^1;
let g be PartFunc of REAL, REAL;
assume
A1: f = g;
for x0 being Real st x0 in dom(g) holds g is_continuous_in x0
by A1,Th6,TMAP_1:44,TOPMETR:17;
hence thesis by FCONT_1:def 2;
end;
Lm5: for f being continuous one-to-one Function of R^1, R^1, g being PartFunc
of REAL, REAL st f = g holds g| [.0,1.] is increasing or g| [.0,1.] is
decreasing
proof
let f be continuous one-to-one Function of R^1, R^1;
let g be PartFunc of REAL, REAL;
assume
A1: f = g;
then dom f = REAL & g is continuous by Th7,FUNCT_2:def 1,TOPMETR:17;
hence thesis by A1,FCONT_2:17;
end;
theorem
for f being continuous one-to-one Function of R^1, R^1 holds (for x, y
being Point of I[01], p, q, fx, fy being Real
st x = p & y = q & p < q & fx = f
.x & fy = f.y holds fx < fy) or
for x, y being Point of I[01], p, q, fx, fy being Real
st x = p & y = q & p < q & fx = f.x & fy = f.y holds fx > fy
proof
let f be continuous one-to-one Function of R^1, R^1;
A1: [.0,1.] /\ dom f = [.0,1.] /\ the carrier of R^1 by FUNCT_2:def 1
.= [.0,1.] by BORSUK_1:1,40,TOPMETR:20,XBOOLE_1:28;
reconsider g = f as PartFunc of REAL, REAL by TOPMETR:17;
per cases by Lm5;
suppose
g| [.0,1.] is increasing;
hence thesis by A1,BORSUK_1:40,RFUNCT_2:20;
end;
suppose
g| [.0,1.] is decreasing;
hence thesis by A1,BORSUK_1:40,RFUNCT_2:21;
end;
end;
theorem Th9:
for r, gg, a, b being Real, x being Element of
Closed-Interval-MSpace (a, b) st a <= b & x = r & ].r-gg, r+gg.[ c= [.a,b.]
holds ].r-gg, r+gg.[ = Ball (x, gg)
proof
let r, gg, a, b be Real, x be Element of Closed-Interval-MSpace(a,b);
assume that
A1: a <= b and
A2: x=r and
A3: ].r-gg, r+gg.[ c= [.a,b.];
reconsider g = gg as Element of REAL by XREAL_0:def 1;
reconsider r as Element of REAL by XREAL_0:def 1;
set CM = Closed-Interval-MSpace(a,b);
set N1 = Ball (x, g);
A4: the carrier of CM c= the carrier of RealSpace by TOPMETR:def 1;
A5: N1 c= ].r-g,r+g.[
proof
let i be object;
assume i in N1;
then i in {q where q is Element of CM : dist(x,q)<g} by METRIC_1:17;
then consider q be Element of CM such that
A6: q = i and
A7: dist(x,q) < g;
reconsider a9 = i as Element of REAL by A4,A6,METRIC_1:def 13;
reconsider x2 = x, q2 = q as Element of CM;
reconsider x1 = x, q1 = q as Element of REAL by A4,METRIC_1:def 13;
dist(x2,q2) = (the distance of CM).(x2,q2) by METRIC_1:def 1
.= real_dist.(x2,q2) by METRIC_1:def 13,TOPMETR:def 1;
then real_dist.(q1,x1) < g by A7,METRIC_1:9;
then |.a9-r.| < g by A2,A6,METRIC_1:def 12;
hence thesis by RCOMP_1:1;
end;
].r-g,r+g.[ c= N1
proof
let i be object;
assume
A8: i in ].r-g,r+g.[;
then reconsider a9 = i as Element of REAL;
reconsider a99 = i as Element of CM by A1,A3,A8,TOPMETR:10;
|.a9-r.| < g by A8,RCOMP_1:1;
then
A9: real_dist.(a9,r) < g by METRIC_1:def 12;
dist(x,a99) = (the distance of CM).(x,a99) by METRIC_1:def 1
.= real_dist.(x,a99) by METRIC_1:def 13,TOPMETR:def 1;
then dist(x,a99) < g by A2,A9,METRIC_1:9;
hence thesis by METRIC_1:11;
end;
hence thesis by A5;
end;
theorem Th10:
for a, b being Real, X being Subset of REAL st a < b & not a in
X & not b in X holds X in Family_open_set Closed-Interval-MSpace(a,b) implies X
is open
proof
let a, b be Real, X be Subset of REAL;
assume that
A1: a < b and
A2: not a in X and
A3: not b in X;
assume
A4: X in Family_open_set Closed-Interval-MSpace(a,b);
then reconsider V = X as Subset of Closed-Interval-MSpace(a,b);
for r be Element of REAL st r in X holds ex N be Neighbourhood of r st N c= X
proof
let r be Element of REAL;
assume
A5: r in X;
reconsider r as Real;
r in V by A5;
then reconsider x = r as Element of Closed-Interval-MSpace(a,b);
the carrier of Closed-Interval-MSpace(a,b) = [.a,b.] by A1,TOPMETR:10;
then x in [.a,b.];
then x in {l where l is Real: a <= l & l <= b } by RCOMP_1:def 1;
then
A6: ex r2 be Real st r2 = x & a <= r2 & r2 <= b;
A7: r-a <> 0 by A2,A5;
ex N be Neighbourhood of r st N c= X
proof
consider r1 be Real such that
A8: r1 > 0 and
A9: Ball(x,r1) c= X by A4,A5,PCOMPS_1:def 4;
per cases;
suppose
A10: r <= (a+b)/2;
set gg = min(r-a, r1);
gg > 0
proof
per cases by XXREAL_0:15;
suppose
gg = r-a;
hence thesis by A7,A6,XREAL_1:48;
end;
suppose
gg = r1;
hence thesis by A8;
end;
end;
then reconsider N = ].r-gg,r+gg.[ as Neighbourhood of r by
RCOMP_1:def 6;
take N;
].r-gg,r+gg.[ c= [.a,b.]
proof
2*r <= 2*((a+b)/2) by A10,XREAL_1:64;
then
A11: 2*r - a <= a+b -a by XREAL_1:13;
let i be object;
assume i in ].r-gg,r+gg.[;
then i in {l where l is Real: r-gg<l & l<r+gg }
by RCOMP_1:def 2;
then consider j be Real such that
A12: j = i and
A13: r-gg < j and
A14: j < r+gg;
A15: gg <= r-a by XXREAL_0:17;
then r + gg <= r + (r - a) by XREAL_1:6;
then r + gg <= a+b - a by A11,XXREAL_0:2;
then
A16: j <= b by A14,XXREAL_0:2;
gg+a <= r by A15,XREAL_1:19;
then r-gg >= a by XREAL_1:19;
then a <= j by A13,XXREAL_0:2;
then j in {l where l is Real: a <= l & l <= b } by A16;
hence thesis by A12,RCOMP_1:def 1;
end;
then ].r-gg,r+gg.[ = Ball (x, gg) by A1,Th9;
then ].r-gg,r+gg.[ c= Ball(x,r1) by PCOMPS_1:1,XXREAL_0:17;
hence thesis by A9;
end;
suppose
A17: r > (a+b)/2;
set gg = min(b-r, r1);
A18: b - r <> 0 by A3,A5;
gg > 0
proof
per cases by XXREAL_0:15;
suppose
gg = b-r;
hence thesis by A6,A18,XREAL_1:48;
end;
suppose
gg = r1;
hence thesis by A8;
end;
end;
then reconsider N = ].r-gg,r+gg.[ as Neighbourhood of r by
RCOMP_1:def 6;
take N;
].r-gg,r+gg.[ c= [.a,b.]
proof
2*r >= ((a+b)/2)*2 by A17,XREAL_1:64;
then
A19: 2*r - b >= a+b - b by XREAL_1:13;
let i be object;
assume i in ].r-gg,r+gg.[;
then i in {l where l is Real: r-gg<l & l<r+gg }
by RCOMP_1:def 2;
then consider j be Real such that
A20: j = i and
A21: r-gg < j and
A22: j < r+gg;
A23: gg <= b - r by XXREAL_0:17;
then r + gg <= b by XREAL_1:19;
then
A24: j <= b by A22,XXREAL_0:2;
r-gg >= r-(b-r) by A23,XREAL_1:13;
then r-gg >= a by A19,XXREAL_0:2;
then a <= j by A21,XXREAL_0:2;
then j in {l where l is Real: a <= l & l <= b } by A24;
hence thesis by A20,RCOMP_1:def 1;
end;
then ].r-gg,r+gg.[ = Ball (x, gg) by A1,Th9;
then N c= Ball(x,r1) by PCOMPS_1:1,XXREAL_0:17;
hence thesis by A9;
end;
end;
hence thesis;
end;
hence thesis by RCOMP_1:20;
end;
theorem Th11:
for X being open Subset of REAL, a, b being Real st X c= [.a,b.]
holds not a in X & not b in X
proof
let X be open Subset of REAL, a,b be Real;
assume
A1: X c= [.a,b.];
assume
A2: a in X or b in X;
per cases by A2;
suppose
a in X;
then consider g be Real such that
A3: 0<g and
A4: ].a-g,a+g.[ c= X by RCOMP_1:19;
g/2 <> 0 by A3;
then
A5: a - g/2 < a-0 by A3,XREAL_1:15;
g > g/2 by A3,XREAL_1:216;
then
A6: a-g < a-g/2 by XREAL_1:15;
a+0 < a+g by A3,XREAL_1:8;
then a-g/2 < a + g by A5,XXREAL_0:2;
then a-g/2 in {l where l is Real : a-g<l & l<a+g } by A6;
then
A7: a-g/2 in ].a-g,a+g.[ by RCOMP_1:def 2;
].a-g,a+g.[ c= [.a,b.] by A1,A4;
then a-g/2 in [.a,b.] by A7;
then a-g/2 in { l where l is Real: a <= l & l <= b }
by RCOMP_1:def 1;
then ex l be Real st l = a-g/2 & a <= l & l <= b;
hence thesis by A5;
end;
suppose
b in X;
then consider g be Real such that
A8: 0 < g and
A9: ].b-g,b+g.[ c= X by RCOMP_1:19;
g/2 <> 0 by A8;
then
A10: b+g/2 > b+0 by A8,XREAL_1:6;
g > g/2 by A8,XREAL_1:216;
then
A11: b+g/2 < b+g by XREAL_1:8;
b-g < b-0 by A8,XREAL_1:15;
then b-g < b+g/2 by A10,XXREAL_0:2;
then b+g/2 in {l where l is Real: b-g<l & l<b+g } by A11;
then
A12: b+g/2 in ].b-g,b+g.[ by RCOMP_1:def 2;
].b-g,b+g.[ c= [.a,b.] by A1,A9;
then b+g/2 in [.a,b.] by A12;
then b+g/2 in {l where l is Real: a <= l & l <= b}
by RCOMP_1:def 1;
then ex l be Real st l = b+g/2 & a<=l & l <=b;
hence thesis by A10;
end;
end;
theorem Th12:
for a, b being Real, X being Subset of REAL, V being Subset of
Closed-Interval-MSpace(a,b) st V = X holds X is open implies V in
Family_open_set Closed-Interval-MSpace(a,b)
proof
let a, b be Real;
let X be Subset of REAL, V be Subset of Closed-Interval-MSpace(a,b);
assume
A1: V = X;
assume
A2: X is open;
for x be Element of Closed-Interval-MSpace(a,b) st x in V holds ex r be
Real st r>0 & Ball(x,r) c= V
proof
let x be Element of Closed-Interval-MSpace(a,b);
assume
A3: x in V;
then reconsider r = x as Element of REAL by A1;
consider N be Neighbourhood of r such that
A4: N c= X by A1,A2,A3,RCOMP_1:18;
consider g be Real such that
A5: 0<g and
A6: N = ].r-g,r+g.[ by RCOMP_1:def 6;
reconsider g as Element of REAL by XREAL_0:def 1;
A7: Ball(x,g) c= N
proof
let aa be object;
assume aa in Ball(x,g);
then
aa in {q where q is Element of Closed-Interval-MSpace(a,b): dist(x,
q)<g} by METRIC_1:17;
then consider q be Element of Closed-Interval-MSpace(a,b) such that
A8: q = aa and
A9: dist(x,q) < g;
A10: q in the carrier of Closed-Interval-MSpace(a,b) & the carrier of
Closed-Interval-MSpace(a,b) c= the carrier of RealSpace by TOPMETR:def 1;
then reconsider a9 = aa as Real by A8;
reconsider x1 = x, q1 = q as Element of REAL by A10,METRIC_1:def 13;
dist(x,q) = (the distance of Closed-Interval-MSpace(a,b)).(x,q) by
METRIC_1:def 1
.= real_dist.(x,q) by METRIC_1:def 13,TOPMETR:def 1;
then real_dist.(q1,x1) < g by A9,METRIC_1:9;
then |.a9-r.| < g by A8,METRIC_1:def 12;
hence thesis by A6,RCOMP_1:1;
end;
N c= Ball(x,g)
proof
let aa be object;
assume
A11: aa in N;
then reconsider a9 = aa as Element of REAL;
|.a9-r.| < g by A6,A11,RCOMP_1:1;
then
A12: real_dist.(a9,r) < g by METRIC_1:def 12;
aa in X by A4,A11;
then reconsider
a99 = aa, r9 = r as Element of Closed-Interval-MSpace(a,b) by A1;
dist(r9,a99) = (the distance of Closed-Interval-MSpace(a,b)).(r9,
a99) by METRIC_1:def 1
.= real_dist.(r9,a99) by METRIC_1:def 13,TOPMETR:def 1;
then dist(r9,a99) < g by A12,METRIC_1:9;
hence thesis by METRIC_1:11;
end;
then N = Ball(x,g) by A7;
hence thesis by A1,A4,A5;
end;
hence thesis by PCOMPS_1:def 4;
end;
Lm6: for a, b, c being Real st a <= b holds c in the carrier of
Closed-Interval-TSpace(a,b) iff a <= c & c <= b
proof
let a, b, c be Real;
assume a <= b;
then
A1: the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by TOPMETR:18;
hereby
assume c in the carrier of Closed-Interval-TSpace(a,b);
then c in {l where l is Real: a <= l & l <= b} by A1,RCOMP_1:def 1;
then ex c1 be Real st c1 = c & a <= c1 & c1 <= b;
hence a <= c & c <= b;
end;
assume a <= c & c <= b;
then c in {l where l is Real : a <= l & l <= b};
hence thesis by A1,RCOMP_1:def 1;
end;
Lm7: for a, b, c, d be Real,
f being Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(c,d), x being Point of Closed-Interval-TSpace(a,b) for g
being PartFunc of REAL, REAL, x1 being Real st a < b & c < d & f
is_continuous_at x & x <> a & x <> b & f.a = c & f.b = d & f is one-to-one & f
= g & x = x1 holds g is_continuous_in x1
proof
let a, b, c, d be Real,
f be Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(c,d), x be Point of Closed-Interval-TSpace(a,b);
let g be PartFunc of REAL, REAL, x1 be Real;
assume that
A1: a < b and
A2: c < d and
A3: f is_continuous_at x and
A4: x <> a and
A5: x <> b and
A6: f.a = c and
A7: f.b = d and
A8: f is one-to-one and
A9: f = g and
A10: x = x1;
A11: dom f = the carrier of Closed-Interval-TSpace(a,b) by FUNCT_2:def 1;
for N1 being Neighbourhood of g.x1 ex N being Neighbourhood of x1 st g
.:N c= N1
proof
reconsider fx = f.x as Point of Closed-Interval-TSpace(c,d);
set Rm = min ( g.x1 - c, d - g.x1 );
let N1 be Neighbourhood of g.x1;
Closed-Interval-TSpace(c,d) = TopSpaceMetr Closed-Interval-MSpace(c,d
) by TOPMETR:def 7;
then
A12: the topology of Closed-Interval-TSpace(c,d) = Family_open_set
Closed-Interval-MSpace(c,d) by TOPMETR:12;
Rm > 0
proof
A13: b in dom f by A1,A11,Lm6;
A14: a in dom f by A1,A11,Lm6;
per cases by XXREAL_0:15;
suppose
A15: Rm = g.x1 - c;
g.x1 in the carrier of Closed-Interval-TSpace(c,d) by A9,A10,FUNCT_2:5;
then
A16: g.x1 >= c by A2,Lm6;
Rm <> 0 by A4,A6,A8,A9,A10,A11,A14,A15,FUNCT_1:def 4;
hence thesis by A15,A16,XREAL_1:48;
end;
suppose
A17: Rm = d - g.x1;
g.x1 in the carrier of Closed-Interval-TSpace(c,d) by A9,A10,FUNCT_2:5;
then
A18: g.x1 <= d by A2,Lm6;
d - g.x1 <> d - d by A5,A7,A8,A9,A10,A11,A13,FUNCT_1:def 4;
hence thesis by A17,A18,XREAL_1:48;
end;
end;
then reconsider
Wuj = ].g.x1 - Rm, g.x1 + Rm.[ as Neighbourhood of g.x1 by RCOMP_1:def 6;
consider Ham be Neighbourhood of g.x1 such that
A19: Ham c= N1 and
A20: Ham c= Wuj by RCOMP_1:17;
A21: Wuj c= ].c,d.[
proof
let aa be object;
assume aa in Wuj;
then aa in {l where l is Real: g.x1 - Rm < l & l < g.x1 + Rm} by
RCOMP_1:def 2;
then consider A be Real such that
A22: A = aa and
A23: g.x1 - Rm < A and
A24: A < g.x1 + Rm;
Rm <= d - g.x1 by XXREAL_0:17;
then g.x1 + Rm <= g.x1 + (d - g.x1) by XREAL_1:6;
then
A25: A < d by A24,XXREAL_0:2;
Rm <= g.x1-c by XXREAL_0:17;
then c + Rm <= g.x1 by XREAL_1:19;
then c <= g.x1 - Rm by XREAL_1:19;
then c < A by A23,XXREAL_0:2;
then A in {l where l is Real: c < l & l < d} by A25;
hence thesis by A22,RCOMP_1:def 2;
end;
].c,d.[ c= [.c,d.] by XXREAL_1:25;
then
A26: Wuj c= [.c,d.] by A21;
then Wuj c= the carrier of Closed-Interval-MSpace(c,d) by A2,TOPMETR:10;
then reconsider N21 = Ham as Subset of Closed-Interval-MSpace(c,d) by A20,
XBOOLE_1:1;
the carrier of Closed-Interval-MSpace(c,d) = the carrier of
TopSpaceMetr(Closed-Interval-MSpace(c,d)) by TOPMETR:12
.= the carrier of Closed-Interval-TSpace(c,d) by TOPMETR:def 7;
then reconsider N19 = N21 as Subset of Closed-Interval-TSpace(c,d);
N21 in Family_open_set Closed-Interval-MSpace(c,d) by Th12;
then N19 is open by A12;
then reconsider G = N19 as a_neighborhood of fx by A9,A10,CONNSP_2:3
,RCOMP_1:16;
consider H being a_neighborhood of x such that
A27: f.:H c= G by A3,TMAP_1:def 2;
consider V being Subset of Closed-Interval-TSpace(a,b) such that
A28: V is open and
A29: V c= H and
A30: x in V by CONNSP_2:6;
A31: the carrier of Closed-Interval-MSpace(a,b) = the carrier of
TopSpaceMetr(Closed-Interval-MSpace(a,b)) by TOPMETR:12
.= the carrier of Closed-Interval-TSpace(a,b) by TOPMETR:def 7;
then reconsider V2 = V as Subset of Closed-Interval-MSpace(a,b);
V c= the carrier of Closed-Interval-MSpace(a,b) by A31;
then V c= [.a,b.] by A1,TOPMETR:10;
then reconsider V1 = V as Subset of REAL by XBOOLE_1:1;
A32: Ham c= [.c,d.] by A20,A26;
A33: not a in V1 & not b in V1
proof
assume
A34: a in V1 or b in V1;
per cases by A34;
suppose
a in V1;
then f.a in f.:H by A11,A29,FUNCT_1:def 6;
hence contradiction by A6,A32,A27,Th11;
end;
suppose
b in V1;
then f.b in f.:H by A11,A29,FUNCT_1:def 6;
hence contradiction by A7,A32,A27,Th11;
end;
end;
Closed-Interval-TSpace(a,b) = TopSpaceMetr Closed-Interval-MSpace(a,b
) by TOPMETR:def 7;
then the topology of Closed-Interval-TSpace(a,b) = Family_open_set
Closed-Interval-MSpace(a,b) by TOPMETR:12;
then V2 in Family_open_set Closed-Interval-MSpace(a,b) by A28;
then V1 is open by A1,A33,Th10;
then consider N being Neighbourhood of x1 such that
A35: N c= V1 by A10,A30,RCOMP_1:18;
N c= H by A29,A35;
then
A36: g.:N c= g.:H by RELAT_1:123;
f.:H c= N1 by A19,A27;
hence thesis by A9,A36,XBOOLE_1:1;
end;
hence thesis by FCONT_1:5;
end;
theorem Th13:
for a, b, c, d, x1 being Real, f being Function of
Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d), x being Point of
Closed-Interval-TSpace(a,b), g being PartFunc of REAL, REAL st a < b & c < d &
f is_continuous_at x & f.a = c & f.b = d & f is one-to-one & f = g & x = x1
holds g| [.a,b.] is_continuous_in x1
proof
let a, b, c, d, x1 be Real;
let f be Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d
), x be Point of Closed-Interval-TSpace(a,b);
let g be PartFunc of REAL, REAL;
assume that
A1: a < b and
A2: c < d and
A3: f is_continuous_at x and
A4: f.a = c and
A5: f.b = d and
A6: f is one-to-one and
A7: f = g and
A8: x = x1;
A9: for c be Element of REAL st c in dom g holds g/.c = g/.c;
dom g = the carrier of Closed-Interval-TSpace(a,b) by A7,FUNCT_2:def 1;
then dom g = [.a,b.] by A1,TOPMETR:18;
then dom g = dom g /\ [.a,b.];
then
A10: g = g| [.a,b.] by A9,PARTFUN2:15;
per cases;
suppose
A11: x1 = a;
for N1 being Neighbourhood of g.x1 ex N being Neighbourhood of x1 st
g.:N c= N1
proof
reconsider f0 = f.a as Point of Closed-Interval-TSpace(c,d) by A2,A4,Lm6;
let N1 be Neighbourhood of g.x1;
reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def 13;
set NN1 = N1 /\ [.c,d.];
N2 in Family_open_set RealSpace by Lm3;
then
A12: N2 in the topology of TopSpaceMetr RealSpace by TOPMETR:12;
NN1 = N1 /\ the carrier of Closed-Interval-TSpace(c,d) by A2,TOPMETR:18;
then reconsider NN = NN1 as Subset of Closed-Interval-TSpace(c,d) by
XBOOLE_1:17;
NN1 = N1 /\ [#] Closed-Interval-TSpace(c,d) by A2,TOPMETR:18;
then NN in the topology of Closed-Interval-TSpace(c,d) by A12,
PRE_TOPC:def 4,TOPMETR:def 6;
then
A13: NN is open;
f.a in the carrier of Closed-Interval-TSpace(c,d) by A2,A4,Lm6;
then g.x1 in N1 & g.x1 in [.c,d.] by A2,A7,A11,RCOMP_1:16,TOPMETR:18;
then g.x1 in NN1 by XBOOLE_0:def 4;
then reconsider N19 = NN as a_neighborhood of f0 by A7,A11,A13,CONNSP_2:3
;
consider H being a_neighborhood of x such that
A14: f.:H c= N19 by A3,A8,A11,TMAP_1:def 2;
consider H1 being Subset of Closed-Interval-TSpace(a,b) such that
A15: H1 is open and
A16: H1 c= H and
A17: x in H1 by CONNSP_2:6;
H1 in the topology of Closed-Interval-TSpace(a,b) by A15;
then consider Q being Subset of R^1 such that
A18: Q in the topology of R^1 and
A19: H1 = Q /\ [#] Closed-Interval-TSpace(a,b) by PRE_TOPC:def 4;
reconsider Q9 = Q as Subset of RealSpace by TOPMETR:12,def 6;
reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def 13;
Q9 in Family_open_set RealSpace by A18,TOPMETR:12,def 6;
then
A20: Q1 is open by Lm4;
x1 in Q1 by A8,A17,A19,XBOOLE_0:def 4;
then consider N being Neighbourhood of x1 such that
A21: N c= Q1 by A20,RCOMP_1:18;
take N;
g.:N c= N1
proof
let aa be object;
assume
A22: aa in g.:N;
then reconsider a9 = aa as Element of REAL;
consider cc be Element of REAL such that
A23: cc in dom g and
A24: cc in N and
A25: a9 = g.cc by A22,PARTFUN2:59;
cc in the carrier of Closed-Interval-TSpace(a,b) by A7,A23,
FUNCT_2:def 1;
then cc in H1 by A19,A21,A24,XBOOLE_0:def 4;
then g.cc in f.:H by A7,A16,FUNCT_2:35;
hence thesis by A14,A25,XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by A10,FCONT_1:5;
end;
suppose
A26: x1 = b;
for N1 being Neighbourhood of g.x1 ex N being Neighbourhood of x1 st
g.:N c= N1
proof
reconsider f0 = f.b as Point of Closed-Interval-TSpace(c,d) by A2,A5,Lm6;
let N1 be Neighbourhood of g.x1;
reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def 13;
set NN1 = N1 /\ [#]Closed-Interval-TSpace(c,d);
reconsider NN = NN1 as Subset of Closed-Interval-TSpace(c,d);
N2 in Family_open_set RealSpace by Lm3;
then N2 in the topology of TopSpaceMetr RealSpace by TOPMETR:12;
then NN in the topology of Closed-Interval-TSpace(c,d) by PRE_TOPC:def 4
,TOPMETR:def 6;
then
A27: NN is open;
g.x1 in N1 & g.x1 in [#] Closed-Interval-TSpace(c,d) by A2,A5,A7,A26,Lm6,
RCOMP_1:16;
then g.x1 in NN1 by XBOOLE_0:def 4;
then reconsider N19 = NN as a_neighborhood of f0 by A7,A26,A27,CONNSP_2:3
;
consider H being a_neighborhood of x such that
A28: f.:H c= N19 by A3,A8,A26,TMAP_1:def 2;
consider H1 being Subset of Closed-Interval-TSpace(a,b) such that
A29: H1 is open and
A30: H1 c= H and
A31: x in H1 by CONNSP_2:6;
H1 in the topology of Closed-Interval-TSpace(a,b) by A29;
then consider Q being Subset of R^1 such that
A32: Q in the topology of R^1 and
A33: H1 = Q /\ [#](Closed-Interval-TSpace(a,b)) by PRE_TOPC:def 4;
reconsider Q9 = Q as Subset of RealSpace by TOPMETR:12,def 6;
reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def 13;
Q9 in Family_open_set RealSpace by A32,TOPMETR:12,def 6;
then
A34: Q1 is open by Lm4;
x1 in Q1 by A8,A31,A33,XBOOLE_0:def 4;
then consider N being Neighbourhood of x1 such that
A35: N c= Q1 by A34,RCOMP_1:18;
take N;
g.:N c= N1
proof
let aa be object;
assume
A36: aa in g.:N;
then reconsider a9 = aa as Element of REAL;
consider cc be Element of REAL such that
A37: cc in dom g and
A38: cc in N and
A39: a9 = g.cc by A36,PARTFUN2:59;
cc in the carrier of Closed-Interval-TSpace(a,b) by A7,A37,
FUNCT_2:def 1;
then cc in H1 by A33,A35,A38,XBOOLE_0:def 4;
then g.cc in f.:H by A7,A30,FUNCT_2:35;
hence thesis by A28,A39,XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by A10,FCONT_1:5;
end;
suppose
x1 <> a & x1 <> b;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A10,Lm7;
end;
end;
theorem Th14:
for a, b, c, d being Real, f being Function of
Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d), g being PartFunc of
REAL, REAL st f is continuous one-to-one & a < b & c < d & f = g & f.a = c & f.
b = d holds g| [.a,b.] is continuous
proof
let a, b, c, d be Real;
let f be Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d
);
let g be PartFunc of REAL, REAL;
assume that
A1: f is continuous one-to-one and
A2: a < b and
A3: c < d & f = g & f.a = c & f.b = d;
for x0 being Real st x0 in dom(g| [.a,b.]) holds g| [.a,b.]
is_continuous_in x0
proof
let x0 be Real;
assume x0 in dom(g| [.a,b.]);
then x0 in [.a,b.] by RELAT_1:57;
then reconsider x1=x0 as Point of Closed-Interval-TSpace(a,b) by A2,
TOPMETR:18;
f is_continuous_at x1 & x0 is Real by A1,TMAP_1:44;
hence thesis by A1,A2,A3,Th13;
end;
hence thesis by FCONT_1:def 2;
end;
begin
:: On the monotonicity of continuous maps
theorem Th15:
for a, b, c, d being Real for f being Function of
Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d) st a < b & c < d & f
is continuous one-to-one & f.a = c & f.b = d holds for x, y be Point of
Closed-Interval-TSpace(a,b),
p, q, fx, fy being Real st x = p & y = q & p < q &
fx = f.x & fy = f.y holds fx < fy
proof
let a, b, c, d be Real;
let f be Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d
);
assume that
A1: a < b and
A2: c < d and
A3: f is continuous one-to-one and
A4: f.a = c & f.b = d;
A5: [.a,b.] = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:18;
A6: dom f = the carrier of Closed-Interval-TSpace(a,b) by FUNCT_2:def 1;
rng f c= REAL by MEMBERED:3;
then reconsider g = f as PartFunc of [.a,b.], REAL by A5,A6,RELSET_1:4;
reconsider g as PartFunc of REAL, REAL by A5,A6,RELSET_1:5;
A7: g| [.a,b.] is continuous by A1,A2,A3,A4,Th14;
A8: [.a,b.] /\ dom f = [.a,b.] /\ the carrier of Closed-Interval-TSpace(a,b)
by FUNCT_2:def 1
.= [.a,b.] by A5;
per cases by A1,A3,A8,A7,FCONT_2:17,XBOOLE_1:18;
suppose
A9: g| [.a,b.] is increasing;
for x, y be Point of Closed-Interval-TSpace(a,b), p, q, fx, fy be
Real st x = p & y = q & p < q & fx = f.x & fy = f.y holds fx < fy
proof
let x, y be Point of Closed-Interval-TSpace(a,b),
p, q, fx, fy be Real;
assume that
A10: x = p and
A11: y = q and
A12: p < q & fx = f.x & fy = f.y;
y in the carrier of Closed-Interval-TSpace(a,b);
then
A13: q in [.a,b.] /\ dom g by A1,A8,A11,TOPMETR:18;
x in the carrier of Closed-Interval-TSpace(a,b);
then p in [.a,b.] /\ dom g by A1,A8,A10,TOPMETR:18;
hence thesis by A9,A10,A11,A12,A13,RFUNCT_2:20;
end;
hence thesis;
end;
suppose
A14: g| [.a,b.] is decreasing;
a in [.a,b.] /\ dom g & b in [.a,b.] /\ dom g by A1,A5,A8,Lm6;
hence thesis by A1,A2,A4,A14,RFUNCT_2:21;
end;
end;
theorem
for f being continuous one-to-one Function of I[01], I[01] st f.0 = 0
& f.1 = 1 holds for x, y being Point of I[01],
p, q, fx, fy being Real st x = p
& y = q & p < q & fx = f.x & fy = f.y holds fx < fy by Th15,TOPMETR:20;
theorem
for a, b, c, d being Real, f being Function of Closed-Interval-TSpace(
a,b), Closed-Interval-TSpace(c,d), P being non empty Subset of
Closed-Interval-TSpace(a,b), PP, QQ being Subset of R^1 st a < b & c < d & PP =
P & f is continuous one-to-one & PP is compact & f.a = c & f.b = d & f.:P = QQ
holds f.(lower_bound [#]PP) = lower_bound [#]QQ
proof
let a, b, c, d be Real;
let f be Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d
), P be non empty Subset of Closed-Interval-TSpace(a,b), PP, QQ be Subset of
R^1;
assume that
A1: a < b & c < d and
A2: PP = P and
A3: f is continuous and
A4: f is one-to-one and
A5: PP is compact and
A6: f.a = c & f.b = d and
A7: f.:P = QQ;
A8: [#] Closed-Interval-TSpace(c,d) = the carrier of Closed-Interval-TSpace(
c,d);
set IT = f.(lower_bound [#]PP);
A9: [#]PP is real-bounded by A5,WEIERSTR:11;
[#]PP <> {} by A2,WEIERSTR:def 1;
then
A10: lower_bound [#]PP in [#]PP by A5,A9,RCOMP_1:13,WEIERSTR:12;
then
A11: lower_bound [#]PP in P by A2,WEIERSTR:def 1;
P c= the carrier of Closed-Interval-TSpace(a,b);
then
A12: [#]PP c= the carrier of Closed-Interval-TSpace(a,b) by A2,WEIERSTR:def 1;
reconsider IT as Real;
A13: for r be Real st r in [#]QQ holds IT<=r
proof
let r be Real;
assume r in [#]QQ;
then r in f.:P by A7,WEIERSTR:def 1;
then r in f.:[#]PP by A2,WEIERSTR:def 1;
then consider x be object such that
A14: x in dom f and
A15: x in [#]PP and
A16: r = f.x by FUNCT_1:def 6;
reconsider x1 = x, x2 = lower_bound [#]PP as Point of
Closed-Interval-TSpace(a,b) by A11,A14;
x1 in the carrier of Closed-Interval-TSpace(a,b);
then reconsider r1 = x, r2 = x2 as Real;
A17: r2 <= r1 by A9,A15,SEQ_4:def 2;
reconsider fr = f.x2, fx = f.x1 as Real;
per cases;
suppose
r2 <> r1;
then r2 < r1 by A17,XXREAL_0:1;
then fr < fx by A1,A3,A4,A6,Th15;
hence thesis by A16;
end;
suppose
r2 = r1;
hence thesis by A16;
end;
end;
[#]Closed-Interval-TSpace(a,b) = the carrier of Closed-Interval-TSpace( a,b);
then P is compact by A2,A5,COMPTS_1:2;
then
for P1 being Subset of Closed-Interval-TSpace(c,d) st P1=QQ holds P1 is
compact by A3,A7,WEIERSTR:8;
then QQ is compact by A7,A8,COMPTS_1:2;
then
A18: [#]QQ is real-bounded by WEIERSTR:11;
lower_bound [#]PP in the carrier of Closed-Interval-TSpace(a,b) by A12,A10;
then lower_bound [#]PP in dom f by FUNCT_2:def 1;
then IT in QQ by A7,A11,FUNCT_1:def 6;
then
A19: IT in [#]QQ by WEIERSTR:def 1;
for s be Real st 0<s ex r be Real st r in [#]QQ & r<IT+s
proof
given s be Real such that
A20: 0<s and
A21: not ex r be Real st r in [#]QQ & r<IT+s;
IT + 0 < IT + s by A20,XREAL_1:8;
hence thesis by A19,A21;
end;
hence thesis by A18,A19,A13,SEQ_4:def 2;
end;
theorem
for a, b, c, d being Real, f being Function of Closed-Interval-TSpace(
a,b), Closed-Interval-TSpace(c,d), P, Q being non empty Subset of
Closed-Interval-TSpace(a,b), PP, QQ being Subset of R^1 st a < b & c < d & PP =
P & QQ = Q & f is continuous one-to-one & PP is compact & f.a = c & f.b = d & f
.:P = Q holds f.(upper_bound [#]PP) = upper_bound [#]QQ
proof
let a, b, c, d be Real;
let f be Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d
), P, Q be non empty Subset of Closed-Interval-TSpace(a,b), PP, QQ be Subset of
R^1;
assume that
A1: a < b & c < d and
A2: PP = P and
A3: QQ = Q and
A4: f is continuous one-to-one and
A5: PP is compact and
A6: f.a = c & f.b = d and
A7: f.:P = Q;
A8: [#] Closed-Interval-TSpace(c,d) = the carrier of Closed-Interval-TSpace(
c,d);
set IT = f.(upper_bound [#]PP);
A9: [#]PP is real-bounded by A5,WEIERSTR:11;
[#]PP <> {} by A2,WEIERSTR:def 1;
then
A10: upper_bound [#]PP in [#]PP by A5,A9,RCOMP_1:12,WEIERSTR:12;
then
A11: upper_bound [#]PP in P by A2,WEIERSTR:def 1;
P c= the carrier of Closed-Interval-TSpace(a,b);
then
A12: [#]PP c= the carrier of Closed-Interval-TSpace(a,b) by A2,WEIERSTR:def 1;
reconsider IT as Real;
A13: for r be Real st r in [#]QQ holds IT>=r
proof
let r be Real;
assume r in [#]QQ;
then r in f.:P by A3,A7,WEIERSTR:def 1;
then r in f.:[#]PP by A2,WEIERSTR:def 1;
then consider x be object such that
A14: x in dom f and
A15: x in [#]PP and
A16: r = f.x by FUNCT_1:def 6;
reconsider x1 = x, x2 = upper_bound [#]PP as Point of
Closed-Interval-TSpace(a,b) by A11,A14;
x1 in the carrier of Closed-Interval-TSpace(a,b);
then reconsider r1 = x, r2 = x2 as Real;
A17: r2 >= r1 by A9,A15,SEQ_4:def 1;
reconsider fr = f.x2, fx = f.x1 as Real;
per cases;
suppose
r2 <> r1;
then r2 > r1 by A17,XXREAL_0:1;
then fr > fx by A1,A4,A6,Th15;
hence thesis by A16;
end;
suppose
r2 = r1;
hence thesis by A16;
end;
end;
[#]Closed-Interval-TSpace(a,b) = the carrier of Closed-Interval-TSpace( a,b);
then P is compact by A2,A5,COMPTS_1:2;
then
for P1 being Subset of Closed-Interval-TSpace(c,d) st P1=QQ holds P1 is
compact by A3,A4,A7,WEIERSTR:8;
then QQ is compact by A3,A7,A8,COMPTS_1:2;
then
A18: [#]QQ is real-bounded by WEIERSTR:11;
upper_bound [#]PP in the carrier of Closed-Interval-TSpace(a,b) by A12,A10;
then upper_bound [#]PP in dom f by FUNCT_2:def 1;
then IT in QQ by A3,A7,A11,FUNCT_1:def 6;
then
A19: IT in [#]QQ by WEIERSTR:def 1;
for s be Real st 0 < s ex r be Real st r in [#]QQ & r > IT-s
proof
given s be Real such that
A20: 0<s and
A21: not ex r be Real st r in [#]QQ & r>IT-s;
IT-s<IT-0 by A20,XREAL_1:15;
hence thesis by A19,A21;
end;
hence thesis by A18,A19,A13,SEQ_4:def 1;
end;
theorem
for a, b being Real st a <= b holds lower_bound [.a,b.] = a &
upper_bound [.a,b.] = b
proof
let a, b be Real;
assume
A1: a <= b;
set X = [.a,b.];
A2: a in { l where l is Real : a <= l & l <= b } by A1;
A3: for s be Real st 0 < s ex r being Real st r in X & r < a+ s
proof
let s be Real;
assume
A4: 0 < s;
A5: a in X by A2,RCOMP_1:def 1;
assume for r being Real st r in X holds r >= a+s;
hence thesis by A4,A5,XREAL_1:29;
end;
A6: b in { l1 where l1 is Real: a <= l1 & l1 <= b } by A1;
A7: for s be Real st 0 < s ex r being Real st r in X & b-s<r
proof
let s be Real;
assume
A8: 0 < s;
A9: b in X by A6,RCOMP_1:def 1;
assume for r being Real st r in X holds r <= b-s;
hence thesis by A8,A9,XREAL_1:44;
end;
A10: for r being Real st r in X holds a <= r
proof
let r be Real;
assume r in X;
then r in { l where l is Real: a <= l & l <= b } by RCOMP_1:def 1;
then ex r1 being Real st r1 = r & a <= r1 & r1 <= b;
hence thesis;
end;
b is UpperBound of X
proof
let r be ExtReal;
assume r in X;
then r in { l where l is Real: a <= l & l <= b } by RCOMP_1:def 1;
then ex r1 being Real st r1 = r & a <= r1 & r1 <= b;
hence thesis;
end;
then
A11: X is bounded_above;
a is LowerBound of X
proof
let r be ExtReal;
assume r in X;
then r in { l where l is Real: a <= l & l <= b } by RCOMP_1:def 1;
then ex r1 being Real st r1 = r & a <= r1 & r1 <= b;
hence thesis;
end;
then
A12: X is bounded_below;
A13: for r being Real st r in X holds b >= r
proof
let r be Real;
assume r in X;
then r in { l where l is Real: a <= l & l <= b } by RCOMP_1:def 1;
then ex r1 being Real st r1 = r & a <= r1 & r1 <= b;
hence thesis;
end;
a in X by A2,RCOMP_1:def 1;
hence thesis by A12,A11,A10,A3,A13,A7,SEQ_4:def 1,def 2;
end;
theorem
for a, b, c, d, e, f, g, h being Real
for F being Function of
Closed-Interval-TSpace (a,b), Closed-Interval-TSpace (c,d) st a < b & c < d & e
< f & a <= e & f <= b & F is being_homeomorphism & F.a = c & F.b = d & g = F.e
& h = F.f holds F.:[.e, f.] = [.g, h.]
proof
let a, b, c, d, e, f, g, h be Real;
let F be Function of Closed-Interval-TSpace (a,b), Closed-Interval-TSpace (c
,d);
assume that
A1: a < b and
A2: c < d and
A3: e < f and
A4: a <= e and
A5: f <= b and
A6: F is being_homeomorphism and
A7: F.a = c & F.b = d and
A8: g = F.e and
A9: h = F.f;
a <= f by A3,A4,XXREAL_0:2;
then f in { l1 where l1 is Real: a <= l1 & l1 <= b } by A5;
then
A10: f in [.a,b.] by RCOMP_1:def 1;
then f in the carrier of Closed-Interval-TSpace (a,b) by A1,TOPMETR:18;
then h in the carrier of Closed-Interval-TSpace (c,d) by A9,FUNCT_2:5;
then
A11: h in [.c,d.] by A2,TOPMETR:18;
e <= b by A3,A5,XXREAL_0:2;
then e in { l1 where l1 is Real: a <= l1 & l1 <= b } by A4;
then
A12: e in [.a,b.] by RCOMP_1:def 1;
then e in the carrier of Closed-Interval-TSpace (a,b) by A1,TOPMETR:18;
then g in the carrier of Closed-Interval-TSpace (c,d) by A8,FUNCT_2:5;
then g in [.c,d.] by A2,TOPMETR:18;
then [.g,h.] c= [.c,d.] by A11,XXREAL_2:def 12;
then
A13: [.g,h.] c= the carrier of Closed-Interval-TSpace (c,d) by A2,TOPMETR:18;
A14: F is continuous one-to-one by A6,TOPS_2:def 5;
A15: [.g, h.] c= F.:[.e, f.]
proof
let aa be object;
A16: F is one-to-one by A6,TOPS_2:def 5;
assume aa in [.g,h.];
then aa in { l1 where l1 is Real: g <= l1 & l1 <= h }
by RCOMP_1:def 1;
then consider l be Real such that
A17: aa = l and
A18: g <= l and
A19: l <= h;
A20: rng F = [#]Closed-Interval-TSpace (c,d) by A6,TOPS_2:def 5;
l in { l1 where l1 is Real: g <= l1 & l1 <= h } by A18,A19;
then
A21: l in [.g,h.] by RCOMP_1:def 1;
reconsider x = F".l as Real;
F is onto by A20,FUNCT_2:def 3;
then
A22: x = (F qua Function)".l by A16,TOPS_2:def 4;
then
A23: x in dom F by A13,A16,A20,A21,FUNCT_1:32;
dom F = [#]Closed-Interval-TSpace (a,b) by A6,TOPS_2:def 5;
then reconsider
e9 = e, f9 = f, x9 = x as Point of Closed-Interval-TSpace (a,b)
by A1,A12,A10,A13,A16,A20,A21,A22,FUNCT_1:32,TOPMETR:18;
reconsider g9 = F.e9, h9 = F.f9, l9 = F.x9 as Point of
Closed-Interval-TSpace (c,d);
reconsider gg = g9, hh = h9, ll = l9 as Real;
A24: x <= f
proof
assume x > f;
then ll > hh by A1,A2,A7,A14,Th15;
hence thesis by A9,A13,A19,A16,A20,A21,A22,FUNCT_1:32;
end;
e <= x
proof
assume e > x;
then gg > ll by A1,A2,A7,A14,Th15;
hence thesis by A8,A13,A18,A16,A20,A21,A22,FUNCT_1:32;
end;
then x in { l1 where l1 is Real: e <= l1 & l1 <= f } by A24;
then
A25: x in [.e, f.] by RCOMP_1:def 1;
aa = F.x by A13,A17,A16,A20,A21,A22,FUNCT_1:32;
hence thesis by A23,A25,FUNCT_1:def 6;
end;
F.:[.e, f.] c= [.g, h.]
proof
let aa be object;
assume aa in F.:[.e, f.];
then consider x be object such that
A26: x in dom F and
A27: x in [.e, f.] and
A28: aa = F.x by FUNCT_1:def 6;
x in { l where l is Real: e <= l & l <= f } by A27,RCOMP_1:def 1;
then consider x9 be Real such that
A29: x9 = x and
A30: e <= x9 and
A31: x9 <= f;
reconsider Fx = F.x9 as Real;
reconsider e1 = e, f1 = f, x1 = x9 as Point of Closed-Interval-TSpace (a,
b) by A1,A12,A10,A26,A29,TOPMETR:18;
reconsider gg = F.e1, hh = F.f1, FFx = F.x1 as Real;
A32: Fx <= h
proof
per cases;
suppose
f = x;
hence thesis by A9,A29;
end;
suppose
f <> x;
then f > x9 by A29,A31,XXREAL_0:1;
then hh > FFx by A1,A2,A7,A14,Th15;
hence thesis by A9;
end;
end;
g <= Fx
proof
per cases;
suppose
e = x;
hence thesis by A8,A29;
end;
suppose
e <> x;
then e < x9 by A29,A30,XXREAL_0:1;
then gg < FFx by A1,A2,A7,A14,Th15;
hence thesis by A8;
end;
end;
then Fx in { l1 where l1 is Real: g <= l1 & l1 <= h } by A32;
hence thesis by A28,A29,RCOMP_1:def 1;
end;
hence thesis by A15;
end;
theorem
for P, Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2
st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX being Point
of TOP-REAL 2 st ( EX in P /\ Q &
ex g being Function of I[01], (TOP-REAL 2)|P, s2 being Real
st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = EX & 0
<= s2 & s2 <= 1 &
for t being Real st 0 <= t & t < s2 holds not g.t in Q )
proof
let P, Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume that
A1: P meets Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1,p2;
P /\ Q <> {} by A1;
then reconsider P as non empty Subset of TOP-REAL 2;
consider f being Function of I[01], (TOP-REAL 2)|P such that
A4: f is being_homeomorphism and
A5: f.0 = p1 & f.1 = p2 by A3,TOPREAL1:def 1;
A6: f is one-to-one by A4,TOPS_2:def 5;
[#]((TOP-REAL 2)|P) = P by PRE_TOPC:def 5;
then reconsider PQ = P /\ Q as non empty Subset of (TOP-REAL 2)|P by A1,
XBOOLE_1:17;
reconsider P1 = P, Q1=Q as non empty Subset of TOP-REAL 2 by A1;
consider OO be object such that
A7: OO in PQ by XBOOLE_0:def 1;
reconsider PP = P as Subset of TOP-REAL 2;
PP is compact by A3,Th1;
then
A8: P /\ Q is compact by A2,COMPTS_1:9,XBOOLE_1:17;
PQ <> {}((TOP-REAL 2)|P);
then reconsider PQ1 = P /\ Q as non empty Subset of (TOP-REAL 2)|P1;
(TOP-REAL 2)|(P1 /\ Q1) = (TOP-REAL 2)|P1|PQ1 by GOBOARD9:2;
then
A9: PQ is compact by A8,COMPTS_1:3;
set g = f";
reconsider g1 = g as Function;
A10: rng f = [#]((TOP-REAL 2)|P) by A4,TOPS_2:def 5;
[#](I[01]) c= [#](R^1) by PRE_TOPC:def 4;
then reconsider GPQ = g.:PQ as Subset of R^1 by XBOOLE_1:1;
g is continuous by A4,TOPS_2:def 5;
then g.:PQ c= [#] (I[01]) & for P being Subset of I[01] st P=GPQ holds P is
compact by A9,WEIERSTR:8;
then
A11: GPQ is compact by COMPTS_1:2;
then
A12: [#](GPQ) is real-bounded by WEIERSTR:11;
set Ex = lower_bound ([#](GPQ));
reconsider f1 = f as Function;
take f.Ex;
A13: dom g = the carrier of (TOP-REAL 2)|P by FUNCT_2:def 1;
dom g = the carrier of (TOP-REAL 2)|P by FUNCT_2:def 1;
then g.OO in GPQ by A7,FUNCT_1:def 6;
then [#](GPQ)<>{} by WEIERSTR:def 1;
then Ex in [#](GPQ) by A11,A12,RCOMP_1:13,WEIERSTR:12;
then
A14: Ex in GPQ by WEIERSTR:def 1;
then
A15: Ex<=1 by BORSUK_1:43;
A16: dom f = the carrier of I[01] by FUNCT_2:def 1;
A17: for t being Real st 0<=t & t<Ex holds not f.t in Q
proof
let t be Real;
assume that
A18: 0<=t and
A19: t<Ex;
A20: t <= 1 by A15,A19,XXREAL_0:2;
then t in the carrier of I[01] by A18,BORSUK_1:43;
then f.t in the carrier of ((TOP-REAL 2)|P) by FUNCT_2:5;
then
A21: f.t in P by PRE_TOPC:8;
f is onto by A10,FUNCT_2:def 3;
then
A22: g = f1" by A6,TOPS_2:def 4;
assume f.t in Q;
then f.t in PQ by A21,XBOOLE_0:def 4;
then
A23: g.(f.t) in GPQ by A13,FUNCT_1:def 6;
t in dom f by A16,A18,A20,BORSUK_1:43;
then g.(f.t) = t by A6,A22,FUNCT_1:34;
then t in [#]GPQ by A23,WEIERSTR:def 1;
hence thesis by A12,A19,SEQ_4:def 2;
end;
A24: f" is one-to-one by A10,A6,TOPS_2:50;
g is being_homeomorphism by A4,TOPS_2:56;
then rng g = [#]I[01] by TOPS_2:def 5;
then g is onto by FUNCT_2:def 3;
then (f")" = g1" by A24,TOPS_2:def 4;
then
A25: f = g1" by A10,A6,TOPS_2:51;
A26: (ex pq be object st pq in dom g & pq in PQ & Ex = g.pq )& 0<=Ex by A14,
BORSUK_1:43,FUNCT_1:def 6;
g is one-to-one by A10,A6,TOPS_2:50;
hence thesis by A4,A5,A25,A26,A15,A17,FUNCT_1:34;
end;
theorem
for P, Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2
st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX be Point of
TOP-REAL 2 st ( EX in P /\ Q &
ex g being Function of I[01], (TOP-REAL 2)|P, s2 being Real
st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = EX & 0 <=
s2 & s2 <= 1 &
for t being Real st 1 >= t & t > s2 holds not g.t in Q )
proof
let P, Q be Subset of TOP-REAL 2, p1,p2 be Point of TOP-REAL 2;
assume that
A1: P meets Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1,p2;
P /\ Q <> {} by A1;
then reconsider P as non empty Subset of TOP-REAL 2;
consider f being Function of I[01], (TOP-REAL 2)|P such that
A4: f is being_homeomorphism and
A5: f.0 = p1 & f.1 = p2 by A3,TOPREAL1:def 1;
A6: f is one-to-one by A4,TOPS_2:def 5;
[#]((TOP-REAL 2)|P) = P by PRE_TOPC:def 5;
then reconsider PQ = P /\ Q as non empty Subset of (TOP-REAL 2)|P by A1,
XBOOLE_1:17;
reconsider P1 = P, Q1=Q as non empty Subset of TOP-REAL 2 by A1;
consider OO be object such that
A7: OO in PQ by XBOOLE_0:def 1;
reconsider PP = P as Subset of TOP-REAL 2;
PP is compact by A3,Th1;
then
A8: P /\ Q is compact by A2,COMPTS_1:9,XBOOLE_1:17;
PQ <> {}((TOP-REAL 2)|P);
then reconsider PQ1 = P /\ Q as non empty Subset of (TOP-REAL 2)|P1;
(TOP-REAL 2)|(P1 /\ Q1) = (TOP-REAL 2)|P1|PQ1 by GOBOARD9:2;
then
A9: PQ is compact by A8,COMPTS_1:3;
set g = f";
reconsider g1 = g as Function;
A10: rng f = [#]((TOP-REAL 2)|P) by A4,TOPS_2:def 5;
A11: f" is one-to-one by A10,A6,TOPS_2:50;
g is being_homeomorphism by A4,TOPS_2:56;
then rng g = [#]I[01] by TOPS_2:def 5;
then g is onto by FUNCT_2:def 3;
then (f")" = g1" by A11,TOPS_2:def 4;
then
A12: f = g1" by A10,A6,TOPS_2:51;
[#](I[01]) c= [#](R^1) by PRE_TOPC:def 4;
then reconsider GPQ = g.:PQ as Subset of R^1 by XBOOLE_1:1;
g is continuous by A4,TOPS_2:def 5;
then g.:PQ c= [#] (I[01]) & for P being Subset of I[01] st P=GPQ holds P is
compact by A9,WEIERSTR:8;
then
A13: GPQ is compact by COMPTS_1:2;
then
A14: [#](GPQ) is real-bounded by WEIERSTR:11;
set Ex = upper_bound ([#](GPQ));
reconsider f1 = f as Function;
take f.Ex;
A15: dom g = the carrier of (TOP-REAL 2)|P by FUNCT_2:def 1;
dom g = the carrier of (TOP-REAL 2)|P by FUNCT_2:def 1;
then g.OO in GPQ by A7,FUNCT_1:def 6;
then [#](GPQ)<>{} by WEIERSTR:def 1;
then Ex in [#](GPQ) by A13,A14,RCOMP_1:12,WEIERSTR:12;
then
A16: Ex in GPQ by WEIERSTR:def 1;
then
A17: 0<=Ex by BORSUK_1:43;
A18: dom f = the carrier of I[01] by FUNCT_2:def 1;
A19: for t being Real st 1>=t & t>Ex holds not f.t in Q
proof
let t be Real;
assume that
A20: 1 >= t and
A21: t > Ex;
t in the carrier of I[01] by A17,A20,A21,BORSUK_1:43;
then f.t in the carrier of ((TOP-REAL 2)|P) by FUNCT_2:5;
then
A22: f.t in P by PRE_TOPC:8;
f is onto by A10,FUNCT_2:def 3;
then
A23: g = f1" by A6,TOPS_2:def 4;
assume f.t in Q;
then f.t in PQ by A22,XBOOLE_0:def 4;
then
A24: g.(f.t) in GPQ by A15,FUNCT_1:def 6;
t in dom f by A18,A17,A20,A21,BORSUK_1:43;
then g.(f.t) = t by A6,A23,FUNCT_1:34;
then t in [#](GPQ) by A24,WEIERSTR:def 1;
hence thesis by A14,A21,SEQ_4:def 1;
end;
A25: (ex pq be object st pq in dom g & pq in PQ & Ex = g.pq )& Ex<=1 by A16,
BORSUK_1:43,FUNCT_1:def 6;
g is one-to-one by A10,A6,TOPS_2:50;
hence thesis by A4,A5,A12,A17,A25,A19,FUNCT_1:34;
end;
:: from TOPREAL6, 2011.07.29, A.T.
registration
cluster non empty finite real-bounded for Subset of REAL;
existence
proof
reconsider a = {0} as finite Subset of REAL;
take a;
thus thesis;
end;
end;
Lm8: R^1 = TopStruct (#the carrier of RealSpace,Family_open_set RealSpace#) by
PCOMPS_1:def 5,TOPMETR:def 6;
theorem Th23:
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is closed iff B is closed
proof
let A be Subset of REAL, B be Subset of R^1 such that
A1: A = B;
thus A is closed implies B is closed
proof
assume A is closed;
then A`` is closed;
then A` is open by RCOMP_1:def 5;
then A` in the topology of R^1 by Lm8,Th5;
hence [#]R^1 \ B is open by A1,TOPMETR:17;
end;
assume B is closed;
then B` in the topology of R^1 by PRE_TOPC:def 2;
then A` is open by A1,Lm8,Th5,TOPMETR:17;
then A`` is closed by RCOMP_1:def 5;
hence thesis;
end;
theorem
for A being Subset of REAL, B being Subset of R^1 st A = B holds Cl A = Cl B
proof
let A be Subset of REAL, B be Subset of R^1 such that
A1: A = B;
thus Cl A c= Cl B
proof
let a be object;
assume
A2: a in Cl A;
for G being Subset of R^1 st G is open & a in G holds B meets G
proof
let G be Subset of R^1 such that
A3: G is open and
A4: a in G;
reconsider H = G as Subset of REAL by TOPMETR:17;
G in Family_open_set RealSpace by A3,Lm8;
then H is open by Th5;
then A /\ H is non empty by A2,A4,MEASURE6:63;
hence thesis by A1;
end;
hence thesis by A2,PRE_TOPC:def 7,TOPMETR:17;
end;
let a be object;
assume
A5: a in Cl B;
for O being open Subset of REAL st a in O holds O /\ A is non empty
proof
let O be open Subset of REAL such that
A6: a in O;
reconsider P = O as Subset of R^1 by TOPMETR:17;
P in Family_open_set RealSpace by Th5;
then P is open by Lm8;
then P meets B by A5,A6,PRE_TOPC:def 7;
hence thesis by A1;
end;
hence thesis by A5,MEASURE6:63;
end;
registration
let a, b be Real;
cluster [.a,b.] -> compact for Subset of REAL;
coherence by RCOMP_1:6;
end;
theorem Th25:
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is compact iff B is compact
proof
let A be Subset of REAL, B be Subset of R^1 such that
A1: A = B;
thus A is compact implies B is compact
proof
assume
A2: A is compact;
per cases;
suppose
A = {};
then reconsider C = B as empty Subset of R^1 by A1;
C is compact;
hence thesis;
end;
suppose A <> {};
then reconsider A as non empty real-bounded Subset of REAL
by A2,RCOMP_1:10;
reconsider i = inf A, s = sup A as Real;
reconsider X = [.i,s.] as Subset of R^1 by TOPMETR:17;
A3: i <= s by XXREAL_2:40;
then
A4: Closed-Interval-TSpace(i,s) = R^1|X by TOPMETR:19;
A5: B is closed by A1,A2,Th23;
A6: X <> {} by A3,XXREAL_1:30;
A7: B c= X by A1,XXREAL_2:69;
Closed-Interval-TSpace(i,s) is compact by A3,HEINE:4;
then X is compact by A6,A4,COMPTS_1:3;
hence thesis by A5,A7,COMPTS_1:9;
end;
end;
assume B is compact;
then [#]B is compact by WEIERSTR:13;
hence thesis by A1,WEIERSTR:def 1;
end;
registration
cluster finite -> compact for Subset of REAL;
coherence by Th25,TOPMETR:17;
end;
theorem
for a, b being Real holds a <> b iff Cl ].a,b.[ = [.a,b.]
proof
let a, b be Real;
thus a <> b implies Cl ].a,b.[ = [.a,b.]
proof
assume
A1: a <> b;
per cases by A1,XXREAL_0:1;
suppose
A2: a > b;
hence Cl ].a,b.[ = {} by MEASURE6:60,XXREAL_1:28
.= [.a,b.] by A2,XXREAL_1:29;
end;
suppose
A3: a < b;
then
A4: (a+b)/2 < b by XREAL_1:226;
thus Cl ].a,b.[ c= [.a,b.] by MEASURE6:57,XXREAL_1:25;
let p be object;
A5: ].a,b.[ = {w where w is Real: a < w & w < b } by RCOMP_1:def 2;
assume
A6: p in [.a,b.];
[.a,b.] = {w where w is Real: a <= w & w <= b } by RCOMP_1:def 1;
then consider r being Real such that
A7: p = r and
A8: a <= r and
A9: r <= b by A6;
a < (a+b)/2 by A3,XREAL_1:226;
then
A10: (a+b)/2 in ].a,b.[ by A5,A4;
now
per cases by A8,A9,XXREAL_0:1;
case
A11: a < r & r < b;
A12: ].a,b.[ c= Cl ].a,b.[ by MEASURE6:58;
r in ].a,b.[ by A5,A11;
hence thesis by A7,A12;
end;
case
A13: a = r;
for O being open Subset of REAL st a in O holds O /\ ].a,b.[ is
non empty
proof
let O be open Subset of REAL;
assume a in O;
then consider g being Real such that
A14: 0 < g and
A15: ].a-g,a+g.[ c= O by RCOMP_1:19;
A16: a-g < a-0 by A14,XREAL_1:15;
A17: ]. a-g,a+g.[ = {w where w is Real: a-g < w & w < a+g } by
RCOMP_1:def 2;
per cases;
suppose
A18: a+g < b;
A19: a+0 < a+g by A14,XREAL_1:6;
then
A20: a < (a+(a+g))/2 by XREAL_1:226;
A21: (a+(a+g))/2 < a+g by A19,XREAL_1:226;
then (a+(a+g))/2 < b by A18,XXREAL_0:2;
then
A22: (a+(a+g))/2 in ].a,b.[ by A5,A20;
a-g < (a+(a+g))/2 by A16,A20,XXREAL_0:2;
then (a+(a+g))/2 in ].a-g,a+g.[ by A17,A21;
hence thesis by A15,A22,XBOOLE_0:def 4;
end;
suppose
A23: a+g >= b;
(a+b)/2 < b by A3,XREAL_1:226;
then
A24: (a+b)/2 < a+g by A23,XXREAL_0:2;
a < (a+b)/2 by A3,XREAL_1:226;
then a-g < (a+b)/2 by A16,XXREAL_0:2;
then (a+b)/2 in ].a-g,a+g.[ by A17,A24;
hence thesis by A10,A15,XBOOLE_0:def 4;
end;
end;
hence thesis by A7,A13,MEASURE6:63;
end;
case
A25: b = r;
for O being open Subset of REAL st b in O holds O /\ ].a,b.[ is
non empty
proof
let O be open Subset of REAL;
assume b in O;
then consider g being Real such that
A26: 0 < g and
A27: ].b-g,b+g.[ c= O by RCOMP_1:19;
A28: b-g < b-0 by A26,XREAL_1:15;
A29: b+0 < b+g by A26,XREAL_1:6;
A30: ]. b-g,b+g.[ = {w where w is Real: b-g < w & w < b+g } by
RCOMP_1:def 2;
per cases;
suppose
A31: b-g > a;
A32: (b+(b-g))/2 < b by A28,XREAL_1:226;
A33: b-g < (b+(b-g))/2 by A28,XREAL_1:226;
then a < (b+(b-g))/2 by A31,XXREAL_0:2;
then
A34: (b+(b-g))/2 in ].a,b.[ by A5,A32;
(b+(b-g))/2 < b by A28,XREAL_1:226;
then (b+(b-g))/2 < b+g by A29,XXREAL_0:2;
then (b+(b-g))/2 in ].b-g,b+g.[ by A30,A33;
hence thesis by A27,A34,XBOOLE_0:def 4;
end;
suppose
A35: b-g <= a;
(a+b)/2 < b by A3,XREAL_1:226;
then
A36: (a+b)/2 < b+g by A29,XXREAL_0:2;
a < (a+b)/2 by A3,XREAL_1:226;
then b-g < (a+b)/2 by A35,XXREAL_0:2;
then (a+b)/2 in ].b-g,b+g.[ by A30,A36;
hence thesis by A10,A27,XBOOLE_0:def 4;
end;
end;
hence thesis by A7,A25,MEASURE6:63;
end;
end;
hence thesis;
end;
end;
assume that
A37: Cl ].a,b.[ = [.a,b.] and
A38: a = b;
[.a,b.] = {a} by A38,XXREAL_1:17;
hence contradiction by A37,A38,MEASURE6:60,XXREAL_1:28;
end;
theorem
for T being TopStruct, f being RealMap of T, g being Function of
T, R^1 st f = g holds f is continuous iff g is continuous
proof
let T be TopStruct, f be RealMap of T, g be Function of T, R^1 such that
A1: f = g;
thus f is continuous implies g is continuous
proof
assume
A2: for Y being Subset of REAL st Y is closed holds f"Y is closed;
let P be Subset of R^1 such that
A3: P is closed;
reconsider R = P as Subset of REAL by TOPMETR:17;
R is closed by A3,Th23;
hence thesis by A1,A2;
end;
assume
A4: for Y being Subset of R^1 st Y is closed holds g"Y is closed;
let P be Subset of REAL such that
A5: P is closed;
reconsider R = P as Subset of R^1 by TOPMETR:17;
R is closed by A5,Th23;
hence thesis by A1,A4;
end;