:: Extremal Properties of Vertices on Special Polygons I :: by Yatsuka Nakamura and Czes\law Byli\'nski :: :: Received May 11, 1994 :: Copyright (c) 1994-2012 Association of Mizar Users begin theorem :: SPPOL_1:1 for n, k being Nat st n < k holds n <= k - 1 proofend; theorem :: SPPOL_1:2 for k, m, n being Element of NAT st 1 <= k - m & k - m <= n holds ( k - m in Seg n & k - m is Element of NAT ) proofend; scheme :: SPPOL_1:sch 1 FinSeqFam{ F1() -> non empty set , F2() -> FinSequence of F1(), F3( FinSequence of F1(), Element of NAT ) -> set , P1[ Nat] } : { F3(F2(),i) where i is Element of NAT : ( i in dom F2() & P1[i] ) } is finite proofend; scheme :: SPPOL_1:sch 2 FinSeqFam9{ F1() -> non empty set , F2() -> FinSequence of F1(), F3( FinSequence of F1(), Element of NAT ) -> set , P1[ set ] } : { F3(F2(),i) where i is Element of NAT : ( 1 <= i & i <= len F2() & P1[i] ) } is finite proofend; theorem Th3: :: SPPOL_1:3 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).| proofend; theorem :: SPPOL_1:4 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).| proofend; begin theorem Th5: :: SPPOL_1:5 for n being Element of NAT for u1, u2 being Point of (Euclid n) for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds dist (u1,u2) = |.(v1 - v2).| proofend; theorem :: SPPOL_1:6 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds ex s being Real st ( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds s <= r ) ) proofend; theorem Th7: :: SPPOL_1:7 for n being Element of NAT for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds p1 = q2 proofend; theorem :: SPPOL_1:8 for n being Element of NAT for p1, p2, q1, q2 being Point of (TOP-REAL n) holds ( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) proofend; registration let n be Element of NAT ; let p1, p2 be Point of (TOP-REAL n); cluster LSeg (p1,p2) -> compact ; coherence LSeg (p1,p2) is compact proofend; cluster LSeg (p1,p2) -> closed ; coherence LSeg (p1,p2) is closed by COMPTS_1:7; end; definition let n be Element of NAT ; let p be Point of (TOP-REAL n); let P be Subset of (TOP-REAL n); predp is_extremal_in P means :Def1: :: SPPOL_1:def 1 ( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds p = p2 ) ); end; :: deftheorem Def1 defines is_extremal_in SPPOL_1:def_1_:_ for n being Element of NAT for p being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) holds ( p is_extremal_in P iff ( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds p = p2 ) ) ); theorem :: SPPOL_1:9 for n being Element of NAT for p being Point of (TOP-REAL n) for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds p is_extremal_in Q proofend; theorem :: SPPOL_1:10 for n being Element of NAT for p being Point of (TOP-REAL n) holds p is_extremal_in {p} proofend; theorem Th11: :: SPPOL_1:11 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg (p1,p2) proofend; theorem :: SPPOL_1:12 for n being Element of NAT for p2, p1 being Point of (TOP-REAL n) holds p2 is_extremal_in LSeg (p1,p2) by Th11; theorem :: SPPOL_1:13 for n being Element of NAT for p, p1, p2 being Point of (TOP-REAL n) holds ( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 ) proofend; begin theorem Th14: :: SPPOL_1:14 for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <> p2 `1 & p1 `2 <> p2 `2 holds ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) proofend; definition let P be Subset of (TOP-REAL 2); attrP is horizontal means :Def2: :: SPPOL_1:def 2 for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `2 = q `2 ; attrP is vertical means :Def3: :: SPPOL_1:def 3 for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `1 = q `1 ; end; :: deftheorem Def2 defines horizontal SPPOL_1:def_2_:_ for P being Subset of (TOP-REAL 2) holds ( P is horizontal iff for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `2 = q `2 ); :: deftheorem Def3 defines vertical SPPOL_1:def_3_:_ for P being Subset of (TOP-REAL 2) holds ( P is vertical iff for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `1 = q `1 ); Lm1: for P being Subset of (TOP-REAL 2) st not P is trivial & P is horizontal holds not P is vertical proofend; registration cluster non trivial horizontal -> non vertical for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st not b1 is trivial & b1 is horizontal holds not b1 is vertical by Lm1; cluster non trivial vertical -> non horizontal for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st not b1 is trivial & b1 is vertical holds not b1 is horizontal ; end; theorem Th15: :: SPPOL_1:15 for p, q being Point of (TOP-REAL 2) holds ( p `2 = q `2 iff LSeg (p,q) is horizontal ) proofend; theorem Th16: :: SPPOL_1:16 for p, q being Point of (TOP-REAL 2) holds ( p `1 = q `1 iff LSeg (p,q) is vertical ) proofend; theorem :: SPPOL_1:17 for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `1 <> p2 `1 & p1 `2 = p2 `2 holds LSeg (p,q) is horizontal proofend; theorem :: SPPOL_1:18 for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `2 <> p2 `2 & p1 `1 = p2 `1 holds LSeg (p,q) is vertical proofend; registration let f be FinSequence of the carrier of (TOP-REAL 2); let i be Element of NAT ; cluster LSeg (f,i) -> closed ; coherence LSeg (f,i) is closed proofend; end; theorem Th19: :: SPPOL_1:19 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) holds ( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) proofend; theorem Th20: :: SPPOL_1:20 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f holds not LSeg (f,i) is trivial proofend; theorem :: SPPOL_1:21 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f & LSeg (f,i) is vertical holds not LSeg (f,i) is horizontal by Lm1, Th20; theorem Th22: :: SPPOL_1:22 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is finite proofend; theorem Th23: :: SPPOL_1:23 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is finite proofend; Lm2: for f being FinSequence of the carrier of (TOP-REAL 2) for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite proofend; theorem :: SPPOL_1:24 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is Subset-Family of (TOP-REAL 2) proofend; theorem Th25: :: SPPOL_1:25 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset-Family of (TOP-REAL 2) proofend; Lm3: for f being FinSequence of the carrier of (TOP-REAL 2) for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2) proofend; theorem Th26: :: SPPOL_1:26 for Q being Subset of (TOP-REAL 2) for f being FinSequence of the carrier of (TOP-REAL 2) st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } holds Q is closed proofend; registration let f be FinSequence of the carrier of (TOP-REAL 2); cluster L~ f -> closed ; coherence L~ f is closed by Th26; end; Lm4: for f being FinSequence of the carrier of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for k being Element of NAT st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds Q is closed proofend; definition let IT be FinSequence of (TOP-REAL 2); attrIT is alternating means :Def4: :: SPPOL_1:def 4 for i being Element of NAT st 1 <= i & i + 2 <= len IT holds ( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 ); end; :: deftheorem Def4 defines alternating SPPOL_1:def_4_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is alternating iff for i being Element of NAT st 1 <= i & i + 2 <= len IT holds ( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 ) ); theorem Th27: :: SPPOL_1:27 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 holds (f /. (i + 1)) `2 = (f /. (i + 2)) `2 proofend; theorem Th28: :: SPPOL_1:28 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 holds (f /. (i + 1)) `1 = (f /. (i + 2)) `1 proofend; theorem Th29: :: SPPOL_1:29 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) proofend; theorem :: SPPOL_1:30 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) proofend; Lm5: for f being FinSequence of the carrier of (TOP-REAL 2) for i being Element of NAT for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) proofend; theorem :: SPPOL_1:31 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) proofend; theorem Th32: :: SPPOL_1:32 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical holds LSeg (f,(i + 1)) is horizontal proofend; theorem Th33: :: SPPOL_1:33 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is horizontal holds LSeg (f,(i + 1)) is vertical proofend; theorem :: SPPOL_1:34 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) holds ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) proofend; theorem Th35: :: SPPOL_1:35 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds f /. (i + 1) = q proofend; theorem Th36: :: SPPOL_1:36 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) proofend; theorem Th37: :: SPPOL_1:37 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds for s being Real st s > 0 holds ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) proofend; definition let f1, f2 be FinSequence of the carrier of (TOP-REAL 2); let P be Subset of (TOP-REAL 2); predf1,f2 are_generators_of P means :Def5: :: SPPOL_1:def 5 ( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) ); end; :: deftheorem Def5 defines are_generators_of SPPOL_1:def_5_:_ for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) holds ( f1,f2 are_generators_of P iff ( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) ) ); theorem :: SPPOL_1:38 for i being Element of NAT for P being Subset of (TOP-REAL 2) for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds f1 /. i is_extremal_in P proofend; :: Moved from KURATO_2, AK, 22.02.2006 theorem :: SPPOL_1:39 for n being Element of NAT for p, q being Point of (TOP-REAL n) for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds dist (p9,q9) = |.(p - q).| by Th5; :: Moved from SPRECT_3, AK, 22.02.2006 theorem :: SPPOL_1:40 for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & r in LSeg (p,q) holds p `2 = r `2 proofend; theorem :: SPPOL_1:41 for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is vertical & r in LSeg (p,q) holds p `1 = r `1 proofend; registration cluster non empty functional compact horizontal for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is compact & not b1 is empty & b1 is horizontal ) proofend; cluster non empty functional compact vertical for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is compact & not b1 is empty & b1 is vertical ) proofend; end;