:: On the Minimal Distance Between Set in {E}uclidean Space
:: by Andrzej Trybulec
::
:: Received August 19, 2002
:: Copyright (c) 2002 Association of Mizar Users


begin

theorem Th1: :: JORDAN1K:1
for X being set
for Y being non empty set
for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being set st
( x in X & y = f . x )
proof end;

theorem :: JORDAN1K:2
for X being set
for Y being non empty set
for f being Function of X,Y st f is onto holds
for y being Element of Y ex x being Element of X st y = f . x
proof end;

theorem Th3: :: JORDAN1K:3
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is onto holds
(f .: A) ` c= f .: (A ` )
proof end;

theorem Th4: :: JORDAN1K:4
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
f .: (A ` ) c= (f .: A) `
proof end;

theorem Th5: :: JORDAN1K:5
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is bijective holds
(f .: A) ` = f .: (A ` )
proof end;

begin

theorem Th6: :: JORDAN1K:6
for T being TopSpace
for A being Subset of T holds
( A is_a_component_of {} T iff A is empty )
proof end;

theorem Th7: :: 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
proof end;

theorem :: JORDAN1K:8
for n being Element of NAT st n >= 1 holds
for P being Subset of (Euclid n) st P is bounded holds
not P ` is bounded
proof end;

theorem Th9: :: JORDAN1K:9
for M being non empty MetrSpace
for C being non empty Subset of (TopSpaceMetr M)
for p being Point of (TopSpaceMetr M) holds (dist_min C) . p >= 0
proof end;

theorem Th10: :: JORDAN1K:10
for r being Real
for M being non empty MetrSpace
for C being non empty Subset of (TopSpaceMetr M)
for 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 end;

theorem Th11: :: JORDAN1K:11
for M being non empty MetrSpace
for A, B being non empty Subset of (TopSpaceMetr M) holds min_dist_min A,B >= 0
proof end;

theorem Th12: :: JORDAN1K:12
for M being non empty MetrSpace
for A, B being compact Subset of (TopSpaceMetr M) st A meets B holds
min_dist_min A,B = 0
proof end;

theorem Th13: :: JORDAN1K:13
for r being Real
for M being non empty MetrSpace
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 end;

begin

theorem Th14: :: JORDAN1K:14
for n being Element of NAT
for P, Q being Subset of (TOP-REAL n) holds
( not P is_a_component_of Q ` or P is_inside_component_of Q or P is_outside_component_of Q )
proof end;

theorem :: JORDAN1K:15
for n being Element of NAT st n >= 1 holds
BDD ({} (TOP-REAL n)) = {} (TOP-REAL n)
proof end;

