:: by Artur Korni{\l}owicz

::

:: Received October 6, 2004

:: Copyright (c) 2004 Association of Mizar Users

begin

Lm1: dom proj2 = the carrier of (TOP-REAL 2)

by FUNCT_2:def 1;

Lm2: for r being real number

for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds

ex x being Point of (TOP-REAL 2) st

( x in X & proj2 . x = r )

proof end;

Lm3: now

let a, A, B, C be set ; :: thesis: ( not a in (A \/ B) \/ C or a in A or a in B or a in C )

assume a in (A \/ B) \/ C ; :: thesis: ( a in A or a in B or a in C )

then ( a in A \/ B or a in C ) by XBOOLE_0:def 3;

hence ( a in A or a in B or a in C ) by XBOOLE_0:def 3; :: thesis: verum

end;
assume a in (A \/ B) \/ C ; :: thesis: ( a in A or a in B or a in C )

then ( a in A \/ B or a in C ) by XBOOLE_0:def 3;

hence ( a in A or a in B or a in C ) by XBOOLE_0:def 3; :: thesis: verum

Lm4: for A, B, C, D being set st A misses D & B misses D & C misses D holds

(A \/ B) \/ C misses D

proof end;

theorem :: JORDAN21:1

proof end;

theorem Th2: :: JORDAN21:2

for s1, t being real number

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s1 < s } holds

P is convex

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s1 < s } holds

P is convex

proof end;

theorem Th3: :: JORDAN21:3

for s2, t being real number

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s < s2 } holds

P is convex

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s < s2 } holds

P is convex

proof end;

theorem Th4: :: JORDAN21:4

for s, t1 being real number

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t1 < t } holds

P is convex

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t1 < t } holds

P is convex

proof end;

theorem Th5: :: JORDAN21:5

for s, t2 being real number

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t < t2 } holds

P is convex

for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t < t2 } holds

P is convex

proof end;

theorem :: JORDAN21:6

proof end;

theorem :: JORDAN21:7

proof end;

theorem :: JORDAN21:8

proof end;

theorem :: JORDAN21:9

proof end;

theorem :: JORDAN21:10

proof end;

theorem Th11: :: JORDAN21:11

for P being Subset of the carrier of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 holds

( not p1 in Segment (P,p1,p2,q1,q2) & not p2 in Segment (P,p1,p2,q1,q2) )

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 holds

( not p1 in Segment (P,p1,p2,q1,q2) & not p2 in Segment (P,p1,p2,q1,q2) )

proof end;

definition

let D be Subset of (TOP-REAL 2);

attr D is with_the_max_arc means :Def1: :: JORDAN21:def 1

D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2);

end;
attr D is with_the_max_arc means :Def1: :: JORDAN21:def 1

D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2);

:: deftheorem Def1 defines with_the_max_arc JORDAN21:def 1 :

for D being Subset of (TOP-REAL 2) holds

( D is with_the_max_arc iff D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) );

registration

cluster with_the_max_arc -> non empty Element of K18( the carrier of (TOP-REAL 2));

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is with_the_max_arc holds

not b_{1} is empty

end;
coherence

for b

not b

proof end;

registration

cluster being_simple_closed_curve -> with_the_max_arc Element of K18( the carrier of (TOP-REAL 2));

coherence

for b_{1} being Simple_closed_curve holds b_{1} is with_the_max_arc

end;
coherence

for b

proof end;

registration

cluster non empty closed connected compact non horizontal non vertical being_simple_closed_curve with_the_max_arc Element of K18( the carrier of (TOP-REAL 2));

existence

not for b_{1} being Simple_closed_curve holds b_{1} is empty

end;
existence

not for b

proof end;

theorem Th12: :: JORDAN21:12

for D being with_the_max_arc Subset of (TOP-REAL 2) holds not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty

proof end;

theorem Th13: :: JORDAN21:13

for C being compact Subset of (TOP-REAL 2) holds

( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )

( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )

proof end;

begin

theorem :: JORDAN21:14

canceled;

theorem :: JORDAN21:15

canceled;

theorem :: JORDAN21:16

canceled;

theorem :: JORDAN21:17

canceled;

theorem :: JORDAN21:18

canceled;

theorem :: JORDAN21:19

canceled;

theorem :: JORDAN21:20

canceled;

theorem :: JORDAN21:21

canceled;

theorem :: JORDAN21:22

canceled;

theorem Th23: :: JORDAN21:23

proof end;

theorem Th24: :: JORDAN21:24

proof end;

theorem :: JORDAN21:25

proof end;

begin

theorem Th26: :: JORDAN21:26

proof end;

theorem Th27: :: JORDAN21:27

proof end;

theorem Th28: :: JORDAN21:28

proof end;

theorem Th29: :: JORDAN21:29

proof end;

theorem Th30: :: JORDAN21:30

for C being Simple_closed_curve holds

( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )

( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )

proof end;

theorem Th31: :: JORDAN21:31

for C being Simple_closed_curve holds

( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )

( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )

proof end;

theorem :: JORDAN21:32

for C being Simple_closed_curve

