:: On Some Points of a Simple Closed Curve :: by Artur Korni{\l}owicz :: :: Received October 6, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TOPREAL2, SUBSET_1, EUCLID, PRE_TOPC, NUMBERS, RELAT_1, STRUCT_0, FUNCT_1, XBOOLE_0, JORDAN2C, XXREAL_2, REAL_1, ARYTM_3, CONVEX1, MCART_1, RLTOPSP1, ARYTM_1, CARD_1, XXREAL_0, TOPREAL1, TARSKI, JORDAN6, PSCOMP_1, RCOMP_1, RELAT_2, SPPOL_1, JORDAN3, JORDAN21, SEQ_4; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XXREAL_0, XCMPLX_0, REAL_1, FUNCT_1, RELSET_1, SEQ_4, DOMAIN_1, XXREAL_2, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, TBSP_1, RCOMP_1, PSCOMP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, JORDAN2C, SPPOL_1, JORDAN6, JORDAN5C; constructors REAL_1, RCOMP_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL1, SPPOL_1, PSCOMP_1, JORDAN5C, JORDAN6, JORDAN2C, SEQ_4, CONVEX1, BINOP_2, TOPMETR, COMPLEX1; registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, TOPREAL5, JORDAN6, TOPREAL6, RLTOPSP1, JORDAN2C; requirements SUBSET, BOOLE, NUMERALS, ARITHM; begin :: On the Subsets of TOP-REAL 2 reserve C for Simple_closed_curve, P for Subset of TOP-REAL 2, p for Point of TOP-REAL 2, n for Element of NAT; theorem :: JORDAN21:1 for p being Point of TOP-REAL n holds {p} is bounded; theorem :: JORDAN21:2 :: P is an open east halfline for s1,t being Real, P being Subset of TOP-REAL 2 st P = { |[ s,t ]| where s is Real: s1 < s } holds P is convex; theorem :: JORDAN21:3 :: P is an open west halfline for s2,t being Real, P being Subset of TOP-REAL 2 st P = { |[ s,t ]| where s is Real : s < s2 } holds P is convex; theorem :: JORDAN21:4 :: P is an open north halfline for s,t1 being Real, P being Subset of TOP-REAL 2 st P = { |[ s,t ]| where t is Real : t1 < t } holds P is convex; theorem :: JORDAN21:5 :: P is an open south halfline for s,t2 being Real, P being Subset of TOP-REAL 2 st P = { |[ s,t ]| where t is Real : t < t2 } holds P is convex; theorem :: JORDAN21:6 north_halfline p \ {p} is convex; theorem :: JORDAN21:7 south_halfline p \ {p} is convex; theorem :: JORDAN21:8 west_halfline p \ {p} is convex; theorem :: JORDAN21:9 east_halfline p \ {p} is convex; theorem :: JORDAN21:10 for A being Subset of the carrier of TOP-REAL 2 holds UBD A misses A; theorem :: JORDAN21:11 for P being Subset of the carrier of TOP-REAL 2, 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); definition let D be Subset of TOP-REAL 2; attr D is with_the_max_arc means :: JORDAN21:def 1 D meets Vertical_Line((W-bound D+ E-bound D)/2); end; registration cluster with_the_max_arc -> non empty for Subset of TOP-REAL 2; end; registration cluster -> with_the_max_arc for Simple_closed_curve; end; registration cluster non empty for Simple_closed_curve; end; reserve D for compact with_the_max_arc Subset of TOP-REAL 2; theorem :: JORDAN21:12 for D being with_the_max_arc Subset of TOP-REAL 2 holds proj2.:( D /\ Vertical_Line((W-bound D + E-bound D) / 2)) is not empty; theorem :: 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 bounded_below bounded_above; begin :: Middle Points theorem :: JORDAN21:14 Lower_Middle_Point C in C; theorem :: JORDAN21:15 (Lower_Middle_Point C)`2 <> (Upper_Middle_Point C)`2; theorem :: JORDAN21:16 Lower_Middle_Point C <> Upper_Middle_Point C; begin :: Upper_Arc and Lower_Arc theorem :: JORDAN21:17 W-bound C = W-bound Upper_Arc C; theorem :: JORDAN21:18 E-bound C = E-bound Upper_Arc C; theorem :: JORDAN21:19 W-bound C = W-bound Lower_Arc C; theorem :: JORDAN21:20 E-bound C = E-bound Lower_Arc C; theorem :: JORDAN21:21 Upper_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2) is not empty & proj2.:(Upper_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2)) is not empty; theorem :: JORDAN21:22 Lower_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2) is not empty & proj2.:(Lower_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2)) is not empty; theorem :: JORDAN21:23 for P being compact connected Subset of TOP-REAL 2 st P c= C & W-min C in P & E-max C in P holds Upper_Arc C c= P or Lower_Arc C c= P; registration let C; cluster Lower_Arc C -> with_the_max_arc; cluster Upper_Arc C -> with_the_max_arc; end; begin :: UMP and LMP 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))) ]|; 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))) ]|; end; theorem :: JORDAN21:24 for C being non vertical compact Subset of TOP-REAL 2 holds UMP C <> W-min C; theorem :: JORDAN21:25 for C being non vertical compact Subset of TOP-REAL 2 holds UMP C <> E-max C; theorem :: JORDAN21:26 for C being non vertical compact Subset of TOP-REAL 2 holds LMP C <> W-min C; theorem :: JORDAN21:27 for C being non vertical compact Subset of TOP-REAL 2 holds LMP C <> E-max C; theorem :: JORDAN21:28 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; theorem :: JORDAN21:29 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; theorem :: JORDAN21:30 UMP D in D; theorem :: JORDAN21:31 LMP D in D; theorem :: JORDAN21:32 LSeg(UMP P, |[ (W-bound P + E-bound P) / 2, N-bound P]|) is vertical; theorem :: JORDAN21:33 LSeg(LMP P, |[ (W-bound P + E-bound P) / 2, S-bound P]|) is vertical; theorem :: JORDAN21:34 LSeg(UMP D, |[ (W-bound D + E-bound D) / 2, N-bound D]|) /\ D = { UMP D }; theorem :: JORDAN21:35 LSeg(LMP D, |[ (W-bound D + E-bound D) / 2, S-bound D]|) /\ D = { LMP D }; theorem :: JORDAN21:36 (LMP C)`2 < (UMP C)`2; theorem :: JORDAN21:37 UMP C <> LMP C; theorem :: JORDAN21:38 S-bound C < (UMP C)`2; theorem :: JORDAN21:39 (UMP C)`2 <= N-bound C; theorem :: JORDAN21:40 S-bound C <= (LMP C)`2; theorem :: JORDAN21:41 (LMP C)`2 < N-bound C; theorem :: JORDAN21:42 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]|); 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 & A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non empty & proj2.:(B /\ Vertical_Line ((W-bound A + E-bound A) / 2)) is bounded_above holds (UMP A)`2 <= (UMP B)`2; 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 & A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non empty & proj2.:(B /\ Vertical_Line ((W-bound A + E-bound A) / 2)) is bounded_below holds (LMP B)`2 <= (LMP A)`2; theorem :: JORDAN21:45 for A, B being Subset of TOP-REAL 2 st A c= B & UMP B in A & A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non 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; theorem :: JORDAN21:46 for A, B being Subset of TOP-REAL 2 st A c= B & LMP B in A & A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non 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; theorem :: JORDAN21:47 (UMP Upper_Arc C)`2 <= N-bound C; theorem :: JORDAN21:48 S-bound C <= (LMP Lower_Arc C)`2; theorem :: JORDAN21:49 not (LMP C in Lower_Arc C & UMP C in Lower_Arc C); theorem :: JORDAN21:50 not (LMP C in Upper_Arc C & UMP C in Upper_Arc C);