:: On Some Points of a Simple Closed Curve :: by Artur Korni{\l}owicz :: :: Received October 6, 2004 :: Copyright (c) 2004-2012 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 ) proofend; 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 proofend; theorem :: JORDAN21:1 for n being Element of NAT for p being Point of (TOP-REAL n) holds {p} is bounded proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: JORDAN21:6 for p being Point of (TOP-REAL 2) holds (north_halfline p) \ {p} is convex proofend; theorem :: JORDAN21:7 for p being Point of (TOP-REAL 2) holds (south_halfline p) \ {p} is convex proofend; theorem :: JORDAN21:8 for p being Point of (TOP-REAL 2) holds (west_halfline p) \ {p} is convex proofend; theorem :: JORDAN21:9 for p being Point of (TOP-REAL 2) holds (east_halfline p) \ {p} is convex proofend; theorem :: JORDAN21:10 for A being Subset of the carrier of (TOP-REAL 2) holds UBD A misses A proofend; 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) ) proofend; definition let D be Subset of (TOP-REAL 2); attrD 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 Element of K6( the carrier 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 proofend; end; registration cluster being_simple_closed_curve -> with_the_max_arc for Element of K6( the carrier of (TOP-REAL 2)); coherence for b1 being Simple_closed_curve holds b1 is with_the_max_arc proofend; end; registration cluster non empty closed connected compact bounded non horizontal non vertical being_simple_closed_curve with_the_max_arc for Element of K6( the carrier of (TOP-REAL 2)); existence not for b1 being Simple_closed_curve holds b1 is empty proofend; 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 proofend; 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 ) proofend; begin theorem Th14: :: JORDAN21:14 for C being Simple_closed_curve holds Lower_Middle_Point C in C proofend; theorem Th15: :: JORDAN21:15 for C being Simple_closed_curve holds (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2 proofend; theorem :: JORDAN21:16 for C being Simple_closed_curve holds Lower_Middle_Point C <> Upper_Middle_Point C proofend; begin theorem Th17: :: JORDAN21:17 for C being Simple_closed_curve holds W-bound C = W-bound (Upper_Arc C) proofend; theorem Th18: :: JORDAN21:18 for C being Simple_closed_curve holds E-bound C = E-bound (Upper_Arc C) proofend; theorem Th19: :: JORDAN21:19 for C being Simple_closed_curve holds W-bound C = W-bound (Lower_Arc C) proofend; theorem Th20: :: JORDAN21:20 for C being Simple_closed_curve holds E-bound C = E-bound (Lower_Arc C) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; registration let C be Simple_closed_curve; cluster Lower_Arc C -> with_the_max_arc ; coherence Lower_Arc C is with_the_max_arc proofend; cluster Upper_Arc C -> with_the_max_arc ; coherence Upper_Arc C is with_the_max_arc proofend; 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; :: 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 proofend; theorem Th25: :: JORDAN21:25 for C being compact non vertical Subset of (TOP-REAL 2) holds UMP C <> E-max C proofend; theorem Th26: :: JORDAN21:26 for C being compact non vertical Subset of (TOP-REAL 2) holds LMP C <> W-min C proofend; theorem Th27: :: JORDAN21:27 for C being compact non vertical Subset of (TOP-REAL 2) holds LMP C <> E-max C proofend; theorem :: JORDAN21:28 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 proofend; theorem :: JORDAN21:29 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 proofend; theorem Th30: :: JORDAN21:30 for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds UMP D in D proofend; theorem Th31: :: JORDAN21:31 for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds LMP D in D proofend; theorem Th32: :: JORDAN21:32 for P being Subset of (TOP-REAL 2) holds LSeg ((UMP P),|[(((W-bound P) + (E-bound P)) / 2),(N-bound P)]|) is vertical proofend; theorem Th33: :: JORDAN21:33 for P being Subset of (TOP-REAL 2) holds LSeg ((LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]|) is vertical proofend; theorem Th34: :: JORDAN21:34 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)} proofend; theorem Th35: :: JORDAN21:35 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)} proofend; theorem Th36: :: JORDAN21:36 for C being Simple_closed_curve holds (LMP C) `2 < (UMP C) `2 proofend; theorem Th37: :: JORDAN21:37 for C being Simple_closed_curve holds UMP C <> LMP C proofend; theorem Th38: :: JORDAN21:38 for C being Simple_closed_curve holds S-bound C < (UMP C) `2 proofend; theorem Th39: :: JORDAN21:39 for C being Simple_closed_curve holds (UMP C) `2 <= N-bound C proofend; theorem Th40: :: JORDAN21:40 for C being Simple_closed_curve holds S-bound C <= (LMP C) `2 proofend; theorem Th41: :: JORDAN21:41 for C being Simple_closed_curve holds (LMP C) `2 < N-bound C proofend; theorem Th42: :: JORDAN21:42 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)]|) proofend; theorem :: JORDAN21:43 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 proofend; theorem :: JORDAN21:44 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 proofend; theorem :: JORDAN21:45 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 proofend; theorem :: JORDAN21:46 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 proofend; theorem :: JORDAN21:47 for C being Simple_closed_curve holds (UMP (Upper_Arc C)) `2 <= N-bound C proofend; theorem :: JORDAN21:48 for C being Simple_closed_curve holds S-bound C <= (LMP (Lower_Arc C)) `2 proofend; theorem :: JORDAN21:49 for C being Simple_closed_curve holds ( not LMP C in Lower_Arc C or not UMP C in Lower_Arc C ) proofend; theorem :: JORDAN21:50 for C being Simple_closed_curve holds ( not LMP C in Upper_Arc C or not UMP C in Upper_Arc C ) proofend;