:: On the Minimal Distance Between Set in {E}uclidean Space
:: by Andrzej Trybulec
::
:: Received August 19, 2002
:: Copyright (c) 2002-2011 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 A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & it = min_dist_min (A9,B9) );
existence
ex b₁ being Real ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b₁ = min_dist_min (A9,B9) )

proof end;

uniqueness
for b₁, b₂ being Real st ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b₁ = min_dist_min (A9,B9) ) & ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b₂ = min_dist_min (A9,B9) ) holds
b₁ = b₂ ;

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 b₄ being Real holds
( b₄ = dist_min (A,B) iff ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & b₄ = 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) -> 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;