:: On the Order on a Special Polygon
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received November 30, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: SPRECT_2:1
canceled;
theorem :: SPRECT_2:2
canceled;
theorem :: SPRECT_2:3
canceled;
theorem :: SPRECT_2:4
canceled;
theorem Th5: :: SPRECT_2:5
theorem Th6: :: SPRECT_2:6
theorem Th7: :: SPRECT_2:7
theorem Th8: :: SPRECT_2:8
theorem Th9: :: SPRECT_2:9
theorem Th10: :: SPRECT_2:10
theorem Th11: :: SPRECT_2:11
theorem Th12: :: SPRECT_2:12
theorem Th13: :: SPRECT_2:13
theorem Th14: :: SPRECT_2:14
theorem Th15: :: SPRECT_2:15
theorem Th16: :: SPRECT_2:16
theorem Th17: :: SPRECT_2:17
theorem Th18: :: SPRECT_2:18
theorem Th19: :: SPRECT_2:19
theorem Th20: :: SPRECT_2:20
theorem Th21: :: SPRECT_2:21
theorem Th22: :: SPRECT_2:22
theorem Th23: :: SPRECT_2:23
theorem Th24: :: SPRECT_2:24
:: deftheorem Def1 defines is_in_the_area_of SPRECT_2:def 1 :
theorem Th25: :: SPRECT_2:25
theorem Th26: :: SPRECT_2:26
theorem :: SPRECT_2:27
theorem Th28: :: SPRECT_2:28
theorem Th29: :: SPRECT_2:29
theorem Th30: :: SPRECT_2:30
theorem Th31: :: SPRECT_2:31
theorem Th32: :: SPRECT_2:32
:: deftheorem Def2 defines is_a_h.c._for SPRECT_2:def 2 :
:: deftheorem Def3 defines is_a_v.c._for SPRECT_2:def 3 :
theorem Th33: :: SPRECT_2:33
:: deftheorem Def4 defines clockwise_oriented SPRECT_2:def 4 :
theorem Th34: :: SPRECT_2:34
theorem Th35: :: SPRECT_2:35
theorem Th36: :: SPRECT_2:36
theorem Th37: :: SPRECT_2:37
theorem :: SPRECT_2:38
theorem Th39: :: SPRECT_2:39
theorem :: SPRECT_2:40
theorem Th41: :: SPRECT_2:41
theorem Th42: :: SPRECT_2:42
theorem Th43: :: SPRECT_2:43
theorem Th44: :: SPRECT_2:44
theorem Th45: :: SPRECT_2:45
theorem Th46: :: SPRECT_2:46
theorem Th47: :: SPRECT_2:47
theorem Th48: :: SPRECT_2:48
theorem Th49: :: SPRECT_2:49
theorem Th50: :: SPRECT_2:50
theorem Th51: :: SPRECT_2:51
theorem Th52: :: SPRECT_2:52
theorem Th53: :: SPRECT_2:53
theorem Th54: :: SPRECT_2:54
theorem Th55: :: SPRECT_2:55
theorem Th56: :: SPRECT_2:56
theorem Th57: :: SPRECT_2:57
theorem :: SPRECT_2:58
theorem Th59: :: SPRECT_2:59
theorem Th60: :: SPRECT_2:60
theorem Th61: :: SPRECT_2:61
theorem Th62: :: SPRECT_2:62
theorem Th63: :: SPRECT_2:63
theorem Th64: :: SPRECT_2:64
theorem Th65: :: SPRECT_2:65
theorem Th66: :: SPRECT_2:66
theorem :: SPRECT_2:67
theorem Th68: :: SPRECT_2:68
theorem Th69: :: SPRECT_2:69
theorem Th70: :: SPRECT_2:70
theorem Th71: :: SPRECT_2:71
Lm1:
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i in dom f & j in dom f & mid f,i,j is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) holds
(<*(NW-corner (L~ f))*> ^ (mid f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2
Lm2:
for f being non constant standard special_circular_sequence holds LSeg (S-max (L~ f)),(SE-corner (L~ f)) misses LSeg (NW-corner (L~ f)),(N-min (L~ f))
Lm3:
for f being non constant standard special_circular_sequence
for i, j being Element of NAT st i in dom f & j in dom f & mid f,i,j is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds
(<*(NW-corner (L~ f))*> ^ (mid f,i,j)) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2
theorem Th72: :: SPRECT_2:72
theorem :: SPRECT_2:73
Lm4:
for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds
(N-min (L~ f)) .. f < (E-max (L~ f)) .. f
Lm5:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm6:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-min (L~ z)) .. z
theorem :: SPRECT_2:74
Lm7:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-max (L~ z)) .. z < (S-max (L~ z)) .. z
Lm8:
for f being non constant standard special_circular_sequence holds (LSeg (N-min (L~ f)),(NW-corner (L~ f))) /\ (LSeg (NE-corner (L~ f)),(E-max (L~ f))) = {}
theorem :: SPRECT_2:75
theorem Th76: :: SPRECT_2:76
theorem Th77: :: SPRECT_2:77
Lm9:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (S-min (L~ z)) .. z
Lm10:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) & N-min (L~ z) <> W-max (L~ z) holds
(E-min (L~ z)) .. z < (W-max (L~ z)) .. z
Lm11:
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (W-min (L~ z)) .. z
theorem :: SPRECT_2:78
theorem Th79: :: SPRECT_2:79
theorem :: SPRECT_2:80
theorem :: SPRECT_2:81