:: by Andrzej Trybulec

::

:: Received August 18, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

theorem Th1: :: JORDAN_A:1

for T being non empty TopSpace

for f being continuous RealMap of T

for A being compact Subset of T holds f .: A is compact

for f being continuous RealMap of T

for A being compact Subset of T holds f .: A is compact

proof end;

theorem Th2: :: JORDAN_A:2

for A being compact Subset of REAL

for B being non empty Subset of REAL st B c= A holds

lower_bound B in A

for B being non empty Subset of REAL st B c= A holds

lower_bound B in A

proof end;

theorem :: JORDAN_A:3

for n being Nat

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

for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]

for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: A)

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

for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]

for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: A)

proof end;

theorem :: JORDAN_A:4

for n being Nat

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

for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]

for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

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

for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]

for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

proof end;

theorem Th5: :: JORDAN_A:5

for C being Simple_closed_curve

for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds

LE E-max C,q,C

for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds

LE E-max C,q,C

proof end;

theorem Th6: :: JORDAN_A:6

for C being Simple_closed_curve

for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds

LE q, E-max C,C

for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds

LE q, E-max C,C

proof end;

definition

let n be Nat;

A1: [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:def 2;

ex b_{1} being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st

for p, q being Point of (TOP-REAL n) holds b_{1} . (p,q) = |.(p - q).|

for b_{1}, b_{2} being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st ( for p, q being Point of (TOP-REAL n) holds b_{1} . (p,q) = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds b_{2} . (p,q) = |.(p - q).| ) holds

b_{1} = b_{2}

end;
A1: [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:def 2;

func Eucl_dist n -> RealMap of [:(TOP-REAL n),(TOP-REAL n):] means :Def1: :: JORDAN_A:def 1

for p, q being Point of (TOP-REAL n) holds it . (p,q) = |.(p - q).|;

existence for p, q being Point of (TOP-REAL n) holds it . (p,q) = |.(p - q).|;

ex b

for p, q being Point of (TOP-REAL n) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Eucl_dist JORDAN_A:def 1 :

for n being Nat

for b_{2} being RealMap of [:(TOP-REAL n),(TOP-REAL n):] holds

( b_{2} = Eucl_dist n iff for p, q being Point of (TOP-REAL n) holds b_{2} . (p,q) = |.(p - q).| );

for n being Nat

for b

( b

definition

let T be non empty TopSpace;

let f be RealMap of T;

( f is continuous iff for p being Point of T

for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N )

end;
let f be RealMap of T;

redefine attr f is continuous means :: JORDAN_A:def 2

for p being Point of T

for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N;

compatibility for p being Point of T

for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N;

( f is continuous iff for p being Point of T

for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N )

proof end;

:: deftheorem defines continuous JORDAN_A:def 2 :

for T being non empty TopSpace

for f being RealMap of T holds

( f is continuous iff for p being Point of T

for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N );

for T being non empty TopSpace

for f being RealMap of T holds

( f is continuous iff for p being Point of T

for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N );

Lm1: for X, Y being TopSpace holds TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):]

proof end;

registration
end;

theorem Th7: :: JORDAN_A:7

for n being Nat

for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds

dist_min (A,B) > 0

for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds

dist_min (A,B) > 0

proof end;

theorem Th8: :: JORDAN_A:8

for C being Simple_closed_curve

for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds

Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q)

for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds

Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q)

proof end;

theorem Th9: :: JORDAN_A:9

for C being Simple_closed_curve

for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds

Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)

for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds

Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)

proof end;

theorem Th10: :: JORDAN_A:10

for C being Simple_closed_curve

for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds

Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))

for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds

Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))

proof end;

theorem Th11: :: JORDAN_A:11

for C being Simple_closed_curve

for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds

Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)

for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds

Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)

proof end;

theorem Th12: :: JORDAN_A:12

for C being Simple_closed_curve

for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds

Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))

for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds

Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))

proof end;

theorem Th13: :: JORDAN_A:13

for C being Simple_closed_curve

for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds

Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)))

for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds

Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)))

proof end;

theorem Th14: :: JORDAN_A:14

for C being Simple_closed_curve

for p being Point of (TOP-REAL 2) holds R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C))

for p being Point of (TOP-REAL 2) holds R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C))

