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


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 object st
( x in X & y = f . x ) by FUNCT_2:11;

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 `) by Th3, Th4;

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 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;

theorem Th14: :: JORDAN1K:14
for n being 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 ) by JORDAN2C:def 2, JORDAN2C:def 3;

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

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

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

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

theorem :: JORDAN1K:19
for n being 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;

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

theorem Th21: :: JORDAN1K:21
for q, q1, 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 q, q1, q2 being Point of (TOP-REAL 2) holds dist ((q1 - q),(q2 - q)) = dist (q1,q2) by Th21;

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)) = |.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 p, q 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 p, q1, q2 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;

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 p, q 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 x, y 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;

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

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

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) -> object ;
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) -> object ;
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 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 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 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 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 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 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 Nat
for p, q being Point of (TOP-REAL n) holds dist_min ({p},{q}) = dist (p,q)
proof end;

definition
let n be 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 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 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 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:48;

theorem Th46: :: JORDAN1K:46
for n being 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 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 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 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 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;