:: Extremal Properties of Vertices on Special Polygons I
:: by Yatsuka Nakamura and Czes\law Byli\'nski
::
:: Copyright (c) 1994-2021 Association of Mizar Users

theorem :: SPPOL_1:1
for n, k being Nat st n < k holds
n <= k - 1
proof end;

theorem :: SPPOL_1:2
for n, k, m being Nat st 1 <= k - m & k - m <= n holds
( k - m in Seg n & k - m is Element of NAT )
proof end;

scheme :: SPPOL_1:sch 1
FinSeqFam{ F1() -> non empty set , F2() -> FinSequence of F1(), F3( FinSequence of F1(), Nat) -> set , P1[ Nat] } :
{ F3(F2(),i) where i is Nat : ( i in dom F2() & P1[i] ) } is finite
proof end;

scheme :: SPPOL_1:sch 2
FinSeqFam9{ F1() -> non empty set , F2() -> FinSequence of F1(), F3( FinSequence of F1(), Nat) -> set , P1[ set ] } :
{ F3(F2(),i) where i is Nat : ( 1 <= i & i <= len F2() & P1[i] ) } is finite
proof end;

theorem Th3: :: SPPOL_1:3
for n being Nat
for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).|
proof end;

theorem :: SPPOL_1:4
for n being Nat
for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).|
proof end;

theorem Th5: :: SPPOL_1:5
for n being Nat
for u1, u2 being Point of ()
for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds
dist (u1,u2) = |.(v1 - v2).|
proof end;

theorem :: SPPOL_1:6
for n being Nat
for p1, p2 being Point of ()
for P being non empty Subset of () 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 ) )
proof end;

theorem Th7: :: SPPOL_1:7
for n being Nat
for p1, p2, q1, q2 being Point of () st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds
p1 = q2
proof end;

theorem :: SPPOL_1:8
for n being Nat
for p1, p2, q1, q2 being Point of () holds
( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )
proof end;

registration
let n be Nat;
let p1, p2 be Point of ();
cluster LSeg (p1,p2) -> compact ;
coherence
LSeg (p1,p2) is compact
proof end;
cluster LSeg (p1,p2) -> closed ;
coherence
LSeg (p1,p2) is closed
by COMPTS_1:7;
end;

definition
let n be Nat;
let p be Point of ();
let P be Subset of ();
pred p is_extremal_in P means :: SPPOL_1:def 1
( p in P & ( for p1, p2 being Point of () st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds
p = p2 ) );
end;

:: deftheorem defines is_extremal_in SPPOL_1:def 1 :
for n being Nat
for p being Point of ()
for P being Subset of () holds
( p is_extremal_in P iff ( p in P & ( for p1, p2 being Point of () st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds
p = p2 ) ) );

theorem :: SPPOL_1:9
for n being Nat
for p being Point of ()
for P, Q being Subset of () st p is_extremal_in P & Q c= P & p in Q holds
p is_extremal_in Q
proof end;

theorem :: SPPOL_1:10
for n being Nat
for p being Point of () holds p is_extremal_in {p}
proof end;

theorem Th11: :: SPPOL_1:11
for n being Nat
for p1, p2 being Point of () holds p1 is_extremal_in LSeg (p1,p2) by ;

theorem :: SPPOL_1:12
for n being Nat
for p1, p2 being Point of () holds p2 is_extremal_in LSeg (p1,p2) by Th11;

theorem :: SPPOL_1:13
for n being Nat
for p, p1, p2 being Point of () holds
( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 ) ;

theorem Th14: :: SPPOL_1:14
for p1, p2 being Point of () st p1 1 <> p2 1 & p1 2 <> p2 2 holds
ex p being Point of () st
( p in LSeg (p1,p2) & p 1 <> p1 1 & p 1 <> p2 1 & p 2 <> p1 2 & p 2 <> p2 2 )
proof end;

definition
let P be Subset of ();
attr P is horizontal means :: SPPOL_1:def 2
for p, q being Point of () st p in P & q in P holds
p 2 = q 2 ;
attr P is vertical means :: SPPOL_1:def 3
for p, q being Point of () st p in P & q in P holds
p 1 = q 1 ;
end;

:: deftheorem defines horizontal SPPOL_1:def 2 :
for P being Subset of () holds
( P is horizontal iff for p, q being Point of () st p in P & q in P holds
p 2 = q 2 );

:: deftheorem defines vertical SPPOL_1:def 3 :
for P being Subset of () holds
( P is vertical iff for p, q being Point of () st p in P & q in P holds
p 1 = q 1 );

Lm1: for P being Subset of () st not P is trivial & P is horizontal holds
not P is vertical

proof end;

registration
cluster non trivial horizontal -> non vertical for Element of bool the carrier of ();
coherence
for b1 being Subset of () 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 ();
coherence
for b1 being Subset of () 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 () holds
( p 2 = q 2 iff LSeg (p,q) is horizontal )
proof end;

theorem Th16: :: SPPOL_1:16
for p, q being Point of () holds
( p 1 = q 1 iff LSeg (p,q) is vertical )
proof end;

theorem :: SPPOL_1:17
for p, p1, p2, q being Point of () 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
proof end;