proof end;

theorem Th15: :: JORDAN_A:15

for C being Simple_closed_curve

for p being Point of (TOP-REAL 2) holds L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)

for p being Point of (TOP-REAL 2) holds L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)

proof end;

theorem Th16: :: JORDAN_A:16

for C being Simple_closed_curve

for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds

Segment (p,(W-min C),C) is_an_arc_of p, W-min C

for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds

Segment (p,(W-min C),C) is_an_arc_of p, W-min C

proof end;

theorem Th17: :: JORDAN_A:17

for C being Simple_closed_curve

for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds

Segment (p,q,C) is_an_arc_of p,q

for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds

Segment (p,q,C) is_an_arc_of p,q

proof end;

theorem Th19: :: JORDAN_A:19

for C being Simple_closed_curve

for q being Point of (TOP-REAL 2) st q in C holds

Segment (q,(W-min C),C) is compact

for q being Point of (TOP-REAL 2) st q in C holds

Segment (q,(W-min C),C) is compact

proof end;

theorem Th20: :: JORDAN_A:20

for C being Simple_closed_curve

for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds

Segment (q1,q2,C) is compact

for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds

Segment (q1,q2,C) is compact

proof end;

definition

let C be Simple_closed_curve;

ex b_{1} being FinSequence of (TOP-REAL 2) st