theorem :: JORDAN1K:16
for n being Element of NAT holds BDD ([#] (TOP-REAL n)) = {} (TOP-REAL n)
proof end;

theorem :: JORDAN1K:17
for n being Element of NAT st n >= 1 holds
UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n)
proof end;

theorem :: JORDAN1K:18
for n being Element of NAT holds UBD ([#] (TOP-REAL n)) = {} (TOP-REAL n)
proof end;

theorem :: JORDAN1K:19
for n being Element of NAT
for P being connected Subset of (TOP-REAL n)
for Q being Subset of (TOP-REAL n) holds
( not P misses Q or P c= UBD Q or P c= BDD Q )
proof end;

begin

theorem Th20: :: JORDAN1K:20
for q being Point of (TOP-REAL 2)
for r being Real holds dist |[0 ,0 ]|,(r * q) = (abs r) * (dist |[0 ,0 ]|,q)
proof end;

theorem Th21: :: JORDAN1K:21
for q1, q, q2 being Point of (TOP-REAL 2) holds dist (q1 + q),(q2 + q) = dist q1,q2
proof end;

theorem Th22: :: JORDAN1K:22
for p, q being Point of (TOP-REAL 2) st p <> q holds
dist p,q > 0
proof end;

theorem Th23: :: JORDAN1K:23
for q1, q, q2 being Point of (TOP-REAL 2) holds dist (q1 - q),(q2 - q) = dist q1,q2
proof end;

theorem Th24: :: JORDAN1K:24
for p, q being Point of (TOP-REAL 2) holds dist p,q = dist (- p),(- q)
proof end;

theorem Th25: :: JORDAN1K:25
for q, q1, q2 being Point of (TOP-REAL 2) holds dist (q - q1),(q - q2) = dist q1,q2
proof end;

theorem Th26: :: JORDAN1K:26
for p, q being Point of (TOP-REAL 2)
for r being Real holds dist (r * p),(r * q) = (abs r) * (dist p,q)
proof end;

theorem Th27: :: JORDAN1K:27
for p, q being Point of (TOP-REAL 2)
for r being Real st r <= 1 holds
dist p,((r * p) + ((1 - r) * q)) = (1 - r) * (dist p,q)
proof end;

theorem Th28: :: JORDAN1K:28
for q, p being Point of (TOP-REAL 2)
for r being Real st 0 <= r holds
dist q,((r * p) + ((1 - r) * q)) = r * (dist p,q)
proof end;

theorem Th29: :: JORDAN1K:29
for p, q1, q2 being Point of (TOP-REAL 2) st p in LSeg q1,q2 holds
(dist q1,p) + (dist p,q2) = dist q1,q2
proof end;

theorem :: JORDAN1K:30
for q1, q2, p being Point of (TOP-REAL 2) st q1 in LSeg q2,p & q1 <> q2 holds
dist q1,p < dist q2,p
proof end;

theorem Th31: :: JORDAN1K:31
for r being Real
for y being Point of (Euclid 2) st y = |[0 ,0 ]| holds
Ball y,r = { q where q is Point of (TOP-REAL 2) : |.q.| < r }
proof end;

begin

theorem Th32: :: JORDAN1K:32
for p being Point of (TOP-REAL 2)
for r, s1, s2 being Real holds (AffineMap r,s1,r,s2) . p = (r * p) + |[s1,s2]|
proof end;

theorem Th33: :: JORDAN1K:33
for q, p being Point of (TOP-REAL 2)
for r being Real holds (AffineMap r,(q `1 ),r,(q `2 )) . p = (r * p) + q
proof end;

theorem Th34: :: JORDAN1K:34
for s1, s2, t1, t2 being Real st s1 > 0 & s2 > 0 holds
(AffineMap s1,t1,s2,t2) * (AffineMap (1 / s1),(- (t1 / s1)),(1 / s2),(- (t2 / s2))) = id (REAL 2)
proof end;

theorem Th35: :: JORDAN1K:35
for q being Point of (TOP-REAL 2)
for r being Real
for y, x being Point of (Euclid 2) st y = |[0 ,0 ]| & x = q & r > 0 holds
(AffineMap r,(q `1 ),r,(q `2 )) .: (Ball y,1) = Ball x,r
proof end;

theorem Th36: :: JORDAN1K:36
for A, B, C, D being Real st A > 0 & C > 0 holds
AffineMap A,B,C,D is onto
proof end;

theorem :: JORDAN1K:37
for r being Real
for x being Point of (Euclid 2) holds (Ball x,r) ` is connected Subset of (TOP-REAL 2)
proof end;

begin

definition
let n be Element of NAT ;
let A, B be Subset of (TOP-REAL n);
func dist_min A,B -> Real means :Def1: :: JORDAN1K:def 1
 ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & it = min_dist_min A',B' );
existence
ex b1 being Real ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & b1 = min_dist_min A',B' )
proof end;
uniqueness
for b1, b2 being Real st ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & b1 = min_dist_min A',B' ) & ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & b2 = min_dist_min A',B' ) holds
b1 = b2 ;
end;

:: deftheorem Def1 defines dist_min JORDAN1K:def 1 :
for n being Element of NAT
for A, B being Subset of (TOP-REAL n)
for b4 being Real holds
( b4 = dist_min A,B iff ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & b4 = min_dist_min A',B' ) );

definition
let M be non empty MetrSpace;
let P, Q be non empty compact Subset of (TopSpaceMetr M);
:: original: min_dist_min
redefine func min_dist_min P,Q -> Element of REAL ;
commutativity
for P, Q being non empty compact Subset of (TopSpaceMetr M) holds min_dist_min P,Q = min_dist_min Q,P
proof end;
:: original: max_dist_max
redefine func max_dist_max P,Q -> Element of REAL ;
commutativity
for P, Q being non empty compact Subset of (TopSpaceMetr M) holds max_dist_max P,Q = max_dist_max Q,P
proof end;
end;

definition
let n be Element of NAT ;
let A, B be non empty compact Subset of (TOP-REAL n);
:: original: dist_min
redefine func dist_min A,B -> Real;
commutativity
for A, B being non empty compact Subset of (TOP-REAL n) holds dist_min A,B = dist_min B,A
proof end;
end;

theorem Th38: :: JORDAN1K:38
for n being Element of NAT
for A, B being non empty Subset of (TOP-REAL n) holds dist_min A,B >= 0
proof end;

theorem Th39: :: JORDAN1K:39
for n being Element of NAT
for A, B being compact Subset of (TOP-REAL n) st A meets B holds
dist_min A,B = 0
proof end;

theorem Th40: :: JORDAN1K:40
for n being Element of NAT
for r being Real
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 end;

theorem Th41: :: JORDAN1K:41
for n being Element of NAT
for D being Subset of (TOP-REAL n)
for A, C being non empty Subset of (TOP-REAL n) st C c= D holds
dist_min A,D <= dist_min A,C
proof end;

theorem Th42: :: JORDAN1K:42
for n being Element of NAT
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 end;

theorem Th43: :: JORDAN1K:43
for n being Element of NAT
for p, q being Point of (TOP-REAL n) holds dist_min {p},{q} = dist p,q
proof end;

definition
let n be Element of NAT ;
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;
coherence
dist_min {p},B is Real ;
end;

:: deftheorem defines dist JORDAN1K:def 2 :
for n being Element of NAT
for p being Point of (TOP-REAL n)
for B being Subset of (TOP-REAL n) holds dist p,B = dist_min {p},B;

theorem :: JORDAN1K:44
for n being Element of NAT
for A being non empty Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) holds dist p,A >= 0 by Th38;

theorem :: JORDAN1K:45
for n being Element of NAT
for A being compact Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st p in A holds
dist p,A = 0 by Th39, ZFMISC_1:54;

theorem Th46: :: JORDAN1K:46
for n being Element of NAT
for A being non empty compact Subset of (TOP-REAL n)
for 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 end;

theorem :: JORDAN1K:47
for n being Element of NAT
for C being non empty Subset of (TOP-REAL n)
for D being Subset of (TOP-REAL n) st C c= D holds
for q being Point of (TOP-REAL n) holds dist q,D <= dist q,C by Th41;

theorem :: JORDAN1K:48
for n being Element of NAT
for r being Real
for A being non empty Subset of (TOP-REAL n)
for 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 end;

theorem :: JORDAN1K:49
for n being Element of NAT
for p, q being Point of (TOP-REAL n) holds dist p,{q} = dist p,q by Th43;

theorem Th50: :: JORDAN1K:50
for n being Element of NAT
for A being non empty Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n) st q in A holds
dist p,A <= dist p,q
proof end;

theorem :: JORDAN1K:51
for A being non empty compact Subset of (TOP-REAL 2)
for B being open Subset of (TOP-REAL 2) st A c= B holds
for p being Point of (TOP-REAL 2) st not p in B holds
dist p,B < dist p,A
proof end;