for P being connected compact Subset of (TOP-REAL 2) st P c= C & W-min C in P & E-max C in P & not Upper_Arc C c= P holds

Lower_Arc C c= P

for P being connected compact Subset of (TOP-REAL 2) st P c= C & W-min C in P & E-max C in P & not Upper_Arc C c= P holds

Lower_Arc C c= P

proof end;

registration

let C be Simple_closed_curve;

cluster Lower_Arc C -> with_the_max_arc ;

coherence

Lower_Arc C is with_the_max_arc

coherence

Upper_Arc C is with_the_max_arc

end;
cluster Lower_Arc C -> with_the_max_arc ;

coherence

Lower_Arc C is with_the_max_arc

proof end;

cluster Upper_Arc C -> with_the_max_arc ;coherence

Upper_Arc C is with_the_max_arc

proof end;

begin

definition

let P be Subset of the carrier of (TOP-REAL 2);

func UMP P -> Point of (TOP-REAL 2) equals :: JORDAN21:def 2

|[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

correctness

coherence

|[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]| is Point of (TOP-REAL 2);

;

func LMP P -> Point of (TOP-REAL 2) equals :: JORDAN21:def 3

|[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

correctness

coherence

|[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]| is Point of (TOP-REAL 2);

;

end;
func UMP P -> Point of (TOP-REAL 2) equals :: JORDAN21:def 2

|[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

correctness

coherence

|[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]| is Point of (TOP-REAL 2);

;

func LMP P -> Point of (TOP-REAL 2) equals :: JORDAN21:def 3

|[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

correctness

coherence

|[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]| is Point of (TOP-REAL 2);

;

:: deftheorem defines UMP JORDAN21:def 2 :

for P being Subset of the carrier of (TOP-REAL 2) holds UMP P = |[(((E-bound P) + (W-bound P)) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

:: deftheorem defines LMP JORDAN21:def 3 :

for P being Subset of the carrier of (TOP-REAL 2) holds LMP P = |[(((E-bound P) + (W-bound P)) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;

theorem :: JORDAN21:33

canceled;

theorem :: JORDAN21:34

canceled;

theorem :: JORDAN21:35

canceled;

theorem :: JORDAN21:36

canceled;

theorem Th37: :: JORDAN21:37

proof end;

theorem Th38: :: JORDAN21:38

proof end;

theorem Th39: :: JORDAN21:39

proof end;

theorem Th40: :: JORDAN21:40

proof end;

theorem :: JORDAN21:41

for p being Point of (TOP-REAL 2)

for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds

p `2 <= (UMP C) `2

for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds

p `2 <= (UMP C) `2

proof end;

theorem :: JORDAN21:42

for p being Point of (TOP-REAL 2)

for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds

(LMP C) `2 <= p `2

for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds

(LMP C) `2 <= p `2

proof end;

theorem Th43: :: JORDAN21:43

proof end;

theorem Th44: :: JORDAN21:44

proof end;

theorem Th45: :: JORDAN21:45

for P being Subset of (TOP-REAL 2) holds LSeg ((UMP P),|[(((W-bound P) + (E-bound P)) / 2),(N-bound P)]|) is vertical

proof end;

theorem Th46: :: JORDAN21:46

for P being Subset of (TOP-REAL 2) holds LSeg ((LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]|) is vertical

proof end;

theorem Th47: :: JORDAN21:47

for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg ((UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|)) /\ D = {(UMP D)}

proof end;

theorem Th48: :: JORDAN21:48

for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg ((LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|)) /\ D = {(LMP D)}

proof end;

theorem Th49: :: JORDAN21:49

proof end;

theorem Th50: :: JORDAN21:50

proof end;

theorem Th51: :: JORDAN21:51

proof end;

theorem Th52: :: JORDAN21:52

proof end;

theorem Th53: :: JORDAN21:53

proof end;

theorem Th54: :: JORDAN21:54

proof end;

theorem Th55: :: JORDAN21:55

for C being Simple_closed_curve holds LSeg ((UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]|) misses LSeg ((LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|)

proof end;

theorem :: JORDAN21:56

for A, B being Subset of (TOP-REAL 2) st A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above holds

(UMP A) `2 <= (UMP B) `2

(UMP A) `2 <= (UMP B) `2

proof end;

theorem :: JORDAN21:57

for A, B being Subset of (TOP-REAL 2) st A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_below holds

(LMP B) `2 <= (LMP A) `2

(LMP B) `2 <= (LMP A) `2

proof end;

theorem :: JORDAN21:58

for A, B being Subset of (TOP-REAL 2) st A c= B & UMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_above & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) holds

UMP A = UMP B

UMP A = UMP B

proof end;

theorem :: JORDAN21:59

for A, B being Subset of (TOP-REAL 2) st A c= B & LMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_below & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) holds

LMP A = LMP B

LMP A = LMP B

proof end;

theorem :: JORDAN21:60

proof end;

theorem :: JORDAN21:61

proof end;

theorem :: JORDAN21:62

proof end;

theorem :: JORDAN21:63

proof end;