( b_{1} /. 1 = W-min C & b_{1} is one-to-one & 8 <= len b_{1} & rng b_{1} c= C & ( for i being Nat st 1 <= i & i < len b_{1} holds

LE b_{1} /. i,b_{1} /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len b_{1} holds

(Segment ((b_{1} /. i),(b_{1} /. (i + 1)),C)) /\ (Segment ((b_{1} /. (i + 1)),(b_{1} /. (i + 2)),C)) = {(b_{1} /. (i + 1))} ) & (Segment ((b_{1} /. (len b_{1})),(b_{1} /. 1),C)) /\ (Segment ((b_{1} /. 1),(b_{1} /. 2),C)) = {(b_{1} /. 1)} & (Segment ((b_{1} /. ((len b_{1}) -' 1)),(b_{1} /. (len b_{1})),C)) /\ (Segment ((b_{1} /. (len b_{1})),(b_{1} /. 1),C)) = {(b_{1} /. (len b_{1}))} & Segment ((b_{1} /. ((len b_{1}) -' 1)),(b_{1} /. (len b_{1})),C) misses Segment ((b_{1} /. 1),(b_{1} /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len b_{1} & i,j aren't_adjacent holds

Segment ((b_{1} /. i),(b_{1} /. (i + 1)),C) misses Segment ((b_{1} /. j),(b_{1} /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len b_{1} holds

Segment ((b_{1} /. (len b_{1})),(b_{1} /. 1),C) misses Segment ((b_{1} /. i),(b_{1} /. (i + 1)),C) ) )

end;
mode Segmentation of C -> FinSequence of (TOP-REAL 2) means :Def3: :: JORDAN_A:def 3

( it /. 1 = W-min C & it is one-to-one & 8 <= len it & rng it c= C & ( for i being Nat st 1 <= i & i < len it holds

LE it /. i,it /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len it holds

(Segment ((it /. i),(it /. (i + 1)),C)) /\ (Segment ((it /. (i + 1)),(it /. (i + 2)),C)) = {(it /. (i + 1))} ) & (Segment ((it /. (len it)),(it /. 1),C)) /\ (Segment ((it /. 1),(it /. 2),C)) = {(it /. 1)} & (Segment ((it /. ((len it) -' 1)),(it /. (len it)),C)) /\ (Segment ((it /. (len it)),(it /. 1),C)) = {(it /. (len it))} & Segment ((it /. ((len it) -' 1)),(it /. (len it)),C) misses Segment ((it /. 1),(it /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len it & i,j aren't_adjacent holds

Segment ((it /. i),(it /. (i + 1)),C) misses Segment ((it /. j),(it /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len it holds

Segment ((it /. (len it)),(it /. 1),C) misses Segment ((it /. i),(it /. (i + 1)),C) ) );

existence ( it /. 1 = W-min C & it is one-to-one & 8 <= len it & rng it c= C & ( for i being Nat st 1 <= i & i < len it holds

LE it /. i,it /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len it holds

(Segment ((it /. i),(it /. (i + 1)),C)) /\ (Segment ((it /. (i + 1)),(it /. (i + 2)),C)) = {(it /. (i + 1))} ) & (Segment ((it /. (len it)),(it /. 1),C)) /\ (Segment ((it /. 1),(it /. 2),C)) = {(it /. 1)} & (Segment ((it /. ((len it) -' 1)),(it /. (len it)),C)) /\ (Segment ((it /. (len it)),(it /. 1),C)) = {(it /. (len it))} & Segment ((it /. ((len it) -' 1)),(it /. (len it)),C) misses Segment ((it /. 1),(it /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len it & i,j aren't_adjacent holds

Segment ((it /. i),(it /. (i + 1)),C) misses Segment ((it /. j),(it /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len it holds

Segment ((it /. (len it)),(it /. 1),C) misses Segment ((it /. i),(it /. (i + 1)),C) ) );

ex b

( b

LE b

(Segment ((b

Segment ((b

Segment ((b

proof end;

:: deftheorem Def3 defines Segmentation JORDAN_A:def 3 :

for C being Simple_closed_curve

for b_{2} being FinSequence of (TOP-REAL 2) holds

( b_{2} is Segmentation of C iff ( b_{2} /. 1 = W-min C & b_{2} is one-to-one & 8 <= len b_{2} & rng b_{2} c= C & ( for i being Nat st 1 <= i & i < len b_{2} holds

LE b_{2} /. i,b_{2} /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len b_{2} holds

(Segment ((b_{2} /. i),(b_{2} /. (i + 1)),C)) /\ (Segment ((b_{2} /. (i + 1)),(b_{2} /. (i + 2)),C)) = {(b_{2} /. (i + 1))} ) & (Segment ((b_{2} /. (len b_{2})),(b_{2} /. 1),C)) /\ (Segment ((b_{2} /. 1),(b_{2} /. 2),C)) = {(b_{2} /. 1)} & (Segment ((b_{2} /. ((len b_{2}) -' 1)),(b_{2} /. (len b_{2})),C)) /\ (Segment ((b_{2} /. (len b_{2})),(b_{2} /. 1),C)) = {(b_{2} /. (len b_{2}))} & Segment ((b_{2} /. ((len b_{2}) -' 1)),(b_{2} /. (len b_{2})),C) misses Segment ((b_{2} /. 1),(b_{2} /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len b_{2} & i,j aren't_adjacent holds

Segment ((b_{2} /. i),(b_{2} /. (i + 1)),C) misses Segment ((b_{2} /. j),(b_{2} /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len b_{2} holds

Segment ((b_{2} /. (len b_{2})),(b_{2} /. 1),C) misses Segment ((b_{2} /. i),(b_{2} /. (i + 1)),C) ) ) );

for C being Simple_closed_curve

for b

( b

LE b

(Segment ((b

Segment ((b

Segment ((b

registration

let C be Simple_closed_curve;

coherence

for b_{1} being Segmentation of C holds not b_{1} is trivial

end;
coherence

for b

proof end;

theorem Th21: :: JORDAN_A:21

for C being Simple_closed_curve

for S being Segmentation of C

for i being Nat st 1 <= i & i <= len S holds

S /. i in C

for S being Segmentation of C

for i being Nat st 1 <= i & i <= len S holds

S /. i in C

proof end;

definition

let C be Simple_closed_curve;

let i be Nat;

let S be Segmentation of C;

coherence

( ( 1 <= i & i < len S implies Segment ((S /. i),(S /. (i + 1)),C) is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len S ) implies Segment ((S /. (len S)),(S /. 1),C) is Subset of (TOP-REAL 2) ) );

consistency

for b_{1} being Subset of (TOP-REAL 2) holds verum;

;

end;
let i be Nat;

let S be Segmentation of C;

func Segm (S,i) -> Subset of (TOP-REAL 2) equals :Def4: :: JORDAN_A:def 4

Segment ((S /. i),(S /. (i + 1)),C) if ( 1 <= i & i < len S )

otherwise Segment ((S /. (len S)),(S /. 1),C);

correctness Segment ((S /. i),(S /. (i + 1)),C) if ( 1 <= i & i < len S )

otherwise Segment ((S /. (len S)),(S /. 1),C);

coherence

( ( 1 <= i & i < len S implies Segment ((S /. i),(S /. (i + 1)),C) is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len S ) implies Segment ((S /. (len S)),(S /. 1),C) is Subset of (TOP-REAL 2) ) );

consistency

for b

;

:: deftheorem Def4 defines Segm JORDAN_A:def 4 :

for C being Simple_closed_curve

for i being Nat

for S being Segmentation of C holds

( ( 1 <= i & i < len S implies Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) ) & ( ( not 1 <= i or not i < len S ) implies Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) );

for C being Simple_closed_curve

for i being Nat

for S being Segmentation of C holds

( ( 1 <= i & i < len S implies Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) ) & ( ( not 1 <= i or not i < len S ) implies Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) );

theorem :: JORDAN_A:22

for C being Simple_closed_curve

for i being Nat

for S being Segmentation of C st i in dom S holds

Segm (S,i) c= C

for i being Nat

for S being Segmentation of C st i in dom S holds

Segm (S,i) c= C

proof end;

registration

let C be Simple_closed_curve;

let S be Segmentation of C;

let i be Nat;

coherence

( not Segm (S,i) is empty & Segm (S,i) is compact )

end;
let S be Segmentation of C;

let i be Nat;

coherence

( not Segm (S,i) is empty & Segm (S,i) is compact )

proof end;

theorem :: JORDAN_A:23

for C being Simple_closed_curve

for S being Segmentation of C

for p being Point of (TOP-REAL 2) st p in C holds

ex i being Nat st

( i in dom S & p in Segm (S,i) )

for S being Segmentation of C

for p being Point of (TOP-REAL 2) st p in C holds

ex i being Nat st

( i in dom S & p in Segm (S,i) )

proof end;

theorem Th24: :: JORDAN_A:24

for C being Simple_closed_curve

for S being Segmentation of C

for i, j being Nat st 1 <= i & i < j & j < len S & i,j aren't_adjacent holds

Segm (S,i) misses Segm (S,j)

for S being Segmentation of C

for i, j being Nat st 1 <= i & i < j & j < len S & i,j aren't_adjacent holds

Segm (S,i) misses Segm (S,j)

proof end;

theorem Th25: :: JORDAN_A:25

for C being Simple_closed_curve

for S being Segmentation of C

for j being Nat st 1 < j & j < (len S) -' 1 holds

Segm (S,(len S)) misses Segm (S,j)

for S being Segmentation of C

for j being Nat st 1 < j & j < (len S) -' 1 holds

Segm (S,(len S)) misses Segm (S,j)

proof end;

theorem Th26: :: JORDAN_A:26

for C being Simple_closed_curve

for S being Segmentation of C

for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent holds

(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}

for S being Segmentation of C

for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent holds

(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}

proof end;

theorem Th27: :: JORDAN_A:27

for C being Simple_closed_curve

for S being Segmentation of C

for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent holds

Segm (S,i) meets Segm (S,j)

for S being Segmentation of C

for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent holds

Segm (S,i) meets Segm (S,j)

proof end;

theorem Th28: :: JORDAN_A:28

for C being Simple_closed_curve

for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)}

for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)}

proof end;

theorem Th29: :: JORDAN_A:29

for C being Simple_closed_curve

for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,1)

for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,1)

proof end;

theorem Th30: :: JORDAN_A:30

for C being Simple_closed_curve

for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))}

for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))}

proof end;

theorem Th31: :: JORDAN_A:31

for C being Simple_closed_curve

for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,((len S) -' 1))

for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,((len S) -' 1))

proof end;

definition

let n be Nat;

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

ex b_{1} being Real ex W being Subset of (Euclid n) st

( W = C & b_{1} = diameter W )

uniqueness

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

( W = C & b_{1} = diameter W ) & ex W being Subset of (Euclid n) st

( W = C & b_{2} = diameter W ) holds

b_{1} = b_{2};

;

end;
let C be Subset of (TOP-REAL n);

func diameter C -> Real means :Def5: :: JORDAN_A:def 5

ex W being Subset of (Euclid n) st

( W = C & it = diameter W );

existence ex W being Subset of (Euclid n) st

( W = C & it = diameter W );

ex b

( W = C & b

proof end;

correctness uniqueness

for b

( W = C & b

( W = C & b

b

;

:: deftheorem Def5 defines diameter JORDAN_A:def 5 :

for n being Nat

for C being Subset of (TOP-REAL n)

for b_{3} being Real holds

( b_{3} = diameter C iff ex W being Subset of (Euclid n) st

( W = C & b_{3} = diameter W ) );

for n being Nat

for C being Subset of (TOP-REAL n)

for b

( b

( W = C & b

definition

let C be Simple_closed_curve;

let S be Segmentation of C;

ex b_{1} being Real ex S1 being non empty finite Subset of REAL st

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b_{1} = max S1 )

uniqueness

for b_{1}, b_{2} being Real st ex S1 being non empty finite Subset of REAL st

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b_{1} = max S1 ) & ex S1 being non empty finite Subset of REAL st

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b_{2} = max S1 ) holds

b_{1} = b_{2};

;

end;
let S be Segmentation of C;

func diameter S -> Real means :Def6: :: JORDAN_A:def 6

ex S1 being non empty finite Subset of REAL st

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & it = max S1 );

existence ex S1 being non empty finite Subset of REAL st

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & it = max S1 );

ex b

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b

proof end;

correctness uniqueness

for b

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b

b

;

:: deftheorem Def6 defines diameter JORDAN_A:def 6 :

for C being Simple_closed_curve

for S being Segmentation of C

for b_{3} being Real holds

( b_{3} = diameter S iff ex S1 being non empty finite Subset of REAL st

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b_{3} = max S1 ) );

for C being Simple_closed_curve

for S being Segmentation of C

for b

( b

( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b

theorem :: JORDAN_A:32

for C being Simple_closed_curve

for S being Segmentation of C

for i being Nat holds diameter (Segm (S,i)) <= diameter S

for S being Segmentation of C

for i being Nat holds diameter (Segm (S,i)) <= diameter S

proof end;

theorem Th33: :: JORDAN_A:33

for C being Simple_closed_curve

for S being Segmentation of C

for e being Real st ( for i being Nat holds diameter (Segm (S,i)) < e ) holds

diameter S < e

for S being Segmentation of C

for e being Real st ( for i being Nat holds diameter (Segm (S,i)) < e ) holds

diameter S < e

proof end;

theorem :: JORDAN_A:34

for C being Simple_closed_curve

for e being Real st e > 0 holds

ex S being Segmentation of C st diameter S < e

for e being Real st e > 0 holds

ex S being Segmentation of C st diameter S < e

proof end;

definition

let C be Simple_closed_curve;

let S be Segmentation of C;

ex b_{1} being Real ex S1, S2 being non empty finite Subset of REAL st

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b_{1} = min ((min S1),(min S2)) )

uniqueness

for b_{1}, b_{2} being Real st ex S1, S2 being non empty finite Subset of REAL st

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b_{1} = min ((min S1),(min S2)) ) & ex S1, S2 being non empty finite Subset of REAL st

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b_{2} = min ((min S1),(min S2)) ) holds

b_{1} = b_{2};

;

end;
let S be Segmentation of C;

func S-Gap S -> Real means :Def7: :: JORDAN_A:def 7

ex S1, S2 being non empty finite Subset of REAL st

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & it = min ((min S1),(min S2)) );

existence ex S1, S2 being non empty finite Subset of REAL st

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & it = min ((min S1),(min S2)) );

ex b

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b

proof end;

correctness uniqueness

for b

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b

b

;

:: deftheorem Def7 defines S-Gap JORDAN_A:def 7 :

for C being Simple_closed_curve

for S being Segmentation of C

for b_{3} being Real holds

( b_{3} = S-Gap S iff ex S1, S2 being non empty finite Subset of REAL st

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b_{3} = min ((min S1),(min S2)) ) );

for C being Simple_closed_curve

for S being Segmentation of C

for b

( b

( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b

theorem Th35: :: JORDAN_A:35

for C being Simple_closed_curve

for S being Segmentation of C ex F being non empty finite Subset of REAL st

( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Nat : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F )

for S being Segmentation of C ex F being non empty finite Subset of REAL st

( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Nat : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F )

proof end;