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


Lm1: dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;

Lm2: for r being Real
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 :: thesis: for a, A, B, C being set holds
( not a in (A \/ B) \/ C or a in A or a in B or a in C )
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 (TOP-REAL n) holds {p} is bounded
proof end;

theorem Th2: :: JORDAN21:2
for s1, t being Real
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
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
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
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
for p being Point of (TOP-REAL 2) holds (north_halfline p) \ {p} is convex
proof end;

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

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

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

theorem :: JORDAN21:10
for A being Subset of the carrier of (TOP-REAL 2) holds UBD A misses A
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) )
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;

:: 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 for Subset of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) 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 for Simple_closed_curve;
coherence
for b1 being Simple_closed_curve holds b1 is with_the_max_arc
proof end;
end;

registration
cluster non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc for Simple_closed_curve;
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 (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 )
proof end;

theorem Th14: :: JORDAN21:14
for C being Simple_closed_curve holds Lower_Middle_Point C in C
proof end;

theorem Th15: :: JORDAN21:15
for C being Simple_closed_curve holds (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2
proof end;

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

theorem Th17: :: JORDAN21:17
for C being Simple_closed_curve holds W-bound C = W-bound (Upper_Arc C)
proof end;

theorem Th18: :: JORDAN21:18
for C being Simple_closed_curve holds E-bound C = E-bound (Upper_Arc C)
proof end;

theorem Th19: :: JORDAN21:19
for C being Simple_closed_curve holds W-bound C = W-bound (Lower_Arc C)
proof end;

theorem Th20: :: JORDAN21:20
for C being Simple_closed_curve holds E-bound C = E-bound (Lower_Arc C)
proof end;

theorem Th21: :: JORDAN21:21
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 )
proof end;

theorem Th22: :: JORDAN21:22
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 )
proof end;

theorem :: JORDAN21:23
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
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
proof end;
cluster Upper_Arc C -> with_the_max_arc ;
coherence
Upper_Arc C is with_the_max_arc
proof end;
end;

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;

:: 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 Th24: :: JORDAN21:24
for C being compact non vertical Subset of (TOP-REAL 2) holds UMP C <> W-min C
proof end;

theorem Th25: :: JORDAN21:25
for C being compact non vertical Subset of (TOP-REAL 2