Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### On the Rectangular Finite Sequences of the Points of the Plane

**by****Andrzej Trybulec, and****Yatsuka Nakamura**- Received November 30, 1997
- MML identifier: SPRECT_1

- [ Mizar article, MML identifier index ]

environ vocabulary REALSET1, SEQM_3, FUNCT_1, RELAT_1, FUNCOP_1, BOOLE, FINSEQ_1, PRE_TOPC, CONNSP_1, EUCLID, COMPTS_1, TOPREAL1, SPPOL_1, MCART_1, SPPOL_2, PSCOMP_1, FINSEQ_6, GOBOARD5, GOBOARD1, CARD_1, ORDINAL2, GOBOARD2, MATRIX_2, TREES_1, MATRIX_1, ABSVALUE, ARYTM_1, RCOMP_1, SEQ_2, FUNCT_5, SQUARE_1, LATTICES, ARYTM_3, JORDAN1, SUBSET_1, GOBOARD9, TOPS_1, SPRECT_1, FINSEQ_4, ARYTM; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, ABSVALUE, CARD_1, FUNCOP_1, SQUARE_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_4, FINSEQ_6, SEQM_3, SEQ_4, MATRIX_1, MATRIX_2, REALSET1, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, EUCLID, TOPREAL1, JORDAN1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, SPPOL_1, SPPOL_2, PSCOMP_1; constructors PSCOMP_1, NAT_1, SPPOL_1, SPPOL_2, TOPREAL4, REALSET1, GOBOARD2, ENUMSET1, MATRIX_2, REAL_1, ABSVALUE, GOBOARD9, JORDAN1, CONNSP_1, TOPS_1, FUNCOP_1, SQUARE_1, RCOMP_1, FINSEQ_4, COMPTS_1, PARTFUN1; clusters STRUCT_0, EUCLID, PSCOMP_1, RELSET_1, FINSEQ_6, YELLOW_6, GOBOARD2, FINSEQ_5, GOBOARD9, TEX_2, RELAT_1, GOBOARD5, PRE_TOPC, WAYBEL_2, TOPREAL1, FINSEQ_1, REALSET1, XBOOLE_0, SEQ_2, NAT_1, MEMBERED, SEQM_3; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries theorem :: SPRECT_1:1 for A being trivial set for B being set st B c= A holds B is trivial; definition cluster non constant -> non trivial Function; end; definition cluster trivial -> constant Function; end; theorem :: SPRECT_1:2 for f being Function st rng f is trivial holds f is constant; definition let f be constant Function; cluster rng f -> trivial; end; definition cluster non empty constant FinSequence; end; theorem :: SPRECT_1:3 for f,g being FinSequence st f^g is constant holds f is constant & g is constant; theorem :: SPRECT_1:4 for x,y being set st <*x,y*> is constant holds x = y; theorem :: SPRECT_1:5 for x,y,z being set st <*x,y,z*> is constant holds x = y & y = z & z = x; begin :: Topology theorem :: SPRECT_1:6 for GX being non empty TopSpace, A being Subset of GX, B being non empty Subset of GX holds A is_a_component_of B implies A <> {}; theorem :: SPRECT_1:7 for GX being TopStruct, A, B being Subset of GX holds A is_a_component_of B implies A c= B; theorem :: SPRECT_1:8 for T being non empty TopSpace, A being non empty Subset of T, B1,B2,S being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & S is_a_component_of A & B1 \/ B2 = A holds S = B1 or S = B2; theorem :: SPRECT_1:9 for T being non empty TopSpace, A being non empty Subset of T, B1,B2,C1,C2 being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & C1 is_a_component_of A & C2 is_a_component_of A & B1 \/ B2 = A & C1 \/ C2 = A holds { B1,B2 } = { C1,C2 }; begin :: Topology of Plane reserve S for Subset of TOP-REAL 2, C,C1,C2 for non empty compact Subset of TOP-REAL 2, p,q for Point of TOP-REAL 2; theorem :: SPRECT_1:10 for p,q,r being Point of TOP-REAL 2 holds L~<*p,q,r*> = LSeg(p,q) \/ LSeg(q,r); definition let n be Nat; let f be non trivial FinSequence of TOP-REAL n; cluster L~f -> non empty; end; definition let f be FinSequence of TOP-REAL 2; cluster L~f -> compact; end; theorem :: SPRECT_1:11 for A,B being Subset of TOP-REAL 2 st A c= B & B is horizontal holds A is horizontal; theorem :: SPRECT_1:12 for A,B being Subset of TOP-REAL 2 st A c= B & B is vertical holds A is vertical; definition cluster R^2-unit_square -> special_polygonal non horizontal non vertical; end; definition cluster non vertical non horizontal non empty compact Subset of TOP-REAL 2; end; begin :: Special points of a compact non empty subset of the plane theorem :: SPRECT_1:13 N-min C in C & N-max C in C; theorem :: SPRECT_1:14 S-min C in C & S-max C in C; theorem :: SPRECT_1:15 W-min C in C & W-max C in C; theorem :: SPRECT_1:16 E-min C in C & E-max C in C; theorem :: SPRECT_1:17 C is vertical iff W-bound C = E-bound C; theorem :: SPRECT_1:18 C is horizontal iff S-bound C = N-bound C; theorem :: SPRECT_1:19 NW-corner C = NE-corner C implies C is vertical; theorem :: SPRECT_1:20 SW-corner C = SE-corner C implies C is vertical; theorem :: SPRECT_1:21 NW-corner C = SW-corner C implies C is horizontal; theorem :: SPRECT_1:22 NE-corner C = SE-corner C implies C is horizontal; reserve i,j,k for Nat, t,r1,r2,s1,s2 for Real; theorem :: SPRECT_1:23 W-bound C <= E-bound C; theorem :: SPRECT_1:24 S-bound C <= N-bound C; theorem :: SPRECT_1:25 LSeg(SE-corner C, NE-corner C) = { p : p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C }; theorem :: SPRECT_1:26 LSeg(SW-corner C, SE-corner C) = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C}; theorem :: SPRECT_1:27 LSeg(NW-corner C, NE-corner C) = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C}; theorem :: SPRECT_1:28 LSeg(SW-corner C, NW-corner C) = { p : p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C}; theorem :: SPRECT_1:29 LSeg(SW-corner C,NW-corner C) /\ LSeg(NW-corner C,NE-corner C) = {NW-corner C }; theorem :: SPRECT_1:30 LSeg(NW-corner C,NE-corner C) /\ LSeg(NE-corner C,SE-corner C) = {NE-corner C} ; theorem :: SPRECT_1:31 LSeg(SE-corner C,NE-corner C) /\ LSeg(SW-corner C,SE-corner C) = {SE-corner C} ; theorem :: SPRECT_1:32 LSeg(NW-corner C,SW-corner C) /\ LSeg(SW-corner C,SE-corner C) = {SW-corner C} ; begin :: Neither vertical nor horizontal reserve D1 for non vertical non empty compact Subset of TOP-REAL 2, D2 for non horizontal non empty compact Subset of TOP-REAL 2, D for non vertical non horizontal non empty compact Subset of TOP-REAL 2; theorem :: SPRECT_1:33 W-bound D1 < E-bound D1; theorem :: SPRECT_1:34 S-bound D2 < N-bound D2; theorem :: SPRECT_1:35 LSeg(SW-corner D1,NW-corner D1) misses LSeg(SE-corner D1,NE-corner D1); theorem :: SPRECT_1:36 LSeg(SW-corner D2,SE-corner D2) misses LSeg(NW-corner D2,NE-corner D2); begin :: SpStSeq definition let C be Subset of TOP-REAL 2; func SpStSeq C -> FinSequence of TOP-REAL 2 equals :: SPRECT_1:def 1 <*NW-corner C,NE-corner C,SE-corner C*>^ <*SW-corner C,NW-corner C*>; end; theorem :: SPRECT_1:37 (SpStSeq S)/.1 = NW-corner S; theorem :: SPRECT_1:38 (SpStSeq S)/.2 = NE-corner S; theorem :: SPRECT_1:39 (SpStSeq S)/.3 = SE-corner S; theorem :: SPRECT_1:40 (SpStSeq S)/.4 = SW-corner S; theorem :: SPRECT_1:41 (SpStSeq S)/.5 = NW-corner S; theorem :: SPRECT_1:42 len SpStSeq S = 5; theorem :: SPRECT_1:43 L~SpStSeq S = (LSeg(NW-corner S,NE-corner S) \/ LSeg(NE-corner S,SE-corner S)) \/ (LSeg(SE-corner S,SW-corner S) \/ LSeg(SW-corner S,NW-corner S)); definition let D be non vertical non empty compact Subset of TOP-REAL 2; cluster SpStSeq D -> non constant; end; definition let D be non horizontal non empty compact Subset of TOP-REAL 2; cluster SpStSeq D -> non constant; end; definition let D be non vertical non horizontal non empty compact Subset of TOP-REAL 2; cluster SpStSeq D -> special unfolded circular s.c.c. standard; end; theorem :: SPRECT_1:44 L~SpStSeq D = [.W-bound D,E-bound D,S-bound D,N-bound D.]; :::: Special points of SpStSeq D (or C) theorem :: SPRECT_1:45 for T being non empty TopStruct, X being Subset of T, f be RealMap of T holds rng(f||X) = f.:X; theorem :: SPRECT_1:46 for T being non empty TopSpace, X being non empty compact Subset of T, f be continuous RealMap of T holds f.:X is bounded_below; theorem :: SPRECT_1:47 for T being non empty TopSpace, X being non empty compact Subset of T, f be continuous RealMap of T holds f.:X is bounded_above; definition cluster non empty bounded_above bounded_below Subset of REAL; end; theorem :: SPRECT_1:48 W-bound S = inf(proj1.:S); theorem :: SPRECT_1:49 S-bound S = inf(proj2.:S); theorem :: SPRECT_1:50 N-bound S = sup(proj2.:S); theorem :: SPRECT_1:51 E-bound S = sup(proj1.:S); theorem :: SPRECT_1:52 for A,B being non empty bounded_below Subset of REAL holds inf(A \/ B) = min(inf A,inf B); theorem :: SPRECT_1:53 for A,B being non empty bounded_above Subset of REAL holds sup(A \/ B) = max(sup A,sup B); theorem :: SPRECT_1:54 S = C1 \/ C2 implies W-bound S = min(W-bound C1, W-bound C2); theorem :: SPRECT_1:55 S = C1 \/ C2 implies S-bound S = min(S-bound C1, S-bound C2); theorem :: SPRECT_1:56 S = C1 \/ C2 implies N-bound S = max(N-bound C1, N-bound C2); theorem :: SPRECT_1:57 S = C1 \/ C2 implies E-bound S = max(E-bound C1, E-bound C2); definition let p,q; cluster LSeg(p,q) -> compact; end; definition cluster {}REAL -> bounded; end; definition let r1,r2; cluster [.r1,r2.] -> bounded; end; definition cluster bounded -> bounded_below bounded_above Subset of REAL; cluster bounded_below bounded_above -> bounded Subset of REAL; end; canceled; theorem :: SPRECT_1:59 r1 <= r2 implies (t in [.r1,r2.] iff ex s1 st 0 <=s1 & s1 <= 1 & t = s1*r1 + (1-s1)*r2); theorem :: SPRECT_1:60 p`1 <= q`1 implies proj1.:LSeg(p,q) = [.p`1,q`1.]; theorem :: SPRECT_1:61 p`2 <= q`2 implies proj2.:LSeg(p,q) = [.p`2,q`2.]; theorem :: SPRECT_1:62 p`1 <= q`1 implies W-bound LSeg(p,q) = p`1; theorem :: SPRECT_1:63 p`2 <= q`2 implies S-bound LSeg(p,q) = p`2; theorem :: SPRECT_1:64 p`2 <= q`2 implies N-bound LSeg(p,q) = q`2; theorem :: SPRECT_1:65 p`1 <= q`1 implies E-bound LSeg(p,q) = q`1; theorem :: SPRECT_1:66 W-bound L~SpStSeq C = W-bound C; theorem :: SPRECT_1:67 S-bound L~SpStSeq C = S-bound C; theorem :: SPRECT_1:68 N-bound L~SpStSeq C = N-bound C; theorem :: SPRECT_1:69 E-bound L~SpStSeq C = E-bound C; theorem :: SPRECT_1:70 NW-corner L~SpStSeq C = NW-corner C; theorem :: SPRECT_1:71 NE-corner L~SpStSeq C = NE-corner C; theorem :: SPRECT_1:72 SW-corner L~SpStSeq C = SW-corner C; theorem :: SPRECT_1:73 SE-corner L~SpStSeq C = SE-corner C; theorem :: SPRECT_1:74 W-most L~SpStSeq C = LSeg(SW-corner C,NW-corner C); theorem :: SPRECT_1:75 N-most L~SpStSeq C = LSeg(NW-corner C,NE-corner C); theorem :: SPRECT_1:76 S-most L~SpStSeq C = LSeg(SW-corner C,SE-corner C); theorem :: SPRECT_1:77 E-most L~SpStSeq C = LSeg(SE-corner C,NE-corner C); theorem :: SPRECT_1:78 proj2.:LSeg(SW-corner C,NW-corner C) = [.S-bound C,N-bound C.]; theorem :: SPRECT_1:79 proj1.:LSeg(NW-corner C,NE-corner C) = [.W-bound C,E-bound C.]; theorem :: SPRECT_1:80 proj2.:LSeg(NE-corner C,SE-corner C) = [.S-bound C,N-bound C.]; theorem :: SPRECT_1:81 proj1.:LSeg(SE-corner C,SW-corner C) = [.W-bound C,E-bound C.]; theorem :: SPRECT_1:82 W-min L~SpStSeq C = SW-corner C; theorem :: SPRECT_1:83 W-max L~SpStSeq C = NW-corner C; theorem :: SPRECT_1:84 N-min L~SpStSeq C = NW-corner C; theorem :: SPRECT_1:85 N-max L~SpStSeq C = NE-corner C; theorem :: SPRECT_1:86 E-min L~SpStSeq C = SE-corner C; theorem :: SPRECT_1:87 E-max L~SpStSeq C = NE-corner C; theorem :: SPRECT_1:88 S-min L~SpStSeq C = SW-corner C; theorem :: SPRECT_1:89 S-max L~SpStSeq C = SE-corner C; begin :: rectangular definition let f be FinSequence of TOP-REAL 2; attr f is rectangular means :: SPRECT_1:def 2 ex D st f = SpStSeq D; end; definition let D; cluster SpStSeq D -> rectangular; end; definition cluster rectangular FinSequence of TOP-REAL 2; end; reserve s for rectangular FinSequence of TOP-REAL 2; theorem :: SPRECT_1:90 len s = 5; definition cluster rectangular -> non constant FinSequence of TOP-REAL 2; end; definition cluster rectangular -> standard special unfolded circular s.c.c. (non empty FinSequence of TOP-REAL 2); end; :::: Special points of L~f, f - rectangular theorem :: SPRECT_1:91 s/.1 = N-min L~s & s/.1 = W-max L~s; theorem :: SPRECT_1:92 s/.2 = N-max L~s & s/.2 = E-max L~s; theorem :: SPRECT_1:93 s/.3 = S-max L~s & s/.3 = E-min L~s; theorem :: SPRECT_1:94 s/.4 = S-min L~s & s/.4 = W-min L~s; begin :: Jordan theorem :: SPRECT_1:95 r1 < r2 & s1 < s2 implies [.r1,r2,s1,s2.] is Jordan; definition let f be rectangular FinSequence of TOP-REAL 2; cluster L~f -> Jordan; end; definition let S be Subset of TOP-REAL 2; redefine attr S is Jordan means :: SPRECT_1:def 3 S`<> {} & ex A1,A2 being Subset of TOP-REAL 2 st S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of S` & A2 is_a_component_of S`; end; theorem :: SPRECT_1:96 for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp f misses RightComp f; definition let f be non constant standard special_circular_sequence; cluster LeftComp f -> non empty; cluster RightComp f -> non empty; end; theorem :: SPRECT_1:97 for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp f <> RightComp f;

Back to top