:: Extremal Properties of Vertices on Special Polygons I
:: by Yatsuka Nakamura and Czes\law Byli\'nski
::
:: Received May 11, 1994
:: Copyright (c) 1994 Association of Mizar Users
theorem :: SPPOL_1:1
canceled;
theorem :: SPPOL_1:2
canceled;
theorem :: SPPOL_1:3
canceled;
theorem :: SPPOL_1:4
canceled;
theorem :: SPPOL_1:5
canceled;
theorem :: SPPOL_1:6
for
n,
k being
Nat st
n < k holds
n <= k - 1
theorem :: SPPOL_1:7
theorem :: SPPOL_1:8
canceled;
theorem :: SPPOL_1:9
canceled;
theorem :: SPPOL_1:10
canceled;
theorem :: SPPOL_1:11
canceled;
theorem :: SPPOL_1:12
canceled;
theorem :: SPPOL_1:13
canceled;
theorem :: SPPOL_1:14
canceled;
theorem Th15: :: SPPOL_1:15
theorem :: SPPOL_1:16
theorem :: SPPOL_1:17
canceled;
theorem :: SPPOL_1:18
canceled;
theorem :: SPPOL_1:19
canceled;
theorem Th20: :: SPPOL_1:20
theorem Th21: :: SPPOL_1:21
theorem :: SPPOL_1:22
theorem :: SPPOL_1:23
theorem Th24: :: SPPOL_1:24
theorem :: SPPOL_1:25
theorem :: SPPOL_1:26
theorem :: SPPOL_1:27
canceled;
theorem Th28: :: SPPOL_1:28
theorem :: SPPOL_1:29
:: deftheorem Def1 defines is_extremal_in SPPOL_1:def 1 :
theorem :: SPPOL_1:30
theorem :: SPPOL_1:31
theorem Th32: :: SPPOL_1:32
theorem :: SPPOL_1:33
theorem :: SPPOL_1:34
theorem Th35: :: SPPOL_1:35
:: deftheorem Def2 defines horizontal SPPOL_1:def 2 :
:: deftheorem Def3 defines vertical SPPOL_1:def 3 :
Lm1:
for P being Subset of (TOP-REAL 2) st not P is trivial & P is horizontal holds
not P is vertical
theorem Th36: :: SPPOL_1:36
theorem Th37: :: SPPOL_1:37
theorem :: SPPOL_1:38
theorem :: SPPOL_1:39
theorem Th40: :: SPPOL_1:40
theorem Th41: :: SPPOL_1:41
theorem Th42: :: SPPOL_1:42
theorem :: SPPOL_1:43
theorem Th44: :: SPPOL_1:44
theorem Th45: :: SPPOL_1:45
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
theorem :: SPPOL_1:46
theorem Th47: :: SPPOL_1:47
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)
theorem Th48: :: SPPOL_1:48
theorem :: SPPOL_1:49
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
:: deftheorem Def4 defines alternating SPPOL_1:def 4 :
theorem Th50: :: SPPOL_1:50
theorem Th51: :: SPPOL_1:51
theorem Th52: :: SPPOL_1:52
theorem :: SPPOL_1:53
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 )
theorem :: SPPOL_1:54
theorem Th55: :: SPPOL_1:55
theorem Th56: :: SPPOL_1:56
theorem :: SPPOL_1:57
theorem Th58: :: SPPOL_1:58
theorem Th59: :: SPPOL_1:59
theorem Th60: :: SPPOL_1:60
:: deftheorem Def5 defines are_generators_of SPPOL_1:def 5 :
theorem :: SPPOL_1:61
theorem :: SPPOL_1:62
theorem :: SPPOL_1:63
theorem :: SPPOL_1:64