:: 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);