:: by Andrzej Trybulec

::

:: Received August 19, 2002

:: Copyright (c) 2002-2012 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 )

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

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 `)

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) `

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 `)

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

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

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

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

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

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

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

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 )

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: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 )

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

for r being Real holds dist (|[0,0]|,(r * q)) = (abs r) * (dist (|[0,0]|,q))

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

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

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

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)

(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)

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 }

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

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

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)

(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)

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 :: JORDAN1K:37

for r being Real

for x being Point of (Euclid 2) holds (Ball (x,r)) ` is connected Subset of (TOP-REAL 2)

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

ex b_{1} being Real ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st

( A = A9 & B = B9 & b_{1} = min_dist_min (A9,B9) )

for b_{1}, b_{2} being Real st ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st

( A = A9 & B = B9 & b_{1} = min_dist_min (A9,B9) ) & ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st

( A = A9 & B = B9 & b_{2} = min_dist_min (A9,B9) ) holds

b_{1} = b_{2}
;

end;
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 A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st

( A = A9 & B = B9 & it = min_dist_min (A9,B9) );

ex b

( A = A9 & B = B9 & b

proof end;

uniqueness for b

( A = A9 & B = B9 & b

( A = A9 & B = B9 & b

b

:: 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_{4} being Real holds

( b_{4} = dist_min (A,B) iff ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st

( A = A9 & B = B9 & b_{4} = min_dist_min (A9,B9) ) );

for n being Element of NAT

for A, B being Subset of (TOP-REAL n)

for b

( b

( A = A9 & B = B9 & 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)

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)

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

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)

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

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

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

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

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)

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

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)

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

coherence

dist_min ({p},B) is Real ;

end;
let p be Point of (TOP-REAL n);

let B be Subset of (TOP-REAL n);

coherence

dist_min ({p},B) is Real ;

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

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

theorem :: JORDAN1K:45

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

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

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

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

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)

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)

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;