:: On Some Points of a Simple Closed Curve
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 2004 Association of Mizar Users

begin

Lm1: dom proj2 = the carrier of ()
by FUNCT_2:def 1;

Lm2: for r being real number
for X being Subset of () st r in proj2 .: X holds
ex x being Point of () 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;

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
for n being Element of NAT
for p being Point of () holds {p} is Bounded
proof end;

theorem Th2: :: JORDAN21:2
for s1, t being real number
for P being Subset of () 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 () 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 () 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 () st P = { |[s,t]| where t is Real : t < t2 } holds
P is convex
proof end;

theorem :: JORDAN21:6
for p being Point of () holds () \ {p} is convex
proof end;

theorem :: JORDAN21:7
for p being Point of () holds () \ {p} is convex
proof end;

theorem :: JORDAN21:8
for p being Point of () holds () \ {p} is convex
proof end;

theorem :: JORDAN21:9
for p being Point of () holds () \ {p} is convex
proof end;

theorem :: JORDAN21:10
for A being Subset of the carrier of () holds UBD A misses A
proof end;

theorem Th11: :: JORDAN21:11
for P being Subset of the carrier of ()
for p1, p2, q1, q2 being Point of () 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 ();
attr D is with_the_max_arc means :Def1: :: JORDAN21:def 1
D meets Vertical_Line ((() + ()) / 2);
end;

:: deftheorem Def1 defines with_the_max_arc JORDAN21:def 1 :
for D being Subset of () holds
( D is with_the_max_arc iff D meets Vertical_Line ((() + ()) / 2) );

registration
cluster with_the_max_arc -> non empty Element of K18( the carrier of ());
coherence
for b1 being Subset of () st b1 is with_the_max_arc holds
not b1 is empty
proof end;
end;

registration
cluster being_simple_closed_curve -> with_the_max_arc Element of K18( the carrier of ());
coherence
for b1 being Simple_closed_curve holds b1 is with_the_max_arc
proof end;
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 ());
existence
not for b1 being Simple_closed_curve holds b1 is empty
proof end;
end;

theorem Th12: :: JORDAN21:12
for D being with_the_max_arc Subset of () holds not proj2 .: (D /\ (Vertical_Line ((() + ()) / 2))) is empty
proof end;

theorem Th13: :: JORDAN21:13
for C being compact Subset of () holds
( proj2 .: (C /\ (Vertical_Line ((() + ()) / 2))) is closed & proj2 .: (C /\ (Vertical_Line ((() + ()) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line ((() + ()) / 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
for C being Simple_closed_curve holds Lower_Middle_Point C in C
proof end;

theorem Th24: :: JORDAN21:24
for C being Simple_closed_curve holds `2 <> `2
proof end;

theorem :: JORDAN21:25
for C being Simple_closed_curve holds Lower_Middle_Point C <> Upper_Middle_Point C
proof end;

begin

theorem Th26: :: JORDAN21:26
for C being Simple_closed_curve holds W-bound C = W-bound ()
proof end;

theorem Th27: :: JORDAN21:27
for C being Simple_closed_curve holds E-bound C = E-bound ()
proof end;

theorem Th28: :: JORDAN21:28
for C being Simple_closed_curve holds W-bound C = W-bound ()
proof end;

theorem Th29: :: JORDAN21:29
for C being Simple_closed_curve holds E-bound C = E-bound ()
proof end;

theorem Th30: :: JORDAN21:30
for C being Simple_closed_curve holds
( not () /\ (Vertical_Line ((() + ()) / 2)) is empty & not proj2 .: (() /\ (Vertical_Line ((() + ()) / 2))) is empty )
proof end;

theorem Th31: :: JORDAN21:31
for C being Simple_closed_curve holds
( not () /\ (Vertical_Line ((() + ()) / 2)) is empty & not proj2 .: (() /\ (Vertical_Line ((() + ()) / 2))) is empty )
proof end;

theorem :: JORDAN21:32
for C being Simple_closed_curve
for P being connected compact Subset of () 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 end;

begin

definition
let P be Subset of the carrier of ();
func UMP P -> Point of () equals :: JORDAN21:def 2
|[((() + ()) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line ((() + ()) / 2)))))]|;
correctness
coherence
|[((() + ()) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line ((() + ()) / 2)))))]| is Point of ()
;
;
func LMP P -> Point of () equals :: JORDAN21:def 3
|[((() + ()) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line ((() + ()) / 2)))))]|;
correctness
coherence
|[((() + ()) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line ((() + ()) / 2)))))]| is Point of ()
;
;
end;

:: deftheorem defines UMP JORDAN21:def 2 :
for P being Subset of the carrier of () holds UMP P = |[((() + ()) / 2),(upper_bound (proj2 .: (P /\ (Vertical_Line ((() + ()) / 2)))))]|;

:: deftheorem defines LMP JORDAN21:def 3 :
for P being Subset of the carrier of () holds LMP P = |[((() + ()) / 2),(lower_bound (proj2 .: (P /\ (Vertical_Line ((() + ()) / 2)))))]|;

