:: JORDAN1K semantic presentation

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;

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

proof end;

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 Th19: :: 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) = (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 Th30: :: 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;

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 Th37: :: 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 A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & it = min_dist_min A',B' );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def1 defines dist_min JORDAN1K:def 1 :

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

proof end;

:: original: max_dist_max
redefine func max_dist_max P,Q -> Element of REAL ;
commutativity

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

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 ;

end;

:: deftheorem defines dist JORDAN1K:def 2 :

theorem Th44: :: 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 Th45: :: 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

proof end;

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 Th47: :: 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 Th48: :: 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 Th49: :: 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 Th51: :: 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;

theorem Th52: :: JORDAN1K:52

for C, D being Simple_closed_curve holds UBD C meets UBD D

proof end;

theorem Th53: :: JORDAN1K:53

for C being Simple_closed_curve
for q, p being Point of (TOP-REAL 2) st q in UBD C & p in BDD C holds
dist q,C < dist q,p

proof end;

registration

let C be Simple_closed_curve;
cluster BDD C -> non empty ;
coherence

proof end;

end;

theorem Th54: :: JORDAN1K:54

for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st not p in BDD C holds
dist p,C <= dist p,(BDD C)

proof end;

theorem Th55: :: JORDAN1K:55

for C, D being Simple_closed_curve holds
( not C c= BDD D or not D c= BDD C )

proof end;

theorem Th56: :: JORDAN1K:56

for C, D being Simple_closed_curve st C c= BDD D holds
D c= UBD C

proof end;

theorem :: JORDAN1K:57

for C being Simple_closed_curve
for n being Nat holds L~ (Cage C,n) c= UBD C

proof end;

definition

let C be Simple_closed_curve;
func Lower_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN1K:def 3
First_Point (Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2));
coherence ;
func Upper_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN1K:def 4
First_Point (Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2));
coherence ;

end;

:: deftheorem defines Lower_Middle_Point JORDAN1K:def 3 :

:: deftheorem defines Upper_Middle_Point JORDAN1K:def 4 :

theorem Th58: :: JORDAN1K:58

for C being Simple_closed_curve holds Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)

proof end;

theorem Th59: :: JORDAN1K:59

for C being Simple_closed_curve holds Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)

proof end;

theorem :: JORDAN1K:60

for C being Simple_closed_curve holds (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2

proof end;

theorem :: JORDAN1K:61

for C being Simple_closed_curve holds (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2

proof end;

theorem :: JORDAN1K:62

for C being Simple_closed_curve holds Lower_Middle_Point C in Lower_Arc C

proof end;

theorem :: JORDAN1K:63

for C being Simple_closed_curve holds Upper_Middle_Point C in Upper_Arc C

proof end;