:: On the Minimal Distance Between Set in {E}uclidean Space
:: by Andrzej Trybulec
::
:: Received August 19, 2002
:: Copyright (c) 2002-2017 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, FUNCT_1, FUNCT_2, SUBSET_1, RELAT_1, TARSKI,
PRE_TOPC, CONNSP_1, RELAT_2, XXREAL_0, EUCLID, XXREAL_2, STRUCT_0,
REAL_1, METRIC_1, PCOMPS_1, WEIERSTR, CARD_1, SEQ_4, RCOMP_1, JORDAN2C,
COMPLEX1, SQUARE_1, MCART_1, ARYTM_1, ARYTM_3, RLTOPSP1, JGRAPH_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, SQUARE_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, XXREAL_2, SEQ_4, DOMAIN_1, STRUCT_0, PRE_TOPC, COMPTS_1,
CONNSP_1, METRIC_1, METRIC_6, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID,
WEIERSTR, JORDAN2C, TOPREAL6, JGRAPH_2;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, CONNSP_1, COMPTS_1, TBSP_1,
MONOID_0, WEIERSTR, JORDAN2C, TOPREAL6, JGRAPH_2, FUNCSDOM, BINOP_2,
CONVEX1;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, PCOMPS_1, MONOID_0,
EUCLID, TOPMETR, JORDAN2C, BORSUK_3, TOPREAL6, JGRAPH_2, RELSET_1,
JORDAN1, VALUED_0, JORDAN5A, SQUARE_1, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions XBOOLE_0, TARSKI, FUNCT_2, XXREAL_2;
equalities EUCLID, SQUARE_1, SUBSET_1, STRUCT_0, RLTOPSP1, RLVECT_1;
expansions XBOOLE_0, TARSKI, FUNCT_2;
theorems XBOOLE_1, XBOOLE_0, SPRECT_1, JORDAN2C, SUBSET_1, GOBOARD9, TSEP_1,
CONNSP_1, PRE_TOPC, ZFMISC_1, EUCLID, WEIERSTR, TOPREAL3, TBSP_1,
SQUARE_1, ABSVALUE, FUNCT_1, METRIC_1, FUNCT_2, JGRAPH_2, RELAT_1,
TOPMETR, PCOMPS_1, TARSKI, XREAL_0, TOPRNS_1, XCMPLX_1, COMPLEX1, SEQ_4,
XREAL_1, XXREAL_0, TOPS_2, TOPREAL6, COMPTS_1, RLVECT_1;
begin :: Preliminaries
reserve X for set,
Y for non empty set;
theorem Th1:
for f being Function of X,Y st f is onto for y being Element of Y
ex x being object st x in X & y = f.x
by FUNCT_2:11;
theorem
for f being Function of X,Y st f is onto for y being Element of Y ex x
being Element of X st y = f.x
proof
let f be Function of X,Y such that
A1: f is onto;
let y be Element of Y;
ex x being object st x in X & f.x = y by A1,Th1;
hence thesis;
end;
theorem Th3:
for f being Function of X,Y, A being Subset of X st f is onto
holds (f.:A)` c= f.:A`
proof
let f be Function of X,Y, A be Subset of X such that
A1: f is onto;
let e be object;
assume
A2: e in (f.:A)`;
then reconsider y = e as Element of Y;
consider u being object such that
A3: u in X and
A4: y = f.u by A1,Th1;
reconsider x=u as Element of X by A3;
now
assume x in A;
then y in f.:A by A4,FUNCT_2:35;
hence contradiction by A2,XBOOLE_0:def 5;
end;
then x in A` by A3,SUBSET_1:29;
hence thesis by A4,FUNCT_2:35;
end;
theorem Th4:
for f being Function of X,Y, A being Subset of X st f is
one-to-one holds f.:A` c= (f.:A)`
proof
let f be Function of X,Y, A be Subset of X such that
A1: f is one-to-one;
let e be object;
assume
A2: e in f.:A`;
then reconsider y = e as Element of Y;
consider x1 being object such that
A3: x1 in X and
A4: x1 in A` and
A5: y = f.x1 by A2,FUNCT_2:64;
assume not e in (f.:A)`;
then
A6: ex x2 being object st x2 in X & x2 in A & y = f.x2
by FUNCT_2:64,SUBSET_1:29;
not x1 in A by A4,XBOOLE_0:def 5;
hence contradiction by A1,A3,A5,A6,FUNCT_2:19;
end;
theorem Th5:
for f being Function of X,Y, A being Subset of X st f is
bijective holds (f.:A)` = f.:A`
by Th3,Th4;
begin :: Topological and metrizable spaces
theorem Th6:
for T being TopSpace for A be Subset of T holds A
is_a_component_of {}T iff A is empty
proof
let T be TopSpace;
let A be Subset of T;
thus A is_a_component_of {}T implies A is empty by SPRECT_1:5,XBOOLE_1:3;
assume
A1: A is empty;
then reconsider B = A as Subset of T|{}T by XBOOLE_1:2;
for C being Subset of T|{}T st C is connected holds B c= C implies B = C
by A1;
then B is a_component by A1,CONNSP_1:def 5;
hence thesis by CONNSP_1:def 6;
end;
theorem Th7:
for T being non empty TopSpace for A,B,C being Subset of T st A
c= B & A is_a_component_of C & B is_a_component_of C holds A = B
proof
let T be non empty TopSpace;
let A,B,C be Subset of T such that
A1: A c= B and
A2: A is_a_component_of C and
A3: B is_a_component_of C;
per cases;
suppose
C = {};
then
A4: C = {}T;
then A = {} by A2,Th6;
hence thesis by A3,A4,Th6;
end;
suppose
C is non empty;
then A <> {} by A2,SPRECT_1:4;
hence thesis by A1,A2,A3,GOBOARD9:1,XBOOLE_1:69;
end;
end;
reserve n for Nat;
theorem
n >= 1 implies for P being Subset of Euclid n holds P is bounded
implies P` is not bounded
proof
assume
A1: n>=1;
REAL n c= the carrier of Euclid n;
then reconsider W = REAL n as Subset of Euclid n;
let P be Subset of Euclid n;
A2: P \/ P` = [#]Euclid n by PRE_TOPC:2
.= W;
assume P is bounded & P` is bounded;
hence contradiction by A1,A2,JORDAN2C:33,TBSP_1:13;
end;
reserve r for Real,
M for non empty MetrSpace;
theorem Th9:
for C being non empty Subset of TopSpaceMetr M, p being Point of
TopSpaceMetr M holds (dist_min C).p >= 0
proof
let C be non empty Subset of TopSpaceMetr M, p be Point of TopSpaceMetr M;
A1: TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#) by
PCOMPS_1:def 5;
then reconsider x = p as Point of M;
set B = [#]((dist x).:C);
A2: B = (dist x).:C by WEIERSTR:def 1;
A3: for r being Real st r in B holds 0 <= r
proof
let r be Real;
assume r in B;
then consider y being object such that
y in dom dist x and
A4: y in C and
A5: r = (dist x).y by A2,FUNCT_1:def 6;
reconsider y9 = y as Point of M by A1,A4;
r = dist(x,y9) by A5,WEIERSTR:def 4;
hence thesis by METRIC_1:5;
end;
dom dist x = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
then lower_bound B >= 0 by A2,A3,SEQ_4:43;
then lower_bound((dist x).:C) >= 0 by WEIERSTR:def 3;
hence thesis by WEIERSTR:def 6;
end;
theorem Th10:
for C being non empty Subset of TopSpaceMetr M, p being Point of
M st for q being Point of M st q in C holds dist(p,q) >= r holds (dist_min C).p
>= r
proof
let C be non empty Subset of TopSpaceMetr M, p be Point of M such that
A1: for q being Point of M st q in C holds dist(p,q) >= r;
set B = [#]((dist p).:C);
A2: B = (dist p).:C by WEIERSTR:def 1;
A3: TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#) by
PCOMPS_1:def 5;
A4: for s being Real st s in B holds r <= s
proof
let s be Real;
assume s in B;
then consider y being object such that
y in dom dist p and
A5: y in C and
A6: s = (dist p).y by A2,FUNCT_1:def 6;
reconsider y9 = y as Point of M by A3,A5;
s = dist(p,y9) by A6,WEIERSTR:def 4;
hence thesis by A1,A5;
end;
dom dist p = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
then lower_bound B >= r by A2,A4,SEQ_4:43;
then lower_bound((dist p).:C) >= r by WEIERSTR:def 3;
hence thesis by WEIERSTR:def 6;
end;
theorem Th11:
for A,B being non empty Subset of TopSpaceMetr M holds min_dist_min(A,B) >= 0
proof
let A,B be non empty Subset of TopSpaceMetr M;
set X = [#]((dist_min A).:B);
A1: X = (dist_min A).:B by WEIERSTR:def 1;
A2: for r being Real st r in X holds 0 <= r
proof
let r be Real;
assume r in X;
then consider y being object such that
y in dom dist_min A and
A3: y in B and
A4: r = (dist_min A).y by A1,FUNCT_1:def 6;
reconsider y as Point of TopSpaceMetr M by A3;
(dist_min A).y >= 0 by Th9;
hence thesis by A4;
end;
dom dist_min A = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
then lower_bound X >= 0 by A1,A2,SEQ_4:43;
then lower_bound((dist_min A).:B) >= 0 by WEIERSTR:def 3;
hence thesis by WEIERSTR:def 7;
end;
theorem Th12:
for A,B being compact Subset of TopSpaceMetr M st A meets B
holds min_dist_min(A,B) = 0
proof
let A,B be compact Subset of TopSpaceMetr M;
assume A meets B;
then consider p being object such that
A1: p in A and
A2: p in B by XBOOLE_0:3;
TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#) by
PCOMPS_1:def 5;
then reconsider p as Point of M by A1;
min_dist_min(A,B) >= 0 & min_dist_min(A,B) <= dist(p,p) by A1,A2,Th11,
WEIERSTR:34;
hence thesis by METRIC_1:1;
end;
theorem Th13:
for A,B being non empty Subset of TopSpaceMetr M st for p,q
being Point of M st p in A & q in B holds dist(p,q) >= r holds min_dist_min(A,B
) >= r
proof
let A,B be non empty Subset of TopSpaceMetr M such that
A1: for p,q being Point of M st p in A & q in B holds dist(p,q) >= r;
set X = [#]((dist_min A).:B);
A2: X = (dist_min A).:B by WEIERSTR:def 1;
A3: for s being Real st s in X holds r <= s
proof
let s be Real;
assume s in X;
then consider y being object such that
y in dom dist_min A and
A4: y in B and
A5: s = (dist_min A).y by A2,FUNCT_1:def 6;
reconsider y as Point of TopSpaceMetr M by A4;
reconsider p = y as Point of M by TOPMETR:12;
for q being Point of M st q in A holds dist(p,q) >= r by A1,A4;
hence thesis by A5,Th10;
end;
dom dist_min A = the carrier of TopSpaceMetr M by FUNCT_2:def 1;
then lower_bound X >= r by A2,A3,SEQ_4:43;
then lower_bound((dist_min A).:B) >= r by WEIERSTR:def 3;
hence thesis by WEIERSTR:def 7;
end;
begin :: Euclid topological spaces
theorem Th14:
for P,Q being Subset of TOP-REAL n st P is_a_component_of Q`
holds P is_inside_component_of Q or P is_outside_component_of Q
by JORDAN2C:def 2,def 3;
theorem
n>= 1 implies BDD {}TOP-REAL n = {}TOP-REAL n
proof
set X = {B where B is Subset of TOP-REAL n: B is_inside_component_of {}(
TOP-REAL n)};
assume n>= 1;
then
A1: [#](TOP-REAL n) is not bounded by JORDAN2C:35;
now
[#](TOP-REAL n) is a_component;
then
A2: [#](the TopStruct of TOP-REAL n) is a_component by CONNSP_1:45;
(TOP-REAL n)| [#]TOP-REAL n = the TopStruct of TOP-REAL n by TSEP_1:93;
then
A3: [#]TOP-REAL n is_a_component_of [#]TOP-REAL n by A2,CONNSP_1:def 6;
assume X <> {};
then consider x being object such that
A4: x in X by XBOOLE_0:def 1;
consider B being Subset of TOP-REAL n such that
x = B and
A5: B is_inside_component_of {}(TOP-REAL n) by A4;
B is_a_component_of ({}(TOP-REAL n))` by A5,JORDAN2C:def 2;
then B = [#]TOP-REAL n by A3,Th7;
hence contradiction by A1,A5,JORDAN2C:def 2;
end;
hence thesis by JORDAN2C:def 4,ZFMISC_1:2;
end;
theorem
BDD [#]TOP-REAL n = {}TOP-REAL n
proof
BDD [#]TOP-REAL n c= ([#]TOP-REAL n)` by JORDAN2C:25;
then BDD [#]TOP-REAL n c= {}TOP-REAL n by XBOOLE_1:37;
hence thesis by XBOOLE_1:3;
end;
theorem
n>= 1 implies UBD {}TOP-REAL n = [#]TOP-REAL n
proof
set X = {B where B is Subset of TOP-REAL n: B is_outside_component_of {}
TOP-REAL n};
assume n>= 1;
then
A1: [#](TOP-REAL n) is not bounded by JORDAN2C:35;
thus UBD {}TOP-REAL n c= [#]TOP-REAL n;
[#](TOP-REAL n) is a_component;
then
A2: [#](the TopStruct of TOP-REAL n) is a_component by CONNSP_1:45;
(TOP-REAL n)| [#]TOP-REAL n = the TopStruct of TOP-REAL n by TSEP_1:93;
then
A3: [#]TOP-REAL n is_a_component_of [#]TOP-REAL n by A2,CONNSP_1:def 6;
[#]TOP-REAL n = ({}TOP-REAL n)`;
then [#]TOP-REAL n is_outside_component_of {}TOP-REAL n by A1,A3,
JORDAN2C:def 3;
then [#]TOP-REAL n in X;
then [#]TOP-REAL n c= union X by ZFMISC_1:74;
hence thesis by JORDAN2C:def 5;
end;
theorem
UBD [#]TOP-REAL n = {}TOP-REAL n
proof
UBD [#]TOP-REAL n c= ([#]TOP-REAL n)` by JORDAN2C:26;
then UBD [#]TOP-REAL n c= {}TOP-REAL n by XBOOLE_1:37;
hence thesis by XBOOLE_1:3;
end;
theorem
for P being connected Subset of TOP-REAL n, Q being Subset of TOP-REAL
n st P misses Q holds P c= UBD Q or P c= BDD Q
proof
let P be connected Subset of TOP-REAL n, Q being Subset of TOP-REAL n such
that
A1: P misses Q;
per cases;
suppose
P is empty;
hence thesis;
end;
suppose
Q = [#]TOP-REAL n;
then P = {} by A1,XBOOLE_1:67;
hence thesis;
end;
suppose that
A2: P is not empty and
Q <> [#]TOP-REAL n;
P c= Q` by A1,SUBSET_1:23;
then consider C being Subset of TOP-REAL n such that
A3: C is_a_component_of Q` and
A4: P c= C by A2,GOBOARD9:3;
C is_inside_component_of Q or C is_outside_component_of Q by A3,Th14;
then C c= UBD Q or C c= BDD Q by JORDAN2C:22,23;
hence thesis by A4;
end;
end;
begin :: Euclid plane
reserve n for Nat,
p,q,q1,q2 for Point of TOP-REAL 2,
r,s1,s2,t1,t2 for Real,
x,y for Point of Euclid 2;
theorem Th20:
dist(|[0,0]|,r*q) = |.r.|*dist(|[0,0]|,q)
proof
A1: r^2 >= 0 & q`1^2 >=0 by XREAL_1:63;
A2: q`2^2 >=0 by XREAL_1:63;
A3: |[0,0]|`1 = 0 & |[0,0]|`2 = 0 by EUCLID:52;
then
A4: dist(|[0,0]|,q) = sqrt((0-q`1)^2 + (0-q`2)^2) by TOPREAL6:92
.= sqrt(q`1^2 + q`2^2);
thus dist(|[0,0]|,r*q) = sqrt((0-(r*q)`1)^2 + (0-(r*q)`2)^2) by A3,
TOPREAL6:92
.= sqrt(((r*q)`1)^2 + (-(r*q)`2)^2)
.= sqrt((r*q`1)^2 + ((r*q)`2)^2) by TOPREAL3:4
.= sqrt(r^2*q`1^2 + (r*q`2)^2) by TOPREAL3:4
.= sqrt(r^2*(q`1^2 + q`2^2))
.= sqrt(r^2)*sqrt(q`1^2 + q`2^2) by A1,A2,SQUARE_1:29
.= |.r.|*dist(|[0,0]|,q) by A4,COMPLEX1:72;
end;
theorem Th21:
dist(q1+q,q2+q) = dist(q1,q2)
proof
A1: (q1+q)`1-(q2+q)`1 = q1`1+q`1-(q2+q)`1 by TOPREAL3:2
.= q1`1+q`1-(q2`1+q`1) by TOPREAL3:2
.= q1`1-q2`1+0;
A2: (q1+q)`2-(q2+q)`2 = q1`2+q`2-(q2+q)`2 by TOPREAL3:2
.= q1`2+q`2-(q2`2+q`2) by TOPREAL3:2
.= q1`2-q2`2+0;
thus dist(q1+q,q2+q) = sqrt (((q1+q)`1-(q2+q)`1)^2 + ((q1+q)`2-(q2+q)`2)^2)
by TOPREAL6:92
.= dist(q1,q2) by A1,A2,TOPREAL6:92;
end;
theorem Th22:
p <> q implies dist(p,q) > 0
proof
ex p9, q9 being Point of Euclid 2 st p9 = p & q9 = q & dist(p,q) = dist(
p9,q9) by TOPREAL6:def 1;
hence thesis by METRIC_1:7;
end;
theorem Th23:
dist(q1-q,q2-q) = dist(q1,q2) by Th21;
theorem Th24:
dist(p,q) = dist(-p,-q)
proof
thus dist(p,q) = dist(q-q,p-q) by Th23
.= dist(q-q,p+-q)
.= dist(|[0,0]|,p+-q) by EUCLID:54,RLVECT_1:5
.= dist(p-p,p+-q) by EUCLID:54,RLVECT_1:5
.= dist(p+-p,p+-q)
.= dist(-p,-q) by Th21;
end;
theorem Th25:
dist(q-q1,q-q2) = dist(q1,q2)
proof
-(q-q1)= q1-q & -(q-q2) = q2-q by RLVECT_1:33;
hence dist(q-q1,q-q2) = dist(q1-q,q2-q) by Th24
.= dist(q1,q2) by Th23;
end;
theorem Th26:
dist(r*p,r*q) = |.r.|*dist(p,q)
proof
thus dist(r*p,r*q) = dist(r*p-r*p,r*p-r*q) by Th25
.= dist(|[0,0]|,r*p-r*q) by EUCLID:54,RLVECT_1:5
.= dist(|[0,0]|,r*(p-q)) by RLVECT_1:34
.= |.r.|*dist(|[0,0]|,p-q) by Th20
.= |.r.|*dist(p-p,p-q) by EUCLID:54,RLVECT_1:5
.= |.r.|*dist(p,q) by Th25;
end;
theorem Th27:
r <= 1 implies dist(p,r*p+(1-r)*q) = (1-r)*dist(p,q)
proof
assume r <= 1;
then 1+ r <= 1 + 1 by XREAL_1:6;
then 1-r >= 1-1 by XREAL_1:21;
then
A1: |.1-r.| = 1-r by ABSVALUE:def 1;
thus dist(p,r*p+(1-r)*q) = dist((r+(1-r))*p,r*p+(1-r)*q) by RLVECT_1:def 8
.= dist(r*p+(1-r)*p,r*p+(1-r)*q) by RLVECT_1:def 6
.= dist((1-r)*p,(1-r)*q) by Th21
.= (1-r)*dist(p,q) by A1,Th26;
end;
theorem Th28:
0 <= r implies dist(q,r*p+(1-r)*q) = r*dist(p,q)
proof
assume 0 <= r;
then
A1: |.r.| = r by ABSVALUE:def 1;
thus dist(q,r*p+(1-r)*q) = dist(r*p+(1-r)*q,(r+(1-r))*q) by RLVECT_1:def 8
.= dist(r*q+(1-r)*q,r*p+(1-r)*q) by RLVECT_1:def 6
.= dist(r*q,r*p) by Th21
.= r*dist(p,q) by A1,Th26;
end;
theorem Th29:
p in LSeg(q1,q2) implies dist(q1,p) + dist(p,q2) = dist(q1,q2)
proof
assume p in LSeg(q1,q2);
then consider r such that
A1: p = (1-r)*q1+r*q2 & 0<=r & r<=1;
dist(q1,p) = r*dist(q1,q2) & dist(q2,p) = (1-r)*dist(q1,q2) by A1,Th27,Th28;
hence thesis;
end;
theorem
q1 in LSeg(q2,p) & q1 <> q2 implies dist(q1,p) < dist(q2,p)
proof
assume that
A1: q1 in LSeg(q2,p) and
A2: q1 <> q2;
dist(q2,q1) + dist(q1,p) = dist(q2,p) by A1,Th29;
hence thesis by A2,Th22,XREAL_1:29;
end;
theorem Th31:
y = |[0,0]| implies Ball(y,r) = {q : |.q.| < r }
proof
set X = { q : |.|[0,0]|-q.| < r }, Y = {q : |.q.| < r };
A1: X c= Y
proof
let u be object;
assume u in X;
then consider q such that
A2: u = q & |.|[0,0]|-q.| < r;
|.|[0,0]|-q.| = |.q-|[0,0]|.| by TOPRNS_1:27
.= |.q.| by EUCLID:54,RLVECT_1:13;
hence thesis by A2;
end;
A3: Y c= X
proof
let u be object;
assume u in Y;
then consider q such that
A4: u = q & |.q.| < r;
|.|[0,0]|-q.| = |.q-|[0,0]|.| by TOPRNS_1:27
.= |.q.| by EUCLID:54,RLVECT_1:13;
hence thesis by A4;
end;
assume y = |[0,0]|;
hence Ball(y,r) = { q : |.|[0,0]|-q.| < r } by JGRAPH_2:2
.= {q : |.q.| < r } by A1,A3;
end;
begin :: Affine maps
theorem Th32:
AffineMap(r,s1,r,s2).p = r*p+|[s1,s2]|
proof
thus AffineMap(r,s1,r,s2).p = |[r*(p`1)+s1,r*(p`2)+s2]| by JGRAPH_2:def 2
.= |[(r*p)`1+s1,r*(p`2)+s2]| by TOPREAL3:4
.= |[(r*p)`1+s1,(r*p)`2+s2]| by TOPREAL3:4
.= |[(r*p)`1,(r*p)`2]|+ |[s1,s2]| by EUCLID:56
.= r*p + |[s1,s2]| by EUCLID:53;
end;
theorem Th33:
AffineMap(r,q`1,r,q`2).p = r*p+q
proof
thus AffineMap(r,q`1,r,q`2).p = r*p+|[q`1,q`2]| by Th32
.= r*p+q by EUCLID:53;
end;
theorem Th34:
s1 > 0 & s2 > 0 implies AffineMap(s1,t1,s2,t2)*AffineMap(1/s1,-
t1/s1,1/s2,-t2/s2) = id REAL 2
proof
the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
then reconsider f = id REAL 2 as Function of the carrier of TOP-REAL 2, the
carrier of TOP-REAL 2;
assume that
A1: s1 > 0 and
A2: s2 > 0;
now
let p be Point of TOP-REAL 2;
set q = |[1/s1*(p`1)-t1/s1,1/s2*(p`2)-t2/s2]|;
A3: q`2 = 1/s2*(p`2)-t2/s2 by EUCLID:52;
p in the carrier of TOP-REAL 2;
then
A4: p in REAL 2 by EUCLID:22;
A5: s1*(1/s1) = 1 by A1,XCMPLX_1:106;
thus (AffineMap(s1,t1,s2,t2)*AffineMap(1/s1,-t1/s1,1/s2,-t2/s2)).p =
AffineMap(s1,t1,s2,t2).(AffineMap(1/s1,-t1/s1,1/s2,-t2/s2).p) by FUNCT_2:15
.= AffineMap(s1,t1,s2,t2). |[1/s1*(p`1)+-t1/s1,1/s2*(p`2)+-t2/s2]| by
JGRAPH_2:def 2
.= |[s1*(q`1)+t1,s2*(q`2)+t2]| by JGRAPH_2:def 2
.= |[s1*(1/s1*(p`1)-t1/s1)+t1,s2*(q`2)+t2]| by EUCLID:52
.= |[s1*(1/s1)*(p`1)-s1*(t1/s1)+t1,s2*(q`2)+t2]|
.= |[ 1 *(p`1)-1 *t1+t1,s2*(q`2)+t2]| by A1,A5,XCMPLX_1:87
.= |[p`1,s2*(1/s2*(p`2))-s2*(t2/s2)+t2]| by A3
.= |[p`1,s2*(1/s2)*(p`2)-t2+t2]| by A2,XCMPLX_1:87
.= |[p`1,1 *(p`2)-1 *t2+t2]| by A2,XCMPLX_1:106
.= p by EUCLID:53
.= f.p by A4,FUNCT_1:18;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th35:
y = |[0,0]| & x = q & r > 0 implies AffineMap(r,q`1,r,q`2).:Ball
(y,1) = Ball(x,r)
proof
assume that
A1: y = |[0,0]| and
A2: x = q and
A3: r > 0;
reconsider A = Ball(y,1), B = Ball(x,r) as Subset of TOP-REAL 2 by TOPREAL3:8
;
A4: B c= AffineMap(r,q`1,r,q`2).:A
proof
let u be object;
assume
A5: u in B;
then reconsider q1 = u as Point of TOP-REAL 2;
reconsider x1 = q1 as Element of Euclid 2 by TOPREAL3:8;
set q2 = AffineMap(1/r,-q`1/r,1/r,-q`2/r).q1;
consider z1,z2 being Point of Euclid 2 such that
A6: z1 = q and
A7: z2 = r*q2+q and
A8: dist(q,r*q2+q) = dist(z1,z2) by TOPREAL6:def 1;
consider z3,z4 being Point of Euclid 2 such that
A9: z3 = |[0,0]| and
A10: z4 = q2 and
A11: dist(|[0,0]|,q2) = dist(z3,z4) by TOPREAL6:def 1;
z2 = AffineMap(r,q`1,r,q`2).q2 by A7,Th33
.= (AffineMap(r,q`1,r,q`2)*AffineMap(1/r,-q`1/r,1/r,-q`2/r)).q1 by
FUNCT_2:15
.= (id REAL 2).q1 by A3,Th34
.= x1;
then dist(x,x1) = dist(|[0,0]|+q,r*q2 + q) by A2,A6,A8,EUCLID:54,RLVECT_1:4
.= dist(|[0,0]|,r*q2) by Th21
.= |.r.|*dist(|[0,0]|,q2) by Th20
.= r*dist(y,z4) by A1,A3,A9,A11,ABSVALUE:def 1;
then r*dist(y,z4) < 1 *r by A5,METRIC_1:11;
then dist(y,z4) < 1 by A3,XREAL_1:64;
then
A12: q2 in A by A10,METRIC_1:11;
AffineMap(r,q`1,r,q`2).q2 = (AffineMap(r,q`1,r,q`2)*AffineMap(1/r,-q
`1/r,1/r,-q`2/r)).q1 by FUNCT_2:15
.= (id REAL 2).q1 by A3,Th34
.= (id TOP-REAL 2).q1 by EUCLID:22
.= q1;
hence thesis by A12,FUNCT_2:35;
end;
AffineMap(r,q`1,r,q`2).:A c= B
proof
let u be object;
assume
A13: u in AffineMap(r,q`1,r,q`2).:A;
then reconsider q1 = u as Point of TOP-REAL 2;
consider q2 such that
A14: q2 in A and
A15: q1 = AffineMap(r,q`1,r,q`2).q2 by A13,FUNCT_2:65;
reconsider x1 = q1, x2 = q2 as Element of Euclid 2 by TOPREAL3:8;
A16: dist(y,x2) < 1 by A14,METRIC_1:11;
A17: ex z3,z4 being Point of Euclid 2 st z3 = |[0,0]| & z4 = q2 & dist(|[0,
0]|,q2) = dist(z3,z4) by TOPREAL6:def 1;
A18: ex z1,z2 being Point of Euclid 2 st z1 = q & z2 = r*q2+q & dist(q,r*q2
+q) = dist(z1,z2) by TOPREAL6:def 1;
q1 = r*q2 + q by A15,Th33;
then dist(x,x1) = dist(|[0,0]|+q,r*q2 + q) by A2,A18,EUCLID:54,RLVECT_1:4
.= dist(|[0,0]|,r*q2) by Th21
.= |.r.|*dist(|[0,0]|,q2) by Th20
.= r*dist(y,x2) by A1,A3,A17,ABSVALUE:def 1;
then dist(x,x1) < r by A3,A16,XREAL_1:157;
hence thesis by METRIC_1:11;
end;
hence thesis by A4;
end;
theorem Th36:
for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C,D) is onto
proof
let A,B,C,D be Real such that
A1: A>0 & C>0;
thus rng AffineMap(A,B,C,D) c= the carrier of TOP-REAL 2;
let e be object;
assume e in the carrier of TOP-REAL 2;
then reconsider q1 = e as Point of TOP-REAL 2;
set q2 = AffineMap(1/A,-B/A,1/C,-D/C).q1;
A2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
AffineMap(A,B,C,D).q2 = (AffineMap(A,B,C,D)*AffineMap(1/A,-B/A,1/C,-D/C)
).q1 by FUNCT_2:15
.= (id REAL 2).q1 by A1,Th34
.= q1 by A2;
hence thesis by FUNCT_2:4;
end;
theorem
Ball(x,r)` is connected Subset of TOP-REAL 2
proof
set C = Ball(x,r)`;
per cases;
suppose
r <= 0;
then Ball(x,r) = {} TOP-REAL 2 by TBSP_1:12;
then
A1: C = [#] TOP-REAL 2 by TOPREAL3:8;
thus thesis by A1;
end;
suppose
A2: r > 0;
reconsider q = x as Point of TOP-REAL 2 by TOPREAL3:8;
reconsider y = |[0,0]| as Point of Euclid 2 by TOPREAL3:8;
reconsider Q = Ball(x,r), J = Ball(y,1) as Subset of TOP-REAL 2 by
TOPREAL3:8;
A3: Q = AffineMap(r,q`1,r,q`2).:J by A2,Th35;
reconsider P = Q`, K = J` as Subset of TOP-REAL 2;
A4: K = (REAL 2)\ Ball(y,1) by TOPREAL3:8
.= (REAL 2)\ {q1 : |.q1.| < 1 } by Th31;
AffineMap(r,q`1,r,q`2) is one-to-one & AffineMap(r,q`1,r,q`2) is onto
by A2,Th36,JGRAPH_2:44;
then
the carrier of TOP-REAL 2 = the carrier of Euclid 2 & P = AffineMap(r,
q`1,r, q`2).:K by A3,Th5,TOPREAL3:8;
hence thesis by A4,JORDAN2C:53,TOPS_2:61;
end;
end;
begin :: Minimal distance between subsets
definition
let n;
let A,B be Subset of TOP-REAL n;
func dist_min(A,B) -> Real means
:Def1:
ex A9,B9 being Subset of
TopSpaceMetr Euclid n st A = A9 & B = B9 & it = min_dist_min(A9,B9);
existence
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider A9=A, B9=B as Subset of TopSpaceMetr Euclid n;
take min_dist_min(A9,B9), A9, B9;
thus thesis;
end;
uniqueness;
end;
definition
let M be non empty MetrSpace;
let P,Q be non empty compact Subset of TopSpaceMetr M;
redefine func min_dist_min(P,Q);
commutativity
proof
let P,Q be non empty compact Subset of TopSpaceMetr M;
consider y1,y2 being Point of M such that
A1: y1 in Q & y2 in P and
A2: dist(y1,y2) = min_dist_min(Q,P) by WEIERSTR:30;
consider x1,x2 being Point of M such that
A3: x1 in P & x2 in Q and
A4: dist(x1,x2) = min_dist_min(P,Q) by WEIERSTR:30;
dist(x1,x2) <= dist(y1,y2) & dist(y1,y2) <= dist(x1,x2) by A1,A2,A3,A4,
WEIERSTR:34;
hence thesis by A2,A4,XXREAL_0:1;
end;
redefine func max_dist_max(P,Q);
commutativity
proof
let P,Q be non empty compact Subset of TopSpaceMetr M;
consider y1,y2 being Point of M such that
A5: y1 in Q & y2 in P and
A6: dist(y1,y2) = max_dist_max(Q,P) by WEIERSTR:33;
consider x1,x2 being Point of M such that
A7: x1 in P & x2 in Q and
A8: dist(x1,x2) = max_dist_max(P,Q) by WEIERSTR:33;
dist(x1,x2) <= dist(y1,y2) & dist(y1,y2) <= dist(x1,x2) by A5,A6,A7,A8,
WEIERSTR:34;
hence thesis by A6,A8,XXREAL_0:1;
end;
end;
definition
let n;
let A,B be non empty compact Subset of TOP-REAL n;
redefine func dist_min(A,B);
commutativity
proof
let A,B be non empty compact Subset of TOP-REAL n;
consider A9,B9 being Subset of TopSpaceMetr Euclid n such that
A1: A = A9 & B = B9 and
A2: dist_min(A,B) = min_dist_min(A9,B9) by Def1;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider
A9,B9 as non empty compact Subset of TopSpaceMetr Euclid n by A1,
COMPTS_1:23;
dist_min(A,B) = min_dist_min(B9,A9) by A2;
hence thesis by A1,Def1;
end;
end;
theorem Th38:
for A,B being non empty Subset of TOP-REAL n holds dist_min(A,B) >= 0
proof
let A,B be non empty Subset of TOP-REAL n;
ex A9,B9 be Subset of TopSpaceMetr Euclid n st A = A9 & B = B9 &
dist_min(A,B) = min_dist_min(A9,B9) by Def1;
hence thesis by Th11;
end;
theorem Th39:
for A,B being compact Subset of TOP-REAL n st A meets B holds
dist_min(A,B) = 0
proof
let A,B be compact Subset of TOP-REAL n such that
A1: A meets B;
consider A9,B9 be Subset of TopSpaceMetr Euclid n such that
A2: A = A9 & B = B9 and
A3: dist_min(A,B) = min_dist_min(A9,B9) by Def1;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then A9 is compact & B9 is compact by A2,COMPTS_1:23;
hence thesis by A1,A2,A3,Th12;
end;
theorem Th40:
for A,B being non empty Subset of TOP-REAL n st for p,q being
Point of TOP-REAL n st p in A & q in B holds dist(p,q) >= r holds dist_min(A,B)
>= r
proof
let A,B be non empty Subset of TOP-REAL n such that
A1: for p,q being Point of TOP-REAL n st p in A & q in B holds dist(p,q) >= r;
A2: for p,q being Point of Euclid n st p in A & q in B holds dist(p,q) >= r
proof
let a,b being Point of Euclid n such that
A3: a in A & b in B;
reconsider p =a, q = b as Point of TOP-REAL n by TOPREAL3:8;
ex a, b being Point of Euclid n st p = a & q = b & dist(p,q) = dist(a,
b) by TOPREAL6:def 1;
hence thesis by A1,A3;
end;
ex A9,B9 be Subset of TopSpaceMetr Euclid n st A = A9 & B = B9 &
dist_min(A,B) = min_dist_min(A9,B9) by Def1;
hence thesis by A2,Th13;
end;
theorem Th41:
for D being Subset of TOP-REAL n, A,C being non empty Subset of
TOP-REAL n st C c= D holds dist_min(A,D) <= dist_min(A,C)
proof
let D be Subset of TOP-REAL n;
let A,C be non empty Subset of TOP-REAL n such that
A1: C c= D;
consider A9,D9 be Subset of TopSpaceMetr Euclid n such that
A2: A = A9 and
A3: D = D9 & dist_min(A,D) = min_dist_min(A9,D9) by Def1;
reconsider f = dist_min A9 as Function of the carrier of TopSpaceMetr Euclid
n, REAL by TOPMETR:17;
reconsider Y = f.:D9 as Subset of REAL;
A4: Y is bounded_below
proof
take 0;
let r be ExtReal;
assume r in Y;
then ex c being Element of TopSpaceMetr Euclid n st c in D9 & r = f.c by
FUNCT_2:65;
hence thesis by A2,Th9;
end;
A5: lower_bound Y = lower_bound([#]((dist_min A9).:D9)) by WEIERSTR:def 1
.= lower_bound((dist_min A9).:D9) by WEIERSTR:def 3
.= min_dist_min(A9,D9) by WEIERSTR:def 7;
consider A99,C9 be Subset of TopSpaceMetr Euclid n such that
A6: A = A99 and
A7: C = C9 and
A8: dist_min(A,C) = min_dist_min(A99,C9) by Def1;
dom f = the carrier of TopSpaceMetr Euclid n by FUNCT_2:def 1;
then reconsider X = f.:C9 as non empty Subset of REAL by A7;
lower_bound X = lower_bound([#]((dist_min A9).:C9)) by WEIERSTR:def 1
.= lower_bound((dist_min A9).:C9) by WEIERSTR:def 3
.= min_dist_min(A9,C9) by WEIERSTR:def 7;
hence thesis by A1,A2,A3,A6,A7,A8,A5,A4,RELAT_1:123,SEQ_4:47;
end;
theorem Th42:
for A,B being non empty compact Subset of TOP-REAL n ex p,q
being Point of TOP-REAL n st p in A & q in B & dist_min(A,B) = dist(p,q)
proof
let A,B be non empty compact Subset of TOP-REAL n;
consider A9,B9 being Subset of TopSpaceMetr Euclid n such that
A1: A = A9 & B = B9 and
A2: dist_min(A,B) = min_dist_min(A9,B9) by Def1;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then A9 is compact & B9 is compact by A1,COMPTS_1:23;
then consider x1,x2 being Point of Euclid n such that
A3: x1 in A9 & x2 in B9 and
A4: dist(x1,x2) = min_dist_min(A9,B9) by A1,WEIERSTR:30;
reconsider p = x1, q = x2 as Point of TOP-REAL n by TOPREAL3:8;
take p,q;
thus p in A & q in B by A1,A3;
thus thesis by A2,A4,TOPREAL6:def 1;
end;
theorem Th43:
for p,q being Point of TOP-REAL n holds dist_min({p},{q}) = dist (p,q)
proof
let p,q be Point of TOP-REAL n;
consider p9,q9 being Point of TOP-REAL n such that
A1: p9 in {p} and
A2: q9 in {q} & dist_min({p},{q}) = dist(p9,q9) by Th42;
p = p9 by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
definition
let n;
let p be Point of TOP-REAL n;
let B be Subset of TOP-REAL n;
func dist(p,B) -> Real equals
dist_min({p},B);
coherence;
end;
theorem
for A being non empty Subset of TOP-REAL n, p being Point of TOP-REAL
n holds dist(p,A) >= 0 by Th38;
theorem
for A being compact Subset of TOP-REAL n, p being Point of TOP-REAL n
st p in A holds dist(p,A) = 0 by Th39,ZFMISC_1:48;
theorem Th46:
for A being non empty compact Subset of TOP-REAL n, p being
Point of TOP-REAL n ex q being Point of TOP-REAL n st q in A & dist(p,A) = dist
(p,q)
proof
let A be non empty compact Subset of TOP-REAL n;
let p be Point of TOP-REAL n;
consider q,p9 being Point of TOP-REAL n such that
A1: q in A and
A2: p9 in {p} & dist_min(A,{p}) = dist(q,p9) by Th42;
take q;
thus q in A by A1;
thus thesis by A2,TARSKI:def 1;
end;
theorem
for C being non empty Subset of TOP-REAL n for D being Subset of
TOP-REAL n st C c= D for q being Point of TOP-REAL n holds dist(q,D) <= dist(q,
C) by Th41;
theorem
for A being non empty Subset of TOP-REAL n, p being Point of TOP-REAL
n st for q being Point of TOP-REAL n st q in A holds dist(p,q) >= r holds dist(
p,A) >= r
proof
let A be non empty Subset of TOP-REAL n, p9 be Point of TOP-REAL n such that
A1: for q being Point of TOP-REAL n st q in A holds dist(p9,q) >= r;
for p,q being Point of TOP-REAL n st p in {p9} & q in A holds dist(p,q) >= r
proof
let p,q be Point of TOP-REAL n such that
A2: p in {p9} and
A3: q in A;
p = p9 by A2,TARSKI:def 1;
hence thesis by A1,A3;
end;
hence thesis by Th40;
end;
theorem
for p,q being Point of TOP-REAL n holds dist(p,{q}) = dist(p,q) by Th43;
theorem Th50:
for A being non empty Subset of TOP-REAL n, p,q being Point of
TOP-REAL n st q in A holds dist(p,A) <= dist(p,q)
proof
let A be non empty Subset of TOP-REAL n;
let p,q be Point of TOP-REAL n;
assume q in A;
then {q} c= A by ZFMISC_1:31;
then dist(p,A) <= dist(p,{q}) by Th41;
hence thesis by Th43;
end;
theorem
for A being compact non empty Subset of TOP-REAL 2, B being open
Subset of TOP-REAL 2 st A c= B for p being Point of TOP-REAL 2 st not p in B
holds dist(p,B) < dist(p,A)
proof
let A be compact non empty Subset of TOP-REAL 2, B being open Subset of
TOP-REAL 2 such that
A1: A c= B;
the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
then reconsider P = B as open Subset of TopSpaceMetr Euclid 2 by PRE_TOPC:30;
let p be Point of TOP-REAL 2 such that
A2: not p in B;
assume
A3: dist(p,B) >= dist(p,A);
dist(p,B) <= dist(p,A) by A1,Th41;
then
A4: dist(p,B) = dist(p,A) by A3,XXREAL_0:1;
consider q being Point of TOP-REAL 2 such that
A5: q in A and
A6: dist(p,A) = dist(p,q) by Th46;
reconsider a = q as Point of Euclid 2 by TOPREAL3:8;
consider r being Real such that
A7: r>0 and
A8: Ball(a,r) c= P by A1,A5,TOPMETR:15;
reconsider r as Element of REAL by XREAL_0:def 1;
set s = r/(2*dist(p,q)), q9 = (1-s)*q + s*p;
a in P by A1,A5;
then
A9: dist(p,q) > 0 by A2,Th22;
then
A10: 2*dist(p,q) > 0 by XREAL_1:129;
then 0 < s by A7,XREAL_1:139;
then
A11: 1-s < 1-0 by XREAL_1:10;
A12: ex p1, q1 being Point of Euclid 2 st p1 = q & q1 = q9 & dist(q,q9) =
dist(p1,q1) by TOPREAL6:def 1;
dist(q,q9) = 1 *r/(2*dist(p,q))*dist(p,q) by A7,A9,Th28
.= r/2/(dist(p,q)/1)*dist(p,q) by XCMPLX_1:84
.= r/2 by A9,XCMPLX_1:87;
then dist(q,q9) < r/1 by A7,XREAL_1:76;
then
A13: q9 in Ball(a,r) by A12,METRIC_1:11;
now
A14: ex p1, q1 being Point of Euclid 2 st p1 = p & q1 = q & dist(p,q) =
dist(p1,q1) by TOPREAL6:def 1;
assume r > dist(p,q);
then p in Ball(a,r) by A14,METRIC_1:11;
hence contradiction by A2,A8;
end;
then 1 *r < 2*dist(p,q) by A7,XREAL_1:98;
then s < 1 by A10,XREAL_1:191;
then dist(p,q9) = (1-s)*dist(p,q) by Th27;
hence contradiction by A4,A6,A8,A9,A13,A11,Th50,XREAL_1:157;
end;