:: Miscellaneous { I }
:: by Andrzej Trybulec
::
:: Received August 28, 2000
:: Copyright (c) 2000-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, XBOOLE_0, SUBSET_1, XXREAL_1, ARYTM_3, REAL_1, XXREAL_0,
COMPLEX1, ARYTM_1, CARD_1, FUNCT_1, MCART_1, ZFMISC_1, PRE_TOPC, RCOMP_1,
TARSKI, STRUCT_0, SETFAM_1, SEQ_1, RELAT_1, VALUED_0, SEQ_2, ORDINAL2,
RELAT_2, PSCOMP_1, LIMFUNC1, CONNSP_1, METRIC_1, SEQ_4, XXREAL_2,
TOPMETR, NAT_1, VALUED_1, EUCLID, MEASURE5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, FUNCT_1,
COMPLEX1, RELSET_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, REAL_1, XXREAL_1, XXREAL_2, NAT_1, VALUED_1, SEQ_1, SEQ_2,
SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1, BORSUK_1, MEASURE5, MEASURE6,
PSCOMP_1, VALUED_0, METRIC_1, TBSP_1, TOPMETR, LIMFUNC1, CONNSP_1,
RLTOPSP1, EUCLID, RECDEF_1, RCOMP_1;
constructors REAL_1, COMPLEX1, PROB_1, LIMFUNC1, BINARITH, CONNSP_1, COMPTS_1,
TBSP_1, TOPMETR, MEASURE6, INTEGRA1, RECDEF_1, SEQ_4, PSCOMP_1, COMSEQ_2,
XTUPLE_0;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
STRUCT_0, PRE_TOPC, COMPTS_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1,
MEASURE6, JORDAN2C, BORSUK_3, INTEGRA1, VALUED_1, FUNCT_2, XXREAL_2,
VALUED_0, FCONT_3, PSCOMP_1, MEASURE5, JORDAN5A, XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RCOMP_1, XBOOLE_0, XXREAL_2;
equalities RCOMP_1, XBOOLE_0, SUBSET_1, PROB_1, LIMFUNC1;
expansions TARSKI, XBOOLE_0, XXREAL_2;
theorems ZFMISC_1, TARSKI, SUBSET_1, FUNCT_2, FUNCT_1, RCOMP_1, SEQ_4, SEQM_3,
ABSVALUE, PSCOMP_1, GOBOARD7, BORSUK_1, TOPMETR, JORDAN6, UNIFORM1,
RELAT_1, SEQ_2, TOPREAL6, TSP_1, SEQ_1, CONNSP_1, XREAL_0, TSEP_1,
XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, JORDAN2C, PRE_TOPC, TOPREAL3,
METRIC_6, XXREAL_0, XXREAL_1, XXREAL_2, VALUED_0, MEASURE6, MEASURE5,
JORDAN5A, XTUPLE_0, ORDINAL1;
schemes FUNCT_2;
begin :: Preliminaries
scheme
NonEmpty{ A()-> non empty set, F(object)-> set}:
the set of all F(a) where a is Element of A() is non empty;
consider a0 being object such that
A1: a0 in A() by XBOOLE_0:def 1;
F(a0) in the set of all F(a) where a is Element of A() by A1;
hence thesis;
end;
reserve
r,s,r0,s0,t for Real;
theorem Th1:
for a,b being Real st r in [.a,b.] & s in [.a,b.] holds (r
+ s)/2 in [.a,b.]
proof
let a,b be Real such that
A1: r in [.a,b.] and
A2: s in [.a,b.];
reconsider a,b,r,s as Real;
A3: s <= b by A2,XXREAL_1:1;
r <= b by A1,XXREAL_1:1;
then r+s <= b+b by A3,XREAL_1:7;
then
A4: (r+s)/2 <= (b+b)/2 by XREAL_1:72;
A5: a <= s by A2,XXREAL_1:1;
a <= r by A1,XXREAL_1:1;
then a+a <= r+s by A5,XREAL_1:7;
then (a+a)/2 <= (r+s)/2 by XREAL_1:72;
hence thesis by A4;
end;
theorem Th2:
|.|.r0-s0.|-|.r-s.|.| <= |.r0-r.| + |.s0-s.|
proof
r0-s0 - (r-s) = r0-r - (s0-s);
then
A1: |.r0-s0 - (r-s).| <= |.r0-r.| + |.s0-s.| by COMPLEX1:57;
|.|.r0-s0.| - |.r-s.|.| <= |.r0-s0 - (r-s).| by COMPLEX1:64;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th3:
t in ].r,s.[ implies |.t.| < max(|.r.|,|.s.|)
proof
assume
A1: t in ].r,s.[;
reconsider r,t,s as Real;
A2: r < t by A1,XXREAL_1:4;
A3: t < s by A1,XXREAL_1:4;
per cases;
suppose
A4: t >= 0;
then t = |.t.| by ABSVALUE:def 1;
then |.t.| < |.s.| by A3,A4,ABSVALUE:def 1;
hence thesis by XXREAL_0:30;
end;
suppose
A5: t < 0;
then
A6: -t = |.t.| by ABSVALUE:def 1;
-r =|.r.| by A2,A5,ABSVALUE:def 1;
then |.t.| < |.r.| by A2,A6,XREAL_1:24;
hence thesis by XXREAL_0:30;
end;
end;
scheme
DoubleChoice{ A,B,C() -> non empty set, P[object,object,object]}:
ex a being Function
of A(), B(), b being Function of A(), C() st for i being Element of A() holds P
[i,a.i,b.i]
provided
A1: for i being Element of A() ex ai being Element of B(), bi being
Element of C() st P[i,ai,bi]
proof
defpred P1[object,object] means P[$1,($2)`1,($2)`2];
A2: for e being Element of A() ex u being Element of [:B(),C():] st P1[e,u]
proof
let e be Element of A();
consider ai being Element of B(), bi being Element of C() such that
A3: P[e,ai,bi] by A1;
reconsider u = [ai,bi] as Element of [:B(),C():] by ZFMISC_1:87;
take u;
thus thesis by A3;
end;
consider f being Function of A(), [:B(),C():] such that
A4: for e being Element of A() holds P1[e,f.e] from FUNCT_2:sch 3(A2);
take pr1 f, pr2 f;
let i be Element of A();
A5: (f.i)`2 = (pr2 f).i by FUNCT_2:def 6;
(f.i)`1 = (pr1 f).i by FUNCT_2:def 5;
hence thesis by A4,A5;
end;
theorem Th4:
for S,T being non empty TopSpace, G being Subset of [:S,T:] st
for x being Point of [:S,T:] st x in G ex GS being Subset of S, GT being Subset
of T st GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G holds G is
open
proof
let S,T be non empty TopSpace, G being Subset of [:S,T:] such that
A1: for x being Point of [:S,T:] st x in G ex GS being Subset of S, GT
being Subset of T st GS is open & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G;
set A = {[:GS,GT:] where GS is Subset of S, GT is Subset of T : GS is open &
GT is open & [:GS,GT:] c= G };
A c= bool the carrier of [:S,T:]
proof
let e be object;
assume e in A;
then
ex GS being Subset of S, GT being Subset of T st e = [:GS, GT:] & GS
is open & GT is open & [:GS,GT:] c= G;
hence thesis;
end;
then reconsider A as Subset-Family of [:S,T:];
reconsider A as Subset-Family of [:S,T:];
for x being object holds x in G iff ex Y being set st x in Y & Y in A
proof
let x be object;
thus x in G implies ex Y being set st x in Y & Y in A
proof
assume x in G;
then consider GS being Subset of S, GT being Subset of T such that
A2: GS is open and
A3: GT is open and
A4: x in [:GS,GT:] and
A5: [:GS,GT:] c= G by A1;
take [:GS,GT:];
thus thesis by A2,A3,A4,A5;
end;
given Y being set such that
A6: x in Y and
A7: Y in A;
ex GS being Subset of S, GT being Subset of T st Y = [:GS,GT:] & GS
is open & GT is open & [:GS,GT:] c= G by A7;
hence thesis by A6;
end;
then
A8: G = union A by TARSKI:def 4;
for e being set st e in A ex X1 being Subset of S, Y1 being Subset of T
st e = [:X1,Y1:] & X1 is open & Y1 is open
proof
let e be set;
assume e in A;
then ex GS being Subset of S, GT being Subset of T st e = [:GS,GT:] & GS
is open & GT is open & [:GS,GT:] c= G;
hence thesis;
end;
hence thesis by A8,BORSUK_1:5;
end;
begin :: topological properties of sets of real numbers
theorem Th5:
for A,B being compact Subset of REAL holds A /\ B is compact
proof
let A,B be compact Subset of REAL;
let s1 be Real_Sequence such that
A1: rng s1 c= A /\ B;
A2: A /\ B c= B by XBOOLE_1:17;
A /\ B c= A by XBOOLE_1:17;
then rng s1 c= A by A1;
then consider s2 being Real_Sequence such that
A3: s2 is subsequence of s1 and
A4: s2 is convergent and
A5: lim s2 in A by RCOMP_1:def 3;
rng s2 c= rng s1 by A3,VALUED_0:21;
then rng s2 c= A /\ B by A1;
then rng s2 c= B by A2;
then consider s3 being Real_Sequence such that
A6: s3 is subsequence of s2 and
A7: s3 is convergent and
A8: lim s3 in B by RCOMP_1:def 3;
take s3;
thus s3 is subsequence of s1 by A3,A6,VALUED_0:20;
thus s3 is convergent by A7;
lim s3 = lim s2 by A4,A6,SEQ_4:17;
hence thesis by A5,A8,XBOOLE_0:def 4;
end;
theorem
for T being non empty TopSpace for f being continuous RealMap of T for
A being Subset of T st A is connected holds f.:A is interval
proof
let T be non empty TopSpace;
let f be continuous RealMap of T;
let A be Subset of T;
assume
A1: A is connected;
let r,s be ExtReal;
A2: A c= f"(f.:A) by FUNCT_2:42;
assume
A3: r in f.:A;
then consider p being Point of T such that
A4: p in A and
A5: r = f.p by FUNCT_2:65;
assume
A6: s in f.:A;
then consider q being Point of T such that
A7: q in A and
A8: s = f.q by FUNCT_2:65;
assume
A9: not [.r,s.] c= f.:A;
reconsider r,s as Real by A3,A6;
consider t being Element of REAL such that
A10: t in [.r,s.] and
A11: not t in f.:A by A9;
reconsider r,s,t as Real;
set P1 = f"left_open_halfline t, Q1 = f"right_open_halfline t, P = P1 /\ A,
Q = Q1 /\ A, X = left_open_halfline t \/ right_open_halfline t;
A12: Q1 is open by PSCOMP_1:8;
t <= s by A10,XXREAL_1:1;
then
A13: t < s by A6,A11,XXREAL_0:1;
right_open_halfline t = {r1 where r1 is Real: t < r1}
by XXREAL_1:230;
then s in right_open_halfline t by A13;
then q in Q1 by A8,FUNCT_2:38;
then
A14: Q <> {}T by A7,XBOOLE_0:def 4;
left_open_halfline t /\ right_open_halfline t = ].t,t.[ by XXREAL_1:269
.= {} by XXREAL_1:28;
then left_open_halfline t misses right_open_halfline t;
then P1 misses Q1 by FUNCT_1:71;
then P1 /\ Q1 = {};
then
A15: P1 /\ Q1 misses P \/ Q;
reconsider Y = {t} as Subset of REAL;
Y` = REAL \ [.t,t.] by XXREAL_1:17
.= X by XXREAL_1:385;
then
A16: (f"Y)` = f"X by FUNCT_2:100
.= P1 \/ Q1 by RELAT_1:140;
f"{t} misses f"(f.:A) by A11,FUNCT_1:71,ZFMISC_1:50;
then f"{t} misses A by A2,XBOOLE_1:63;
then A c= P1 \/ Q1 by A16,SUBSET_1:23;
then
A17: A = A /\ (P1 \/ Q1) by XBOOLE_1:28
.= P \/ Q by XBOOLE_1:23;
A18: P c= P1 by XBOOLE_1:17;
r <= t by A10,XXREAL_1:1;
then
A19: r < t by A3,A11,XXREAL_0:1;
left_open_halfline t = {r1 where r1 is Real: r1 < t} by XXREAL_1:229;
then r in left_open_halfline t by A19;
then p in P1 by A5,FUNCT_2:38;
then
A20: P <> {}T by A4,XBOOLE_0:def 4;
A21: Q c= Q1 by XBOOLE_1:17;
P1 is open by PSCOMP_1:8;
then P,Q are_separated by A12,A18,A21,A15,TSEP_1:45;
hence contradiction by A1,A17,A20,A14,CONNSP_1:15;
end;
definition
let A,B be Subset of REAL;
func dist(A,B) -> Real means
:Def1:
ex X being Subset of REAL st X =
{|.r-s.| where r, s is Real : r in A & s in B}
& it = lower_bound X;
existence
proof
set Y = {|.r-s.| where r, s is Real : r
in A & s in B};
Y c= REAL
proof
let e be object;
assume e in Y;
then ex r,s being Real st e = |.r-s.| & r in A & s in B;
hence thesis by XREAL_0:def 1;
end;
then reconsider Y0 = Y as Subset of REAL;
take lower_bound Y0;
thus thesis;
end;
uniqueness;
commutativity
proof
let IT be Real, A,B be Subset of REAL;
given X0 being Subset of REAL such that
A1: X0 = {|.r-s.| where r,s is Real: r in A & s in B} and
A2: IT = lower_bound X0;
set Y = {|.r-s.| where r, s is Real : r in B & s in A};
Y c= REAL
proof
let e be object;
assume e in Y;
then ex r,s being Real st e = |.r-s.| & r in B & s in A;
hence thesis by XREAL_0:def 1;
end;
then reconsider Y0 = Y as Subset of REAL;
take Y0;
thus Y0 = {|.r-s.| where r, s is Real : r
in B & s in A};
X0 = Y0
proof
thus X0 c= Y0
proof
let x be object;
assume x in X0;
then consider r,s being Real such that
A3: x = |.r-s.| and
A4: r in A and
A5: s in B by A1;
x = |.s-r.| by A3,UNIFORM1:11;
hence thesis by A4,A5;
end;
let x be object;
assume x in Y0;
then consider r,s being Real such that
A6: x = |.r-s.| and
A7: r in B and
A8: s in A;
x = |.s-r.| by A6,UNIFORM1:11;
hence thesis by A1,A7,A8;
end;
hence thesis by A2;
end;
end;
theorem Th7:
for A,B being Subset of REAL, r, s st r in A & s in B holds
|.r-s.| >= dist(A,B)
proof
let A,B be Subset of REAL;
set Y = {|.r-s.| where r, s is Real : r in A & s in B};
let r,s;
assume that
A1: r in A and
A2: s in B;
Y c= REAL
proof
let e be object;
assume e in Y;
then ex r,s being Real st e = |.r-s.| & r in A & s in B;
hence thesis by XREAL_0:def 1;
end;
then reconsider Y0 = Y as Subset of REAL;
A3: Y0 is bounded_below
proof
take 0;
let r0 be ExtReal;
assume r0 in Y0;
then ex r,s being Real st r0 = |.r-s.| & r in A & s in B;
hence thesis by COMPLEX1:46;
end;
A4: dist(A,B) = lower_bound Y0 by Def1;
|.r-s.| in Y0 by A1,A2;
hence thesis by A4,A3,SEQ_4:def 2;
end;
theorem Th8:
for A,B being Subset of REAL, C,D being non empty Subset of REAL
st C c= A & D c= B holds dist(A,B) <= dist(C,D)
proof
let A,B be Subset of REAL, C,D be non empty Subset of REAL such that
A1: C c= A and
A2: D c= B;
consider s0 being object such that
A3: s0 in D by XBOOLE_0:def 1;
set Y = {|.r-s.| where r, s is Real : r in
C & s in D};
consider r0 being object such that
A4: r0 in C by XBOOLE_0:def 1;
A5: Y c= REAL
proof
let e be object;
assume e in Y;
then ex r,s being Real st e = |.r-s.| & r in C & s in D;
hence thesis by XREAL_0:def 1;
end;
reconsider r0,s0 as Real by A4,A3;
|.r0-s0.| in Y by A4,A3;
then reconsider Y as non empty Subset of REAL by A5;
set X = {|.r-s.| where r, s is Real : r in
A & s in B};
X c= REAL
proof
let e be object;
assume e in X;
then ex r,s being Real st e = |.r-s.| & r in A & s in B;
hence thesis by XREAL_0:def 1;
end;
then reconsider X as Subset of REAL;
A6: Y c= X
proof
let x be object;
assume x in Y;
then ex r,s being Real st x = |.r-s.| & r in C & s in D;
hence thesis by A1,A2;
end;
A7: X is bounded_below
proof
take 0;
let r0 be ExtReal;
assume r0 in X;
then ex r,s being Real st r0 = |.r-s.| & r in A & s in B;
hence thesis by COMPLEX1:46;
end;
A8: dist(C,D) = lower_bound Y by Def1;
dist(A,B) = lower_bound X by Def1;
hence thesis by A7,A8,A6,SEQ_4:47;
end;
theorem Th9:
for A, B being non empty compact Subset of REAL ex r,s being
Real st r in A & s in B & dist(A,B) = |.r-s.|
proof
defpred P[set,set] means ex r,s being Real st $1 = [r,s] & $2 = |.r-s.|;
let A, B be non empty compact Subset of REAL;
reconsider At = A, Bt = B as non empty compact Subset of R^1 by JORDAN5A:25
,TOPMETR:17;
A1: the carrier of R^1|Bt = Bt by PRE_TOPC:8;
reconsider AB = [:R^1|At, R^1|Bt:] as compact non empty TopSpace;
A2: the carrier of R^1|At = At by PRE_TOPC:8;
A3: now
let x be Element of AB;
x in the carrier of AB;
then x in [:A,B:] by A2,A1,BORSUK_1:def 2;
then consider r,s being object such that
A4: r in REAL and
A5: s in REAL and
A6: x = [r,s] by ZFMISC_1:84;
reconsider r,s as Real by A4,A5;
reconsider t = |.r-s.| as Element of REAL by XREAL_0:def 1;
take t;
thus P[x,t] by A6;
end;
consider f being RealMap of AB such that
A7: for x being Element of AB holds P[x,f.x] from FUNCT_2:sch 3(A3);
for Y being Subset of REAL st Y is open holds f"Y is open
proof
let Y be Subset of REAL such that
A8: Y is open;
for x being Point of AB st x in f"Y ex YS being Subset of R^1|At, YT
being Subset of R^1|Bt st YS is open & YT is open & x in [:YS,YT:] & [:YS,YT:]
c= f"Y
proof
let x be Point of AB;
consider r,s being Real such that
A9: x = [r,s] and
A10: f.x = |.r-s.| by A7;
assume x in f"Y;
then f.x in Y by FUNCT_1:def 7;
then consider N being Neighbourhood of f.x such that
A11: N c= Y by A8,RCOMP_1:18;
consider g being Real such that
A12: 0 < g and
A13: N = ].f.x-g,f.x+g.[ by RCOMP_1:def 6;
reconsider a=r-g/2, b=r+g/2, c =s-g/2, d=s+g/2 as Real;
reconsider S = ].a,b.[, T = ].c,d.[ as Subset of R^1 by TOPMETR:17;
reconsider YT = T /\ B as Subset of R^1|Bt by A1,XBOOLE_1:17;
reconsider YS = S /\ A as Subset of R^1|At by A2,XBOOLE_1:17;
A14: s in T by A12,TOPREAL6:15,XREAL_1:215;
take YS, YT;
A15: T is open by JORDAN6:35;
S is open by JORDAN6:35;
hence YS is open & YT is open by A2,A1,A15,TSP_1:def 1;
A16: r in S by A12,TOPREAL6:15,XREAL_1:215;
x in the carrier of AB;
then
A17: x in [:A,B:] by A2,A1,BORSUK_1:def 2;
then s in B by A9,ZFMISC_1:87;
then
A18: s in YT by A14,XBOOLE_0:def 4;
f.:[:YS,YT:] c= N
proof
let e be object;
assume e in f.:[:YS,YT:];
then consider y being Element of AB such that
A19: y in [:YS,YT:] and
A20: e = f.y by FUNCT_2:65;
consider r1,s1 being Real such that
A21: y = [r1,s1] and
A22: f.y = |.r1-s1.| by A7;
A23: |.|.r1-s1.|-|.r-s.|.| <= |.r1-r.| + |.s1-s.| by Th2;
s1 in YT by A19,A21,ZFMISC_1:87;
then s1 in ].s-g/2,s+g/2.[ by XBOOLE_0:def 4;
then
A24: |.s1-s.| < g/2 by RCOMP_1:1;
r1 in YS by A19,A21,ZFMISC_1:87;
then r1 in ].r-g/2,r+g/2.[ by XBOOLE_0:def 4;
then
A25: |.r1-r.| < g/2 by RCOMP_1:1;
g = g/2 + g/2;
then |.r1-r.| + |.s1-s.| < g by A25,A24,XREAL_1:8;
then |.|.r1-s1.|-|.r-s.|.| < g by A23,XXREAL_0:2;
hence thesis by A13,A10,A20,A22,RCOMP_1:1;
end;
then
A26: f.:[:YS,YT:] c= Y by A11;
r in A by A9,A17,ZFMISC_1:87;
then r in YS by A16,XBOOLE_0:def 4;
hence x in [:YS,YT:] by A9,A18,ZFMISC_1:87;
dom f = the carrier of AB by FUNCT_2:def 1;
hence thesis by A26,FUNCT_1:93;
end;
hence thesis by Th4;
end;
then reconsider f as continuous RealMap of AB by PSCOMP_1:8;
f.:the carrier of AB is with_min by MEASURE6:def 13;
then lower_bound(f.:the carrier of AB) in f.:the carrier of AB
by MEASURE6:def 5;
then consider x being Element of AB such that
A27: x in the carrier of AB and
A28: lower_bound(f.:the carrier of AB) = f.x by FUNCT_2:65;
A29: x in [:A,B:] by A2,A1,A27,BORSUK_1:def 2;
then consider r1,s1 being object such that
A30: r1 in REAL and
A31: s1 in REAL and
A32: x = [r1,s1] by ZFMISC_1:84;
A33: f.:the carrier of AB =
{|.r-s.| where r, s is Real : r in A & s in B}
proof
hereby
let x be object;
assume x in f.:the carrier of AB;
then consider y being Element of AB such that
A34: y in the carrier of AB and
A35: x = f.y by FUNCT_2:65;
consider r1,s1 being Real such that
A36: y = [r1,s1] and
A37: f.y = |.r1-s1.| by A7;
A38: [r1,s1] in [:A,B:] by A2,A1,A34,A36,BORSUK_1:def 2;
then
A39: s1 in B by ZFMISC_1:87;
r1 in A by A38,ZFMISC_1:87;
hence
x in {|.r-s.| where r, s is Real :
r in A & s in B} by A35,A37,A39;
end;
let x be object;
assume x in {|.r-s.| where r, s is Real
: r in A & s in B};
then consider r,s being Real such that
A40: x = |.r-s.| and
A41: r in A and
A42: s in B;
[r,s] in [:A,B:] by A41,A42,ZFMISC_1:87;
then reconsider y = [r,s] as Element of AB by A2,A1,BORSUK_1:def 2;
consider r1,s1 being Real such that
A43: y = [r1,s1] and
A44: f.y = |.r1-s1.| by A7;
A45: s1 = s by A43,XTUPLE_0:1;
r1 = r by A43,XTUPLE_0:1;
hence thesis by A40,A44,A45,FUNCT_2:35;
end;
reconsider r1,s1 as Real by A30,A31;
take r1,s1;
thus r1 in A & s1 in B by A29,A32,ZFMISC_1:87;
consider r,s being Real such that
A46: x = [r,s] and
A47: f.x = |.r-s.| by A7;
A48: s1 = s by A32,A46,XTUPLE_0:1;
r1 = r by A32,A46,XTUPLE_0:1;
hence thesis by A28,A33,A47,A48,Def1;
end;
theorem Th10:
for A, B being non empty compact Subset of REAL holds dist(A,B) >= 0
proof
let A, B be non empty compact Subset of REAL;
set X = {|.r-s.| where r, s is Real : r in
A & s in B};
consider r0 being object such that
A1: r0 in A by XBOOLE_0:def 1;
A2: X c= REAL
proof
let e be object;
assume e in X;
then ex r,s being Real st e = |.r-s.| & r in A & s in B;
hence thesis by XREAL_0:def 1;
end;
consider s0 being object such that
A3: s0 in B by XBOOLE_0:def 1;
reconsider r0,s0 as Real by A1,A3;
|.r0-s0.| in X by A1,A3;
then reconsider X as non empty Subset of REAL by A2;
A4: for t being Real st t in X holds t >= 0
proof
let t be Real;
assume t in X;
then ex r,s being Real st t = |.r-s.| & r in A & s in B;
hence thesis by COMPLEX1:46;
end;
dist(A,B) = lower_bound X by Def1;
hence thesis by A4,SEQ_4:43;
end;
theorem Th11:
for A,B being non empty compact Subset of REAL st A misses B
holds dist(A,B) > 0
proof
let A,B being non empty compact Subset of REAL such that
A1: A misses B;
consider r0,s0 such that
A2: r0 in A and
A3: s0 in B and
A4: dist(A,B) = |.r0-s0.| by Th9;
reconsider r0,s0 as Real;
assume dist(A,B) <= 0;
then |.r0-s0.| = 0 by A4,Th10;
then r0 = s0 by GOBOARD7:2;
hence contradiction by A1,A2,A3,XBOOLE_0:3;
end;
theorem
for e,f being Real, A,B being compact Subset of REAL st A
misses B & A c= [.e,f.] & B c= [.e,f.] for S being sequence of bool REAL
st for i being Nat holds S.i is interval & S.i meets A & S.i meets
B ex r being Real st r in [.e,f.] & not r in A \/ B & for i being
Nat ex k being Nat st i <= k & r in S.k
proof
let e,f be Real, A,B be compact Subset of REAL such that
A1: A misses B and
A2: A c= [.e,f.] and
A3: B c= [.e,f.];
let S be sequence of bool REAL such that
A4: for i being Nat holds S.i is interval & S.i meets A & S.
i meets B;
defpred P[set,Subset of REAL] means $2 is non empty closed_interval
& $2 meets A & $2
meets B & $2 c= S.$1;
A5: for i being Element of NAT ex u being Subset of REAL st P[i,u]
proof
let i be Element of NAT;
A6: S.i is interval by A4;
S.i meets B by A4;
then consider y being object such that
A7: y in S.i and
A8: y in B by XBOOLE_0:3;
S.i meets A by A4;
then consider x being object such that
A9: x in S.i and
A10: x in A by XBOOLE_0:3;
reconsider y as Real by A8;
reconsider x as Real by A10;
per cases;
suppose
A11: x <= y;
take [.x,y.];
thus [.x,y.] is non empty closed_interval by A11,MEASURE5:14;
x in [.x,y.] by A11;
hence [.x,y.] meets A by A10,XBOOLE_0:3;
y in [.x,y.] by A11;
hence [.x,y.] meets B by A8,XBOOLE_0:3;
thus [.x,y.] c= S.i by A9,A7,A6;
end;
suppose
A12: y <= x;
take [.y,x.];
thus [.y,x.] is non empty closed_interval by A12,MEASURE5:14;
x in [.y,x.] by A12;
hence [.y,x.] meets A by A10,XBOOLE_0:3;
y in [.y,x.] by A12;
hence [.y,x.] meets B by A8,XBOOLE_0:3;
thus [.y,x.] c= S.i by A9,A7,A6;
end;
end;
consider T be sequence of bool REAL such that
A13: for i being Element of NAT holds P[i,T.i] from FUNCT_2:sch 3(A5);
T.0 meets B by A13;
then
A14: B is non empty;
deffunc G(Nat)=T.$1 /\ B;
deffunc F(Nat)=T.$1 /\ A;
consider SA being sequence of bool REAL such that
A15: for i being Element of NAT holds SA.i = F(i) from FUNCT_2:sch 4;
consider SB being sequence of bool REAL such that
A16: for i being Element of NAT holds SB.i = G(i) from FUNCT_2:sch 4;
defpred P[Nat,Real,Real] means $2 in SA.$1 & $3 in SB.$1 & dist(
SA.$1,SB.$1) = |.$2 - $3.|;
A17: for i being Element of NAT
ex ai,bi being Element of REAL st P[i,ai,bi]
proof
let i be Element of NAT;
reconsider Si = T.i as non empty closed_interval Subset of REAL by A13;
A18: T.i meets B by A13;
A19: SA.i = Si /\ A by A15;
A20: SB.i = Si /\ B by A16;
T.i meets A by A13;
then reconsider
SAi = SA.i, SBi = SB.i as non empty compact Subset of REAL by A18,A19,A20
,Th5;
consider ai,bi being Real such that
A21: ai in SAi and
A22: bi in SBi and
A23: dist(SAi,SBi) = |.ai - bi.| by Th9;
reconsider ai,bi as Element of REAL by XREAL_0:def 1;
take ai,bi;
thus thesis by A21,A22,A23;
end;
consider sa,sb being Real_Sequence such that
A24: for i being Element of NAT holds P[i,sa.i,sb.i] from DoubleChoice(
A17);
rng sa c= [.e,f.]
proof
let u be object;
assume u in rng sa;
then consider x being object such that
A25: x in dom sa and
A26: u = sa.x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A25;
sa.n in SA.n by A24;
then u in T.n /\ A by A15,A26;
then u in A by XBOOLE_0:def 4;
hence thesis by A2;
end;
then consider ga being Real_Sequence such that
A27: ga is subsequence of sa and
A28: ga is convergent and
A29: lim ga in [.e,f.] by RCOMP_1:def 3;
consider Nseq being increasing sequence of NAT such that
A30: ga = sa*Nseq by A27,VALUED_0:def 17;
set gb = sb*Nseq;
rng gb c= [.e,f.]
proof
let u be object;
assume u in rng gb;
then consider x being object such that
A31: x in dom gb and
A32: u = gb.x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A31;
gb.n = sb.(Nseq.n) by FUNCT_2:15;
then gb.n in SB.(Nseq.n) by A24;
then u in T.(Nseq.n) /\ B by A16,A32;
then u in B by XBOOLE_0:def 4;
hence thesis by A3;
end;
then consider fb being Real_Sequence such that
A33: fb is subsequence of gb and
A34: fb is convergent and
A35: lim fb in [.e,f.] by RCOMP_1:def 3;
consider Nseq1 being increasing sequence of NAT such that
A36: fb = gb*Nseq1 by A33,VALUED_0:def 17;
set fa = ga*Nseq1, r = (lim fa + lim fb)/2;
set d0 = dist(A,B), ff = (1/2)(#)(fa+fb);
A37: fa is convergent by A28,SEQ_4:16;
then
A38: fa+fb is convergent by A34,SEQ_2:5;
then
A39: ff is convergent by SEQ_2:7;
T.0 meets A by A13;
then A is non empty;
then d0 > 0 by A1,A14,Th11;
then
A40: d0/2 > 0 by XREAL_1:139;
r = (1/2)*(lim fa + lim fb) .= (1/2)*lim(fa+fb) by A34,A37,SEQ_2:6
.= lim ff by A38,SEQ_2:8;
then consider k0 being Nat such that
A41: for i being Nat st k0 <= i holds |.ff.i - r.| < d0/2 by A39
,A40,SEQ_2:def 7;
A42: k0 in NAT by ORDINAL1:def 12;
take r;
lim fa = lim ga by A28,SEQ_4:17;
hence r in [.e,f.] by A29,A35,Th1;
now
set i = Nseq.(Nseq1.k0), di = dist(SA.i,SB.i);
A43: 2*|.(sa.i+sb.i)/2 - r.| = |.2.|*|.(sa.i+sb.i)/2 - r.| by ABSVALUE:def 1
.= |.2*((sa.i+sb.i)/2 - r).| by COMPLEX1:65
.= |.sa.i+sb.i-2*r.|;
A44: fa.k0 = ga.(Nseq1.k0) by FUNCT_2:15,A42
.= sa.i by A30,FUNCT_2:15;
T.i meets B by A13;
then T.i /\ B <> {};
then
A45: SB.i is non empty by A16;
A46: SB.i = T.i /\ B by A16;
then
A47: SB.i c= B by XBOOLE_1:17;
A48: SB.i c= T.i by A46,XBOOLE_1:17;
A49: SA.i = T.i /\ A by A15;
then
A50: SA.i c= A by XBOOLE_1:17;
T.i meets A by A13;
then T.i /\ A <> {};
then
A51: SA.i is non empty by A15;
then
A52: d0 <= di by A45,A50,A47,Th8;
d0/2 <= di/2 by A51,A45,A50,A47,Th8,XREAL_1:72;
then
A53: di/2 + d0/2 <= di/2 + di/2 by XREAL_1:6;
ff.k0 = (1/2)*((fa+fb).k0) by SEQ_1:9
.= ((fa+fb).k0)/2
.= (fa.k0+fb.k0)/2 by SEQ_1:7;
then
A54: |.(fa.k0+fb.k0)/2 - r.| < d0/2 by A41;
T.i is non empty closed_interval by A13;
then
A55: ex a,b being Real st a <= b & T.i = [.a,b.] by MEASURE5:14;
A56: sb.i in SB.i by A24;
A57: SA.i c= T.i by A49,XBOOLE_1:17;
A58: fb.k0 = gb.(Nseq1.k0) by A36,FUNCT_2:15,A42
.= sb.i by FUNCT_2:15;
2*(d0/2) = d0;
then
A59: 2*|.(sa.i+sb.i)/2 - r.| < d0 by A54,A44,A58,XREAL_1:68;
A60: sa.i in SA.i by A24;
then
A61: di <= |.sb.i-sa.i.| by A56,Th7;
A62: now
per cases;
suppose
sa.i <= sb.i;
then sb.i - sa.i >= 0 by XREAL_1:48;
then di <= sb.i-sa.i by A61,ABSVALUE:def 1;
then d0 <= sb.i-sa.i by A52,XXREAL_0:2;
then |.sa.i+sb.i-2*r.| <= sb.i-sa.i by A59,A43,XXREAL_0:2;
then
A63: r in [.sa.i,sb.i.] by RCOMP_1:2;
[.sa.i,sb.i.] c= T.i by A55,A60,A56,A57,A48,XXREAL_2:def 12;
hence r in T.i by A63;
end;
suppose
A64: sb.i <= sa.i;
A65: |.sb.i-sa.i.| = |.sa.i-sb.i.| by UNIFORM1:11;
sa.i - sb.i >= 0 by A64,XREAL_1:48;
then di <= sa.i-sb.i by A61,A65,ABSVALUE:def 1;
then d0 <= sa.i-sb.i by A52,XXREAL_0:2;
then |.sb.i+sa.i-2*r.| <= sa.i-sb.i by A59,A43,XXREAL_0:2;
then
A66: r in [.sb.i,sa.i.] by RCOMP_1:2;
[.sb.i,sa.i.] c= T.i by A55,A60,A56,A57,A48,XXREAL_2:def 12;
hence r in T.i by A66;
end;
end;
assume
A67: r in A \/ B;
per cases by A67,XBOOLE_0:def 3;
suppose
A68: r in B;
SB.i = T.i /\ B by A16;
then
A69: r in SB.i by A62,A68,XBOOLE_0:def 4;
A70: |.(fa.k0-fb.k0)/2.| = |.(fa.k0-fb.k0).|/|.2.| by COMPLEX1:67
.= |.(fa.k0-fb.k0).|/2 by ABSVALUE:def 1;
fa.k0 - r = (fa.k0-fb.k0)/2 + ((fa.k0+fb.k0)/2 - r);
then
A71: |.fa.k0 - r.| <= |.(fa.k0-fb.k0)/2.| + |.(fa.k0+fb.k0)/2 - r.|
by COMPLEX1:56;
|.(fa.k0-fb.k0)/2.| + |.(fa.k0+fb.k0)/2 - r.| < |.(fa.k0-fb.k0
)/2.| + d0/2 by A54,XREAL_1:6;
then |.fa.k0 - r.| < |.(fa.k0-fb.k0).|/2 + d0/2 by A71,A70,XXREAL_0:2;
then |.fa.k0 - r.| < di/2 + d0/2 by A24,A44,A58;
then
A72: |.fa.k0 - r.| < di by A53,XXREAL_0:2;
fa.k0 in SA.i by A24,A44;
hence contradiction by A69,A72,Th7;
end;
suppose
A73: r in A;
SA.i = T.i /\ A by A15;
then
A74: r in SA.i by A62,A73,XBOOLE_0:def 4;
A75: |.(fb.k0-fa.k0)/2.| = |.(fb.k0-fa.k0).|/|.2.| by COMPLEX1:67
.= |.(fb.k0-fa.k0).|/2 by ABSVALUE:def 1;
fb.k0 - r = (fb.k0-fa.k0)/2 + ((fb.k0+fa.k0)/2 - r);
then
A76: |.fb.k0 - r.| <= |.(fb.k0-fa.k0)/2.| + |.(fb.k0+fa.k0)/2 - r.|
by COMPLEX1:56;
A77: |.fb.k0-fa.k0.| = |.fa.k0-fb.k0.| by UNIFORM1:11
.= di by A24,A44,A58;
|.(fb.k0-fa.k0)/2.| + |.(fb.k0+fa.k0)/2 - r.| < |.(fb.k0-fa.k0
)/2.| + d0/2 by A54,XREAL_1:6;
then |.fb.k0 - r.| < |.(fb.k0-fa.k0).|/2 + d0/2 by A76,A75,XXREAL_0:2;
then
A78: |.fb.k0 - r.| < di by A53,A77,XXREAL_0:2;
fb.k0 in SB.i by A24,A58;
hence contradiction by A74,A78,Th7;
end;
end;
hence not r in A \/ B;
let i being Nat;
set k = max(k0,i);
A79: k in NAT by ORDINAL1:def 12;
take j = Nseq.(Nseq1.k);
A80: fb.k = gb.(Nseq1.k) by A36,FUNCT_2:15,A79
.= sb.j by FUNCT_2:15;
A81: i <= k by XXREAL_0:25;
A82: sb.j in SB.j by A24;
T.j meets B by A13;
then T.j /\ B <> {};
then
A83: SB.j is non empty by A16;
A84: dom Nseq = NAT by FUNCT_2:def 1;
T.j meets A by A13;
then T.j /\ A <> {};
then
A85: SA.j is non empty by A15;
A86: i <= Nseq.i by SEQM_3:14;
A87: SA.j = T.j /\ A by A15;
then
A88: SA.j c= T.j by XBOOLE_1:17;
ff.k = (1/2)*((fa+fb).k) by A79,SEQ_1:9
.= ((fa+fb).k)/2
.= (fa.k+fb.k)/2 by A79,SEQ_1:7;
then
A89: |.(fa.k+fb.k)/2 - r.| < d0/2 by A41,A79,XXREAL_0:25;
A90: 2*(d0/2) = d0;
fa.k = ga.(Nseq1.k) by FUNCT_2:15,A79
.= sa.j by A30,FUNCT_2:15;
then
A91: 2*|.(sa.j+sb.j)/2 - r.| < d0 by A89,A80,A90,XREAL_1:68;
T.j is non empty closed_interval by A13;
then
A92: ex a,b be Real st a <= b & T.j = [.a,b.] by MEASURE5:14;
A93: SB.j = T.j /\ B by A16;
then
A94: SB.j c= B by XBOOLE_1:17;
A95: SB.j c= T.j by A93,XBOOLE_1:17;
A96: i in NAT by ORDINAL1:def 12;
dom Nseq1 = NAT by FUNCT_2:def 1;
then Nseq1.i <= Nseq1.k by A81,VALUED_0:def 15,A79,A96;
then
A97: Nseq.(Nseq1.i) <= j by A84,VALUED_0:def 15;
i <= Nseq1.i by SEQM_3:14;
then Nseq.i <= Nseq.(Nseq1.i) by A84,VALUED_0:def 15,A96;
then i <= Nseq.(Nseq1.i) by A86,XXREAL_0:2;
hence i <= j by A97,XXREAL_0:2;
set di = dist(SA.j,SB.j);
A98: 2*|.(sa.j+sb.j)/2 - r.| = |.2.|*|.(sa.j+sb.j)/2 - r.| by ABSVALUE:def 1
.= |.2*((sa.j+sb.j)/2 - r).| by COMPLEX1:65
.= |.sa.j+sb.j-2*r.|;
SA.j c= A by A87,XBOOLE_1:17;
then
A99: d0 <= di by A85,A83,A94,Th8;
A100: sa.j in SA.j by A24;
then
A101: di <= |.sb.j-sa.j.| by A82,Th7;
A102: now
per cases;
suppose
sa.j <= sb.j;
then sb.j - sa.j >= 0 by XREAL_1:48;
then di <= sb.j-sa.j by A101,ABSVALUE:def 1;
then d0 <= sb.j-sa.j by A99,XXREAL_0:2;
then |.sa.j+sb.j-2*r.| <= sb.j-sa.j by A91,A98,XXREAL_0:2;
then
A103: r in [.sa.j,sb.j.] by RCOMP_1:2;
[.sa.j,sb.j.] c= T.j by A92,A100,A82,A88,A95,XXREAL_2:def 12;
hence r in T.j by A103;
end;
suppose
A104: sb.j <= sa.j;
A105: |.sb.j-sa.j.| = |.sa.j-sb.j.| by UNIFORM1:11;
sa.j - sb.j >= 0 by A104,XREAL_1:48;
then di <= sa.j-sb.j by A101,A105,ABSVALUE:def 1;
then d0 <= sa.j-sb.j by A99,XXREAL_0:2;
then |.sb.j+sa.j-2*r.| <= sa.j-sb.j by A91,A98,XXREAL_0:2;
then
A106: r in [.sb.j,sa.j.] by RCOMP_1:2;
[.sb.j,sa.j.] c= T.j by A92,A100,A82,A88,A95,XXREAL_2:def 12;
hence r in T.j by A106;
end;
end;
T.j c= S.j by A13;
hence thesis by A102;
end;
:: Moved from JORDAN1A, AK, 23.02.2006
theorem Th13:
for S being closed Subset of TOP-REAL 2 st S is bounded holds
proj2.:S is closed
proof
let S be closed Subset of TOP-REAL 2;
assume S is bounded;
then Cl(proj2.:S) = proj2.:Cl S by TOPREAL6:84
.= proj2.:S by PRE_TOPC:22;
hence thesis;
end;
theorem Th14:
for S being Subset of TOP-REAL 2 st S is bounded holds
proj2.:S is real-bounded
proof
let S be Subset of TOP-REAL 2;
assume S is bounded;
then reconsider C = S as bounded Subset of Euclid 2 by JORDAN2C:11;
consider r being Real, x being Point of Euclid 2 such that
A1: 0 < r and
A2: C c= Ball(x,r) by METRIC_6:def 3;
reconsider P = Ball(x,r) as Subset of TOP-REAL 2 by TOPREAL3:8;
reconsider p = x as Point of TOP-REAL 2 by TOPREAL3:8;
set t = max(|.p`2-r.|,|.p`2+r.|);
now
assume that
A3: |.p`2-r.| <= 0 and
A4: |.p`2+r.| <= 0;
|.p`2-r.| = 0 by A3,COMPLEX1:46;
then |.r-p`2.| = 0 by UNIFORM1:11;
then
A5: r-p`2 = 0 by ABSVALUE:2;
|.p`2+r.| = 0 by A4,COMPLEX1:46;
hence contradiction by A1,A5,ABSVALUE:2;
end;
then
A6: t > 0 by XXREAL_0:30;
A7: proj2.:P = ].p`2-r,p`2+r.[ by TOPREAL6:44;
for s st s in proj2.:S holds |.s.| < t
proof
let s;
proj2.:S c= proj2.:P by A2,RELAT_1:123;
hence thesis by A7,Th3;
end;
hence thesis by A6,SEQ_4:4;
end;
theorem
for S being compact Subset of TOP-REAL 2 holds proj2.:S is compact
proof
let S being compact Subset of TOP-REAL 2;
proj2.:S is closed by Th13;
hence thesis by Th14,RCOMP_1:11;
end;