theorem :: SPPOL_1:18
for p, p1, p2, q being Point of () 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
proof end;

registration
let f be FinSequence of the carrier of ();
let i be Nat;
cluster LSeg (f,i) -> closed ;
coherence
LSeg (f,i) is closed
proof end;
end;

theorem Th19: :: SPPOL_1:19
for i being Nat
for f being FinSequence of the carrier of () holds
( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal )
proof end;

theorem Th20: :: SPPOL_1:20
for i being Nat
for f being FinSequence of the carrier of () st f is one-to-one & 1 <= i & i + 1 <= len f holds
not LSeg (f,i) is trivial
proof end;

theorem :: SPPOL_1:21
for i being Nat
for f being FinSequence of the carrier of () 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 ;

theorem Th22: :: SPPOL_1:22
for f being FinSequence of the carrier of () holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } is finite
proof end;

theorem Th23: :: SPPOL_1:23
for f being FinSequence of the carrier of () holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is finite
proof end;

Lm2: for f being FinSequence of the carrier of ()
for k being Nat holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite

proof end;

theorem :: SPPOL_1:24
for f being FinSequence of the carrier of () holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i <= len f ) } is Subset-Family of ()
proof end;

theorem Th25: :: SPPOL_1:25
for f being FinSequence of the carrier of () holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is Subset-Family of ()
proof end;

Lm3: for f being FinSequence of the carrier of ()
for k being Nat holds { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of ()

proof end;

theorem Th26: :: SPPOL_1:26
for Q being Subset of ()
for f being FinSequence of the carrier of () st Q = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } holds
Q is closed
proof end;

registration
let f be FinSequence of the carrier of ();
cluster L~ f -> closed ;
coherence
L~ f is closed
by Th26;
end;

Lm4: for f being FinSequence of the carrier of ()
for Q being Subset of ()
for k being Nat st Q = union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds
Q is closed

proof end;

definition
let IT be FinSequence of ();
attr IT is alternating means :: SPPOL_1:def 4
for i being 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 defines alternating SPPOL_1:def 4 :
for IT being FinSequence of () holds
( IT is alternating iff for i being 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 Nat
for f being FinSequence of the carrier of () 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
proof end;

theorem Th28: :: SPPOL_1:28
for i being Nat
for f being FinSequence of the carrier of () 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
proof end;

theorem Th29: :: SPPOL_1:29
for i being Nat
for f being FinSequence of the carrier of ()
for p1, p2, p3 being Point of () 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 )
proof end;

theorem :: SPPOL_1:30
for i being Nat
for f being FinSequence of the carrier of ()
for p1, p2, p3 being Point of () 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 )
proof end;

Lm5: for f being FinSequence of the carrier of ()
for i being Nat
for p1, p2 being Point of () st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds
ex p being Point of () st
( p in LSeg (p1,p2) & p 1 <> p1 1 & p 1 <> p2 1 & p 2 <> p1 2 & p 2 <> p2 2 )

proof end;

theorem :: SPPOL_1:31
for i being Nat
for f being FinSequence of the carrier of () 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)))
proof end;

theorem Th32: :: SPPOL_1:32
for i being Nat
for f being FinSequence of the carrier of () 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
proof end;

theorem Th33: :: SPPOL_1:33
for i being Nat
for f being FinSequence of the carrier of () 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
proof end;

theorem :: SPPOL_1:34
for i being Nat
for f being FinSequence of the carrier of () 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 ) by ;

theorem Th35: :: SPPOL_1:35
for i being Nat
for f being FinSequence of the carrier of ()
for p, q being Point of () 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
proof end;

theorem Th36: :: SPPOL_1:36
for i being Nat
for f being FinSequence of the carrier of () 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)))
proof end;

theorem Th37: :: SPPOL_1:37
for i being Nat
for f being FinSequence of the carrier of ()
for p, q being Point of ()
for u being Point of () 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 () st
( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) )
proof end;

definition
let f1, f2 be FinSequence of the carrier of ();
let P be Subset of ();
pred f1,f2 are_generators_of P means :: 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 defines are_generators_of SPPOL_1:def 5 :
for f1, f2 being FinSequence of the carrier of ()
for P being Subset of () 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 Nat
for P being Subset of ()
for f1, f2 being FinSequence of the carrier of () st f1,f2 are_generators_of P & 1 < i & i < len f1 holds
f1 /. i is_extremal_in P
proof end;

:: Moved from KURATO_2, AK, 22.02.2006
theorem :: SPPOL_1:39
for n being Nat
for p, q being Point of ()
for p9, q9 being Point of () 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 () st LSeg (p,q) is horizontal & r in LSeg (p,q) holds
p 2 = r 2
proof end;

theorem :: SPPOL_1:41
for p, q, r being Point of () st LSeg (p,q) is vertical & r in LSeg (p,q) holds
p 1 = r 1
proof end;

registration
cluster non empty functional compact horizontal for Element of bool the carrier of ();
existence
ex b1 being Subset of () st
( b1 is compact & not b1 is empty & b1 is horizontal )
proof end;
cluster non empty functional compact vertical for Element of bool the carrier of ();
existence
ex b1 being Subset of () st
( b1 is compact & not b1 is empty & b1 is vertical )
proof end;
end;