:: Again on the Order on a Special Polygon
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 16, 2000
:: Copyright (c) 2000-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, FINSEQ_6, SUBSET_1, RELAT_1,
FINSEQ_4, XXREAL_0, FINSEQ_5, ARYTM_1, ARYTM_3, ORDINAL4, RFINSEQ,
PARTFUN1, FUNCT_1, GOBOARD5, PRE_TOPC, EUCLID, CARD_1, PSCOMP_1,
TOPREAL1, SPRECT_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, FINSEQ_6,
NAT_1, NAT_D, PRE_TOPC, EUCLID, TOPREAL1, GOBOARD5, PSCOMP_1, SPRECT_2;
constructors FINSEQ_4, RFINSEQ, FINSEQ_5, GOBOARD5, PSCOMP_1, SPRECT_2, NAT_D,
RELSET_1;
registrations XBOOLE_0, RELSET_1, XREAL_0, FINSEQ_6, STRUCT_0, SPRECT_2,
REVROT_1, ORDINAL1, FUNCT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
reserve D for non empty set,
f for FinSequence of D,
g for circular FinSequence of D,
p,p1,p2,p3,q for Element of D;
theorem :: SPRECT_5:1
q in rng(f|(p..f)) implies q..f <= p..f;
theorem :: SPRECT_5:2
p in rng f & q in rng f & p..f <= q..f implies q..(f:-p) = q..f - p..f + 1;
theorem :: SPRECT_5:3
p in rng f & q in rng f & p..f <= q..f implies p..(f-:q) = p..f;
theorem :: SPRECT_5:4
p in rng f & q in rng f & p..f <= q..f implies q..Rotate(f,p) = q
..f - p..f + 1;
theorem :: SPRECT_5:5
p1 in rng f & p2 in rng f & p3 in rng f & p1..f <= p2..f & p2..f
< p3..f implies p2..Rotate(f,p1) < p3..Rotate(f,p1);
theorem :: SPRECT_5:6
p1 in rng f & p2 in rng f & p3 in rng f & p1..f < p2..f & p2..f <= p3
..f implies p2..Rotate(f,p1) <= p3..Rotate(f,p1);
theorem :: SPRECT_5:7
p in rng g & len g > 1 implies p..g < len g;
begin :: Ordering of special points on a standard special sequence
reserve f for non constant standard special_circular_sequence,
p,p1,p2,p3,q for Point of TOP-REAL 2;
registration
let f;
cluster f/^1 -> one-to-one;
end;
theorem :: SPRECT_5:8
1 < q..f & q in rng f implies (f/.1)..Rotate(f,q) = len f + 1 - q ..f;
theorem :: SPRECT_5:9
p in rng f & q in rng f & p..f < q..f implies p..Rotate(f,q) =
len f + p..f - q..f;
theorem :: SPRECT_5:10
p1 in rng f & p2 in rng f & p3 in rng f & p1..f < p2..f & p2..f
< p3..f implies p3..Rotate(f,p2) < p1..Rotate(f,p2);
theorem :: SPRECT_5:11
p1 in rng f & p2 in rng f & p3 in rng f & p1..f < p2..f & p2..f
< p3..f implies p1..Rotate(f,p3) < p2..Rotate(f,p3);
theorem :: SPRECT_5:12
p1 in rng f & p2 in rng f & p3 in rng f & p1..f <= p2..f & p2..f < p3
..f implies p1..Rotate(f,p3) <= p2..Rotate(f,p3);
theorem :: SPRECT_5:13
(S-min L~f)..f < len f;
theorem :: SPRECT_5:14
(S-max L~f)..f < len f;
theorem :: SPRECT_5:15
(E-min L~f)..f < len f;
theorem :: SPRECT_5:16
(E-max L~f)..f < len f;
theorem :: SPRECT_5:17
(N-min L~f)..f < len f;
theorem :: SPRECT_5:18
(N-max L~f)..f < len f;
theorem :: SPRECT_5:19
(W-max L~f)..f < len f;
theorem :: SPRECT_5:20
(W-min L~f)..f < len f;
begin :: Ordering of special points on a clockwise oriented sequence
reserve z for clockwise_oriented non constant standard
special_circular_sequence;
theorem :: SPRECT_5:21
f/.1 = W-min L~f implies (W-min L~f)..f < (W-max L~f)..f;
theorem :: SPRECT_5:22
f/.1 = W-min L~f implies (W-max L~f)..f > 1;
theorem :: SPRECT_5:23
z/.1 = W-min L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z
< (N-min L~z)..z;
theorem :: SPRECT_5:24
z/.1 = W-min L~z implies (N-min L~z)..z < (N-max L~z)..z;
theorem :: SPRECT_5:25
z/.1 = W-min L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z
< (E-max L~z)..z;
theorem :: SPRECT_5:26
z/.1 = W-min L~z implies (E-max L~z)..z < (E-min L~z)..z;
theorem :: SPRECT_5:27
z/.1 = W-min L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z
< (S-max L~z)..z;
theorem :: SPRECT_5:28
z/.1 = W-min L~z & S-min L~z <> W-min L~z implies (S-max L~z)..z < (
S-min L~z)..z;
theorem :: SPRECT_5:29
f/.1 = S-max L~f implies (S-max L~f)..f < (S-min L~f)..f;
theorem :: SPRECT_5:30
f/.1 = S-max L~f implies (S-min L~f)..f > 1;
theorem :: SPRECT_5:31
z/.1 = S-max L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z
< (W-min L~z)..z;
theorem :: SPRECT_5:32
z/.1 = S-max L~z implies (W-min L~z)..z < (W-max L~z)..z;
theorem :: SPRECT_5:33
z/.1 = S-max L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z
< (N-min L~z)..z;
theorem :: SPRECT_5:34
z/.1 = S-max L~z implies (N-min L~z)..z < (N-max L~z)..z;
theorem :: SPRECT_5:35
z/.1 = S-max L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z
< (E-max L~z)..z;
theorem :: SPRECT_5:36
z/.1 = S-max L~z & E-min L~z <> S-max L~z implies (E-max L~z)..z < (
E-min L~z)..z;
theorem :: SPRECT_5:37
f/.1 = E-max L~f implies (E-max L~f)..f < (E-min L~f)..f;
theorem :: SPRECT_5:38
f/.1 = E-max L~f implies (E-min L~f)..f > 1;
theorem :: SPRECT_5:39
z/.1 = E-max L~z & S-max L~z <> E-min L~z implies (E-min L~z)..z
< (S-max L~z)..z;
theorem :: SPRECT_5:40
z/.1 = E-max L~z implies (S-max L~z)..z < (S-min L~z)..z;
theorem :: SPRECT_5:41
z/.1 = E-max L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z
< (W-min L~z)..z;
theorem :: SPRECT_5:42
z/.1 = E-max L~z implies (W-min L~z)..z < (W-max L~z)..z;
theorem :: SPRECT_5:43
z/.1 = E-max L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z
< (N-min L~z)..z;
theorem :: SPRECT_5:44
z/.1 = E-max L~z & N-max L~z <> E-max L~z implies (N-min L~z)..z < (
N-max L~z)..z;
theorem :: SPRECT_5:45
f/.1 = N-max L~f & N-max L~f <> E-max L~f implies (N-max L~f)..f < (
E-max L~f)..f;
theorem :: SPRECT_5:46
z/.1 = N-max L~z implies (E-max L~z)..z < (E-min L~z)..z;
theorem :: SPRECT_5:47
z/.1 = N-max L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z < (
S-max L~z)..z;
theorem :: SPRECT_5:48
z/.1 = N-max L~z implies (S-max L~z)..z < (S-min L~z)..z;
theorem :: SPRECT_5:49
z/.1 = N-max L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z < (
W-min L~z)..z;
theorem :: SPRECT_5:50
z/.1 = N-max L~z implies (W-min L~z)..z < (W-max L~z)..z;
theorem :: SPRECT_5:51
z/.1 = N-max L~z & N-min L~z <> W-max L~z implies (W-max L~z)..z < (
N-min L~z)..z;
theorem :: SPRECT_5:52
f/.1 = E-min L~f & E-min L~f <> S-max L~f implies (E-min L~f)..f < (
S-max L~f)..f;
theorem :: SPRECT_5:53
z/.1 = E-min L~z implies (S-max L~z)..z < (S-min L~z)..z;
theorem :: SPRECT_5:54
z/.1 = E-min L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z < (
W-min L~z)..z;
theorem :: SPRECT_5:55
z/.1 = E-min L~z implies (W-min L~z)..z < (W-max L~z)..z;
theorem :: SPRECT_5:56
z/.1 = E-min L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z < (
N-min L~z)..z;
theorem :: SPRECT_5:57
z/.1 = E-min L~z implies (N-min L~z)..z < (N-max L~z)..z;
theorem :: SPRECT_5:58
z/.1 = E-min L~z & E-max L~z <> N-max L~z implies (N-max L~z)..z < (
E-max L~z)..z;
theorem :: SPRECT_5:59
f/.1 = S-min L~f & S-min L~f <> W-min L~f implies (S-min L~f)..f < (
W-min L~f)..f;
theorem :: SPRECT_5:60
z/.1 = S-min L~z implies (W-min L~z)..z < (W-max L~z)..z;
theorem :: SPRECT_5:61
z/.1 = S-min L~z & W-max L~z <> N-min L~z implies (W-max L~z)..z < (
N-min L~z)..z;
theorem :: SPRECT_5:62
z/.1 = S-min L~z implies (N-min L~z)..z < (N-max L~z)..z;
theorem :: SPRECT_5:63
z/.1 = S-min L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z < (
E-max L~z)..z;
theorem :: SPRECT_5:64
z/.1 = S-min L~z implies (E-max L~z)..z < (E-min L~z)..z;
theorem :: SPRECT_5:65
z/.1 = S-min L~z & S-max L~z <> E-min L~z implies (E-min L~z)..z < (
S-max L~z)..z;
theorem :: SPRECT_5:66
f/.1 = W-max L~f & W-max L~f <> N-min L~f implies (W-max L~f)..f < (
N-min L~f)..f;
theorem :: SPRECT_5:67
z/.1 = W-max L~z implies (N-min L~z)..z < (N-max L~z)..z;
theorem :: SPRECT_5:68
z/.1 = W-max L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z < (
E-max L~z)..z;
theorem :: SPRECT_5:69
z/.1 = W-max L~z implies (E-max L~z)..z < (E-min L~z)..z;
theorem :: SPRECT_5:70
z/.1 = W-max L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z < (
S-max L~z)..z;
theorem :: SPRECT_5:71
z/.1 = W-max L~z implies (S-max L~z)..z < (S-min L~z)..z;
theorem :: SPRECT_5:72
z/.1 = W-max L~z & W-min L~z <> S-min L~z implies (S-min L~z)..z < (
W-min L~z)..z;