:: The Brouwer Fixed Point Theorem for Intervals
:: by Toshihiko Watanabe
::
:: Received August 17, 1992
:: Copyright (c) 1992-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, XXREAL_1, REAL_1, PRE_TOPC, TOPMETR, XXREAL_0, STRUCT_0,
SUBSET_1, RCOMP_1, PCOMPS_1, METRIC_1, CARD_1, TARSKI, ARYTM_1, ARYTM_3,
FUNCT_1, COMPLEX1, SETFAM_1, XBOOLE_0, VALUED_1, BORSUK_1, RELAT_1,
ORDINAL2, TMAP_1, TOPS_2, RELAT_2, XXREAL_2, SEQ_4, FUNCT_3, TREAL_1,
FUNCT_2, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XXREAL_2, XREAL_0, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, REAL_1, SEQ_4, RCOMP_1, PRE_TOPC, TOPS_2, CONNSP_1, METRIC_1,
DOMAIN_1, STRUCT_0, PCOMPS_1, TOPMETR, TSEP_1, TMAP_1, BORSUK_1;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, CONNSP_1, TOPS_2,
TMAP_1, TOPMETR, XXREAL_2, BINOP_2, RVSUM_1, PCOMPS_1, BINOP_1;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, CONNSP_1,
ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_2, XXREAL_2;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, FUNCT_2, XXREAL_2;
theorems TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, ABSVALUE, RCOMP_1, SEQ_2, SEQ_4,
METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, PCOMPS_1, BORSUK_1,
TOPMETR, HEINE, TSEP_1, TMAP_1, RELAT_1, TBSP_1, RELSET_1, XREAL_0,
XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1;
schemes FUNCT_2;
begin
:: 1. Properties of Topological Intervals.
reserve a,b,c,d for Real;
Lm1: for x being set st x in [.a,b.] holds x is Element of REAL;
Lm2: for x being Point of Closed-Interval-TSpace(a,b) st a <= b
holds x is Element of REAL
proof
let x be Point of Closed-Interval-TSpace(a,b);
assume a <= b;
then the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by TOPMETR:18;
hence thesis by Lm1;
end;
theorem Th1:
for A being Subset of R^1 st A = [.a,b.] holds A is closed
proof
let A be Subset of R^1;
assume
A1: A = [.a,b.];
reconsider B = A` as Subset of TopSpaceMetr(RealSpace) by TOPMETR:def 6;
reconsider a, b as Real;
reconsider D = B as Subset of RealSpace by TOPMETR:12;
set C = D`;
A2: the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace) by
TOPMETR:12;
for c being Point of RealSpace st c in B ex r being Real st r > 0
& Ball(c,r) c= B
proof
let c be Point of RealSpace;
reconsider n = c as Element of REAL by METRIC_1:def 13;
assume c in B;
then not n in [.a,b.] by A1,XBOOLE_0:def 5;
then
A3: not n in {p where p is Real : a <= p & p <= b} by RCOMP_1:def 1;
now
per cases by A3;
suppose
A4: not a <= n;
take r = a - n;
now
let x be object;
assume
A5: x in Ball(c,r);
then reconsider t = x as Element of REAL by METRIC_1:def 13;
reconsider u = x as Point of RealSpace by A5;
Ball(c,r) = {q where q is Element of RealSpace :dist(c,q)<r} by
METRIC_1:17;
then
ex v being Element of RealSpace st v = u & dist(c,v)<r by A5;
then (real_dist).(t,n) < r by METRIC_1:def 1,def 13;
then
A6: |.t-n.| < r by METRIC_1:def 12;
t - n <= |.t-n.| by ABSVALUE:4;
then t - n < a - n by A6,XXREAL_0:2;
then not ex q being Real
st q = t & a <= q & q <= b by XREAL_1:9;
then not t in {p where p is Real: a <= p & p <= b};
then not u in C by A1,A2,RCOMP_1:def 1,TOPMETR:def 6;
hence x in B by SUBSET_1:29;
end;
hence r > 0 & Ball(c,r) c= B by A4,XREAL_1:50;
end;
suppose
A7: not n <= b;
take r = n - b;
now
let x be object;
assume
A8: x in Ball(c,r);
then reconsider t = x as Element of REAL by METRIC_1:def 13;
reconsider u = x as Point of RealSpace by A8;
Ball(c,r) = {q where q is Element of RealSpace :dist(c,q)<r} by
METRIC_1:17;
then
ex v being Element of RealSpace st v = u & dist(c,v)<r by A8;
then (real_dist).(n,t) < r by METRIC_1:def 1,def 13;
then
A9: |.n-t.| < r by METRIC_1:def 12;
n - t <= |.n-t.| by ABSVALUE:4;
then n - t < n - b by A9,XXREAL_0:2;
then not ex q being Real
st q = t & a <= q & q <= b by XREAL_1:10;
then not t in {p where p is Real: a <= p & p <= b};
then not u in C by A1,A2,RCOMP_1:def 1,TOPMETR:def 6;
hence x in B by SUBSET_1:29;
end;
hence r > 0 & Ball(c,r) c= B by A7,XREAL_1:50;
end;
end;
hence ex r being Real st r > 0 & Ball(c,r) c= B;
end;
then A` is open by TOPMETR:15,def 6;
hence thesis by TOPS_1:3;
end;
theorem Th2:
a <= b implies Closed-Interval-TSpace(a,b) is closed
proof
assume a <= b;
then the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by TOPMETR:18;
then
for A be Subset of R^1 holds A = the carrier of Closed-Interval-TSpace(a
,b) implies A is closed by Th1;
hence thesis by BORSUK_1:def 11;
end;
theorem
a <= c & d <= b & c <= d implies
Closed-Interval-TSpace(c,d) is closed SubSpace of Closed-Interval-TSpace(a,b)
proof
assume that
A1: a <= c and
A2: d <= b and
A3: c <= d;
[.c,d.] c= [.a,b.] by A1,A2,XXREAL_1:34;
then
A4: the carrier of Closed-Interval-TSpace(c,d) c= [.a,b.] by A3,TOPMETR:18;
A5: Closed-Interval-TSpace(c,d) is closed SubSpace of R^1 by A3,Th2;
a <= d by A1,A3,XXREAL_0:2;
then the carrier of Closed-Interval-TSpace(c,d) c= the carrier of
Closed-Interval-TSpace(a,b) by A2,A4,TOPMETR:18,XXREAL_0:2;
hence thesis by A5,TSEP_1:14;
end;
theorem
a <= c & b <= d & c <= b implies Closed-Interval-TSpace(a,d) =
Closed-Interval-TSpace(a,b) union Closed-Interval-TSpace(c,d) &
Closed-Interval-TSpace(c,b) = Closed-Interval-TSpace(a,b) meet
Closed-Interval-TSpace(c,d)
proof
assume that
A1: a <= c and
A2: b <= d and
A3: c <= b;
A4: the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] & the carrier of
Closed-Interval-TSpace(c,d) = [.c,d.] by A1,A2,A3,TOPMETR:18,XXREAL_0:2;
a <= b by A1,A3,XXREAL_0:2;
then
A5: the carrier of Closed-Interval-TSpace(a,d) = [.a,d.] by A2,TOPMETR:18
,XXREAL_0:2;
A6: the carrier of Closed-Interval-TSpace(c,b) = [.c,b.] by A3,TOPMETR:18;
[.a,b.] \/ [.c,d.] = [.a,d.] by A1,A2,A3,XXREAL_1:174;
hence Closed-Interval-TSpace(a,d) = Closed-Interval-TSpace(a,b) union
Closed-Interval-TSpace(c,d) by A4,A5,TSEP_1:def 2;
A7: [.a,b.] /\ [.c,d.] = [.c,b.] by A1,A2,XXREAL_1:143;
then (the carrier of Closed-Interval-TSpace(a,b)) /\ (the carrier of
Closed-Interval-TSpace(c,d)) <> {} by A3,A4,XXREAL_1:1;
then (the carrier of Closed-Interval-TSpace(a,b)) meets (the carrier of
Closed-Interval-TSpace(c,d)) by XBOOLE_0:def 7;
then Closed-Interval-TSpace(a,b) meets Closed-Interval-TSpace(c,d) by
TSEP_1:def 3;
hence thesis by A4,A6,A7,TSEP_1:def 4;
end;
definition
let a,b be Real;
assume
A1: a <= b;
func (#)(a,b) -> Point of Closed-Interval-TSpace(a,b) equals
:Def1:
a;
coherence
proof
a in [.a,b.] by A1,XXREAL_1:1;
hence thesis by A1,TOPMETR:18;
end;
correctness;
func (a,b)(#) -> Point of Closed-Interval-TSpace(a,b) equals
:Def2:
b;
coherence
proof
b in [.a,b.] by A1,XXREAL_1:1;
hence thesis by A1,TOPMETR:18;
end;
correctness;
end;
theorem
0[01] = (#)(0,1) & 1[01] = (0,1)(#) by Def1,Def2,BORSUK_1:def 14,def 15;
theorem
a <= b & b <= c implies (#)(a,b) = (#)(a,c) & (b,c)(#) = (a,c)(#)
proof
assume that
A1: a <= b and
A2: b <= c;
thus (#)(a,b) = a by A1,Def1
.= (#)(a,c) by A1,A2,Def1,XXREAL_0:2;
thus (b,c)(#) = c by A2,Def2
.= (a,c)(#) by A1,A2,Def2,XXREAL_0:2;
end;
begin
:: 2. Continuous Mappings Between Topological Intervals.
definition
let a,b be Real such that
A1: a <= b;
let t1,t2 be Point of Closed-Interval-TSpace(a,b);
func L[01](t1,t2) -> Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(a,b) means
:Def3:
for s being Point of Closed-Interval-TSpace(0,1) holds
it.s = (1-s)*t1 + s*t2;
existence
proof
reconsider r1 = t1, r2 = t2 as Element of REAL by A1,Lm2;
deffunc U(Real) = In((1-$1)*r1 + $1*r2,REAL);
consider LI being Function of REAL,REAL such that
A2: for r being Element of REAL holds LI.r= U(r) from FUNCT_2:sch 4;
A3: [.a,b.] = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:18;
now
let y be object;
assume
A4: y in rng(LI|[.0,1.]);
then reconsider d = y as Element of REAL;
y in LI.:[.0,1.] by A4,RELAT_1:115;
then consider x being object such that
x in dom LI and
A5: x in [.0,1.] and
A6: y = LI.x by FUNCT_1:def 6;
reconsider c = x as Element of REAL by A5;
A7: d = U(c) by A2,A6;
r1 in [.a,b.] by A3;
then r1 in { p where p is Real: a <= p & p <= b}
by RCOMP_1:def 1;
then
A8: ex v1 being Real st v1 = r1 & a <= v1 & v1 <= b;
c in { p where p is Real:
0 <= p & p <= 1} by A5,RCOMP_1:def 1;
then
A9: ex u being Real st u = c & 0 <= u & u <= 1;
r2 in [.a,b.] by A3;
then r2 in { p where p is Real: a <= p & p <= b}
by RCOMP_1:def 1;
then
A10: ex v2 being Real st v2 = r2 & a <= v2 & v2 <= b;
then
A11: c*a <= c*r2 by A9,XREAL_1:64;
A12: c*r2 <= c*b by A9,A10,XREAL_1:64;
A13: 0 <= 1 - c by A9,XREAL_1:48;
then (1 - c)*r1 <= (1 - c)*b by A8,XREAL_1:64;
then
A14: d <= (1 - c)*b + c*b by A7,A12,XREAL_1:7;
(1 - c)*a <= (1 - c)*r1 by A8,A13,XREAL_1:64;
then (1 - c)*a + c*a <= d by A7,A11,XREAL_1:7;
then y in { q where q is Real: a <= q & q <= b} by A14;
hence y in [.a,b.] by RCOMP_1:def 1;
end;
then
A15: rng(LI|[.0,1.]) c= the carrier of Closed-Interval-TSpace(a,b) by A3;
A16: dom(LI|[.0,1.]) = (dom LI) /\ [.0,1.] by RELAT_1:61;
[.0,1.] = REAL /\ [.0,1.] & dom LI = REAL by FUNCT_2:def 1,XBOOLE_1:28;
then dom(LI|[.0,1.]) = the carrier of Closed-Interval-TSpace(0,1) by A16,
TOPMETR:18;
then reconsider F = LI|[.0,1.] as Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(a,b) by A15,FUNCT_2:def 1,RELSET_1:4;
take F;
let s be Point of Closed-Interval-TSpace(0,1);
A17: s in REAL by XREAL_0:def 1;
the carrier of Closed-Interval-TSpace(0,1) = [.0,1.] by TOPMETR:18;
hence F.s = LI.s by FUNCT_1:49
.= U(s) by A2,A17
.= (1-s)*t1 + s*t2;
end;
uniqueness
proof
let F1, F2 be Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(a,b);
assume
A18: for s being Point of Closed-Interval-TSpace(0,1) holds
F1.s = (1-s)*t1 + s*t2;
assume
A19: for s being Point of Closed-Interval-TSpace(0,1) holds
F2.s = (1-s)*t1 + s*t2;
for s being Point of Closed-Interval-TSpace(0,1) holds F1.s = F2.s
proof
reconsider r1 = t1, r2 = t2 as Real;
let s be Point of Closed-Interval-TSpace(0,1);
reconsider r = s as Real;
thus F1.s = (1-r)*r1 + r*r2 by A18
.= F2.s by A19;
end;
hence F1 = F2;
end;
end;
theorem Th7:
a <= b implies for t1,t2 being Point of Closed-Interval-TSpace(a,b)
for s being Point of Closed-Interval-TSpace(0,1) holds
L[01](t1,t2).s = (t2 - t1)*s + t1
proof
assume
A1: a <= b;
let t1,t2 be Point of Closed-Interval-TSpace(a,b);
let s be Point of Closed-Interval-TSpace(0,1);
thus L[01](t1,t2).s = (1-s)*t1 + s*t2 by A1,Def3
.= (t2 - t1)*s + t1;
end;
theorem Th8:
a <= b implies for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds
L[01](t1,t2) is continuous
proof
assume
A1: a <= b;
let t1,t2 be Point of Closed-Interval-TSpace(a,b);
reconsider r1 = t1, r2 = t2 as Real;
deffunc U(Real) = In((r2 - r1)*$1 + r1,REAL);
consider L being Function of REAL,REAL such that
A2: for r being Element of REAL holds L.r= U(r) from FUNCT_2:sch 4;
A3: for r being Real holds L.r= (r2 - r1)*r + r1
proof let r be Real;
reconsider r as Element of REAL by XREAL_0:def 1;
L.r= U(r) by A2;
hence thesis;
end;
reconsider f = L as Function of R^1, R^1 by TOPMETR:17;
A4: for s being Point of Closed-Interval-TSpace(0,1), w being Point of R^1
st s = w holds L[01](t1,t2).s = f.w
proof
let s be Point of Closed-Interval-TSpace(0,1), w be Point of R^1;
reconsider r = s as Real;
assume
A5: s = w;
thus L[01](t1,t2).s = U(r) by A1,Th7
.= f.w by A3,A5;
end;
A6: [.0,1.] = the carrier of Closed-Interval-TSpace(0,1) by TOPMETR:18;
A7: f is continuous by A3,TOPMETR:21;
for s being Point of Closed-Interval-TSpace(0,1) holds L[01](t1,t2)
is_continuous_at s
proof
let s be Point of Closed-Interval-TSpace(0,1);
reconsider w = s as Point of R^1 by A6,TARSKI:def 3,TOPMETR:17;
for G being Subset of Closed-Interval-TSpace(a,b) st G is open & L[01]
(t1,t2).s in G ex H being Subset of Closed-Interval-TSpace(0,1) st H is open &
s in H & L[01](t1,t2).:H c= G
proof
let G be Subset of Closed-Interval-TSpace(a,b);
assume G is open;
then consider G0 being Subset of R^1 such that
A8: G0 is open and
A9: G0 /\ [#] Closed-Interval-TSpace(a,b) = G by TOPS_2:24;
A10: f is_continuous_at w by A7,TMAP_1:44;
assume L[01](t1,t2).s in G;
then f.w in G by A4;
then f.w in G0 by A9,XBOOLE_0:def 4;
then consider H0 being Subset of R^1 such that
A11: H0 is open and
A12: w in H0 and
A13: f.:H0 c= G0 by A8,A10,TMAP_1:43;
now
reconsider H = H0 /\ [#] Closed-Interval-TSpace(0,1) as Subset of
Closed-Interval-TSpace(0,1);
take H;
thus H is open by A11,TOPS_2:24;
thus s in H by A12,XBOOLE_0:def 4;
thus L[01](t1,t2).:H c= G
proof
let t be object;
assume t in L[01](t1,t2).:H;
then consider r be object such that
r in dom L[01](t1,t2) and
A14: r in H and
A15: t = L[01](t1,t2).r by FUNCT_1:def 6;
A16: r in the carrier of Closed-Interval-TSpace(0,1) by A14;
reconsider r as Point of Closed-Interval-TSpace(0,1) by A14;
r in dom L[01](t1,t2) by A16,FUNCT_2:def 1;
then
A17: t in L[01](t1,t2).:(the carrier of Closed-Interval-TSpace(0,1))
by A15,FUNCT_1:def 6;
reconsider p = r as Point of R^1 by A6,TARSKI:def 3,TOPMETR:17;
p in [#] R^1;
then
A18: p in dom f by FUNCT_2:def 1;
t=f.p & p in H0 by A4,A14,A15,XBOOLE_0:def 4;
then t in f.:H0 by A18,FUNCT_1:def 6;
hence thesis by A9,A13,A17,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
hence thesis by TMAP_1:43;
end;
hence thesis by TMAP_1:44;
end;
theorem
a <= b implies for t1,t2 being Point of Closed-Interval-TSpace(a,b)
holds L[01](t1,t2).(#)(0,1) = t1 & L[01](t1,t2).(0,1)(#) = t2
proof
assume
A1: a <= b;
let t1,t2 be Point of Closed-Interval-TSpace(a,b);
reconsider r1 = t1, r2 = t2 as Real;
0 = (#)(0,1) by Def1;
hence L[01](t1,t2).(#)(0,1) = (1-0)*r1 + 0*r2 by A1,Def3
.= t1;
1 = (0,1)(#) by Def2;
hence L[01](t1,t2).(0,1)(#) = (1-1)*r1 + 1*r2 by A1,Def3
.= t2;
end;
theorem
L[01]((#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1)
proof
for x being Point of Closed-Interval-TSpace(0,1) holds L[01]((#)(0,1),(0
,1)(#)).x = x
proof
let x be Point of Closed-Interval-TSpace(0,1);
reconsider y = x as Real;
(#)(0,1) = 0 & (0,1)(#) = 1 by Def1,Def2;
hence L[01]((#)(0,1),(0,1)(#)).x = (1-y)*0 + y*1 by Def3
.= x;
end;
hence thesis by FUNCT_2:124;
end;
definition
let a,b be Real such that
A1: a < b;
let t1,t2 be Point of Closed-Interval-TSpace(0,1);
func P[01](a,b,t1,t2) -> Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(0,1) means
:Def4:
for s being Point of Closed-Interval-TSpace(a,b) holds
it.s = ((b-s)*t1 + (s-a)*t2)/(b-a);
existence
proof
reconsider a1 = a, b1 = b as Real;
reconsider r1 = t1, r2 = t2 as Real;
deffunc U(Real) = In(((b1-$1)*r1 + ($1-a1)*r2)/(b1-a1),REAL);
consider PI being Function of REAL,REAL such that
A2: for r being Element of REAL holds PI.r= U(r) from FUNCT_2:sch 4;
A3: [.0,1.] = the carrier of Closed-Interval-TSpace(0,1) by TOPMETR:18;
now
let y be object;
assume
A4: y in rng(PI|[.a,b.]);
then reconsider d = y as Real;
y in PI.:[.a,b.] by A4,RELAT_1:115;
then consider x being object such that
x in dom PI and
A5: x in [.a,b.] and
A6: y = PI.x by FUNCT_1:def 6;
reconsider c = x as Element of REAL by A5;
A7: d = U(c) by A2,A6;
r1 in [.0,1.] by A3;
then r1 in { p where p is Real: 0 <= p & p <= 1} by RCOMP_1:def 1;
then
A8: ex v1 being Real st v1 = r1 & 0 <= v1 & v1 <= 1;
c in { p where p is Real: a <= p & p <= b} by A5,RCOMP_1:def 1;
then
A9: ex u being Real st u = c & a <= u & u <= b;
then
A10: 0 <= c - a by XREAL_1:48;
r2 in [.0,1.] by A3;
then r2 in { p where p is Real: 0 <= p & p <= 1} by RCOMP_1:def 1;
then
A11: ex v2 being Real st v2 = r2 & 0 <= v2 & v2 <= 1;
then
A12: (c - a)*r2 <= c - a by A10,XREAL_1:153;
A13: 0 < b - a by A1,XREAL_1:50;
A14: 0 <= b - c by A9,XREAL_1:48;
then (b - c)*r1 <= b - c by A8,XREAL_1:153;
then (b - c)*r1 + (c - a)*r2 <= (b + - c) + (c - a) by A12,XREAL_1:7;
then d <= (b - a)/(b - a) by A13,A7,XREAL_1:72;
then d <= 1 by A13,XCMPLX_1:60;
then y in { q where q is Real: 0 <= q & q <= 1}
by A8,A11,A13,A7,A14,A10;
hence y in [.0,1.] by RCOMP_1:def 1;
end;
then
A15: rng(PI|[.a,b.]) c= the carrier of Closed-Interval-TSpace(0,1) by A3;
A16: dom(PI|[.a,b.]) = (dom PI) /\ [.a,b.] by RELAT_1:61;
[.a,b.] = REAL /\ [.a,b.] & dom PI = REAL by FUNCT_2:def 1,XBOOLE_1:28;
then dom(PI|[.a,b.]) = the carrier of Closed-Interval-TSpace(a,b) by A1,A16
,TOPMETR:18;
then reconsider F = PI|[.a,b.] as Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(0,1) by A15,FUNCT_2:def 1,RELSET_1:4;
take F;
let s be Point of Closed-Interval-TSpace(a,b);
A17: s in REAL by XREAL_0:def 1;
the carrier of Closed-Interval-TSpace(a,b) = [.a,b.] by A1,TOPMETR:18;
hence F.s = PI.s by FUNCT_1:49
.= U(s) by A2,A17
.= ((b-s)*t1 + (s-a)*t2)/(b-a);
end;
uniqueness
proof
let F1, F2 be Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(0,1);
assume
A18: for s being Point of Closed-Interval-TSpace(a,b)
holds F1.s = ((b-s)*t1 + (s-a)*t2)/(b-a);
assume
A19: for s being Point of Closed-Interval-TSpace(a,b)
holds F2.s = ((b-s)*t1 + (s-a)*t2)/(b-a);
let s be Point of Closed-Interval-TSpace(a,b);
reconsider r = s as Real;
reconsider r1 = t1, r2 = t2 as Real;
thus F1.s = ((b-r)*r1 + (r-a)*r2)/(b-a) by A18
.= F2.s by A19;
end;
end;
theorem Th11:
a < b implies for t1,t2 being Point of Closed-Interval-TSpace(0,1)
for s being Point of Closed-Interval-TSpace(a,b) holds
P[01](a,b,t1,t2).s = ((t2 - t1)/(b-a))*s + (b*t1 -a*t2)/(b-a)
proof
assume
A1: a < b;
let t1,t2 be Point of Closed-Interval-TSpace(0,1);
let s be Point of Closed-Interval-TSpace(a,b);
thus P[01](a,b,t1,t2).s = ((b-s)*t1 + (s-a)*t2)/(b-a) by A1,Def4
.= (s*(t2 - t1) + (b*t1 -a*t2))/(b-a)
.= (s*(t2 - t1))/(b-a) + (b*t1 -a*t2)/(b-a) by XCMPLX_1:62
.= (s*(t2 - t1))* (1/(b-a)) + (b*t1 -a*t2)/(b-a) by XCMPLX_1:99
.= ((t2 - t1)* (1/(b-a)))*s + (b*t1 -a*t2)/(b-a)
.= ((t2 - t1)/(b-a))*s + (b*t1 -a*t2)/(b-a) by XCMPLX_1:99;
end;
theorem Th12:
a < b implies for t1,t2 being Point of Closed-Interval-TSpace(0,1)
holds P[01](a,b,t1,t2) is continuous
proof
assume
A1: a < b;
reconsider a, b as Real;
A2: [.a,b.] = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:18;
let t1,t2 be Point of Closed-Interval-TSpace(0,1);
reconsider r1 = t1, r2 = t2 as Real;
deffunc U(Real) = In(((r2 - r1)/(b-a))*$1 + (b*r1 -a*r2)/(b-a),REAL);
consider P being Function of REAL,REAL such that
A3: for r being Element of REAL holds P.r= U(r) from FUNCT_2:sch 4;
A4: for r being Real
holds P.r= ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(b-a)
proof let r be Real;
reconsider r as Element of REAL by XREAL_0:def 1;
P.r= U(r) by A3;
hence thesis;
end;
reconsider f = P as Function of R^1, R^1 by TOPMETR:17;
A5: for s being Point of Closed-Interval-TSpace(a,b), w being Point of R^1
st s = w holds P[01](a,b,t1,t2).s = f.w
proof
let s be Point of Closed-Interval-TSpace(a,b), w be Point of R^1;
reconsider r = s as Real;
assume
A6: s = w;
thus P[01](a,b,t1,t2).s = ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(b-a) by A1
,Th11
.= U(r)
.= f.w by A4,A6;
end;
A7: f is continuous by A4,TOPMETR:21;
for s being Point of Closed-Interval-TSpace(a,b) holds P[01](a,b,t1,t2)
is_continuous_at s
proof
let s be Point of Closed-Interval-TSpace(a,b);
reconsider w = s as Point of R^1 by A2,TARSKI:def 3,TOPMETR:17;
for G being Subset of Closed-Interval-TSpace(0,1) st G is open & P[01]
(a,b,t1,t2).s in G ex H being Subset of Closed-Interval-TSpace(a,b) st H is
open & s in H & P[01](a,b,t1,t2).:H c= G
proof
let G be Subset of Closed-Interval-TSpace(0,1);
assume G is open;
then consider G0 being Subset of R^1 such that
A8: G0 is open and
A9: G0 /\ [#] Closed-Interval-TSpace(0,1) = G by TOPS_2:24;
A10: f is_continuous_at w by A7,TMAP_1:44;
assume P[01](a,b,t1,t2).s in G;
then f.w in G by A5;
then f.w in G0 by A9,XBOOLE_0:def 4;
then consider H0 being Subset of R^1 such that
A11: H0 is open and
A12: w in H0 and
A13: f.: H0 c= G0 by A8,A10,TMAP_1:43;
now
reconsider H = H0 /\ [#] Closed-Interval-TSpace(a,b) as Subset of
Closed-Interval-TSpace(a,b);
take H;
thus H is open by A11,TOPS_2:24;
thus s in H by A12,XBOOLE_0:def 4;
thus P[01](a,b,t1,t2).:H c= G
proof
let t be object;
assume t in P[01](a,b,t1,t2).:H;
then consider r be object such that
r in dom P[01](a,b,t1,t2) and
A14: r in H and
A15: t = P[01](a,b,t1,t2).r by FUNCT_1:def 6;
A16: r in the carrier of Closed-Interval-TSpace(a,b) by A14;
reconsider r as Point of Closed-Interval-TSpace(a,b) by A14;
r in dom P[01](a,b,t1,t2) by A16,FUNCT_2:def 1;
then
A17: t in P[01](a,b,t1,t2).: (the carrier of Closed-Interval-TSpace(
a,b)) by A15,FUNCT_1:def 6;
reconsider p = r as Point of R^1 by A2,TARSKI:def 3,TOPMETR:17;
p in [#] R^1;
then
A18: p in dom f by FUNCT_2:def 1;
t=f.p & p in H0 by A5,A14,A15,XBOOLE_0:def 4;
then t in f.:H0 by A18,FUNCT_1:def 6;
hence thesis by A9,A13,A17,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
hence thesis by TMAP_1:43;
end;
hence thesis by TMAP_1:44;
end;
theorem
a < b implies for t1,t2 being Point of Closed-Interval-TSpace(0,1)
holds P[01](a,b,t1,t2).(#)(a,b) = t1 & P[01](a,b,t1,t2).(a,b)(#) = t2
proof
assume
A1: a < b;
then
A2: b - a <> 0;
let t1,t2 be Point of Closed-Interval-TSpace(0,1);
reconsider r1 = t1, r2 = t2 as Real;
a = (#)(a,b) by A1,Def1;
hence P[01](a,b,t1,t2).(#)(a,b) = ((b-a)*r1 + (a-a)*r2)/(b-a) by A1,Def4
.= t1 by A2,XCMPLX_1:89;
b = (a,b)(#) by A1,Def2;
hence P[01](a,b,t1,t2).(a,b)(#) = ((b-b)*r1 + (b-a)*r2)/(b-a) by A1,Def4
.= t2 by A2,XCMPLX_1:89;
end;
theorem
P[01](0,1,(#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1)
proof
for x being Point of Closed-Interval-TSpace(0,1) holds P[01](0,1,(#)(0,1
),(0,1)(#)).x = x
proof
let x be Point of Closed-Interval-TSpace(0,1);
reconsider y = x as Real;
(#)(0,1)=0 & (0,1)(#) = 1 by Def1,Def2;
hence P[01](0,1,(#)(0,1),(0,1)(#)).x = ((1-y)*0 + (y-0)*1)/(1-0) by Def4
.= x;
end;
hence thesis by FUNCT_2:124;
end;
theorem Th15:
a < b implies
id Closed-Interval-TSpace(a,b) =
L[01]((#)(a,b),(a,b)(#)) * P[01](a,b,(#)(0,1),(0,1)(#)) &
id Closed-Interval-TSpace(0,1) =
P[01](a,b,(#)(0,1),(0,1)(#)) * L[01]((#)(a,b),(a,b)(#))
proof
A1: 0 = (#)(0,1) & 1 = (0,1)(#) by Def1,Def2;
set L = L[01]((#)(a,b),(a,b)(#)), P = P[01](a,b,(#)(0,1),(0,1)(#));
assume
A2: a < b;
then
A3: b - a <> 0;
A4: a = (#)(a,b) & b = (a,b)(#) by A2,Def1,Def2;
for c being Point of Closed-Interval-TSpace(a,b) holds (L*P).c = c
proof
let c be Point of Closed-Interval-TSpace(a,b);
reconsider r = c as Real;
A5: P.c = ((b-r)*0 + (r-a)*1)/(b-a) by A2,A1,Def4
.= (r-a)/(b-a);
thus (L*P).c = L.(P.c) by FUNCT_2:15
.= (1-((r-a)/(b-a)))*a + ((r-a)/(b-a))*b by A2,A4,A5,Def3
.= ((1*(b-a)-(r-a))/(b-a))*a + ((r-a)/(b-a))*b by A3,XCMPLX_1:127
.= ((b-r)/(b-a))*(a/1) + ((r-a)/(b-a))*b
.= ((b-r)*a)/(1*(b-a)) + ((r-a)/(b-a))*b by XCMPLX_1:76
.= ((b-r)*a)/(b-a) + ((r-a)/(b-a))*(b/1)
.= ((b-r)*a)/(b-a) + ((r-a)*b)/(1*(b-a)) by XCMPLX_1:76
.= ((a*b-a*r) + (r-a)*b)/(b-a) by XCMPLX_1:62
.= ((b-a)*r)/(b-a)
.= c by A3,XCMPLX_1:89;
end;
hence id Closed-Interval-TSpace(a,b) = L*P by FUNCT_2:124;
for c being Point of Closed-Interval-TSpace(0,1) holds (P*L).c = c
proof
let c be Point of Closed-Interval-TSpace(0,1);
reconsider r = c as Real;
A6: L.c = (1-r)*a + r*b by A2,A4,Def3
.= r*(b-a) + a;
thus (P*L).c = P.(L.c) by FUNCT_2:15
.= ((b-(r*(b-a) + a))*0 + ((r*(b-a) + a)-a)*1)/(b-a) by A2,A1,A6,Def4
.= c by A3,XCMPLX_1:89;
end;
hence thesis by FUNCT_2:124;
end;
theorem Th16:
a < b implies
id Closed-Interval-TSpace(a,b) =
L[01]((a,b)(#),(#)(a,b)) * P[01](a,b,(0,1)(#),(#)(0,1)) &
id Closed-Interval-TSpace(0,1) =
P[01](a,b,(0,1)(#),(#)(0,1)) * L[01]((a,b)(#),(#)(a,b))
proof
A1: 0 = (#)(0,1) & 1 = (0,1)(#) by Def1,Def2;
set L = L[01]((a,b)(#),(#)(a,b)), P = P[01](a,b,(0,1)(#),(#)(0,1));
assume
A2: a < b;
then
A3: b - a <> 0;
A4: a = (#)(a,b) & b = (a,b)(#) by A2,Def1,Def2;
for c being Point of Closed-Interval-TSpace(a,b) holds (L*P).c = c
proof
let c be Point of Closed-Interval-TSpace(a,b);
reconsider r = c as Real;
A5: P.c = ((b-r)*1 + (r-a)*0)/(b-a) by A2,A1,Def4
.= (b-r)/(b-a);
thus (L*P).c = L.(P.c) by FUNCT_2:15
.= (1-((b-r)/(b-a)))*b + ((b-r)/(b-a))*a by A2,A4,A5,Def3
.= ((1*(b-a)-(b-r))/(b-a))*b + ((b-r)/(b-a))*a by A3,XCMPLX_1:127
.= ((r-a)/(b-a))*(b/1) + ((b-r)/(b-a))*a
.= ((r-a)*b)/(1*(b-a)) + ((b-r)/(b-a))*a by XCMPLX_1:76
.= ((r-a)*b)/(b-a) + ((b-r)/(b-a))*(a/1)
.= ((r-a)*b)/(b-a) + ((b-r)*a)/(1*(b-a)) by XCMPLX_1:76
.= ((b*r-b*a) + (b-r)*a)/(b-a) by XCMPLX_1:62
.= ((b-a)*r)/(b-a)
.= c by A3,XCMPLX_1:89;
end;
hence id Closed-Interval-TSpace(a,b) = L*P by FUNCT_2:124;
for c being Point of Closed-Interval-TSpace(0,1) holds (P*L).c = c
proof
let c be Point of Closed-Interval-TSpace(0,1);
reconsider r = c as Real;
A6: L.c = (1-r)*b + r*a by A2,A4,Def3
.= r*(a-b) + b;
thus (P*L).c = P.(L.c) by FUNCT_2:15
.= ((b-(r*(a-b) + b))*1 + ((r*(a-b) + b)-a)*0)/(b-a) by A2,A1,A6,Def4
.= (r*(-(a-b)))/(b-a)
.= c by A3,XCMPLX_1:89;
end;
hence thesis by FUNCT_2:124;
end;
theorem Th17:
a < b implies
L[01]((#)(a,b),(a,b)(#)) is being_homeomorphism &
L[01]((#)(a,b),(a,b)(#))" = P[01](a,b,(#)(0,1),(0,1)(#)) &
P[01](a,b,(#)(0,1),(0,1)(#)) is being_homeomorphism &
P[01](a,b,(#)(0,1),(0,1)(#))" = L[01]((#)(a,b),(a,b)(#))
proof
set L = L[01]((#)(a,b),(a,b)(#)), P = P[01](a,b,(#)(0,1),(0,1)(#));
assume
A1: a < b;
then
A2: id (the carrier of Closed-Interval-TSpace(0,1)) = P * L by Th15;
then
A3: L is one-to-one by FUNCT_2:23;
A4: L is continuous & P is continuous Function of Closed-Interval-TSpace(a,
b), Closed-Interval-TSpace(0,1) by A1,Th8,Th12;
A5: id (the carrier of Closed-Interval-TSpace(a,b)) = id
Closed-Interval-TSpace(a,b)
.= L * P by A1,Th15;
then
A6: L is onto by FUNCT_2:23;
then
A7: rng L = [#](Closed-Interval-TSpace(a,b));
A8: L" = L qua Function" by A3,A6,TOPS_2:def 4;
dom L = [#]Closed-Interval-TSpace(0,1) & P = L qua Function" by A2,A3,A7,
FUNCT_2:30,def 1;
hence L[01]((#)(a,b),(a,b)(#)) is being_homeomorphism by A3,A7,A8,A4,
TOPS_2:def 5;
thus L[01]((#)(a,b),(a,b)(#))" = P[01](a,b,(#)(0,1),(0,1)(#)) by A2,A3,A7,A8,
FUNCT_2:30;
A9: P is onto by A2,FUNCT_2:23;
then
A10: rng P = [#](Closed-Interval-TSpace(0,1));
A11: L is continuous Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(a,b) & P is continuous by A1,Th8,Th12;
A12: P is one-to-one by A5,FUNCT_2:23;
A13: P" = P qua Function" by A12,A9,TOPS_2:def 4;
dom P = [#]Closed-Interval-TSpace(a,b) & L = P qua Function" by A10,A5,A12,
FUNCT_2:30,def 1;
hence P[01](a,b,(#)(0,1),(0,1)(#)) is being_homeomorphism by A10,A12,A13,A11,
TOPS_2:def 5;
thus thesis by A10,A5,A12,A13,FUNCT_2:30;
end;
theorem
a < b implies
L[01]((a,b)(#),(#)(a,b)) is being_homeomorphism &
L[01]((a,b)(#),(#)(a,b))" = P[01](a,b,(0,1)(#),(#)(0,1)) &
P[01](a,b,(0,1)(#),(#)(0,1)) is being_homeomorphism &
P[01](a,b,(0,1)(#),(#)(0,1))" = L[01]((a,b)(#),(#)(a,b))
proof
set L = L[01]((a,b)(#),(#)(a,b)), P = P[01](a,b,(0,1)(#),(#)(0,1));
assume
A1: a < b;
then
A2: id (the carrier of Closed-Interval-TSpace(0,1)) = P * L by Th16;
then
A3: L is one-to-one by FUNCT_2:23;
A4: L is continuous & P is continuous Function of Closed-Interval-TSpace(a,
b), Closed-Interval-TSpace(0,1) by A1,Th8,Th12;
A5: id (the carrier of Closed-Interval-TSpace(a,b)) = id
Closed-Interval-TSpace(a,b)
.= L * P by A1,Th16;
then
A6: L is onto by FUNCT_2:23;
then
A7: rng L = [#](Closed-Interval-TSpace(a,b));
A8: L" = L qua Function" by A3,A6,TOPS_2:def 4;
dom L = [#]Closed-Interval-TSpace(0,1) & P = L qua Function" by A2,A3,A7,
FUNCT_2:30,def 1;
hence L[01]((a,b)(#),(#)(a,b)) is being_homeomorphism by A3,A7,A8,A4,
TOPS_2:def 5;
thus L[01]((a,b)(#),(#)(a,b))" = P[01](a,b,(0,1)(#),(#)(0,1)) by A2,A3,A7,A8,
FUNCT_2:30;
A9: P is onto by A2,FUNCT_2:23;
then
A10: rng P = [#](Closed-Interval-TSpace(0,1));
A11: L is continuous Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(a,b) & P is continuous by A1,Th8,Th12;
A12: P is one-to-one by A5,FUNCT_2:23;
A13: P" = P qua Function" by A12,A9,TOPS_2:def 4;
dom P = [#]Closed-Interval-TSpace(a,b) & L = P qua Function" by A10,A5,A12,
FUNCT_2:30,def 1;
hence P[01](a,b,(0,1)(#),(#)(0,1)) is being_homeomorphism by A10,A12,A13,A11,
TOPS_2:def 5;
thus thesis by A10,A5,A12,A13,FUNCT_2:30;
end;
begin
:: 3. Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals.
theorem Th19:
I[01] is connected
proof
for A,B being Subset of I[01] st [#]I[01] = A \/ B & A <> {}I[01] & B <>
{}I[01] & A is closed & B is closed holds A meets B
proof
let A,B be Subset of I[01];
assume that
A1: [#]I[01] = A \/ B and
A2: A <> {}I[01] and
A3: B <> {}I[01] and
A4: A is closed and
A5: B is closed;
reconsider P = A, Q = B as Subset of REAL by BORSUK_1:40,XBOOLE_1:1;
assume
A6: A misses B;
set x = the Element of P;
reconsider x as Real;
A7: now
take x;
thus x in P by A2;
end;
set x = the Element of Q;
reconsider x as Real;
A8: now
take x;
thus x in Q by A3;
end;
A9: the carrier of RealSpace = the carrier of TopSpaceMetr(RealSpace) by
TOPMETR:12;
0 is LowerBound of P
proof
let r be ExtReal;
assume r in P;
then r in [.0,1.] by BORSUK_1:40;
then r in {w where w is Real: 0<=w & w<=1} by RCOMP_1:def 1;
then ex u being Real st u = r & 0<=u & u<=1;
hence 0 <= r;
end;
then
A10: P is bounded_below;
0 is LowerBound of Q
proof
let r be ExtReal;
assume r in Q;
then r in [.0,1.] by BORSUK_1:40;
then r in {w where w is Real : 0<=w & w<=1} by RCOMP_1:def 1;
then ex u being Real st u = r & 0<=u & u<=1;
hence 0 <= r;
end;
then
A11: Q is bounded_below;
reconsider A0 = P, B0 = Q as Subset of R^1 by METRIC_1:def 13,TOPMETR:12
,def 6;
A12: I[01] is closed SubSpace of R^1 by Th2,TOPMETR:20;
then
A13: A0 is closed by A4,TSEP_1:12;
A14: B0 is closed by A5,A12,TSEP_1:12;
0 in {w where w is Real: 0<=w & w<=1};
then
A15: 0 in [.0,1.] by RCOMP_1:def 1;
now
per cases by A1,A15,BORSUK_1:40,XBOOLE_0:def 3;
suppose
A16: 0 in P;
reconsider B00 = B0` as Subset of R^1;
set l = lower_bound Q;
l in REAL by XREAL_0:def 1;
then reconsider m = l as Point of RealSpace by METRIC_1:def 13;
reconsider t = m as Point of R^1 by TOPMETR:12,def 6;
set W = {w where w is Real : 0<=w & w<l};
A17: l in Q
proof
assume not l in Q;
then
A18: t in B00 by SUBSET_1:29;
B00 is open by A14,TOPS_1:3;
then consider s being Real such that
A19: s > 0 and
A20: Ball(m,s) c= B0` by A18,TOPMETR:15,def 6;
consider r being Real such that
A21: r in Q and
A22: r < l+s by A8,A11,A19,SEQ_4:def 2;
reconsider r as Element of REAL by XREAL_0:def 1;
l <= r by A11,A21,SEQ_4:def 2;
then l - r <= 0 by XREAL_1:47;
then
A23: -s < -(l - r) by A19,XREAL_1:24;
reconsider rm = r as Point of RealSpace by METRIC_1:def 13;
r - l < s by A22,XREAL_1:19;
then |.r - l.| < s by A23,SEQ_2:1;
then (the distance of RealSpace).(rm,m) < s by METRIC_1:def 12,def 13
;
then dist(m,rm) < s by METRIC_1:def 1;
then rm in {q where q is Element of RealSpace : dist(m,q)<s};
then rm in Ball(m,s) by METRIC_1:17;
hence contradiction by A20,A21,XBOOLE_0:def 5;
end;
then l in [.0,1.] by BORSUK_1:40;
then l in {u where u is Real: 0<=u & u<=1} by RCOMP_1:def 1;
then
A24: ex u0 being Real st u0 = l & 0<=u0 & u0<=1;
now
let x be object;
assume x in W;
then consider w0 being Real such that
A25: w0 = x and
A26: 0<=w0 and
A27: w0<l;
w0 <= 1 by A24,A27,XXREAL_0:2;
then w0 in {u where u is Real: 0<=u & u<=1} by A26;
then w0 in P \/ Q by A1,BORSUK_1:40,RCOMP_1:def 1;
then w0 in P or w0 in Q by XBOOLE_0:def 3;
hence x in P by A11,A25,A27,SEQ_4:def 2;
end;
then
A28: W c= P;
then reconsider D = W as Subset of R^1 by A9,METRIC_1:def 13
,TOPMETR:def 6,XBOOLE_1:1;
A29: not 0 in Q by A6,A16,XBOOLE_0:3;
now
let G be Subset of R^1;
assume
A30: G is open;
assume t in G;
then consider e being Real such that
A31: e > 0 and
A32: Ball(m,e) c= G by A30,TOPMETR:15,def 6;
reconsider e as Element of REAL by XREAL_0:def 1;
reconsider e0 = max(0,l - (e/2)) as Element of REAL by XREAL_0:def 1;
reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13;
A33: e*(1/2) < e*1 by A31,XREAL_1:68;
now
per cases by XXREAL_0:16;
suppose
A34: e0 = 0;
then l <= e/2 by XREAL_1:50,XXREAL_0:25;
then l < e by A33,XXREAL_0:2;
hence |.l-e0.| < e by A24,A34,ABSVALUE:def 1;
end;
suppose
e0 = l - (e/2);
hence |.l-e0.| < e by A31,A33,ABSVALUE:def 1;
end;
end;
then (the distance of RealSpace).(m,e1) < e by METRIC_1:def 12,def 13
;
then dist(m,e1) < e by METRIC_1:def 1;
then e1 in {z where z is Element of RealSpace : dist(m,z)<e};
then
A35: e1 in Ball(m,e) by METRIC_1:17;
e0 = 0 or e0 = l - (e/2) by XXREAL_0:16;
then 0 <= e0 & e0 < l by A29,A17,A24,A31,XREAL_1:44,139,XXREAL_0:25;
then e0 in W;
hence D meets G by A32,A35,XBOOLE_0:3;
end;
then
A36: t in Cl D by PRE_TOPC:24;
A37: Cl A0 = A0 by A13,PRE_TOPC:22;
Cl D c= Cl A0 by A28,PRE_TOPC:19;
hence contradiction by A6,A17,A36,A37,XBOOLE_0:3;
end;
suppose
A38: 0 in Q;
reconsider A00 = A0` as Subset of R^1;
set l = lower_bound P;
l in REAL by XREAL_0:def 1;
then reconsider m = l as Point of RealSpace by METRIC_1:def 13;
reconsider t = m as Point of R^1 by TOPMETR:12,def 6;
set W = {w where w is Real : 0<=w & w<l};
A39: l in P
proof
assume not l in P;
then
A40: t in A00 by SUBSET_1:29;
A00 is open by A13,TOPS_1:3;
then consider s being Real such that
A41: s > 0 and
A42: Ball(m,s) c= A0` by A40,TOPMETR:15,def 6;
consider r being Real such that
A43: r in P and
A44: r < l+s by A7,A10,A41,SEQ_4:def 2;
reconsider r as Element of REAL by XREAL_0:def 1;
l <= r by A10,A43,SEQ_4:def 2;
then l - r <= 0 by XREAL_1:47;
then
A45: -s < -(l - r) by A41,XREAL_1:24;
reconsider rm = r as Point of RealSpace by METRIC_1:def 13;
A46: (real_dist).(r,l) = dist(rm,m) by METRIC_1:def 1,def 13;
r - l < s by A44,XREAL_1:19;
then |.r - l.| < s by A45,SEQ_2:1;
then dist(rm,m) < s by METRIC_1:def 12,A46;
then rm in {q where q is Element of RealSpace : dist(m,q)<s};
then rm in Ball(m,s) by METRIC_1:17;
hence contradiction by A42,A43,XBOOLE_0:def 5;
end;
then l in [.0,1.] by BORSUK_1:40;
then l in {u where u is Real: 0<=u & u<=1} by RCOMP_1:def 1;
then
A47: ex u0 being Real st u0 = l & 0<=u0 & u0<=1;
now
let x be object;
assume x in W;
then consider w0 being Real such that
A48: w0 = x and
A49: 0<=w0 and
A50: w0<l;
w0 <= 1 by A47,A50,XXREAL_0:2;
then w0 in {u where u is Real: 0<=u & u<=1} by A49;
then w0 in P \/ Q by A1,BORSUK_1:40,RCOMP_1:def 1;
then w0 in P or w0 in Q by XBOOLE_0:def 3;
hence x in Q by A10,A48,A50,SEQ_4:def 2;
end;
then
A51: W c= Q;
then reconsider D = W as Subset of R^1 by A9,METRIC_1:def 13
,TOPMETR:def 6,XBOOLE_1:1;
A52: not 0 in P by A6,A38,XBOOLE_0:3;
now
let G be Subset of R^1;
assume
A53: G is open;
assume t in G;
then consider e being Real such that
A54: e > 0 and
A55: Ball(m,e) c= G by A53,TOPMETR:15,def 6;
reconsider e as Element of REAL by XREAL_0:def 1;
reconsider e0 = max(0,l - (e/2)) as Element of REAL by XREAL_0:def 1;
reconsider e1 = e0 as Point of RealSpace by METRIC_1:def 13;
A56: e*(1/2) < e*1 by A54,XREAL_1:68;
A57: (real_dist).(l,e0) = dist(m,e1) by METRIC_1:def 1,def 13;
now
per cases by XXREAL_0:16;
suppose
A58: e0 = 0;
then l <= e/2 by XREAL_1:50,XXREAL_0:25;
then l < e by A56,XXREAL_0:2;
hence |.l-e0.| < e by A47,A58,ABSVALUE:def 1;
end;
suppose
e0 = l - (e/2);
hence |.l-e0.| < e by A54,A56,ABSVALUE:def 1;
end;
end;
then dist(m,e1) < e by METRIC_1:def 12,A57;
then e1 in {z where z is Element of RealSpace : dist(m,z)<e};
then
A59: e1 in Ball(m,e) by METRIC_1:17;
e0 = 0 or e0 = l - (e/2) by XXREAL_0:16;
then 0 <= e0 & e0 < l by A52,A39,A47,A54,XREAL_1:44,139,XXREAL_0:25;
then e0 in W;
hence D meets G by A55,A59,XBOOLE_0:3;
end;
then
A60: t in Cl D by PRE_TOPC:24;
A61: Cl B0 = B0 by A14,PRE_TOPC:22;
Cl D c= Cl B0 by A51,PRE_TOPC:19;
hence contradiction by A6,A39,A60,A61,XBOOLE_0:3;
end;
end;
hence contradiction;
end;
hence thesis by CONNSP_1:10;
end;
theorem
a <= b implies Closed-Interval-TSpace(a,b) is connected
proof
assume
A1: a <= b;
now
per cases by A1,XXREAL_0:1;
suppose
a < b;
then L[01]((#)(a,b),(a,b)(#)) is being_homeomorphism by Th17;
then
A2: rng L[01]((#)(a,b),(a,b)(#) ) = [#](Closed-Interval-TSpace(a,b )) &
L[01]( (#)(a,b),(a,b)(#)) is continuous by TOPS_2:def 5;
set A = the carrier of Closed-Interval-TSpace(0,1);
A = [#](Closed-Interval-TSpace(0,1)) & L[01]((#)(a,b),(a,b)(#)).:(A)
= rng L[01]((#)(a,b),(a,b)(#) ) by RELSET_1:22;
hence thesis by A2,Th19,CONNSP_1:14,TOPMETR:20;
end;
suppose
A3: a = b;
then [.a,b.] = {a} & a = (#)(a,b) by Def1,XXREAL_1:17;
then [#] Closed-Interval-TSpace(a,b) = {(#)(a,b)} by A3,TOPMETR:18;
hence thesis by CONNSP_1:27;
end;
end;
hence thesis;
end;
theorem Th21:
for f being continuous Function of I[01],I[01]
ex x being Point of I[01] st f.x = x
proof
let f be continuous Function of I[01],I[01];
reconsider F = f as Function of [.0,1.], [.0,1.] by BORSUK_1:40;
set A = {a where a is Real : a in [.0,1.] & F.a in [.0,a.]}, B = {b where b
is Real : b in [.0,1.] & F.b in [.b,1.]};
A c= REAL
proof
let x be object;
assume x in A;
then ex a being Real st a = x & a in [.0,1.] & F.a in [.0,a.];
hence thesis;
end;
then reconsider A as Subset of REAL;
A1: Closed-Interval-TSpace(0,1) = TopSpaceMetr(Closed-Interval-MSpace(0,1))
by TOPMETR:def 7;
A2: A c= [.0,1.]
proof
let x be object;
assume
A3: x in A;
then reconsider x as Real;
ex a0 being Real st a0 = x & a0 in [.0,1.] & F.a0 in [.0,a0.] by A3;
hence thesis;
end;
B c= REAL
proof
let x be object;
assume x in B;
then ex b being Real st b = x & b in [.0,1.] & F.b in [.b,1.];
hence thesis;
end;
then reconsider B as Subset of REAL;
A4: the carrier of Closed-Interval-MSpace(0,1) = [.0,1.] by TOPMETR:10;
0 in {w where w is Real: 0<=w & w<=1};
then
A5: 0 in [.0,1.] by RCOMP_1:def 1;
A6: [.0,1.] <> {} by XXREAL_1:1;
then [.0,1.] = dom F by FUNCT_2:def 1;
then F.0 in rng F by A5,FUNCT_1:def 3;
then
A7: 0 in B by A5;
A8: [.0,1.] = {q where q is Real: 0<=q & q<=1 } by RCOMP_1:def 1;
A9: [.0,1.] c= A \/ B
proof
let x be object;
assume
A10: x in [.0,1.];
then reconsider y = x as Real;
ex p being Real st p = y & 0<=p & p<=1 by A8,A10;
then
A11: [.0,1.] = [.0,y.] \/ [.y,1.] by XXREAL_1:174;
[.0,1.] = dom F by A6,FUNCT_2:def 1;
then
A12: F.y in rng F by A10,FUNCT_1:def 3;
now
per cases by A11,A12,XBOOLE_0:def 3;
suppose
A13: F.y in [.0,y.];
A14: A c= A \/ B by XBOOLE_1:7;
y in A by A10,A13;
hence y in A \/ B by A14;
end;
suppose
A15: F.y in [.y,1.];
A16: B c= A \/ B by XBOOLE_1:7;
y in B by A10,A15;
hence y in A \/ B by A16;
end;
end;
hence thesis;
end;
1 in {w where w is Real: 0<=w & w<=1};
then
A17: 1 in [.0,1.] by RCOMP_1:def 1;
A18: B c= [.0,1.]
proof
let x be object;
assume
A19: x in B;
then reconsider x as Real;
ex b0 being Real st b0 = x & b0 in [.0,1.] & F.b0 in [.b0,1.] by A19;
hence thesis;
end;
assume
A20: for x being Point of I[01] holds f.x <> x;
A21: A /\ B = {}
proof
set x = the Element of A /\ B;
assume
A22: A /\ B <> {};
then
x in A by XBOOLE_0:def 4;
then
A23: ex z being Real st z = x & z in [.0,1.] & F.z in [.0,z.];
reconsider x as Real;
x in B by A22,XBOOLE_0:def 4;
then ex b0 being Real st b0 = x & b0 in [.0,1.] & F.b0 in [.b0,1.];
then
A24: F.x in [.0,x.] /\ [.x,1.] by A23,XBOOLE_0:def 4;
x in {q where q is Real: 0<=q & q<=1 } by A23,RCOMP_1:def 1;
then ex u being Real st u = x & 0<=u & u<=1;
then F.x in {x} by A24,XXREAL_1:418;
then F.x = x by TARSKI:def 1;
hence contradiction by A20,A23,BORSUK_1:40;
end;
then
A25: A misses B by XBOOLE_0:def 7;
[.0,1.] = dom F by A6,FUNCT_2:def 1;
then F.1 in rng F by A17,FUNCT_1:def 3;
then
A26: 1 in A by A17;
ex P,Q being Subset of I[01] st [#] I[01] = P \/ Q & P <> {}I[01] & Q
<> {}I[01] & P is closed & Q is closed & P misses Q
proof
reconsider P = A, Q = B as Subset of I[01] by A2,A18,BORSUK_1:40;
take P,Q;
thus
A27: [#]I[01] = P \/ Q by A9,BORSUK_1:40,XBOOLE_0:def 10;
thus P <> {}I[01] & Q <> {}I[01] by A26,A7;
thus P is closed
proof
set z = the Element of (Cl P) /\ Q;
assume not P is closed;
then
A28: Cl P <> P by PRE_TOPC:22;
A29: (Cl P) /\ Q <> {}
proof
assume (Cl P) /\ Q = {};
then (Cl P) misses Q by XBOOLE_0:def 7;
then
A30: Cl P c= Q` by SUBSET_1:23;
P c= Cl P & P = Q` by A25,A27,PRE_TOPC:5,18;
hence contradiction by A28,A30,XBOOLE_0:def 10;
end;
then
A31: z in Cl P by XBOOLE_0:def 4;
A32: z in Q by A29,XBOOLE_0:def 4;
reconsider z as Point of I[01] by A31;
reconsider t0 = z as Real;
A33: ex c being Real st c = t0 & c in [.0,1.] & F.c in [.c,1.] by A32;
then reconsider s0 = F.t0 as Real;
t0 <= s0 by A33,XXREAL_1:1;
then
A34: 0 <= s0 - t0 by XREAL_1:48;
set r = (s0 - t0) * 2";
reconsider m = z, n = f.z as Point of Closed-Interval-MSpace(0,1) by
BORSUK_1:40,TOPMETR:10;
reconsider W = Ball(n,r) as Subset of I[01] by BORSUK_1:40,TOPMETR:10;
A35: W is open & f is_continuous_at z by A1,TMAP_1:50,TOPMETR:14,20;
A36: s0 - t0 <> 0 by A20;
then
A37: 0 / 2 < (s0 - t0) / 2 by A34,XREAL_1:74;
then f.z in W by TBSP_1:11;
then consider V being Subset of I[01] such that
A38: V is open & z in V and
A39: f.:V c= W by A35,TMAP_1:43;
consider s being Real such that
A40: s > 0 and
A41: Ball(m,s) c= V by A1,A38,TOPMETR:15,20;
reconsider s as Real;
set r0 = min(s,r);
reconsider W0 = Ball(m,r0) as Subset of I[01] by BORSUK_1:40,TOPMETR:10;
r0 > 0 by A37,A40,XXREAL_0:15;
then
A42: z in W0 by TBSP_1:11;
set w = the Element of P /\ W0;
W0 is open by A1,TOPMETR:14,20;
then P meets W0 by A31,A42,PRE_TOPC:24;
then
A43: P /\ W0 <> {}I[01] by XBOOLE_0:def 7;
then
A44: w in P by XBOOLE_0:def 4;
A45: w in W0 by A43,XBOOLE_0:def 4;
then reconsider w as Point of Closed-Interval-MSpace(0,1);
reconsider w1 = w as Point of I[01] by A44;
reconsider d = w1 as Real;
A46: d in A by A43,XBOOLE_0:def 4;
Ball(m,r0) = {q where q is Element of Closed-Interval-MSpace(0,1):
dist(m,q)<r0} by METRIC_1:17;
then r0 <= r & ex p being Element of Closed-Interval-MSpace(0,1) st p =
w & dist( m,p)<r0 by A45,XXREAL_0:17;
then dist(w,m) < r by XXREAL_0:2;
then
A47: |.d - t0.| < r by HEINE:1;
d - t0 <= |.d - t0.| by ABSVALUE:4;
then t0 + r = s0 - r & d - t0 < r by A47,XXREAL_0:2;
then
A48: d < s0 - r by XREAL_1:19;
A49: r < (s0 - t0) * 1 by A34,A36,XREAL_1:68;
A50: Ball(n,r) c= [.t0,1.]
proof
let x be object;
assume
A51: x in Ball(n,r);
then reconsider u = x as Point of Closed-Interval-MSpace(0,1);
x in [.0,1.] by A4,A51;
then reconsider t = x as Real;
Ball(n,r)= {q where q is Element of Closed-Interval-MSpace(0,1):
dist(n,q)<r} by METRIC_1:17;
then
ex p being Element of Closed-Interval-MSpace(0,1) st p = u & dist
(n,p)<r by A51;
then |.s0 - t.| < r by HEINE:1;
then
A52: |.s0 - t.| < s0 - t0 by A49,XXREAL_0:2;
s0 - t <= |.s0 - t.| by ABSVALUE:4;
then s0 - t < s0 - t0 by A52,XXREAL_0:2;
then
A53: t0 <= t by XREAL_1:10;
t <= 1 by A4,A51,XXREAL_1:1;
then t in {q where q is Real: t0<=q & q<=1 } by A53;
hence thesis by RCOMP_1:def 1;
end;
A54: Ball(n,r) c= [.d,1.]
proof
let x be object;
assume
A55: x in Ball(n,r);
then reconsider v = x as Point of Closed-Interval-MSpace(0,1);
x in [.0,1.] by A4,A55;
then reconsider t = x as Real;
Ball(n,r)= {q where q is Element of Closed-Interval-MSpace(0,1):
dist(n,q)<r} by METRIC_1:17;
then ex p being Element of Closed-Interval-MSpace(0,1) st p = v &
dist(n,p)<r by A55;
then
A56: |.s0 - t.| < r by HEINE:1;
A57: now
per cases;
suppose
t <= s0;
then 0 <= s0 - t by XREAL_1:48;
then s0 - t < r by A56,ABSVALUE:def 1;
then s0 < r + t by XREAL_1:19;
then s0 - r < t by XREAL_1:19;
hence d < t by A48,XXREAL_0:2;
end;
suppose
A58: s0 < t;
s0 - r < s0 by A37,XREAL_1:44;
then d < s0 by A48,XXREAL_0:2;
hence d < t by A58,XXREAL_0:2;
end;
end;
t <= 1 by A50,A55,XXREAL_1:1;
then t in {w0 where w0 is Real: d<=w0 & w0<=1} by A57;
hence thesis by RCOMP_1:def 1;
end;
Ball(m,r0) c= Ball(m,s) by PCOMPS_1:1,XXREAL_0:17;
then W0 c= V by A41;
then f.w1 in f.:V by A45,FUNCT_2:35;
then f.w1 in W by A39;
then d in B by A54,BORSUK_1:40;
hence contradiction by A25,A46,XBOOLE_0:3;
end;
thus Q is closed
proof
set z = the Element of (Cl Q) /\ P;
assume not Q is closed;
then
A59: Cl Q <> Q by PRE_TOPC:22;
A60: (Cl Q) /\ P <> {}
proof
assume (Cl Q) /\ P = {};
then (Cl Q) misses P by XBOOLE_0:def 7;
then
A61: Cl Q c= P` by SUBSET_1:23;
Q c= Cl Q & Q = P` by A25,A27,PRE_TOPC:5,18;
hence contradiction by A59,A61,XBOOLE_0:def 10;
end;
then
A62: z in Cl Q by XBOOLE_0:def 4;
A63: z in P by A60,XBOOLE_0:def 4;
reconsider z as Point of I[01] by A62;
reconsider t0 = z as Real;
A64: ex c being Real st c = t0 & c in [.0,1.] & F.c in [.0,c.] by A63;
then reconsider s0 = F.t0 as Real;
s0 <= t0 by A64,XXREAL_1:1;
then
A65: 0 <= t0 - s0 by XREAL_1:48;
set r = (t0 - s0) * 2";
reconsider m = z, n = f.z as Point of Closed-Interval-MSpace(0,1) by
BORSUK_1:40,TOPMETR:10;
reconsider W = Ball(n,r) as Subset of I[01] by BORSUK_1:40,TOPMETR:10;
A66: W is open & f is_continuous_at z by A1,TMAP_1:50,TOPMETR:14,20;
A67: t0 - s0 <> 0 by A20;
then
A68: 0 / 2 < (t0 - s0) / 2 by A65,XREAL_1:74;
then f.z in W by TBSP_1:11;
then consider V being Subset of I[01] such that
A69: V is open & z in V and
A70: f.:V c= W by A66,TMAP_1:43;
consider s being Real such that
A71: s > 0 and
A72: Ball(m,s) c= V by A1,A69,TOPMETR:15,20;
reconsider s as Real;
set r0 = min(s,r);
reconsider W0 = Ball(m,r0) as Subset of I[01] by BORSUK_1:40,TOPMETR:10;
r0 > 0 by A68,A71,XXREAL_0:15;
then
A73: z in W0 by TBSP_1:11;
set w = the Element of Q /\ W0;
W0 is open by A1,TOPMETR:14,20;
then Q meets W0 by A62,A73,PRE_TOPC:24;
then
A74: Q /\ W0 <> {}I[01] by XBOOLE_0:def 7;
then
A75: w in Q by XBOOLE_0:def 4;
A76: w in W0 by A74,XBOOLE_0:def 4;
then reconsider w as Point of Closed-Interval-MSpace(0,1);
reconsider w1 = w as Point of I[01] by A75;
reconsider d = w1 as Real;
A77: d in B by A74,XBOOLE_0:def 4;
Ball(m,r0) = {q where q is Element of Closed-Interval-MSpace(0,1):
dist(m,q)<r0} by METRIC_1:17;
then r0 <= r & ex p being Element of Closed-Interval-MSpace(0,1) st p =
w & dist( m,p)<r0 by A76,XXREAL_0:17;
then dist(m,w) < r by XXREAL_0:2;
then
A78: |.t0 - d.| < r by HEINE:1;
t0 - d <= |.t0 - d.| by ABSVALUE:4;
then t0 + - d < r by A78,XXREAL_0:2;
then t0 < r - (-d) by XREAL_1:20;
then s0 + r = t0 - r & t0 < r + - (-d);
then
A79: s0 + r < d by XREAL_1:19;
A80: r < (t0 - s0) * 1 by A65,A67,XREAL_1:68;
A81: Ball(n,r) c= [.0,t0.]
proof
let x be object;
assume
A82: x in Ball(n,r);
then reconsider u = x as Point of Closed-Interval-MSpace(0,1);
x in [.0,1.] by A4,A82;
then reconsider t = x as Real;
Ball(n,r)={q where q is Element of Closed-Interval-MSpace(0,1):
dist(n,q)<r} by METRIC_1:17;
then ex p being Element of Closed-Interval-MSpace(0,1) st p = u &
dist(n,p)<r by A82;
then |.t - s0.| < r by HEINE:1;
then
A83: |.t - s0.| < t0 - s0 by A80,XXREAL_0:2;
t - s0 <= |.t - s0.| by ABSVALUE:4;
then t - s0 < t0 - s0 by A83,XXREAL_0:2;
then
A84: t <= t0 by XREAL_1:9;
0 <= t by A4,A82,XXREAL_1:1;
then t in {q where q is Real: 0<=q & q<=t0 } by A84;
hence thesis by RCOMP_1:def 1;
end;
A85: Ball(n,r) c= [.0,d.]
proof
let x be object;
assume
A86: x in Ball(n,r);
then reconsider v = x as Point of Closed-Interval-MSpace(0,1);
x in [.0,1.] by A4,A86;
then reconsider t = x as Real;
Ball(n,r)= {q where q is Element of Closed-Interval-MSpace(0,1):
dist(n,q)<r} by METRIC_1:17;
then ex p being Element of Closed-Interval-MSpace(0,1) st p = v &
dist(n,p)<r by A86;
then
A87: |.t - s0.| < r by HEINE:1;
A88: now
per cases;
suppose
s0 <= t;
then 0 <= t - s0 by XREAL_1:48;
then t - s0 < r by A87,ABSVALUE:def 1;
then t < s0 + r by XREAL_1:19;
hence t < d by A79,XXREAL_0:2;
end;
suppose
A89: t < s0;
s0 < s0 + r by A68,XREAL_1:29;
then s0 < d by A79,XXREAL_0:2;
hence t < d by A89,XXREAL_0:2;
end;
end;
0 <= t by A81,A86,XXREAL_1:1;
then t in {w0 where w0 is Real: 0<=w0 & w0<=d} by A88;
hence thesis by RCOMP_1:def 1;
end;
Ball(m,r0) c= Ball(m,s) by PCOMPS_1:1,XXREAL_0:17;
then W0 c= V by A72;
then f.w1 in f.:V by A76,FUNCT_2:35;
then f.w1 in W by A70;
then d in A by A85,BORSUK_1:40;
hence contradiction by A25,A77,XBOOLE_0:3;
end;
thus thesis by A21,XBOOLE_0:def 7;
end;
hence contradiction by Th19,CONNSP_1:10;
end;
theorem Th22:
a <= b implies for f being continuous Function of
Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(a,b)
ex x being Point of Closed-Interval-TSpace(a,b) st f.x = x
proof
assume
A1: a <= b;
let f be continuous Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(a,b);
now
per cases by A1,XXREAL_0:1;
suppose
A2: a < b;
set L = L[01]((#)(a,b),(a,b)(#)), P = P[01](a,b,(#)(0,1),(0,1)(#));
A3: P is continuous Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(0,1) by A2,Th12;
set g = (P * f) * L;
A4: id Closed-Interval-TSpace(a,b) = L * P by A2,Th15;
then
A5: f = (L * P) * f by FUNCT_2:17
.= L * (P * f) by RELAT_1:36
.= L * ((P * f) * (L * P)) by A4,FUNCT_2:17
.= L * (g * P) by RELAT_1:36
.= (L * g) * P by RELAT_1:36;
L is continuous Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(a,b) by A1,Th8;
then consider y be Point of Closed-Interval-TSpace(0,1) such that
A6: g.y = y by A3,Th21,TOPMETR:20;
A7: id Closed-Interval-TSpace(0,1) = P * L by A2,Th15;
now
take x = L.y;
thus f.x = (((L * g) * P) * L).y by A5,FUNCT_2:15
.= ((L * g) *(id Closed-Interval-TSpace(0,1))).y by A7,RELAT_1:36
.= (L * g).y by FUNCT_2:17
.= x by A6,FUNCT_2:15;
end;
hence thesis;
end;
suppose
A8: a = b;
then [.a,b.] = {a} & a = (#)(a,b) by Def1,XXREAL_1:17;
then
A9: the carrier of Closed-Interval-TSpace(a,b) = {(#)(a,b)} by A8,TOPMETR:18;
now
take x = (#)(a,b);
thus f.x = x by A9,TARSKI:def 1;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th23:
for X, Y being non empty SubSpace of R^1, f being continuous Function of X,Y
holds
(ex a,b being Real st a <= b & [.a,b.] c= the carrier of X &
[.a,b.] c= the carrier of Y & f.:[.a,b.] c= [.a,b.]) implies
ex x being Point of X st f.x = x
proof
let X, Y be non empty SubSpace of R^1, f be continuous Function of X,Y;
given a,b being Real such that
A1: a <= b and
A2: [.a,b.] c= the carrier of X and
A3: [.a,b.] c= the carrier of Y and
A4: f.:[.a,b.] c= [.a,b.];
reconsider A = [.a,b.] as non empty Subset of X by A1,A2,XXREAL_1:1;
A5: dom(f|A) = (dom f) /\ A by RELAT_1:61;
A = (the carrier of X) /\ A & dom f = the carrier of X by FUNCT_2:def 1
,XBOOLE_1:28;
then
A6: dom(f|A) = the carrier of Closed-Interval-TSpace(a,b) by A1,A5,TOPMETR:18;
A7: A = the carrier of Closed-Interval-TSpace(a,b) by A1,TOPMETR:18;
then reconsider Z = Closed-Interval-TSpace(a,b) as SubSpace of X by TSEP_1:4;
rng(f|A) c= the carrier of Closed-Interval-TSpace(a,b) by A4,A7,RELAT_1:115;
then reconsider g = f|A as Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(a,b) by A6,FUNCT_2:def 1,RELSET_1:4;
A8: Z is SubSpace of Y by A3,A7,TSEP_1:4;
for s being Point of Closed-Interval-TSpace(a,b) holds g is_continuous_at s
proof
let s be Point of Closed-Interval-TSpace(a,b);
reconsider w = s as Point of X by A7,TARSKI:def 3;
for G being Subset of Closed-Interval-TSpace(a,b) st G is open & g.s
in G ex H being Subset of Z st H is open & s in H & g.:H c= G
proof
let G be Subset of Closed-Interval-TSpace(a,b);
A9: f is_continuous_at w by TMAP_1:44;
assume G is open;
then consider G0 being Subset of Y such that
A10: G0 is open and
A11: G0 /\ [#] Closed-Interval-TSpace(a,b) = G by A8,TOPS_2:24;
assume g.s in G;
then f.w in G by A7,FUNCT_1:49;
then f.w in G0 by A11,XBOOLE_0:def 4;
then consider H0 being Subset of X such that
A12: H0 is open and
A13: w in H0 and
A14: f.:H0 c= G0 by A10,A9,TMAP_1:43;
now
reconsider H = H0 /\ [#] Closed-Interval-TSpace(a,b) as Subset of Z;
take H;
thus H is open by A12,TOPS_2:24;
thus s in H by A13,XBOOLE_0:def 4;
thus g.:H c= G
proof
let t be object;
assume t in g.:H;
then consider r be object such that
r in dom g and
A15: r in H and
A16: t = g.r by FUNCT_1:def 6;
A17: r in the carrier of Z by A15;
reconsider r as Point of Closed-Interval-TSpace(a,b) by A15;
r in dom g by A17,FUNCT_2:def 1;
then
A18: t in g.:(the carrier of Z) by A16,FUNCT_1:def 6;
reconsider p = r as Point of X by A7,TARSKI:def 3;
p in [#] X;
then
A19: p in dom f by FUNCT_2:def 1;
t=f.p & p in H0 by A7,A15,A16,FUNCT_1:49,XBOOLE_0:def 4;
then t in f.:H0 by A19,FUNCT_1:def 6;
hence thesis by A11,A14,A18,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
hence thesis by TMAP_1:43;
end;
then reconsider h = g as continuous Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(a,b) by TMAP_1:44;
now
consider y being Point of Closed-Interval-TSpace(a,b) such that
A20: h.y = y by A1,Th22;
reconsider x = y as Point of X by A7,TARSKI:def 3;
take x;
thus f.x = x by A7,A20,FUNCT_1:49;
end;
hence thesis;
end;
::$N Brouwer Fixed Point Theorem for Intervals
theorem
for X, Y being non empty SubSpace of R^1, f being continuous Function of X,Y
holds
(ex a,b being Real st a <= b & [.a,b.] c= the carrier of X &
f.:[.a,b.] c= [.a,b.]) implies
ex x being Point of X st f.x = x
proof
let X, Y be non empty SubSpace of R^1, f be continuous Function of X,Y;
given a,b being Real such that
A1: a <= b and
A2: [.a,b.] c= the carrier of X and
A3: f.:[.a,b.] c= [.a,b.];
set g = (Y incl R^1) * f;
the carrier of Y c= the carrier of R^1 by BORSUK_1:1;
then reconsider B = f.:[.a,b.] as Subset of R^1 by XBOOLE_1:1;
g.:[.a,b.] = (Y incl R^1).:(f.:[.a,b.]) by RELAT_1:126;
then g.:[.a,b.] = ((id R^1)|Y).:B by TMAP_1:def 6;
then g.:[.a,b.] = (id R^1).:B by TMAP_1:55;
then
A4: g.:[.a,b.] c= [.a,b.] by A3,FUNCT_1:92;
A5: (Y incl R^1) is continuous Function of Y,R^1 & R^1 is SubSpace of R^1 by
TMAP_1:87,TSEP_1:2;
the carrier of X c= the carrier of R^1 by BORSUK_1:1;
then
A6: [.a,b.] c= the carrier of R^1 by A2;
now
consider x being Point of X such that
A7: g.x = x by A1,A2,A5,A6,A4,Th23;
the carrier of Y c= the carrier of R^1 by BORSUK_1:1;
then reconsider y = f.x as Point of R^1;
take x;
thus f.x = (Y incl R^1).y by TMAP_1:84
.= x by A7,FUNCT_2:15;
end;
hence thesis;
end;