:: 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;
begin :: Preliminaries
reserve X for set,
Y for non empty set;
theorem :: JORDAN1K:1
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;
theorem :: JORDAN1K:2
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;
theorem :: JORDAN1K:3
for f being Function of X,Y, A being Subset of X st f is onto
holds (f.:A)` c= f.:A`;
theorem :: JORDAN1K:4
for f being Function of X,Y, A being Subset of X st f is
one-to-one holds f.:A` c= (f.:A)`;
theorem :: JORDAN1K:5
for f being Function of X,Y, A being Subset of X st f is
bijective holds (f.:A)` = f.:A`;
begin :: Topological and metrizable spaces
theorem :: JORDAN1K:6
for T being TopSpace for A be Subset of T holds A
is_a_component_of {}T iff A is empty;
theorem :: JORDAN1K:7
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;
reserve n for Nat;
theorem :: JORDAN1K:8
n >= 1 implies for P being Subset of Euclid n holds P is bounded
implies P` is not bounded;
reserve r for Real,
M for non empty MetrSpace;
theorem :: JORDAN1K:9
for C being non empty Subset of TopSpaceMetr M, p being Point of
TopSpaceMetr M holds (dist_min C).p >= 0;
theorem :: JORDAN1K:10
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;
theorem :: JORDAN1K:11
for A,B being non empty Subset of TopSpaceMetr M holds min_dist_min(A,B) >= 0
;
theorem :: JORDAN1K:12
for A,B being compact Subset of TopSpaceMetr M st A meets B
holds min_dist_min(A,B) = 0;
theorem :: JORDAN1K:13
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;
begin :: Euclid topological spaces
theorem :: JORDAN1K:14
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;
theorem :: JORDAN1K:15
n>= 1 implies BDD {}TOP-REAL n = {}TOP-REAL n;
theorem :: JORDAN1K:16
BDD [#]TOP-REAL n = {}TOP-REAL n;
theorem :: JORDAN1K:17
n>= 1 implies UBD {}TOP-REAL n = [#]TOP-REAL n;
theorem :: JORDAN1K:18
UBD [#]TOP-REAL n = {}TOP-REAL n;
theorem :: JORDAN1K:19
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;
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 :: JORDAN1K:20
dist(|[0,0]|,r*q) = |.r.|*dist(|[0,0]|,q);
theorem :: JORDAN1K:21
dist(q1+q,q2+q) = dist(q1,q2);
theorem :: JORDAN1K:22
p <> q implies dist(p,q) > 0;
theorem :: JORDAN1K:23
dist(q1-q,q2-q) = dist(q1,q2);
theorem :: JORDAN1K:24
dist(p,q) = dist(-p,-q);
theorem :: JORDAN1K:25
dist(q-q1,q-q2) = dist(q1,q2);
theorem :: JORDAN1K:26
dist(r*p,r*q) = |.r.|*dist(p,q);
theorem :: JORDAN1K:27
r <= 1 implies dist(p,r*p+(1-r)*q) = (1-r)*dist(p,q);
theorem :: JORDAN1K:28
0 <= r implies dist(q,r*p+(1-r)*q) = r*dist(p,q);
theorem :: JORDAN1K:29
p in LSeg(q1,q2) implies dist(q1,p) + dist(p,q2) = dist(q1,q2);
theorem :: JORDAN1K:30
q1 in LSeg(q2,p) & q1 <> q2 implies dist(q1,p) < dist(q2,p);
theorem :: JORDAN1K:31
y = |[0,0]| implies Ball(y,r) = {q : |.q.| < r };
begin :: Affine maps
theorem :: JORDAN1K:32
AffineMap(r,s1,r,s2).p = r*p+|[s1,s2]|;
theorem :: JORDAN1K:33
AffineMap(r,q`1,r,q`2).p = r*p+q;
theorem :: JORDAN1K:34
s1 > 0 & s2 > 0 implies AffineMap(s1,t1,s2,t2)*AffineMap(1/s1,-
t1/s1,1/s2,-t2/s2) = id REAL 2;
theorem :: JORDAN1K:35
y = |[0,0]| & x = q & r > 0 implies AffineMap(r,q`1,r,q`2).:Ball
(y,1) = Ball(x,r);
theorem :: JORDAN1K:36
for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C,D) is onto;
theorem :: JORDAN1K:37
Ball(x,r)` is connected Subset of TOP-REAL 2;
begin :: Minimal distance between subsets
definition
let n;
let A,B be Subset of TOP-REAL n;
func dist_min(A,B) -> Real means
:: JORDAN1K:def 1
ex A9,B9 being Subset of
TopSpaceMetr Euclid n st A = A9 & B = B9 & it = min_dist_min(A9,B9);
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;
redefine func max_dist_max(P,Q);
commutativity;
end;
definition
let n;
let A,B be non empty compact Subset of TOP-REAL n;
redefine func dist_min(A,B);
commutativity;
end;
theorem :: JORDAN1K:38
for A,B being non empty Subset of TOP-REAL n holds dist_min(A,B) >= 0;
theorem :: JORDAN1K:39
for A,B being compact Subset of TOP-REAL n st A meets B holds
dist_min(A,B) = 0;
theorem :: JORDAN1K:40
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;
theorem :: JORDAN1K:41
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);
theorem :: JORDAN1K:42
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);
theorem :: JORDAN1K:43
for p,q being Point of TOP-REAL n holds dist_min({p},{q}) = dist (p,q);
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
:: JORDAN1K:def 2
dist_min({p},B);
end;
theorem :: JORDAN1K:44
for A being non empty Subset of TOP-REAL n, p being Point of TOP-REAL
n holds dist(p,A) >= 0;
theorem :: JORDAN1K:45
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;
theorem :: JORDAN1K:46
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);
theorem :: JORDAN1K:47
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);
theorem :: JORDAN1K:48
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;
theorem :: JORDAN1K:49
for p,q being Point of TOP-REAL n holds dist(p,{q}) = dist(p,q);
theorem :: JORDAN1K:50
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);
theorem :: JORDAN1K:51
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);