:: On Rectangular Finite Sequences of the Points of the Plane
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received November 30, 1997
:: Copyright (c) 1997-2026 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;
definitions SPPOL_1, TOPREAL1, GOBOARD1, GOBOARD5, TARSKI, JORDAN1, XBOOLE_0,
SEQM_3, XXREAL_2;
equalities TOPREAL1, PSCOMP_1, RLTOPSP1;
expansions SPPOL_1, JORDAN1, XBOOLE_0;
theorems FINSEQ_1, SPPOL_2, SPPOL_1, EUCLID, FUNCT_1, ZFMISC_1, PSCOMP_1,
FINSEQ_3, GOBOARD1, TARSKI, GOBOARD2, ENUMSET1, MCART_1, CARD_2,
TOPREAL1, NAT_1, FINSEQ_4, FINSEQ_6, TOPREAL3, GOBOARD7, JORDAN1,
GOBRD12, GOBOARD9, CONNSP_1, TOPS_2, JORDAN5A, COMPTS_1, FINSEQ_2,
RELAT_1, FUNCT_2, SEQ_4, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0,
PRE_TOPC, XXREAL_1, RLTOPSP1, MEASURE6, SEQM_3, NAT_D, RELSET_1,
XTUPLE_0, MATRIX_0, XREAL_0;
schemes NAT_1;
begin :: Preliminaries
registration
cluster non empty constant for FinSequence;
existence
proof
take <* 0 *>;
thus thesis;
end;
end;
theorem Th1:
for f,g being FinSequence st f^g is constant holds f is constant
& g is constant
proof
let f,g be FinSequence;
assume f^g is constant;
then reconsider h = f^g as constant FinSequence;
rng f c= rng h by FINSEQ_1:29;
hence f is constant;
rng g c= rng h by FINSEQ_1:30;
hence thesis;
end;
theorem Th2:
for x,y being object st <*x,y*> is constant holds x = y
proof
let x,y be object;
A1: rng<*x,y*> = rng(<*x*>^<*y*>) by FINSEQ_1:def 9
.= rng<*x*> \/ rng<*y*> by FINSEQ_1:31
.= rng<*x*> \/ {y} by FINSEQ_1:38
.= {x} \/ {y}by FINSEQ_1:38
.= {x,y} by ENUMSET1:1;
A2: y in {x,y} by TARSKI:def 2;
assume <*x,y*> is constant;
then reconsider s = <*x,y*> as constant Function;
A3: x in {x,y} by TARSKI:def 2;
rng s is trivial;
hence thesis by A1,A3,A2,ZFMISC_1:def 10;
end;
theorem Th3:
for x,y,z being object st <*x,y,z*> is constant holds x = y & y = z & z = x
proof
let x,y,z be object;
A1: rng<*x,y,z*> = rng(<*x*>^<*y*>^<*z*>) by FINSEQ_1:def 10
.= rng(<*x*>^<*y*>) \/ rng<*z*> by FINSEQ_1:31
.= rng(<*x*>^<*y*>) \/ {z} by FINSEQ_1:38
.= rng<*x*> \/ rng<*y*> \/ {z} by FINSEQ_1:31
.= rng<*x*> \/ {y} \/ {z} by FINSEQ_1:38
.= {x} \/ {y} \/ {z} by FINSEQ_1:38
.= {x,y} \/ {z} by ENUMSET1:1
.= {x,y,z} by ENUMSET1:3;
A2: y in {x,y,z} by ENUMSET1:def 1;
assume <*x,y,z*> is constant;
then reconsider s = <*x,y,z*> as constant Function;
A3: x in {x,y,z} by ENUMSET1:def 1;
A4: z in {x,y,z} by ENUMSET1:def 1;
rng s is trivial;
hence thesis by A1,A3,A2,A4,ZFMISC_1:def 10;
end;
begin :: Topology
theorem Th4:
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 <> {}
proof
let GX be non empty TopSpace, A be Subset of GX, B be non empty Subset of GX;
assume A is_a_component_of B;
then consider B1 being Subset of GX|B such that
A1: B1 = A and
A2: B1 is a_component by CONNSP_1:def 6;
B1 <> {}(GX|B) by A2,CONNSP_1:32;
hence thesis by A1;
end;
theorem Th5:
for GX being TopStruct, A, B being Subset of GX holds A
is_a_component_of B implies A c= B
proof
let GX be TopStruct, A, B be Subset of GX;
assume A is_a_component_of B;
then
A1: ex B1 being Subset of GX|B st B1 = A & B1 is a_component by CONNSP_1:def 6;
the carrier of GX|B = B by PRE_TOPC:8;
hence thesis by A1;
end;
theorem Th6:
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
proof
let T be non empty TopSpace, A be non empty Subset of T, B1,B2,S be Subset
of T such that
A1: B1 is_a_component_of A and
A2: B2 is_a_component_of A and
A3: S is_a_component_of A and
A4: B1 \/ B2 = A;
S c= A by A3,Th5;
then S meets A by A3,Th4,XBOOLE_1:67;
then S meets B1 or S meets B2 by A4,XBOOLE_1:70;
hence thesis by A1,A2,A3,GOBOARD9:1;
end;
theorem Th7:
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 }
proof
let T be non empty TopSpace, A be non empty Subset of T, B1,B2,C1,C2 be
Subset of T such that
A1: B1 is_a_component_of A and
A2: B2 is_a_component_of A and
A3: C1 is_a_component_of A and
A4: C2 is_a_component_of A and
A5: B1 \/ B2 = A and
A6: C1 \/ C2 = A;
now
let x be object;
x = B1 or x = B2 iff x = C1 or x = C2 by A1,A2,A3,A4,A5,A6,Th6;
hence x in { B1,B2 } iff x = C1 or x = C2 by TARSKI:def 2;
end;
hence thesis by TARSKI:def 2;
end;
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 Th8:
for p,q,r being Point of TOP-REAL 2 holds L~<*p,q,r*> = LSeg(p,q
) \/ LSeg(q,r)
proof
let p,q,r be Point of TOP-REAL 2;
A1: <*p,q*>/.2 = q by FINSEQ_4:17;
A2: <*r*>/.1 = r by FINSEQ_4:16;
A3: <*p,q,r*> = <*p,q*>^<*r*> by FINSEQ_1:43;
len <*p,q*> = 2 by FINSEQ_1:44;
hence L~<*p,q,r*> = L~<*p,q*> \/ LSeg(q,r) \/ L~<*r*> by A1,A2,A3,SPPOL_2:23
.= L~<*p,q*> \/ LSeg(q,r) \/ {} by SPPOL_2:12
.= LSeg(p,q) \/ LSeg(q,r) by SPPOL_2:21;
end;
registration
let n be Nat;
let f be non trivial FinSequence of TOP-REAL n;
cluster L~f -> non empty;
coherence
proof
A1: len f <> 1 by NAT_D:60;
len f <> 0 by NAT_D:60;
hence thesis by A1,TOPREAL1:22;
end;
end;
registration
let f be FinSequence of TOP-REAL 2;
cluster L~f -> compact;
coherence
proof
defpred X[Nat] means for f being FinSequence of TOP-REAL 2 st
len f = $1 holds L~f is compact;
A1: for m being Nat st X[m] holds X[m+1]
proof
let m be Nat;
assume
A2: for f being FinSequence of TOP-REAL 2 st len f = m holds L~f is compact;
let f be FinSequence of TOP-REAL 2;
assume
A3: len f = m+1;
then consider
q being FinSequence of TOP-REAL 2, x being Point of TOP-REAL 2
such that
A4: f=q^<*x*> by FINSEQ_2:19;
len f = len q + len<*x*> by A4,FINSEQ_1:22
.= len q + 1 by FINSEQ_1:39;
then
A5: L~q is compact by A2,A3;
per cases;
suppose
q is empty;
then L~f = L~<*x*> by A4,FINSEQ_1:34
.= {}TOP-REAL 2 by SPPOL_2:12;
hence thesis;
end;
suppose
q is non empty;
then L~f = L~q \/ LSeg(q/.len q,<*x*>/.1) \/ L~<*x*> by A4,SPPOL_2:23
.= L~q \/ LSeg(q/.len q,<*x*>/.1) \/ {} by SPPOL_2:12
.= L~q \/ LSeg(q/.len q,<*x*>/.1);
hence thesis by A5,COMPTS_1:10;
end;
end;
A6: X[0]
proof
let f be FinSequence of TOP-REAL 2;
assume len f = 0;
then L~f ={}TOP-REAL 2 by TOPREAL1:22;
hence thesis;
end;
for m being Nat holds X[m] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
end;
theorem Th9:
for A,B being Subset of TOP-REAL 2 st A c= B & B is horizontal
holds A is horizontal;
theorem Th10:
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;
coherence
proof
A1: |[0,1]|`2 = 1 by EUCLID:52;
|[0,0]|`2 = 0 by EUCLID:52;
then
A2: LSeg(|[0,0]|,|[0,1]|) is not horizontal by A1,SPPOL_1:15;
set Sq = R^2-unit_square;
thus Sq is special_polygonal;
A3: LSeg(|[0,0]|,|[0,1]|) \/ LSeg(|[0,1]|,|[1,1]|) c= Sq by XBOOLE_1:7;
LSeg(|[0,0]|,|[0,1]|) c= LSeg(|[0,0]|,|[0,1]|) \/ LSeg(|[0,1]|,|[1,1]|
) by XBOOLE_1:7;
hence Sq is not horizontal by A3,A2,Th9,XBOOLE_1:1;
A4: |[1,1]|`1 = 1 by EUCLID:52;
|[0,1]|`1 = 0 by EUCLID:52;
then
A5: LSeg(|[0,1]|,|[1,1]|) is not vertical by A4,SPPOL_1:16;
LSeg(|[0,1]|,|[1,1]|) c= LSeg(|[0,0]|,|[0,1]|) \/ LSeg(|[0,1]|,|[1,1]|
) by XBOOLE_1:7;
hence thesis by A3,A5,Th10,XBOOLE_1:1;
end;
end;
registration
cluster non vertical non horizontal non empty compact for
Subset of TOP-REAL 2;
existence
proof
take R^2-unit_square;
thus thesis;
end;
end;
begin :: Special points of a compact non empty subset of the plane
theorem Th11:
N-min C in C & N-max C in C
proof
A1: N-min C in N-most C by PSCOMP_1:42;
A2: N-max C in N-most C by PSCOMP_1:42;
N-most C c= C by XBOOLE_1:17;
hence thesis by A1,A2;
end;
theorem Th12:
S-min C in C & S-max C in C
proof
A1: S-min C in S-most C by PSCOMP_1:58;
A2: S-max C in S-most C by PSCOMP_1:58;
S-most C c= C by XBOOLE_1:17;
hence thesis by A1,A2;
end;
theorem Th13:
W-min C in C & W-max C in C
proof
A1: W-min C in W-most C by PSCOMP_1:34;
A2: W-max C in W-most C by PSCOMP_1:34;
W-most C c= C by XBOOLE_1:17;
hence thesis by A1,A2;
end;
theorem Th14:
E-min C in C & E-max C in C
proof
A1: E-min C in E-most C by PSCOMP_1:50;
A2: E-max C in E-most C by PSCOMP_1:50;
E-most C c= C by XBOOLE_1:17;
hence thesis by A1,A2;
end;
theorem Th15:
C is vertical iff W-bound C = E-bound C
proof
thus C is vertical implies W-bound C = E-bound C
proof
A1: E-min C in C by Th14;
A2: W-min C in C by Th13;
assume
A3: C is vertical;
thus W-bound C = (W-min C)`1 by EUCLID:52
.= (E-min C)`1 by A3,A2,A1
.= E-bound C by EUCLID:52;
end;
assume
A4: W-bound C = E-bound C;
let p,q;
assume that
A5: p in C and
A6: q in C;
A7: p`1 <= E-bound C by A5,PSCOMP_1:24;
W-bound C <= p`1 by A5,PSCOMP_1:24;
then
A8: p`1 = W-bound C by A4,A7,XXREAL_0:1;
A9: q`1 <= E-bound C by A6,PSCOMP_1:24;
W-bound C <= q`1 by A6,PSCOMP_1:24;
hence thesis by A4,A9,A8,XXREAL_0:1;
end;
theorem Th16:
C is horizontal iff S-bound C = N-bound C
proof
thus C is horizontal implies S-bound C = N-bound C
proof
A1: N-min C in C by Th11;
A2: S-min C in C by Th12;
assume
A3: C is horizontal;
thus S-bound C = (S-min C)`2 by EUCLID:52
.= (N-min C)`2 by A3,A2,A1
.= N-bound C by EUCLID:52;
end;
assume
A4: S-bound C = N-bound C;
let p,q;
assume that
A5: p in C and
A6: q in C;
A7: p`2 <= N-bound C by A5,PSCOMP_1:24;
S-bound C <= p`2 by A5,PSCOMP_1:24;
then
A8: p`2 = S-bound C by A4,A7,XXREAL_0:1;
A9: q`2 <= N-bound C by A6,PSCOMP_1:24;
S-bound C <= q`2 by A6,PSCOMP_1:24;
hence thesis by A4,A9,A8,XXREAL_0:1;
end;
theorem
NW-corner C = NE-corner C implies C is vertical
proof
assume NW-corner C = NE-corner C;
then W-bound C = E-bound C by SPPOL_2:1;
hence thesis by Th15;
end;
theorem
SW-corner C = SE-corner C implies C is vertical
proof
assume SW-corner C = SE-corner C;
then W-bound C = E-bound C by SPPOL_2:1;
hence thesis by Th15;
end;
theorem
NW-corner C = SW-corner C implies C is horizontal
proof
assume NW-corner C = SW-corner C;
then S-bound C = N-bound C by SPPOL_2:1;
hence thesis by Th16;
end;
theorem
NE-corner C = SE-corner C implies C is horizontal
proof
assume NE-corner C = SE-corner C;
then S-bound C = N-bound C by SPPOL_2:1;
hence thesis by Th16;
end;
reserve i,j,k for Nat,
t,r1,r2,s1,s2 for Real;
theorem Th21:
W-bound C <= E-bound C
proof
A1: N-min C in C by Th11;
then
A2: (N-min C)`1 <= E-bound C by PSCOMP_1:24;
W-bound C <= (N-min C)`1 by A1,PSCOMP_1:24;
hence thesis by A2,XXREAL_0:2;
end;
theorem Th22:
S-bound C <= N-bound C
proof
A1: W-min C in C by Th13;
then
A2: (W-min C)`2 <= N-bound C by PSCOMP_1:24;
S-bound C <= (W-min C)`2 by A1,PSCOMP_1:24;
hence thesis by A2,XXREAL_0:2;
end;
theorem Th23:
LSeg(SE-corner C, NE-corner C) = { p : p`1 = E-bound C & p`2 <=
N-bound C & p`2 >= S-bound C }
proof
set L = { p : p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
set q1 = SE-corner C, q2 = NE-corner C;
A1: q1`1 = E-bound C by EUCLID:52;
A2: q1`2 = S-bound C by EUCLID:52;
A3: q2`1 = E-bound C by EUCLID:52;
A4: q2`2 = N-bound C by EUCLID:52;
A5: S-bound C <= N-bound C by Th22;
thus LSeg(q1,q2) c= L
proof
let a be object;
assume
A6: a in LSeg(q1,q2);
then reconsider p = a as Point of TOP-REAL 2;
A7: p`1 = E-bound C by A1,A3,A6,GOBOARD7:5;
A8: p`2 >= S-bound C by A2,A4,A5,A6,TOPREAL1:4;
p`2 <= N-bound C by A2,A4,A5,A6,TOPREAL1:4;
hence thesis by A7,A8;
end;
let a be object;
assume a in L;
then ex p st p = a & p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C;
hence thesis by A1,A2,A3,A4,GOBOARD7:7;
end;
theorem Th24:
LSeg(SW-corner C, SE-corner C) = { p : p`1 <= E-bound C & p`1 >=
W-bound C & p`2 = S-bound C}
proof
set L = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C};
set q1 = SW-corner C, q2 = SE-corner C;
A1: q1`1 = W-bound C by EUCLID:52;
A2: q2`2 = S-bound C by EUCLID:52;
A3: q1`2 = S-bound C by EUCLID:52;
A4: q2`1 = E-bound C by EUCLID:52;
A5: W-bound C <= E-bound C by Th21;
thus LSeg(q1,q2) c= L
proof
let a be object;
assume
A6: a in LSeg(q1,q2);
then reconsider p = a as Point of TOP-REAL 2;
A7: p`2 = S-bound C by A3,A2,A6,GOBOARD7:6;
A8: p`1 >= W-bound C by A1,A4,A5,A6,TOPREAL1:3;
p`1 <= E-bound C by A1,A4,A5,A6,TOPREAL1:3;
hence thesis by A7,A8;
end;
let a be object;
assume a in L;
then ex p st p = a & p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C;
hence thesis by A1,A3,A4,A2,GOBOARD7:8;
end;
theorem Th25:
LSeg(NW-corner C, NE-corner C) = { p : p`1 <= E-bound C & p`1 >=
W-bound C & p`2 = N-bound C}
proof
set L = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C};
set q1 = NW-corner C, q2 = NE-corner C;
A1: q1`1 = W-bound C by EUCLID:52;
A2: q2`2 = N-bound C by EUCLID:52;
A3: q1`2 = N-bound C by EUCLID:52;
A4: q2`1 = E-bound C by EUCLID:52;
A5: W-bound C <= E-bound C by Th21;
thus LSeg(q1,q2) c= L
proof
let a be object;
assume
A6: a in LSeg(q1,q2);
then reconsider p = a as Point of TOP-REAL 2;
A7: p`2 = N-bound C by A3,A2,A6,GOBOARD7:6;
A8: p`1 >= W-bound C by A1,A4,A5,A6,TOPREAL1:3;
p`1 <= E-bound C by A1,A4,A5,A6,TOPREAL1:3;
hence thesis by A7,A8;
end;
let a be object;
assume a in L;
then ex p st p = a & p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C;
hence thesis by A1,A3,A4,A2,GOBOARD7:8;
end;
theorem Th26:
LSeg(SW-corner C, NW-corner C) = { p : p`1 = W-bound C & p`2 <=
N-bound C & p`2 >= S-bound C}
proof
set L = { p : p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
set q1 = SW-corner C, q2 = NW-corner C;
A1: q1`1 = W-bound C by EUCLID:52;
A2: q1`2 = S-bound C by EUCLID:52;
A3: q2`1 = W-bound C by EUCLID:52;
A4: q2`2 = N-bound C by EUCLID:52;
A5: S-bound C <= N-bound C by Th22;
thus LSeg(q1,q2) c= L
proof
let a be object;
assume
A6: a in LSeg(q1,q2);
then reconsider p = a as Point of TOP-REAL 2;
A7: p`1 = W-bound C by A1,A3,A6,GOBOARD7:5;
A8: p`2 >= S-bound C by A2,A4,A5,A6,TOPREAL1:4;
p`2 <= N-bound C by A2,A4,A5,A6,TOPREAL1:4;
hence thesis by A7,A8;
end;
let a be object;
assume a in L;
then ex p st p = a & p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C;
hence thesis by A1,A2,A3,A4,GOBOARD7:7;
end;
theorem
LSeg(SW-corner C,NW-corner C) /\ LSeg(NW-corner C,NE-corner C) = {
NW-corner C }
proof
for a being object holds a in LSeg(SW-corner C,NW-corner C) /\ LSeg(
NW-corner C,NE-corner C) iff a = NW-corner C
proof
let a be object;
thus a in LSeg(SW-corner C,NW-corner C) /\ LSeg(NW-corner C,NE-corner C)
implies a = NW-corner C
proof
assume
A1: a in LSeg(SW-corner C,NW-corner C) /\ LSeg(NW-corner C,NE-corner C);
then a in LSeg(NW-corner C,NE-corner C) by XBOOLE_0:def 4;
then
a in {p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C} by Th25;
then
A2: ex p st p=a & p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C;
a in LSeg(SW-corner C,NW-corner C)by A1,XBOOLE_0:def 4;
then
a in {p : p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C} by Th26;
then
ex p st p = a & p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = NW-corner C;
then
A4: a in LSeg(NW-corner C,NE-corner C) by RLTOPSP1:68;
a in LSeg(SW-corner C,NW-corner C) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th28:
LSeg(NW-corner C,NE-corner C) /\ LSeg(NE-corner C,SE-corner C) =
{NE-corner C}
proof
for a being object holds a in LSeg(NW-corner C,NE-corner C) /\ LSeg(
NE-corner C,SE-corner C) iff a = NE-corner C
proof
let a be object;
thus a in LSeg(NW-corner C,NE-corner C) /\ LSeg(NE-corner C,SE-corner C)
implies a = NE-corner C
proof
assume
A1: a in LSeg(NW-corner C,NE-corner C) /\ LSeg(NE-corner C,SE-corner C);
then a in LSeg(NE-corner C,SE-corner C) by XBOOLE_0:def 4;
then
a in {p : p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C } by Th23
;
then
A2: ex p st p=a & p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C;
a in LSeg(NW-corner C,NE-corner C)by A1,XBOOLE_0:def 4;
then
a in {p :p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C } by Th25;
then
ex p st p = a & p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = NE-corner C;
then
A4: a in LSeg(NE-corner C,SE-corner C) by RLTOPSP1:68;
a in LSeg(NW-corner C,NE-corner C) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th29:
LSeg(SE-corner C,NE-corner C) /\ LSeg(SW-corner C,SE-corner C) =
{SE-corner C}
proof
for a being object holds a in LSeg(NE-corner C,SE-corner C) /\ LSeg(
SE-corner C,SW-corner C) iff a = SE-corner C
proof
let a be object;
thus a in LSeg(NE-corner C,SE-corner C) /\ LSeg(SE-corner C,SW-corner C)
implies a = SE-corner C
proof
assume
A1: a in LSeg(NE-corner C,SE-corner C) /\ LSeg(SE-corner C,SW-corner C);
then a in LSeg(SE-corner C,SW-corner C) by XBOOLE_0:def 4;
then
a in {p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C } by Th24
;
then
A2: ex p st p=a & p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C;
a in LSeg(NE-corner C,SE-corner C)by A1,XBOOLE_0:def 4;
then
a in {p : p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C } by Th23
;
then
ex p st p = a & p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = SE-corner C;
then
A4: a in LSeg(SE-corner C,SW-corner C) by RLTOPSP1:68;
a in LSeg(NE-corner C,SE-corner C) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th30:
LSeg(NW-corner C,SW-corner C) /\ LSeg(SW-corner C,SE-corner C) =
{SW-corner C}
proof
for a being object holds a in LSeg(NW-corner C,SW-corner C) /\ LSeg(
SW-corner C,SE-corner C) iff a = SW-corner C
proof
let a be object;
thus a in LSeg(NW-corner C,SW-corner C) /\ LSeg(SW-corner C,SE-corner C)
implies a = SW-corner C
proof
assume
A1: a in LSeg(NW-corner C,SW-corner C) /\ LSeg(SW-corner C,SE-corner C);
then a in LSeg(SW-corner C,SE-corner C) by XBOOLE_0:def 4;
then a in {p : p`1 <= E-bound C & p`1 >= W-bound C & p`2= S-bound C} by
Th24;
then
A2: ex p st p=a & p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C;
a in LSeg(NW-corner C,SW-corner C)by A1,XBOOLE_0:def 4;
then
a in {p : p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C } by Th26
;
then
ex p st p = a & p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = SW-corner C;
then
A4: a in LSeg(SW-corner C,SE-corner C) by RLTOPSP1:68;
a in LSeg(NW-corner C,SW-corner C) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
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 Th31:
W-bound D1 < E-bound D1
proof
A1: W-bound D1 <> E-bound D1 by Th15;
W-bound D1 <= E-bound D1 by Th21;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th32:
S-bound D2 < N-bound D2
proof
A1: S-bound D2 <> N-bound D2 by Th16;
S-bound D2 <= N-bound D2 by Th22;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th33:
LSeg(SW-corner D1,NW-corner D1) misses LSeg(SE-corner D1, NE-corner D1)
proof
assume
LSeg(SW-corner D1,NW-corner D1) /\ LSeg(SE-corner D1,NE-corner D1) <> {};
then consider a being object such that
A1: a in LSeg(SW-corner D1,NW-corner D1) /\ LSeg(SE-corner D1,NE-corner
D1) by XBOOLE_0:def 1;
a in LSeg(NE-corner D1,SE-corner D1) by A1,XBOOLE_0:def 4;
then
a in {p : p`1= E-bound D1 & p`2 <= N-bound D1 & p`2 >= S-bound D1} by Th23;
then
A2: ex p st p=a & p`1 = E-bound D1 & p`2 <= N-bound D1 & p`2 >= S-bound D1;
a in LSeg(NW-corner D1,SW-corner D1)by A1,XBOOLE_0:def 4;
then a in {p : p`1 = W-bound D1 & p`2 <= N-bound D1 & p`2 >= S-bound D1} by
Th26;
then
ex p st p = a & p`1 = W-bound D1 & p`2 <= N-bound D1 & p`2 >= S-bound D1;
hence contradiction by A2,Th15;
end;
theorem Th34:
LSeg(SW-corner D2,SE-corner D2) misses LSeg(NW-corner D2, NE-corner D2)
proof
assume
LSeg(SW-corner D2,SE-corner D2) /\ LSeg(NW-corner D2,NE-corner D2) <> {};
then consider a being object such that
A1: a in LSeg(SW-corner D2,SE-corner D2) /\ LSeg(NW-corner D2,NE-corner
D2) by XBOOLE_0:def 1;
a in LSeg(NE-corner D2,NW-corner D2) by A1,XBOOLE_0:def 4;
then
a in {p : p`1 <= E-bound D2 & p`1 >= W-bound D2 & p`2= N-bound D2} by Th25;
then
A2: ex p st p=a & p`1 <= E-bound D2 & p`1 >= W-bound D2 & p`2 = N-bound D2;
a in LSeg(SE-corner D2,SW-corner D2)by A1,XBOOLE_0:def 4;
then a in {p : p`1 <= E-bound D2 & p`1 >= W-bound D2 & p`2 = S-bound D2} by
Th24;
then
ex p st p = a & p`1 <= E-bound D2 & p`1 >= W-bound D2 & p`2 = S-bound D2;
hence contradiction by A2,Th16;
end;
begin :: SpStSeq
definition
let C be Subset of TOP-REAL 2;
func SpStSeq C -> FinSequence of TOP-REAL 2 equals
<*NW-corner C,NE-corner C
,SE-corner C*>^ <*SW-corner C,NW-corner C*>;
coherence;
end;
theorem Th35:
(SpStSeq S)/.1 = NW-corner S
proof
1 in dom<*NW-corner S,NE-corner S,SE-corner S*> by FINSEQ_1:81;
hence (SpStSeq S)/.1 = <*NW-corner S,NE-corner S,SE-corner S*>/.1 by
FINSEQ_4:68
.= NW-corner S by FINSEQ_4:18;
end;
theorem Th36:
(SpStSeq S)/.2 = NE-corner S
proof
2 in dom<*NW-corner S,NE-corner S,SE-corner S*> by FINSEQ_1:81;
hence (SpStSeq S)/.2 = <*NW-corner S,NE-corner S,SE-corner S*>/.2 by
FINSEQ_4:68
.= NE-corner S by FINSEQ_4:18;
end;
theorem Th37:
(SpStSeq S)/.3 = SE-corner S
proof
3 in dom<*NW-corner S,NE-corner S,SE-corner S*> by FINSEQ_1:81;
hence (SpStSeq S)/.3 = <*NW-corner S,NE-corner S,SE-corner S*>/.3 by
FINSEQ_4:68
.= SE-corner S by FINSEQ_4:18;
end;
theorem Th38:
(SpStSeq S)/.4 = SW-corner S
proof
set g = <*NW-corner S,NE-corner S,SE-corner S*>;
1 in {1,2} by TARSKI:def 2;
then
A1: 1 in dom <*SW-corner S,NW-corner S*> by FINSEQ_1:2,89;
len g = 3 by FINSEQ_1:45;
hence (SpStSeq S)/.4 = (SpStSeq S)/.(len g + 1)
.= <*SW-corner S,NW-corner S*>/.1 by A1,FINSEQ_4:69
.= SW-corner S by FINSEQ_4:17;
end;
theorem
(SpStSeq S)/.5 = NW-corner S
proof
set g = <*NW-corner S,NE-corner S,SE-corner S*>;
2 in {1,2} by TARSKI:def 2;
then
A1: 2 in dom <*SW-corner S,NW-corner S*> by FINSEQ_1:2,89;
len g = 3 by FINSEQ_1:45;
hence (SpStSeq S)/.5 = (SpStSeq S)/.(len g + 2)
.= <*SW-corner S,NW-corner S*>/.2 by A1,FINSEQ_4:69
.= NW-corner S by FINSEQ_4:17;
end;
theorem Th40:
len SpStSeq S = 5
proof
thus len SpStSeq S = len<*NW-corner S,NE-corner S,SE-corner S*> + len<*
SW-corner S,NW-corner S*> by FINSEQ_1:22
.= len<*SW-corner S,NW-corner S*> + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= 5;
end;
theorem Th41:
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))
proof
len<*NW-corner S,NE-corner S,SE-corner S*> = 3 by FINSEQ_1:45;
then
A1: <*NW-corner S,NE-corner S,SE-corner S*>/. len<*NW-corner S,NE-corner S,
SE-corner S*> = SE-corner S by FINSEQ_4:18;
<*SW-corner S,NW-corner S*>/.1 = SW-corner S by FINSEQ_4:17;
hence L~SpStSeq S = L~<*NW-corner S,NE-corner S,SE-corner S*> \/ LSeg(
SE-corner S,SW-corner S) \/ L~<*SW-corner S,NW-corner S*> by A1,SPPOL_2:23
.= L~<*NW-corner S,NE-corner S,SE-corner S*> \/ LSeg(SE-corner S,
SW-corner S) \/ LSeg(SW-corner S,NW-corner S) by SPPOL_2:21
.= 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) by Th8
.= (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)) by XBOOLE_1:4;
end;
registration
let D be non vertical non empty compact Subset of TOP-REAL 2;
cluster SpStSeq D -> non constant;
coherence
proof
assume SpStSeq D is constant;
then <*NW-corner D,NE-corner D,SE-corner D*> is constant by Th1;
then |[W-bound D, N-bound D]| = |[E-bound D, N-bound D]| by Th3;
then W-bound D = E-bound D by SPPOL_2:1;
hence contradiction by Th15;
end;
end;
registration
let D be non horizontal non empty compact Subset of TOP-REAL 2;
cluster SpStSeq D -> non constant;
coherence
proof
assume SpStSeq D is constant;
then <*SW-corner D,NW-corner D*> is constant by Th1;
then |[W-bound D, N-bound D]| = |[W-bound D, S-bound D]| by Th2;
then N-bound D = S-bound D by SPPOL_2:1;
hence contradiction by Th16;
end;
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;
coherence
proof
reconsider Sb = S-bound D, Nb = N-bound D,
Wb = W-bound D, Eb = E-bound D as Element of REAL
by XREAL_0:def 1;
A1: <*Sb,Nb*> is increasing
proof
let n,m be Nat;
assume that
A2: n in dom <*Sb,Nb*> and
A3: m in dom <*Sb,Nb*>;
len <*S-bound D,N-bound D*> = 2 by FINSEQ_1:44;
then
A4: dom <*S-bound D,N-bound D*> = { 1,2 } by FINSEQ_1:2,def 3;
then
A5: n = 1 or n = 2 by A2,TARSKI:def 2;
assume
A6: n < m;
A7: m = 1 or m = 2 by A4,A3,TARSKI:def 2;
then
A8: <*S-bound D,N-bound D*>.m = N-bound D by A5,A6;
<*S-bound D,N-bound D*>.n = S-bound D by A5,A7,A6;
hence <*Sb,Nb*>.n < <*Sb,Nb*>.m by A8,Th32;
end;
set S = (|[W-bound D,S-bound D]|,|[W-bound D,N-bound D]|) ][(|[E-bound D,
S-bound D]|,|[E-bound D,N-bound D]|);
set Yf1 = <*Nb,Nb,Sb*>, Yf2 = <*Sb,Nb*>;
set Xf1 = <*Wb,Eb,Eb*>, Xf2 = <*Wb,Wb*>;
set f = SpStSeq D;
set f1 = <*NW-corner D,NE-corner D,SE-corner D*>, f2 = <*SW-corner D,
NW-corner D*>;
reconsider Xf = Xf1^Xf2 as FinSequence of REAL;
A9: rng Xf2 = { W-bound D,W-bound D } by FINSEQ_2:127
.= { W-bound D } by ENUMSET1:29;
rng Xf1 = { W-bound D,E-bound D,E-bound D } by FINSEQ_2:128
.= { E-bound D,E-bound D,W-bound D } by ENUMSET1:60
.= { W-bound D,E-bound D } by ENUMSET1:30;
then
A10: rng Xf = { W-bound D,E-bound D } \/ { W-bound D } by A9,FINSEQ_1:31
.= { W-bound D,W-bound D,E-bound D } by ENUMSET1:2
.= { W-bound D,E-bound D } by ENUMSET1:30;
then
A11: rng <*W-bound D,E-bound D*> = rng Xf by FINSEQ_2:127;
A12: <*Wb,Eb*> is increasing
proof
let n,m be Nat;
assume that
A13: n in dom <*Wb,Eb*> and
A14: m in dom <*Wb,Eb*>;
len <*W-bound D,E-bound D*> = 2 by FINSEQ_1:44;
then
A15: dom <*W-bound D,E-bound D*> = { 1,2 } by FINSEQ_1:2,def 3;
then
A16: n = 1 or n = 2 by A13,TARSKI:def 2;
assume
A17: n < m;
A18: m = 1 or m = 2 by A15,A14,TARSKI:def 2;
then
A19: <*W-bound D,E-bound D*>.m = E-bound D by A16,A17;
<*W-bound D,E-bound D*>.n = W-bound D by A16,A18,A17;
hence <*Wb,Eb*>.n < <*Wb,Eb*>.m by A19,Th31;
end;
A20: S-bound D < N-bound D by Th32;
reconsider Yf = Yf1^Yf2 as FinSequence of REAL;
A21: rng Yf2 = { S-bound D,N-bound D } by FINSEQ_2:127;
rng Yf1 = { N-bound D,N-bound D,S-bound D } by FINSEQ_2:128
.= { S-bound D,N-bound D } by ENUMSET1:30;
then
A22: rng Yf = { S-bound D,N-bound D } \/ { S-bound D,N-bound D } by A21,
FINSEQ_1:31
.= { S-bound D,N-bound D };
then
A23: rng <*S-bound D,N-bound D*> = rng Yf by FINSEQ_2:127;
A24: len <*S-bound D,N-bound D*> = 2 by FINSEQ_1:44
.= card rng Yf by A20,A22,CARD_2:57;
A25: len Yf1 = 3 by FINSEQ_1:45;
then 1 in dom Yf1 by FINSEQ_3:25;
then
A26: Yf.1 = Yf1.1 by FINSEQ_1:def 7
.= N-bound D;
A27: len Yf2 = 2 by FINSEQ_1:44;
then
A28: len Yf = 3+2 by A25,FINSEQ_1:22;
2 in dom Yf2 by A27,FINSEQ_3:25;
then
A29: Yf.(3+2) = Yf2.2 by A25,FINSEQ_1:def 7
.= N-bound D;
3 in dom Yf1 by A25,FINSEQ_3:25;
then
A30: Yf.3 = Yf1.3 by FINSEQ_1:def 7
.= S-bound D;
2 in dom Yf1 by A25,FINSEQ_3:25;
then
A31: Yf.2 = Yf1.2 by FINSEQ_1:def 7
.= N-bound D;
A32: len f1 = 3 by FINSEQ_1:45;
then 1 in dom f1 by FINSEQ_3:25;
then
A33: f/.1 = f1/.1 by FINSEQ_4:68
.= NW-corner D by FINSEQ_4:18;
3 in dom f1 by A32,FINSEQ_3:25;
then
A34: f/.3 = f1/.3 by FINSEQ_4:68
.= SE-corner D by FINSEQ_4:18;
2 in dom f1 by A32,FINSEQ_3:25;
then
A35: f/.2 = f1/.2 by FINSEQ_4:68
.= NE-corner D by FINSEQ_4:18;
A36: len f2 = 2 by FINSEQ_1:44;
then
A37: len(f1^f2) = 3+2 by A32,FINSEQ_1:22;
1 in dom f2 by A36,FINSEQ_3:25;
then
A38: f/.(3+1) = f2/.1 by A32,FINSEQ_4:69
.= SW-corner D by FINSEQ_4:17;
then
A39: LSeg(f,3) = LSeg(SE-corner D,SW-corner D) by A37,A34,TOPREAL1:def 3;
2 in dom f2 by A36,FINSEQ_3:25;
then
A40: f/.(3+2) = f2/.2 by A32,FINSEQ_4:69
.= NW-corner D by FINSEQ_4:17;
thus f is special
proof
let i be Nat;
assume 1 <= i;
then 1+1 <= i+1 by XREAL_1:6;
then
A41: 1 < i+1 by XXREAL_0:2;
assume i+1 <= len f;
then
A42: i+1 = 0 or ... or i+1 = 5 by A37;
per cases by A41,A42;
suppose
A43: i = 1;
(f/.1)`2 = N-bound D by A33,EUCLID:52
.= (f/.(1+1))`2 by A35,EUCLID:52;
hence thesis by A43;
end;
suppose
A44: i = 2;
(f/.2)`1 = E-bound D by A35,EUCLID:52
.= (f/.(2+1))`1 by A34,EUCLID:52;
hence thesis by A44;
end;
suppose
A45: i = 3;
(f/.3)`2 = S-bound D by A34,EUCLID:52
.= (f/.(3+1))`2 by A38,EUCLID:52;
hence thesis by A45;
end;
suppose
A46: i = 4;
(f/.4)`1 = W-bound D by A38,EUCLID:52
.= (f/.(4+1))`1 by A40,EUCLID:52;
hence thesis by A46;
end;
end;
4+1 = 5;
then
A47: LSeg(f,4) = LSeg(SW-corner D,NW-corner D) by A37,A38,A40,TOPREAL1:def 3;
2+1 = 3;
then
A48: LSeg(f,2) = LSeg(NE-corner D,SE-corner D) by A37,A35,A34,TOPREAL1:def 3;
1 in dom Yf2 by A27,FINSEQ_3:25;
then
A49: Yf.(3+1) = Yf2.1 by A25,FINSEQ_1:def 7
.= S-bound D;
now
let n be Nat;
assume
A50: n in dom Yf;
then
A51: n <> 0 by FINSEQ_3:25;
n <= 5 by A28,A50,FINSEQ_3:25;
then n = 0 or ... or n = 5;
then per cases by A51;
suppose
n = 1;
hence Yf.n = (f/.n)`2 by A33,A26,EUCLID:52;
end;
suppose
n = 2;
hence Yf.n = (f/.n)`2 by A35,A31,EUCLID:52;
end;
suppose
n = 3;
hence Yf.n = (f/.n)`2 by A34,A30,EUCLID:52;
end;
suppose
n = 4;
hence Yf.n = (f/.n)`2 by A38,A49,EUCLID:52;
end;
suppose
n = 5;
hence Yf.n = (f/.n)`2 by A40,A29,EUCLID:52;
end;
end;
then Yf = Y_axis f by A37,A28,GOBOARD1:def 2;
then
A52: <*S-bound D,N-bound D*> = Incr Y_axis f by A23,A24,A1,SEQ_4:def 21;
1+1 = 2;
then
A53: LSeg(f,1) = LSeg(NW-corner D,NE-corner D) by A37,A33,A35,TOPREAL1:def 3;
thus f is unfolded
proof
let i be Nat;
assume 1 <= i;
then
A54: 1+2 <= i+2 by XREAL_1:6;
assume
A55: i + 2 <= len f;
A56: 2 < i+2 by A54,XXREAL_0:2;
i+2 = 0 or ... or i+2 = 5 by A37,A55;
then per cases by A56;
suppose
i = 1;
hence thesis by A35,A53,A48,Th28;
end;
suppose
i = 2;
hence thesis by A34,A48,A39,Th29;
end;
suppose
i = 3;
hence thesis by A38,A39,A47,Th30;
end;
end;
thus f is circular by A37,A33,A40,FINSEQ_6:def 1;
thus f is s.c.c.
proof
let i,j;
assume that
A57: i+1 < j and
A58: i > 1 & j < len f or j+1 < len f;
j+1 <= 5 by A37,A58,NAT_1:13;
then
A59: j+1 = 0 or ... or j+1 = 5;
A60: i+1+1 = i+(1+1);
then
A61: i+2 <> 0+1;
A62: i+2 <= j by A57,A60,NAT_1:13;
A63: now
per cases by A57,A59,NAT_1:11;
case
j = 2;
then i+2 <= 2 by A62;
then i+2 = 0 or ... or i+2 = 2;
hence i = 0 by A57;
end;
case
j = 3;
then i+2 <= 3 by A62;
then i+2 = 0 or ... or i+2 = 3;
hence i = 0 or i = 1 by A57;
end;
case
A64: j = 4;
then i+2 <= 4 by A62;
then i+2 = 0 or ... or i+2 = 4;
hence i = 0 or i = 2 by A37,A58,A61,A64;
end;
end;
per cases by A63;
suppose
i = 0;
then LSeg(f,i) = {} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
suppose
i = 1 & j = 3;
then LSeg(f,i) misses LSeg(f,j) by A53,A39,Th34;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
suppose
i = 2 & j = 4;
then LSeg(f,i) misses LSeg(f,j) by A48,A47,Th33;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
end;
A65: W-bound D < E-bound D by Th31;
A66: len <*W-bound D,E-bound D*> = 2 by FINSEQ_1:44
.= card rng Xf by A65,A10,CARD_2:57;
A67: len Xf1 = 3 by FINSEQ_1:45;
then 1 in dom Xf1 by FINSEQ_3:25;
then
A68: Xf.1 = Xf1.1 by FINSEQ_1:def 7
.= W-bound D;
A69: len Xf2 = 2 by FINSEQ_1:44;
then
A70: len Xf = 3+2 by A67,FINSEQ_1:22;
2 in dom Xf2 by A69,FINSEQ_3:25;
then
A71: Xf.(3+2) = Xf2.2 by A67,FINSEQ_1:def 7
.= W-bound D;
3 in dom Xf1 by A67,FINSEQ_3:25;
then
A72: Xf.3 = Xf1.3 by FINSEQ_1:def 7
.= E-bound D;
2 in dom Xf1 by A67,FINSEQ_3:25;
then
A73: Xf.2 = Xf1.2 by FINSEQ_1:def 7
.= E-bound D;
1 in dom Xf2 by A69,FINSEQ_3:25;
then
A74: Xf.(3+1) = Xf2.1 by A67,FINSEQ_1:def 7
.= W-bound D;
now
let n be Nat;
assume
A75: n in dom Xf;
then
A76: n <> 0 by FINSEQ_3:25;
n <= 5 by A70,A75,FINSEQ_3:25;
then n = 0 or ... or n = 5;
then per cases by A76;
suppose
n = 1;
hence Xf.n = (f/.n)`1 by A33,A68,EUCLID:52;
end;
suppose
n = 2;
hence Xf.n = (f/.n)`1 by A35,A73,EUCLID:52;
end;
suppose
n = 3;
hence Xf.n = (f/.n)`1 by A34,A72,EUCLID:52;
end;
suppose
n = 4;
hence Xf.n = (f/.n)`1 by A38,A74,EUCLID:52;
end;
suppose
n = 5;
hence Xf.n = (f/.n)`1 by A40,A71,EUCLID:52;
end;
end;
then Xf = X_axis f by A37,A70,GOBOARD1:def 1;
then
A77: <*W-bound D,E-bound D*> = Incr X_axis f by A11,A66,A12,SEQ_4:def 21;
A78: for n,m being Nat st [n,m] in Indices S holds S*(n,m) =
|[(Incr X_axis f).n,(Incr Y_axis f).m]|
proof
let n,m be Nat;
assume [n,m] in Indices S;
then [n,m] in [:{ 1,2 },{ 1,2 }:] by FINSEQ_1:2,MATRIX_0:47;
then
A80: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by MCART_1:23;
per cases by A80,ENUMSET1:def 2;
suppose
A82: [n,m] = [1,1];
then
A83: m = 1 by XTUPLE_0:1;
A84: n = 1 by A82,XTUPLE_0:1;
hence S*(n,m) = |[W-bound D,S-bound D]| by A83,MATRIX_0:50
.= |[(Incr X_axis f).n,(Incr Y_axis f).m]| by A77,A52,A84,A83;
end;
suppose
A85: [n,m] = [1,2];
then
A86: m = 2 by XTUPLE_0:1;
A87: n = 1 by A85,XTUPLE_0:1;
hence S*(n,m) = |[W-bound D,N-bound D]| by A86,MATRIX_0:50
.= |[(Incr X_axis f).n,(Incr Y_axis f).m]| by A77,A52,A87,A86;
end;
suppose
A88: [n,m] = [2,1];
then
A89: m = 1 by XTUPLE_0:1;
A90: n = 2 by A88,XTUPLE_0:1;
hence S*(n,m) = |[E-bound D,S-bound D]| by A89,MATRIX_0:50
.= |[(Incr X_axis f).n,(Incr Y_axis f).m]| by A77,A52,A90,A89;
end;
suppose
A91: [n,m] = [2,2];
then
A92: m = 2 by XTUPLE_0:1;
A93: n = 2 by A91,XTUPLE_0:1;
hence S*(n,m) = |[E-bound D,N-bound D]| by A92,MATRIX_0:50
.= |[(Incr X_axis f).n,(Incr Y_axis f).m]| by A77,A52,A93,A92;
end;
end;
A94: width S = 2 by MATRIX_0:47
.= len Incr Y_axis f by A52,FINSEQ_1:44;
len S = 2 by MATRIX_0:47
.= len Incr X_axis f by A77,FINSEQ_1:44;
then
A95: S = GoB(Incr X_axis f, Incr Y_axis f) by A94,A78,GOBOARD2:def 1
.= GoB f by GOBOARD2:def 2;
then
A96: f/.2 = (GoB f)*(2,2) by A35,MATRIX_0:50;
A97: f/.4 = (GoB f)*(1,1) by A38,A95,MATRIX_0:50;
A98: f/.3 = (GoB f)*(2,1) by A34,A95,MATRIX_0:50;
A99: f/.1 = (GoB f)*(1,2) by A33,A95,MATRIX_0:50;
thus SpStSeq D is standard
proof
thus for k st k in dom f ex i,j st [i,j] in Indices GoB f & f/.k = (GoB
f)*(i,j)
proof
let k;
assume
A100: k in dom f;
then
A101: k >= 1 by FINSEQ_3:25;
k <= 5 by A37,A100,FINSEQ_3:25;
then k = 0 or ... or k = 5;
then per cases by A101;
suppose
A102: k = 1;
take 1,2;
thus [1,2] in Indices GoB f by A95,MATRIX_0:48;
thus thesis by A33,A95,A102,MATRIX_0:50;
end;
suppose
A103: k = 2;
take 2,2;
thus [2,2] in Indices GoB f by A95,MATRIX_0:48;
thus thesis by A35,A95,A103,MATRIX_0:50;
end;
suppose
A104: k = 3;
take 2,1;
thus [2,1] in Indices GoB f by A95,MATRIX_0:48;
thus thesis by A34,A95,A104,MATRIX_0:50;
end;
suppose
A105: k = 4;
take 1,1;
thus [1,1] in Indices GoB f by A95,MATRIX_0:48;
thus thesis by A38,A95,A105,MATRIX_0:50;
end;
suppose
A106: k = 5;
take 1,2;
thus [1,2] in Indices GoB f by A95,MATRIX_0:48;
thus thesis by A40,A95,A106,MATRIX_0:50;
end;
end;
let n be Nat such that
A107: n in dom f and
A108: n+1 in dom f;
A109: n <> 0 by A107,FINSEQ_3:25;
n+1 <= 4+1 by A37,A108,FINSEQ_3:25;
then
A110: n <= 4 by XREAL_1:6;
let m,k,i,j be Nat such that
A111: [m,k] in Indices GoB f and
A112: [i,j] in Indices GoB f and
A113: f/.n = (GoB f)*(m,k) and
A114: f/.(n+1) = (GoB f)*(i,j);
n = 0 or ... or n = 4 by A110;
then per cases by A109;
suppose
A115: n = 1;
A116: [2,2] in Indices GoB f by A95,MATRIX_0:48;
then
A117: i = 1+1 by A96,A112,A114,A115,GOBOARD1:5;
A118: [1,2] in Indices GoB f by A95,MATRIX_0:48;
then m = 1 by A99,A111,A113,A115,GOBOARD1:5;
then
A119: |.m-i.| = 1 by A117,SEQM_3:41;
A120: j = 2 by A96,A112,A114,A115,A116,GOBOARD1:5;
k = 2 by A99,A111,A113,A115,A118,GOBOARD1:5;
hence |.m-i.|+|.k-j.| = 1 by A120,A119,SEQM_3:42;
end;
suppose
A121: n = 2;
A122: [2,1] in Indices GoB f by A95,MATRIX_0:48;
then
A123: j = 1 by A98,A112,A114,A121,GOBOARD1:5;
A124: [2,2] in Indices GoB f by A95,MATRIX_0:48;
then k = 1+1 by A96,A111,A113,A121,GOBOARD1:5;
then
A125: |.k-j.| = 1 by A123,SEQM_3:41;
A126: i = 2 by A98,A112,A114,A121,A122,GOBOARD1:5;
m = 2 by A96,A111,A113,A121,A124,GOBOARD1:5;
hence |.m-i.|+|.k-j.| = 1 by A126,A125,SEQM_3:42;
end;
suppose
A127: n = 3;
A128: [1,1] in Indices GoB f by A95,MATRIX_0:48;
then
A129: i = 1 by A97,A112,A114,A127,GOBOARD1:5;
A130: [2,1] in Indices GoB f by A95,MATRIX_0:48;
then m = 1+1 by A98,A111,A113,A127,GOBOARD1:5;
then
A131: |.m-i.| = 1 by A129,SEQM_3:41;
A132: j = 1 by A97,A112,A114,A127,A128,GOBOARD1:5;
k = 1 by A98,A111,A113,A127,A130,GOBOARD1:5;
hence |.m-i.|+|.k-j.| = 1 by A132,A131,SEQM_3:42;
end;
suppose
A133: n = 4;
A134: [1,1] in Indices GoB f by A95,MATRIX_0:48;
then
A135: k = 1 by A97,A111,A113,A133,GOBOARD1:5;
A136: [1,2] in Indices GoB f by A95,MATRIX_0:48;
then j = 1+1 by A33,A40,A99,A112,A114,A133,GOBOARD1:5;
then
A137: |.k-j.| = 1 by A135,SEQM_3:41;
A138: m = 1 by A97,A111,A113,A133,A134,GOBOARD1:5;
i = 1 by A33,A40,A99,A112,A114,A133,A136,GOBOARD1:5;
hence |.m-i.|+|.k-j.| = 1 by A138,A137,SEQM_3:42;
end;
end;
end;
end;
theorem Th42:
L~SpStSeq D = [.W-bound D,E-bound D,S-bound D,N-bound D.]
proof
L~SpStSeq D = (LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,
SE-corner D)) \/ (LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D
)) by Th41
.= LSeg(SW-corner D,NW-corner D) \/ ( LSeg(NW-corner D,NE-corner D) \/
LSeg(NE-corner D,SE-corner D) ) \/ LSeg(SE-corner D,SW-corner D) by XBOOLE_1:4
.= LSeg(SW-corner D,NW-corner D) \/ LSeg(NW-corner D,NE-corner D) \/
LSeg(NE-corner D,SE-corner D) \/ LSeg(SE-corner D,SW-corner D) by XBOOLE_1:4
.= ( LSeg(SW-corner D,NW-corner D) \/ LSeg(NW-corner D,NE-corner D) ) \/
( LSeg(NE-corner D,SE-corner D) \/ LSeg(SE-corner D,SW-corner D) ) by
XBOOLE_1:4;
hence thesis by SPPOL_2:def 3;
end;
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;
coherence
proof
A1: (f|X).:the carrier of T|X is bounded_below by MEASURE6:def 10;
(f|X).:X = f.:X by RELAT_1:129;
hence thesis by A1,PRE_TOPC:8;
end;
cluster f.:X -> bounded_above;
coherence
proof
A2: (f|X).:the carrier of T|X is bounded_above by MEASURE6:def 11;
(f|X).:X = f.:X by RELAT_1:129;
hence thesis by A2,PRE_TOPC:8;
end;
end;
theorem Th43:
W-bound S = lower_bound(proj1.:S)
proof
thus W-bound S = lower_bound rng(proj1|S) by RELSET_1:22
.= lower_bound(proj1.:S) by RELAT_1:115;
end;
theorem Th44:
S-bound S = lower_bound(proj2.:S)
proof
thus S-bound S = lower_bound rng(proj2|S) by RELSET_1:22
.= lower_bound(proj2.:S) by RELAT_1:115;
end;
theorem Th45:
N-bound S = upper_bound(proj2.:S)
proof
thus N-bound S = upper_bound rng(proj2|S) by RELSET_1:22
.= upper_bound(proj2.:S) by RELAT_1:115;
end;
theorem Th46:
E-bound S = upper_bound(proj1.:S)
proof
thus E-bound S = upper_bound rng(proj1|S) by RELSET_1:22
.= upper_bound(proj1.:S) by RELAT_1:115;
end;
theorem Th47:
S = C1 \/ C2 implies W-bound S = min(W-bound C1, W-bound C2)
proof
assume
A1: S = C1 \/ C2;
A2: W-bound C1 = lower_bound(proj1.:C1) by Th43;
A3: W-bound C2 = lower_bound(proj1.:C2) by Th43;
thus W-bound S = lower_bound(proj1.:S) by Th43
.= lower_bound(proj1.:C1 \/ proj1.:C2) by A1,RELAT_1:120
.= min(W-bound C1, W-bound C2) by A2,A3,SEQ_4:142;
end;
theorem Th48:
S = C1 \/ C2 implies S-bound S = min(S-bound C1, S-bound C2)
proof
assume
A1: S = C1 \/ C2;
A2: S-bound C1 = lower_bound(proj2.:C1) by Th44;
A3: S-bound C2 = lower_bound(proj2.:C2) by Th44;
thus S-bound S = lower_bound(proj2.:S) by Th44
.= lower_bound(proj2.:C1 \/ proj2.:C2) by A1,RELAT_1:120
.= min(S-bound C1, S-bound C2) by A2,A3,SEQ_4:142;
end;
theorem Th49:
S = C1 \/ C2 implies N-bound S = max(N-bound C1, N-bound C2)
proof
assume
A1: S = C1 \/ C2;
A2: N-bound C1 = upper_bound(proj2.:C1) by Th45;
A3: N-bound C2 = upper_bound(proj2.:C2) by Th45;
thus N-bound S = upper_bound(proj2.:S) by Th45
.= upper_bound(proj2.:C1 \/ proj2.:C2) by A1,RELAT_1:120
.= max(N-bound C1, N-bound C2) by A2,A3,SEQ_4:143;
end;
theorem Th50:
S = C1 \/ C2 implies E-bound S = max(E-bound C1, E-bound C2)
proof
assume
A1: S = C1 \/ C2;
A2: E-bound C1 = upper_bound(proj1.:C1) by Th46;
A3: E-bound C2 = upper_bound(proj1.:C2) by Th46;
thus E-bound S = upper_bound(proj1.:S) by Th46
.= upper_bound(proj1.:C1 \/ proj1.:C2) by A1,RELAT_1:120
.= max(E-bound C1, E-bound C2) by A2,A3,SEQ_4:143;
end;
registration
let r1,r2 be Real;
cluster [.r1,r2.] -> real-bounded for Subset of REAL;
coherence
proof
A1: [.r1,r2.] is bounded_above
proof
take r2;
let x be ExtReal;
thus thesis by XXREAL_1:1;
end;
[.r1,r2.] is bounded_below
proof
take r1;
let x be ExtReal;
thus thesis by XXREAL_1:1;
end;
hence thesis by A1;
end;
end;
theorem Th51:
r1 <= r2 implies (t in [.r1,r2.] iff ex s1 st 0 <=s1 & s1 <= 1 &
t = s1*r1 + (1-s1)*r2)
proof
assume
A1: r1 <= r2;
per cases by A1,XXREAL_0:1;
suppose
A2: r1 = r2;
then
A3: [.r1,r2.] = {r1} by XXREAL_1:17;
hereby
reconsider a19 = 1 as Real;
assume
A4: t in [.r1,r2.];
take s = a19;
thus 0 <=s & s <= 1;
thus t = s*r1 + (1-s)*r2 by A3,A4,TARSKI:def 1;
end;
given s1 such that
0 <=s1 and
s1 <= 1 and
A5: t = s1*r1 + (1-s1)*r2;
thus thesis by A2,A3,A5,TARSKI:def 1;
end;
suppose
A6: r1 < r2;
hereby
assume
A7: t in [.r1,r2.];
reconsider s1 = (r2-t)/(r2-r1) as Real;
take s1;
A8: r2 - r1 > 0 by A6,XREAL_1:50;
t <= r2 by A7,XXREAL_1:1;
then 0 <= r2-t by XREAL_1:48;
hence 0 <=s1 by A8;
r1 <= t by A7,XXREAL_1:1;
then r2-t <= r2-r1 by XREAL_1:10;
hence s1 <= 1 by A8,XREAL_1:185;
thus t = t*(r2-r1)/(r2-r1) by A8,XCMPLX_1:89
.= ((r2-t)*r1 + (t-r1)*r2)/(r2-r1)
.= (r2-t)*r1/(r2-r1) + (t-r1)*r2/(r2-r1) by XCMPLX_1:62
.= (r2-t)*r1/(r2-r1) + (t-r1)/(r2-r1)*r2 by XCMPLX_1:74
.= ((r2-t)/(r2-r1))*r1 + (1*(r2-r1)-(r2-t))/(r2-r1)*r2 by XCMPLX_1:74
.= s1*r1 + (1-s1)*r2 by A8,XCMPLX_1:127;
end;
given s1 such that
A9: 0 <=s1 and
A10: s1 <= 1 and
A11: t = s1*r1 + (1-s1)*r2;
A12: s1*r2 + (1-s1)*r2 = 1*r2;
1 - s1 >= 0 by A10,XREAL_1:48;
then
A13: (1-s1)*r1 <= (1-s1)*r2 by A6,XREAL_1:64;
s1*r1 <= s1*r2 by A6,A9,XREAL_1:64;
then
A14: t <= r2 by A11,A12,XREAL_1:6;
s1*r1 + (1-s1)*r1 = 1*r1;
then r1 <= t by A11,A13,XREAL_1:6;
hence thesis by A14,XXREAL_1:1;
end;
end;
theorem Th52:
p`1 <= q`1 implies proj1.:LSeg(p,q) = [.p`1,q`1.]
proof
assume
A1: p`1 <= q`1;
for y being object holds y in [.p`1,q`1.] iff
ex x being object st x in dom
proj1 & x in LSeg(p,q) & y = proj1.x
proof
let y be object;
hereby
assume
A2: y in [.p`1,q`1.];
then reconsider r = y as Real;
consider t such that
A3: 0 <=t and
A4: t <= 1 and
A5: r = t*p`1 + (1-t)*q`1 by A1,A2,Th51;
set o = t*p + (1-t)*q;
reconsider x = o as object;
take x;
o in the carrier of TOP-REAL 2;
hence x in dom proj1 by FUNCT_2:def 1;
o in LSeg(q,p) by A3,A4;
hence x in LSeg(p,q);
thus y = (t*p)`1 + (1-t)*(q`1) by A5,TOPREAL3:4
.= (t*p)`1 + ((1-t)*q)`1 by TOPREAL3:4
.= (t*p + (1-t)*q)`1 by TOPREAL3:2
.= proj1.x by PSCOMP_1:def 5;
end;
given x being object such that
x in dom proj1 and
A6: x in LSeg(p,q) and
A7: y = proj1.x;
reconsider s = x as Point of TOP-REAL 2 by A6;
x in LSeg(q,p) by A6;
then consider r being Real such that
A8: s = (1-r)*q+r*p and
A9: 0<=r and
A10: r<=1;
y = s`1 by A7,PSCOMP_1:def 5
.= ((1-r)*q)`1+(r*p)`1 by A8,TOPREAL3:2
.= (1-r)*(q`1)+(r*p)`1 by TOPREAL3:4
.= (1-r)*(q`1)+r*(p`1) by TOPREAL3:4;
hence thesis by A1,A9,A10,Th51;
end;
hence thesis by FUNCT_1:def 6;
end;
theorem Th53:
p`2 <= q`2 implies proj2.:LSeg(p,q) = [.p`2,q`2.]
proof
assume
A1: p`2 <= q`2;
for y being object holds y in [.p`2,q`2.] iff
ex x being object st x in dom
proj2 & x in LSeg(p,q) & y = proj2.x
proof
let y be object;
hereby
assume
A2: y in [.p`2,q`2.];
then reconsider r = y as Real;
consider t such that
A3: 0 <=t and
A4: t <= 1 and
A5: r = t*p`2 + (1-t)*q`2 by A1,A2,Th51;
set o = t*p + (1-t)*q;
reconsider x = o as object;
take x;
o in the carrier of TOP-REAL 2;
hence x in dom proj2 by FUNCT_2:def 1;
o in LSeg(q,p) by A3,A4;
hence x in LSeg(p,q);
thus y = (t*p)`2 + (1-t)*(q`2) by A5,TOPREAL3:4
.= (t*p)`2 + ((1-t)*q)`2 by TOPREAL3:4
.= (t*p + (1-t)*q)`2 by TOPREAL3:2
.= proj2.x by PSCOMP_1:def 6;
end;
given x being object such that
x in dom proj2 and
A6: x in LSeg(p,q) and
A7: y = proj2.x;
reconsider s = x as Point of TOP-REAL 2 by A6;
x in LSeg(q,p) by A6;
then consider r being Real such that
A8: s = (1-r)*q+r*p and
A9: 0<=r and
A10: r<=1;
y = s`2 by A7,PSCOMP_1:def 6
.= ((1-r)*q)`2+(r*p)`2 by A8,TOPREAL3:2
.= (1-r)*(q`2)+(r*p)`2 by TOPREAL3:4
.= (1-r)*(q`2)+r*(p`2) by TOPREAL3:4;
hence thesis by A1,A9,A10,Th51;
end;
hence thesis by FUNCT_1:def 6;
end;
theorem Th54:
p`1 <= q`1 implies W-bound LSeg(p,q) = p`1
proof
assume
A1: p`1 <= q`1;
then
A2: proj1.:LSeg(p,q) = [.p`1,q`1.] by Th52;
thus W-bound LSeg(p,q) = lower_bound(proj1.:LSeg(p,q)) by Th43
.= p`1 by A1,A2,JORDAN5A:19;
end;
theorem Th55:
p`2 <= q`2 implies S-bound LSeg(p,q) = p`2
proof
assume
A1: p`2 <= q`2;
then
A2: proj2.:LSeg(p,q) = [.p`2,q`2.] by Th53;
thus S-bound LSeg(p,q) = lower_bound(proj2.:LSeg(p,q)) by Th44
.= p`2 by A1,A2,JORDAN5A:19;
end;
theorem Th56:
p`2 <= q`2 implies N-bound LSeg(p,q) = q`2
proof
assume
A1: p`2 <= q`2;
then
A2: proj2.:LSeg(p,q) = [.p`2,q`2.] by Th53;
thus N-bound LSeg(p,q) = upper_bound(proj2.:LSeg(p,q)) by Th45
.= q`2 by A1,A2,JORDAN5A:19;
end;
theorem Th57:
p`1 <= q`1 implies E-bound LSeg(p,q) = q`1
proof
assume
A1: p`1 <= q`1;
then
A2: proj1.:LSeg(p,q) = [.p`1,q`1.] by Th52;
thus E-bound LSeg(p,q) = upper_bound(proj1.:LSeg(p,q)) by Th46
.= q`1 by A1,A2,JORDAN5A:19;
end;
theorem Th58:
W-bound L~SpStSeq C = W-bound C
proof
set S1 = LSeg(NW-corner C,NE-corner C), S2 = LSeg(NE-corner C,SE-corner C),
S3 = LSeg(SE-corner C,SW-corner C), S4 = LSeg(SW-corner C,NW-corner C);
A1: (SE-corner C)`1 = E-bound C by EUCLID:52;
A2: W-bound C <= E-bound C by Th21;
A3: S3 \/ S4 is compact by COMPTS_1:10;
A4: (NE-corner C)`1 = E-bound C by EUCLID:52;
then
A5: W-bound S2 = E-bound C by A1,Th54;
A6: (SW-corner C)`1 = W-bound C by EUCLID:52;
A7: (NW-corner C)`1 = W-bound C by EUCLID:52;
then
A8: W-bound S4 = W-bound C by A6,Th54;
A9: W-bound(S3 \/ S4) = min(W-bound S3,W-bound S4) by Th47
.= min(W-bound C,W-bound C) by A1,A6,A8,Th21,Th54
.= W-bound C;
A10: L~SpStSeq C = (S1 \/ S2) \/ (S3 \/ S4) by Th41;
A11: S1 \/ S2 is compact by COMPTS_1:10;
W-bound(S1 \/ S2) = min(W-bound S1,W-bound S2) by Th47
.= min(E-bound C,W-bound C) by A7,A4,A5,Th21,Th54
.= W-bound C by A2,XXREAL_0:def 9;
hence W-bound L~SpStSeq C = min(W-bound C,W-bound C) by A10,A11,A3,A9,Th47
.= W-bound C;
end;
theorem Th59:
S-bound L~SpStSeq C = S-bound C
proof
set S1 = LSeg(NW-corner C,NE-corner C), S2 = LSeg(NE-corner C,SE-corner C),
S3 = LSeg(SE-corner C,SW-corner C), S4 = LSeg(SW-corner C,NW-corner C);
A1: (SE-corner C)`2 = S-bound C by EUCLID:52;
A2: S-bound C <= N-bound C by Th22;
A3: S3 \/ S4 is compact by COMPTS_1:10;
A4: (NE-corner C)`2 = N-bound C by EUCLID:52;
then
A5: S-bound S2 = S-bound C by A1,Th22,Th55;
A6: (SW-corner C)`2 = S-bound C by EUCLID:52;
A7: (NW-corner C)`2 = N-bound C by EUCLID:52;
then
A8: S-bound S4 = S-bound C by A6,Th22,Th55;
A9: S-bound(S3 \/ S4) = min(S-bound S3,S-bound S4) by Th48
.= min(S-bound C,S-bound C) by A1,A6,A8,Th55
.= S-bound C;
A10: L~SpStSeq C = (S1 \/ S2) \/ (S3 \/ S4) by Th41;
A11: S1 \/ S2 is compact by COMPTS_1:10;
S-bound(S1 \/ S2) = min(S-bound S1,S-bound S2) by Th48
.= min(N-bound C,S-bound C) by A7,A4,A5,Th55
.= S-bound C by A2,XXREAL_0:def 9;
hence S-bound L~SpStSeq C = min(S-bound C,S-bound C) by A10,A11,A3,A9,Th48
.= S-bound C;
end;
theorem Th60:
N-bound L~SpStSeq C = N-bound C
proof
set S1 = LSeg(NW-corner C,NE-corner C), S2 = LSeg(NE-corner C,SE-corner C),
S3 = LSeg(SE-corner C,SW-corner C), S4 = LSeg(SW-corner C,NW-corner C);
A1: (NW-corner C)`2 = N-bound C by EUCLID:52;
A2: S-bound C <= N-bound C by Th22;
A3: S3 \/ S4 is compact by COMPTS_1:10;
A4: (SW-corner C)`2 = S-bound C by EUCLID:52;
then
A5: N-bound S4 = N-bound C by A1,Th22,Th56;
A6: (SE-corner C)`2 = S-bound C by EUCLID:52;
A7: (NE-corner C)`2 = N-bound C by EUCLID:52;
then
A8: N-bound S2 = N-bound C by A6,Th22,Th56;
A9: N-bound(S1 \/ S2) = max(N-bound S1,N-bound S2) by Th49
.= max(N-bound C,N-bound C) by A1,A7,A8,Th56
.= N-bound C;
A10: L~SpStSeq C = (S1 \/ S2) \/ (S3 \/ S4) by Th41;
A11: S1 \/ S2 is compact by COMPTS_1:10;
N-bound(S3 \/ S4) = max(N-bound S3,N-bound S4) by Th49
.= max(S-bound C,N-bound C) by A6,A4,A5,Th56
.= N-bound C by A2,XXREAL_0:def 10;
hence N-bound L~SpStSeq C = max(N-bound C,N-bound C) by A10,A11,A9,A3,Th49
.= N-bound C;
end;
theorem Th61:
E-bound L~SpStSeq C = E-bound C
proof
set S1 = LSeg(NW-corner C,NE-corner C), S2 = LSeg(NE-corner C,SE-corner C),
S3 = LSeg(SE-corner C,SW-corner C), S4 = LSeg(SW-corner C,NW-corner C);
A1: (NW-corner C)`1 = W-bound C by EUCLID:52;
A2: W-bound C <= E-bound C by Th21;
A3: S3 \/ S4 is compact by COMPTS_1:10;
A4: (SW-corner C)`1 = W-bound C by EUCLID:52;
then
A5: E-bound S4 = W-bound C by A1,Th57;
A6: (SE-corner C)`1 = E-bound C by EUCLID:52;
A7: (NE-corner C)`1 = E-bound C by EUCLID:52;
then
A8: E-bound S2 = E-bound C by A6,Th57;
A9: E-bound(S1 \/ S2) = max(E-bound S1,E-bound S2) by Th50
.= max(E-bound C,E-bound C) by A1,A7,A8,Th21,Th57
.= E-bound C;
A10: L~SpStSeq C = (S1 \/ S2) \/ (S3 \/ S4) by Th41;
A11: S1 \/ S2 is compact by COMPTS_1:10;
E-bound(S3 \/ S4) = max(E-bound S3,E-bound S4) by Th50
.= max(W-bound C,E-bound C) by A6,A4,A5,Th21,Th57
.= E-bound C by A2,XXREAL_0:def 10;
hence E-bound L~SpStSeq C = max(E-bound C,E-bound C) by A10,A11,A9,A3,Th50
.= E-bound C;
end;
theorem Th62:
NW-corner L~SpStSeq C = NW-corner C
proof
thus NW-corner L~SpStSeq C = |[W-bound C, N-bound L~SpStSeq C]| by Th58
.= NW-corner C by Th60;
end;
theorem Th63:
NE-corner L~SpStSeq C = NE-corner C
proof
thus NE-corner L~SpStSeq C = |[E-bound C, N-bound L~SpStSeq C]| by Th61
.= NE-corner C by Th60;
end;
theorem Th64:
SW-corner L~SpStSeq C = SW-corner C
proof
thus SW-corner L~SpStSeq C = |[W-bound C, S-bound L~SpStSeq C]| by Th58
.= SW-corner C by Th59;
end;
theorem Th65:
SE-corner L~SpStSeq C = SE-corner C
proof
thus SE-corner L~SpStSeq C = |[E-bound C, S-bound L~SpStSeq C]| by Th61
.= SE-corner C by Th59;
end;
theorem Th66:
W-most L~SpStSeq C = LSeg(SW-corner C,NW-corner C)
proof
set X = L~SpStSeq C;
set S3 = LSeg(SE-corner C,SW-corner C), S4 = LSeg(SW-corner C,NW-corner C);
A1: S4 c= S3 \/ S4 by XBOOLE_1:7;
X = (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
(S3 \/ S4) by Th41;
then
A2: S3 \/ S4 c= X by XBOOLE_1:7;
LSeg(SW-corner X, NW-corner X) = LSeg(SW-corner X, NW-corner C) by Th62
.= LSeg(SW-corner C,NW-corner C) by Th64;
hence thesis by A1,A2,XBOOLE_1:1,28;
end;
theorem Th67:
N-most L~SpStSeq C = LSeg(NW-corner C,NE-corner C)
proof
set X = L~SpStSeq C;
set S1 = LSeg(NW-corner C,NE-corner C), S2 = LSeg(NE-corner C,SE-corner C);
A1: S1 c= S1 \/ S2 by XBOOLE_1:7;
X = (S1 \/ S2) \/ (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,
NW-corner C)) by Th41;
then
A2: S1 \/ S2 c= X by XBOOLE_1:7;
LSeg(NW-corner X, NE-corner X) = LSeg(NW-corner X, NE-corner C) by Th63
.= LSeg(NW-corner C,NE-corner C) by Th62;
hence thesis by A1,A2,XBOOLE_1:1,28;
end;
theorem Th68:
S-most L~SpStSeq C = LSeg(SW-corner C,SE-corner C)
proof
set X = L~SpStSeq C;
set S3 = LSeg(SE-corner C,SW-corner C), S4 = LSeg(SW-corner C,NW-corner C);
A1: S3 c= S3 \/ S4 by XBOOLE_1:7;
X = (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
(S3 \/ S4) by Th41;
then
A2: S3 \/ S4 c= X by XBOOLE_1:7;
LSeg(SW-corner X, SE-corner X) = LSeg(SW-corner X, SE-corner C) by Th65
.= LSeg(SW-corner C,SE-corner C) by Th64;
hence thesis by A1,A2,XBOOLE_1:1,28;
end;
theorem Th69:
E-most L~SpStSeq C = LSeg(SE-corner C,NE-corner C)
proof
set X = L~SpStSeq C;
set S1 = LSeg(NW-corner C,NE-corner C), S2 = LSeg(NE-corner C,SE-corner C);
A1: S2 c= S1 \/ S2 by XBOOLE_1:7;
X = (S1 \/ S2) \/ (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,
NW-corner C)) by Th41;
then
A2: S1 \/ S2 c= X by XBOOLE_1:7;
LSeg(SE-corner X, NE-corner X) = LSeg(SE-corner X, NE-corner C) by Th63
.= LSeg(SE-corner C,NE-corner C) by Th65;
hence thesis by A1,A2,XBOOLE_1:1,28;
end;
theorem Th70:
proj2.:LSeg(SW-corner C,NW-corner C) = [.S-bound C,N-bound C.]
proof
A1: (NW-corner C)`2 = N-bound C by EUCLID:52;
(SW-corner C)`2 = S-bound C by EUCLID:52;
hence thesis by A1,Th22,Th53;
end;
theorem Th71:
proj1.:LSeg(NW-corner C,NE-corner C) = [.W-bound C,E-bound C.]
proof
A1: (NE-corner C)`1 = E-bound C by EUCLID:52;
(NW-corner C)`1 = W-bound C by EUCLID:52;
hence thesis by A1,Th21,Th52;
end;
theorem Th72:
proj2.:LSeg(NE-corner C,SE-corner C) = [.S-bound C,N-bound C.]
proof
A1: (SE-corner C)`2 = S-bound C by EUCLID:52;
(NE-corner C)`2 = N-bound C by EUCLID:52;
hence thesis by A1,Th22,Th53;
end;
theorem Th73:
proj1.:LSeg(SE-corner C,SW-corner C) = [.W-bound C,E-bound C.]
proof
A1: (SW-corner C)`1 = W-bound C by EUCLID:52;
(SE-corner C)`1 = E-bound C by EUCLID:52;
hence thesis by A1,Th21,Th52;
end;
theorem Th74:
W-min L~SpStSeq C = SW-corner C
proof
set X = L~SpStSeq C, S = W-most X;
A1: S = LSeg(SW-corner C,NW-corner C) by Th66;
A2: S-bound C <= N-bound C by Th22;
lower_bound (proj2|S) = lower_bound rng(proj2|S) by RELSET_1:22
.= lower_bound(proj2.:S) by RELAT_1:115
.= lower_bound [.S-bound C,N-bound C.] by A1,Th70
.= S-bound C by A2,JORDAN5A:19;
hence thesis by Th58;
end;
theorem Th75:
W-max L~SpStSeq C = NW-corner C
proof
set X = L~SpStSeq C, S = W-most X;
A1: S = LSeg(SW-corner C,NW-corner C) by Th66;
A2: S-bound C <= N-bound C by Th22;
upper_bound (proj2|S) = upper_bound rng(proj2|S) by RELSET_1:22
.= upper_bound(proj2.:S) by RELAT_1:115
.= upper_bound [.S-bound C,N-bound C.] by A1,Th70
.= N-bound C by A2,JORDAN5A:19;
hence thesis by Th58;
end;
theorem Th76:
N-min L~SpStSeq C = NW-corner C
proof
set X = L~SpStSeq C, S = N-most X;
A1: S = LSeg(NW-corner C,NE-corner C) by Th67;
A2: W-bound C <= E-bound C by Th21;
lower_bound (proj1|S) = lower_bound rng(proj1|S) by RELSET_1:22
.= lower_bound(proj1.:S) by RELAT_1:115
.= lower_bound [.W-bound C,E-bound C.] by A1,Th71
.= W-bound C by A2,JORDAN5A:19;
hence thesis by Th60;
end;
theorem Th77:
N-max L~SpStSeq C = NE-corner C
proof
set X = L~SpStSeq C, S = N-most X;
A1: S = LSeg(NW-corner C,NE-corner C) by Th67;
A2: W-bound C <= E-bound C by Th21;
upper_bound (proj1|S) = upper_bound rng(proj1|S) by RELSET_1:22
.= upper_bound(proj1.:S) by RELAT_1:115
.= upper_bound [.W-bound C,E-bound C.] by A1,Th71
.= E-bound C by A2,JORDAN5A:19;
hence thesis by Th60;
end;
theorem Th78:
E-min L~SpStSeq C = SE-corner C
proof
set X = L~SpStSeq C, S = E-most X;
A1: S = LSeg(SE-corner C,NE-corner C) by Th69;
A2: S-bound C <= N-bound C by Th22;
lower_bound (proj2|S) = lower_bound rng(proj2|S) by RELSET_1:22
.= lower_bound(proj2.:S) by RELAT_1:115
.= lower_bound [.S-bound C,N-bound C.] by A1,Th72
.= S-bound C by A2,JORDAN5A:19;
hence thesis by Th61;
end;
theorem Th79:
E-max L~SpStSeq C = NE-corner C
proof
set X = L~SpStSeq C, S = E-most X;
A1: S = LSeg(SE-corner C,NE-corner C) by Th69;
A2: S-bound C <= N-bound C by Th22;
upper_bound (proj2|S) = upper_bound rng(proj2|S) by RELSET_1:22
.= upper_bound(proj2.:S) by RELAT_1:115
.= upper_bound [.S-bound C,N-bound C.] by A1,Th72
.= N-bound C by A2,JORDAN5A:19;
hence thesis by Th61;
end;
theorem Th80:
S-min L~SpStSeq C = SW-corner C
proof
set X = L~SpStSeq C, S = S-most X;
A1: S = LSeg(SW-corner C,SE-corner C) by Th68;
A2: W-bound C <= E-bound C by Th21;
lower_bound (proj1|S) = lower_bound rng(proj1|S) by RELSET_1:22
.= lower_bound(proj1.:S) by RELAT_1:115
.= lower_bound [.W-bound C,E-bound C.] by A1,Th73
.= W-bound C by A2,JORDAN5A:19;
hence thesis by Th59;
end;
theorem Th81:
S-max L~SpStSeq C = SE-corner C
proof
set X = L~SpStSeq C, S = S-most X;
A1: S = LSeg(SW-corner C,SE-corner C) by Th68;
A2: W-bound C <= E-bound C by Th21;
upper_bound (proj1|S) = upper_bound rng(proj1|S) by RELSET_1:22
.= upper_bound(proj1.:S) by RELAT_1:115
.= upper_bound [.W-bound C,E-bound C.] by A1,Th73
.= E-bound C by A2,JORDAN5A:19;
hence thesis by Th59;
end;
begin :: rectangular
definition
let f be FinSequence of TOP-REAL 2;
attr f is rectangular means
:Def2:
ex D st f = SpStSeq D;
end;
registration
let D;
cluster SpStSeq D -> rectangular;
coherence;
end;
registration
cluster rectangular for FinSequence of TOP-REAL 2;
existence
proof
set D = the non vertical non horizontal non empty compact Subset of TOP-REAL 2;
take SpStSeq D, D;
thus thesis;
end;
end;
reserve s for rectangular FinSequence of TOP-REAL 2;
theorem
len s = 5
proof
ex D st s = SpStSeq D by Def2;
hence thesis by Th40;
end;
registration
cluster rectangular -> non constant for FinSequence of TOP-REAL 2;
coherence;
end;
registration
cluster rectangular -> standard special unfolded circular s.c.c. for
non empty
FinSequence of TOP-REAL 2;
coherence;
end;
:: Special points of L~f, f - rectangular
theorem
s/.1 = N-min L~s & s/.1 = W-max L~s
proof
consider D such that
A1: s = SpStSeq D by Def2;
A2: s/.1 = NW-corner D by A1,Th35;
hence s/.1 = N-min L~s by A1,Th76;
thus thesis by A1,A2,Th75;
end;
theorem
s/.2 = N-max L~s & s/.2 = E-max L~s
proof
consider D such that
A1: s = SpStSeq D by Def2;
A2: s/.2 = NE-corner D by A1,Th36;
hence s/.2 = N-max L~s by A1,Th77;
thus thesis by A1,A2,Th79;
end;
theorem
s/.3 = S-max L~s & s/.3 = E-min L~s
proof
consider D such that
A1: s = SpStSeq D by Def2;
A2: s/.3 = SE-corner D by A1,Th37;
hence s/.3 = S-max L~s by A1,Th81;
thus thesis by A1,A2,Th78;
end;
theorem
s/.4 = S-min L~s & s/.4 = W-min L~s
proof
consider D such that
A1: s = SpStSeq D by Def2;
A2: s/.4 = SW-corner D by A1,Th38;
hence s/.4 = S-min L~s by A1,Th80;
thus thesis by A1,A2,Th74;
end;
begin :: Jordan
theorem Th87:
r1 < r2 & s1 < s2 implies [.r1,r2,s1,s2.] is Jordan
proof
assume that
A1: r1 < r2 and
A2: s1 < s2;
[.r1,r2,s1,s2.] = { p: p`1 = r1 & p`2 <= s2 & p`2 >= s1 or p`1 <= r2 & p
`1 >= r1 & p`2 = s2 or p`1 <= r2 & p`1 >= r1 & p`2 = s1 or p`1 = r2 & p`2 <= s2
& p`2 >= s1} by A1,A2,SPPOL_2:54;
hence thesis by A1,A2,JORDAN1:43;
end;
registration
let f be rectangular FinSequence of TOP-REAL 2;
cluster L~f -> Jordan;
coherence
proof
consider D such that
A1: f = SpStSeq D by Def2;
A2: W-bound D < E-bound D by Th31;
A3: S-bound D < N-bound D by Th32;
L~f = [.W-bound D,E-bound D,S-bound D,N-bound D.] by A1,Th42;
hence thesis by A2,A3,Th87;
end;
end;
definition
let S be Subset of TOP-REAL 2;
redefine attr S is Jordan means :: redefines Jordan (JORDAN1, definition)
:Def3:
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`;
compatibility
proof
hereby
assume
A1: S is Jordan;
hence S` <> {};
consider A1,A2 being Subset of TOP-REAL 2 such that
A2: S` = A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1) \ A1 = (Cl A2) \ A2 and
A5: for C1,C2 being Subset of (TOP-REAL 2)|S` st C1 = A1 & C2 = A2
holds C1 is a_component & C2 is a_component by A1;
A6: A2 /\ S` = A2 by A2,XBOOLE_1:21;
A1 /\ S` = A1 by A2,XBOOLE_1:21;
then reconsider C1 = A1,C2 = A2 as Subset of (TOP-REAL 2)|S` by A6,
TOPS_2:29;
C2 = A2;
then
A7: C1 is a_component by A5;
take A1,A2;
thus S` = A1 \/ A2 by A2;
thus A1 misses A2 by A3;
thus (Cl A1) \ A1 = (Cl A2) \ A2 by A4;
C1 = A1;
then C2 is a_component by A5;
hence A1 is_a_component_of S` & A2 is_a_component_of S` by A7,
CONNSP_1:def 6;
end;
assume
A8: S` <> {};
given A1,A2 being Subset of TOP-REAL 2 such that
A9: S` = A1 \/ A2 and
A10: A1 misses A2 and
A11: (Cl A1) \ A1 = (Cl A2) \ A2 and
A12: A1 is_a_component_of S` and
A13: A2 is_a_component_of S`;
reconsider a1=A1,a2=A2 as Subset of TOP-REAL 2;
A14: ex B being Subset of (TOP-REAL 2)|S` st B = a2 & B is a_component
by A13,CONNSP_1:def 6;
thus S`<> {} by A8;
take a1,a2;
thus S` = a1 \/ a2 by A9;
thus a1 /\ a2 = {} by A10;
thus (Cl a1) \ a1 = (Cl a2) \ a2 by A11;
ex B being Subset of (TOP-REAL 2)|S` st B = a1 & B is a_component
by A12,CONNSP_1:def 6;
hence thesis by A14;
end;
end;
theorem Th88:
for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp
f misses RightComp f
proof
let f be rectangular FinSequence of TOP-REAL 2;
A1: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
A2: RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
A3: (L~f)`=LeftComp f \/ RightComp f by GOBRD12:10;
consider A1,A2 being Subset of TOP-REAL 2 such that
A4: (L~f)` = A1 \/ A2 and
A5: A1 misses A2 and
(Cl A1) \ A1 = (Cl A2) \ A2 and
A6: A1 is_a_component_of (L~f)` and
A7: A2 is_a_component_of (L~f)` by Def3;
(L~f)`<> {} by Def3;
then { LeftComp f, RightComp f } = { A1,A2 } by A4,A6,A7,A1,A2,A3,Th7;
then LeftComp f = A1 & RightComp f = A2 or LeftComp f = A2 & RightComp f =
A1 by ZFMISC_1:6;
hence thesis by A5;
end;
registration
let f be non constant standard special_circular_sequence;
cluster LeftComp f -> non empty;
coherence
proof
A1: Int left_cell(f,1) c= LeftComp f by GOBOARD9:def 1;
1+1 <= len f by GOBOARD7:34,XXREAL_0:2;
hence thesis by A1,GOBOARD9:15,XBOOLE_1:3;
end;
cluster RightComp f -> non empty;
coherence
proof
A2: Int right_cell(f,1) c= RightComp f by GOBOARD9:def 2;
1+1 <= len f by GOBOARD7:34,XXREAL_0:2;
hence thesis by A2,GOBOARD9:16,XBOOLE_1:3;
end;
end;
theorem
for f being rectangular FinSequence of TOP-REAL 2 holds LeftComp f <>
RightComp f
proof
let f be rectangular FinSequence of TOP-REAL 2;
LeftComp f misses RightComp f by Th88;
hence thesis;
end;