:: On Rectangular Finite Sequences of the Points of the Plane
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received November 30, 1997
:: Copyright (c) 1997-2021 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, FUNCT_1, FINSEQ_1, CARD_1, ORDINAL4, RELAT_1,
TARSKI, ZFMISC_1, PRE_TOPC, SUBSET_1, CONNSP_1, STRUCT_0, EUCLID,
RCOMP_1, TOPREAL1, RLTOPSP1, PARTFUN1, ARYTM_3, SPPOL_1, SPPOL_2,
MCART_1, PSCOMP_1, XXREAL_0, REAL_1, FINSEQ_6, GOBOARD5, ORDINAL2, NAT_1,
GOBOARD1, GOBOARD2, MATRIX_1, TREES_1, COMPLEX1, ARYTM_1, XXREAL_1,
XXREAL_2, JORDAN1, GOBOARD9, TOPS_1, SPRECT_1, SEQ_4;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1,
RELSET_1, FINSEQ_1, FINSEQ_4, FINSEQ_6, XXREAL_0, XXREAL_2, SEQM_3,
SEQ_4, MATRIX_0, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1,
RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, JORDAN1, GOBOARD1, GOBOARD2,
GOBOARD5, GOBOARD9, SPPOL_1, SPPOL_2, PSCOMP_1;
constructors REAL_1, COMPLEX1, RCOMP_1, FINSEQ_4, REALSET1, TOPS_1, CONNSP_1,
COMPTS_1, TOPREAL4, GOBOARD2, SPPOL_1, JORDAN1, SPPOL_2, PSCOMP_1,
GOBOARD9, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, RVSUM_1, MEASURE6,
SQUARE_1, COMSEQ_2;
registrations XBOOLE_0, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, SEQ_2,
FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, SPPOL_2,
PSCOMP_1, WAYBEL_2, VALUED_0, XXREAL_2, COMPTS_1, FUNCT_1, RLTOPSP1,
SEQ_4, SUBSET_1, RELSET_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
registration
cluster non empty constant for FinSequence;
end;
theorem :: SPRECT_1:1
for f,g being FinSequence st f^g is constant holds f is constant
& g is constant;
theorem :: SPRECT_1:2
for x,y being set st <*x,y*> is constant holds x = y;
theorem :: SPRECT_1:3
for x,y,z being set st <*x,y,z*> is constant holds x = y & y = z & z = x;
begin :: Topology
theorem :: SPRECT_1:4
for GX being non empty TopSpace, A being Subset of GX, B being
non empty Subset of GX holds A is_a_component_of B implies A <> {};
theorem :: SPRECT_1:5
for GX being TopStruct, A, B being Subset of GX holds A
is_a_component_of B implies A c= B;
theorem :: SPRECT_1:6
for T being non empty TopSpace, A being non empty Subset of T, B1
,B2,S being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A & S
is_a_component_of A & B1 \/ B2 = A holds S = B1 or S = B2;
theorem :: SPRECT_1:7
for T being non empty TopSpace, A being non empty Subset of T, B1
,B2,C1,C2 being Subset of T st B1 is_a_component_of A & B2 is_a_component_of A
& C1 is_a_component_of A & C2 is_a_component_of A & B1 \/ B2 = A & C1 \/ C2 = A
holds { B1,B2 } = { C1,C2 };
begin :: Topology of Plane
reserve S for Subset of TOP-REAL 2,
C,C1,C2 for non empty compact Subset of TOP-REAL 2,
p,q for Point of TOP-REAL 2;
theorem :: SPRECT_1:8
for p,q,r being Point of TOP-REAL 2 holds L~<*p,q,r*> = LSeg(p,q
) \/ LSeg(q,r);
registration
let n be Nat;
let f be non trivial FinSequence of TOP-REAL n;
cluster L~f -> non empty;
end;
registration
let f be FinSequence of TOP-REAL 2;
cluster L~f -> compact;
end;
theorem :: SPRECT_1:9
for A,B being Subset of TOP-REAL 2 st A c= B & B is horizontal
holds A is horizontal;
theorem :: SPRECT_1:10
for A,B being Subset of TOP-REAL 2 st A c= B & B is vertical
holds A is vertical;
registration
cluster R^2-unit_square -> special_polygonal non horizontal non vertical;
end;
registration
cluster non vertical non horizontal non empty compact for
Subset of TOP-REAL 2;
end;
begin :: Special points of a compact non empty subset of the plane
theorem :: SPRECT_1:11
N-min C in C & N-max C in C;
theorem :: SPRECT_1:12
S-min C in C & S-max C in C;
theorem :: SPRECT_1:13
W-min C in C & W-max C in C;
theorem :: SPRECT_1:14
E-min C in C & E-max C in C;
theorem :: SPRECT_1:15
C is vertical iff W-bound C = E-bound C;
theorem :: SPRECT_1:16
C is horizontal iff S-bound C = N-bound C;
theorem :: SPRECT_1:17
NW-corner C = NE-corner C implies C is vertical;
theorem :: SPRECT_1:18
SW-corner C = SE-corner C implies C is vertical;
theorem :: SPRECT_1:19
NW-corner C = SW-corner C implies C is horizontal;
theorem :: SPRECT_1:20
NE-corner C = SE-corner C implies C is horizontal;
reserve i,j,k for Nat,
t,r1,r2,s1,s2 for Real;
theorem :: SPRECT_1:21
W-bound C <= E-bound C;
theorem :: SPRECT_1:22
S-bound C <= N-bound C;
theorem :: SPRECT_1:23
LSeg(SE-corner C, NE-corner C) = { p : p`1 = E-bound C & p`2 <=
N-bound C & p`2 >= S-bound C };
theorem :: SPRECT_1:24
LSeg(SW-corner C, SE-corner C) = { p : p`1 <= E-bound C & p`1 >=
W-bound C & p`2 = S-bound C};
theorem :: SPRECT_1:25
LSeg(NW-corner C, NE-corner C) = { p : p`1 <= E-bound C & p`1 >=
W-bound C & p`2 = N-bound C};
theorem :: SPRECT_1:26
LSeg(SW-corner C, NW-corner C) = { p : p`1 = W-bound C & p`2 <=
N-bound C & p`2 >= S-bound C};
theorem :: SPRECT_1:27
LSeg(SW-corner C,NW-corner C) /\ LSeg(NW-corner C,NE-corner C) = {
NW-corner C };
theorem :: SPRECT_1:28
LSeg(NW-corner C,NE-corner C) /\ LSeg(NE-corner C,SE-corner C) =
{NE-corner C};
theorem :: SPRECT_1:29
LSeg(SE-corner C,NE-corner C) /\ LSeg(SW-corner C,SE-corner C) =
{SE-corner C};
theorem :: SPRECT_1:30
LSeg(NW-corner C,SW-corner C) /\ LSeg(SW-corner C,SE-corner C) =
{SW-corner C};
begin :: Neither vertical nor horizontal
reserve D1 for non vertical non empty compact Subset of TOP-REAL 2,
D2 for non horizontal non empty compact Subset of TOP-REAL 2,
D for non vertical non horizontal non empty compact Subset of TOP-REAL 2;
theorem :: SPRECT_1:31
W-bound D1 < E-bound D1;
theorem :: SPRECT_1:32
S-bound D2 < N-bound D2;
theorem :: SPRECT_1:33
LSeg(SW-corner D1,NW-corner D1) misses LSeg(SE-corner D1, NE-corner D1);
theorem :: SPRECT_1:34
LSeg(SW-corner D2,SE-corner D2) misses LSeg(NW-corner D2, NE-corner D2);
begin :: SpStSeq
definition
let C be Subset of TOP-REAL 2;
func SpStSeq C -> FinSequence of TOP-REAL 2 equals
:: SPRECT_1:def 1
<*NW-corner C,NE-corner C
,SE-corner C*>^ <*SW-corner C,NW-corner C*>;
end;
theorem :: SPRECT_1:35
(SpStSeq S)/.1 = NW-corner S;
theorem :: SPRECT_1:36
(SpStSeq S)/.2 = NE-corner S;
theorem :: SPRECT_1:37
(SpStSeq S)/.3 = SE-corner S;
theorem :: SPRECT_1:38
(SpStSeq S)/.4 = SW-corner S;
theorem :: SPRECT_1:39
(SpStSeq S)/.5 = NW-corner S;
theorem :: SPRECT_1:40
len SpStSeq S = 5;
theorem :: SPRECT_1:41
L~SpStSeq S = (LSeg(NW-corner S,NE-corner S) \/ LSeg(NE-corner S
,SE-corner S)) \/ (LSeg(SE-corner S,SW-corner S) \/ LSeg(SW-corner S,NW-corner
S));
registration
let D be non vertical non empty compact Subset of TOP-REAL 2;
cluster SpStSeq D -> non constant;
end;
registration
let D be non horizontal non empty compact Subset of TOP-REAL 2;
cluster SpStSeq D -> non constant;
end;
registration
let D be non vertical non horizontal non empty compact Subset of TOP-REAL 2;
cluster SpStSeq D -> special unfolded circular s.c.c. standard;
end;
theorem :: SPRECT_1:42
L~SpStSeq D = [.W-bound D,E-bound D,S-bound D,N-bound D.];
registration
let T be non empty TopSpace, X be non empty compact Subset of T,
f be continuous RealMap of T;
cluster f.:X -> bounded_below;
cluster f.:X -> bounded_above;
end;
theorem :: SPRECT_1:43
W-bound S = lower_bound(proj1.:S);
theorem :: SPRECT_1:44
S-bound S = lower_bound(proj2.:S);
theorem :: SPRECT_1:45
N-bound S = upper_bound(proj2.:S);
theorem :: SPRECT_1:46
E-bound S = upper_bound(proj1.:S);
theorem :: SPRECT_1:47
S = C1 \/ C2 implies W-bound S = min(W-bound C1, W-bound C2);
theorem :: SPRECT_1:48
S = C1 \/ C2 implies S-bound S = min(S-bound C1, S-bound C2);
theorem :: SPRECT_1:49
S = C1 \/ C2 implies N-bound S = max(N-bound C1, N-bound C2);
theorem :: SPRECT_1:50
S = C1 \/ C2 implies E-bound S = max(E-bound C1, E-bound C2);
registration
let r1,r2 be Real;
cluster [.r1,r2.] -> real-bounded for Subset of REAL;
end;
theorem :: SPRECT_1:51
r1 <= r2 implies (t in [.r1,r2.] iff ex s1 st 0 <=s1 & s1 <= 1 &
t = s1*r1 + (1-s1)*r2);
theorem :: SPRECT_1:52
p`1 <= q`1 implies proj1.:LSeg(p,q) = [.p`1,q`1.];
theorem :: SPRECT_1:53
p`2 <= q`2 implies proj2.:LSeg(p,q) = [.p`2,q`2.];
theorem :: SPRECT_1:54
p`1 <= q`1 implies W-bound LSeg(p,q) = p`1;
theorem :: SPRECT_1:55
p`2 <= q`2 implies S-bound LSeg(p,q) = p`2;
theorem :: SPRECT_1:56
p`2 <= q`2 implies N-bound LSeg(p,q) = q`2;
theorem :: SPRECT_1:57
p`1 <= q`1 implies E-bound LSeg(p,q) = q`1;
theorem :: SPRECT_1:58
W-bound L~SpStSeq C = W-bound C;
theorem :: SPRECT_1:59
S-bound L~SpStSeq C = S-bound C;
theorem :: SPRECT_1:60
N-bound L~SpStSeq C = N-bound C;
theorem :: SPRECT_1:61
E-bound L~SpStSeq C = E-bound C;
theorem :: SPRECT_1:62
NW-corner L~SpStSeq C = NW-corner C;
theorem :: SPRECT_1:63
NE-corner L~SpStSeq C = NE-corner C;
theorem :: SPRECT_1:64
SW-corner L~SpStSeq C = SW-corner C;
theorem :: SPRECT_1:65
SE-corner L~SpStSeq C = SE-corner C;
theorem :: SPRECT_1:66
W-most L~SpStSeq C = LSeg(SW-corner C,NW-corner C);
theorem :: SPRECT_1:67
N-most L~SpStSeq C = LSeg(NW-corner C,NE-corner C);
theorem :: SPRECT_1:68
S-most L~SpStSeq C = LSeg(SW-corner C,SE-corner C);
theorem :: SPRECT_1:69
E-most L~SpStSeq C = LSeg(SE-corner C,NE-corner C);
theorem :: SPRECT_1:70
proj2.:LSeg(SW-corner C,NW-corner C) = [.S-bound C,N-bound C.];
theorem :: SPRECT_1:71
proj1.:LSeg(NW-corner C,NE-corner C) = [.W-bound C,E-bound C.];
theorem :: SPRECT_1:72
proj2.:LSeg(NE-corner C,SE-corner C) = [.S-bound C,N-bound C.];
theorem :: SPRECT_1:73
proj1.:LSeg(SE-corner C,SW-corner C) = [.W-bound C,E-bound C.];
theorem :: SPRECT_1:74
W-min L~SpStSeq C = SW-corner C;
theorem :: SPRECT_1:75
W-max L~SpStSeq C = NW-corner C;
theorem :: SPRECT_1:76
N-min L~SpStSeq C = NW-corner C;
theorem :: SPRECT_1:77
N-max L~SpStSeq C = NE-corner C;
theorem :: SPRECT_1:78
E-min L~SpStSeq C = SE-corner C;
theorem :: SPRECT_1:79
E-max L~SpStSeq C = NE-corner C;
theorem :: SPRECT_1:80
S-min L~SpStSeq C = SW-corner C;
theorem :: SPRECT_1:81
S-max L~SpStSeq C = SE-corner C;
begin :: rectangular
definition
let f be FinSequence of TOP-REAL 2;
attr f is rectangular means
:: SPRECT_1:def 2
ex D st f = SpStSeq D;
end;
registration
let D;
cluster SpStSeq D -> rectangular;
end;
registration
cluster rectangular for FinSequence of TOP-REAL 2;
end;
reserve s for rectangular FinSequence of TOP-REAL 2;
theorem :: SPRECT_1:82
len s = 5;
registration
cluster rectangular -> non constant for FinSequence of TOP-REAL 2;
end;
registration
cluster rectangular -> standard special unfolded circular s.c.c. for
non empty
FinSequence of TOP-REAL 2;
end;
:: Special points of L~f, f - rectangular
theorem :: SPRECT_1:83
s/.1 = N-min L~s & s/.1 = W-max L~s;
theorem :: SPRECT_1:84
s/.2 = N-max L~s & s/.2 = E-max L~s;
theorem :: SPRECT_1:85
s/.3 = S-max L~s & s/.3 = E-min L~s;
theorem :: SPRECT_1:86
s/.4 = S-min L~s & s/.4 = W-min L~s;
begin :: Jordan
theorem :: SPRECT_1:87
r1 < r2 & s1 < s2 implies [.r1,r2,s1,s2.] is Jordan;
registration
let f be rectangular FinSequence of TOP-REAL 2;
cluster L~f -> Jordan;
end;
definition
let S be Subset of TOP-REAL 2;
redefine attr S is Jordan means
:: SPRECT_1:def 3
S`<> {} & ex A1,A2 being Subset of
TOP-REAL 2 st S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1
is_a_component_of S` & A2 is_a_component_of S`;
end;
theorem :: SPRECT_1:88
for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp
f misses RightComp f;
registration
let f be non constant standard special_circular_sequence;
cluster LeftComp f -> non empty;
cluster RightComp f -> non empty;
end;
theorem :: SPRECT_1:89
for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp f <>
RightComp f;