theorem :: JORDAN21:33
canceled;

theorem :: JORDAN21:34
canceled;

theorem :: JORDAN21:35
canceled;

theorem :: JORDAN21:36
canceled;

theorem Th37: :: JORDAN21:37
for C being compact non vertical Subset of () holds UMP C <> W-min C
proof end;

theorem Th38: :: JORDAN21:38
for C being compact non vertical Subset of () holds UMP C <> E-max C
proof end;

theorem Th39: :: JORDAN21:39
for C being compact non vertical Subset of () holds LMP C <> W-min C
proof end;

theorem Th40: :: JORDAN21:40
for C being compact non vertical Subset of () holds LMP C <> E-max C
proof end;

theorem :: JORDAN21:41
for p being Point of ()
for C being compact Subset of () st p in C /\ (Vertical_Line ((() + ()) / 2)) holds
p `2 <= (UMP C) `2
proof end;

theorem :: JORDAN21:42
for p being Point of ()
for C being compact Subset of () st p in C /\ (Vertical_Line ((() + ()) / 2)) holds
(LMP C) `2 <= p `2
proof end;

theorem Th43: :: JORDAN21:43
for D being compact with_the_max_arc Subset of () holds UMP D in D
proof end;

theorem Th44: :: JORDAN21:44
for D being compact with_the_max_arc Subset of () holds LMP D in D
proof end;

theorem Th45: :: JORDAN21:45
for P being Subset of () holds LSeg ((UMP P),|[((() + ()) / 2),()]|) is vertical
proof end;

theorem Th46: :: JORDAN21:46
for P being Subset of () holds LSeg ((LMP P),|[((() + ()) / 2),()]|) is vertical
proof end;

theorem Th47: :: JORDAN21:47
for D being compact with_the_max_arc Subset of () holds (LSeg ((UMP D),|[((() + ()) / 2),()]|)) /\ D = {(UMP D)}
proof end;

theorem Th48: :: JORDAN21:48
for D being compact with_the_max_arc Subset of () holds (LSeg ((LMP D),|[((() + ()) / 2),()]|)) /\ D = {(LMP D)}
proof end;

theorem Th49: :: JORDAN21:49
for C being Simple_closed_curve holds (LMP C) `2 < (UMP C) `2
proof end;

theorem Th50: :: JORDAN21:50
for C being Simple_closed_curve holds UMP C <> LMP C
proof end;

theorem Th51: :: JORDAN21:51
for C being Simple_closed_curve holds S-bound C < (UMP C) `2
proof end;

theorem Th52: :: JORDAN21:52
for C being Simple_closed_curve holds (UMP C) `2 <= N-bound C
proof end;

theorem Th53: :: JORDAN21:53
for C being Simple_closed_curve holds S-bound C <= (LMP C) `2
proof end;

theorem Th54: :: JORDAN21:54
for C being Simple_closed_curve holds (LMP C) `2 < N-bound C
proof end;

theorem Th55: :: JORDAN21:55
for C being Simple_closed_curve holds LSeg ((UMP C),|[((() + ()) / 2),()]|) misses LSeg ((LMP C),|[((() + ()) / 2),()]|)
proof end;

theorem :: JORDAN21:56
for A, B being Subset of () st A c= B & () + () = () + () & not A /\ (Vertical_Line ((() + ()) / 2)) is empty & proj2 .: (B /\ (Vertical_Line ((() + ()) / 2))) is bounded_above holds
(UMP A) `2 <= (UMP B) `2
proof end;

theorem :: JORDAN21:57
for A, B being Subset of () st A c= B & () + () = () + () & not A /\ (Vertical_Line ((() + ()) / 2)) is empty & proj2 .: (B /\ (Vertical_Line ((() + ()) / 2))) is bounded_below holds
(LMP B) `2 <= (LMP A) `2
proof end;

theorem :: JORDAN21:58
for A, B being Subset of () st A c= B & UMP B in A & not A /\ (Vertical_Line ((() + ()) / 2)) is empty & proj2 .: (B /\ (Vertical_Line ((() + ()) / 2))) is bounded_above & () + () = () + () holds
UMP A = UMP B
proof end;

theorem :: JORDAN21:59
for A, B being Subset of () st A c= B & LMP B in A & not A /\ (Vertical_Line ((() + ()) / 2)) is empty & proj2 .: (B /\ (Vertical_Line ((() + ()) / 2))) is bounded_below & () + () = () + () holds
LMP A = LMP B
proof end;

theorem :: JORDAN21:60
for C being Simple_closed_curve holds (UMP ()) `2 <= N-bound C
proof end;

theorem :: JORDAN21:61
for C being Simple_closed_curve holds S-bound C <= (LMP ()) `2
proof end;

theorem :: JORDAN21:62
for C being Simple_closed_curve holds
( not LMP C in Lower_Arc C or not UMP C in Lower_Arc C )
proof end;

theorem :: JORDAN21:63
for C being Simple_closed_curve holds
( not LMP C in Upper_Arc C or not UMP C in Upper_Arc C )
proof end;