:: Extremal Properties of Vertices on Special Polygons I
:: by Yatsuka Nakamura and Czes\law Byli\'nski
::
:: Received May 11, 1994
:: Copyright (c) 1994-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, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FINSEQ_1,
XBOOLE_0, RELAT_1, FINSET_1, TARSKI, COMPLEX1, REAL_1, PRE_TOPC, EUCLID,
METRIC_1, FUNCT_1, RCOMP_1, RLTOPSP1, CARD_1, SEQ_4, XXREAL_2, PCOMPS_1,
STRUCT_0, SUPINF_2, TEX_2, COMPTS_1, TOPREAL1, BORSUK_1, TOPS_2,
ORDINAL2, MCART_1, ZFMISC_1, PARTFUN1, SETFAM_1, SPPOL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0,
XXREAL_2, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, SEQ_4,
RELAT_1, FUNCT_1,
BINOP_1, PARTFUN1, PRE_TOPC, BORSUK_1, FINSET_1, FINSEQ_1, FINSEQ_4,
DOMAIN_1, STRUCT_0, METRIC_1, PCOMPS_1, TOPS_2, ZFMISC_1, COMPTS_1,
RLVECT_1, RLTOPSP1, EUCLID, TEX_2, TOPREAL1;
constructors SETFAM_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_4, FINSEQ_4,
TOPS_2, COMPTS_1, REALSET2, TDLAT_3, TEX_2, MONOID_0, TOPMETR, TOPREAL1,
PCOMPS_1, XXREAL_2, FUNCSDOM, CONVEX1, BINOP_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0,
INT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TEX_2, EUCLID, TOPREAL1,
FINSET_1, VALUED_0, RLTOPSP1, FUNCT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPREAL1, XXREAL_2;
equalities TOPREAL1, EUCLID, COMPTS_1, SUBSET_1, STRUCT_0, ALGSTR_0, RLTOPSP1;
expansions TARSKI, TOPREAL1, COMPTS_1;
theorems TARSKI, NAT_1, INT_1, ABSVALUE, SUBSET_1, FINSET_1, FINSEQ_1,
PRE_TOPC, METRIC_1, TOPS_1, TOPS_2, SEQ_4, EUCLID, TOPMETR, TOPREAL1,
TOPREAL3, COMPTS_1, TEX_2, FINSEQ_3, ZFMISC_1, HEINE, TDLAT_3, PARTFUN2,
XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0,
RLTOPSP1, RLVECT_1, ORDINAL1;
schemes FRAENKEL;
begin :: Preliminaires
reserve n,i,k,m for Nat;
theorem
for n,k being Nat holds n < k implies n <= k-1
proof
let n,k be Nat;
assume n<k;
then n+1<=k by NAT_1:13;
then n+1-1<=k-1 by XREAL_1:9;
hence thesis;
end;
theorem
1 <= k-m & k-m <= n implies k-m in Seg n & k-m is Element of NAT
proof
assume that
A1: 1<=k-m and
A2: k-m<=n;
k-m is Element of NAT by A1,INT_1:3;
hence thesis by A1,A2,FINSEQ_1:1;
end;
scheme
FinSeqFam { f() -> finite NAT-defined Relation,
F(Relation,Nat) -> object,
P[Nat] }:
{ F(f(),i): i in dom f() & P[i] } is finite
proof
deffunc U(Nat) = F(f(),$1);
set F = {U(i): i in dom f() & P[i]},
F9 = {U(i) where i is Element of NAT: i in dom f()};
A1: F c= F9
proof
let x be object;
assume x in F;
then consider i being Nat such that
A3: x = F(f(),i) & i in dom f() & P[i];
i in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
A2: dom f() is finite;
F9 is finite from FRAENKEL:sch 21(A2);
hence thesis by A1;
end;
scheme
FinSeqFam9 { f() -> FinSequence,
F(FinSequence,Nat) -> object,
P[Nat]}:
{ F(f(),i): 1 <= i & i <= len f() & P[i] } is finite
proof
deffunc U(Nat) = F(f(),$1);
set F = {U(i): 1<=i & i<=len f() & P[i]},
F9 = {U(i) where i is Element of NAT: i in dom f()};
A1: F c= F9
proof
let x be object;
assume x in F;
then consider i being Nat such that
A2: x = F(f(),i) and
A3: 1<=i & i<=len f() and
P[i];
i in dom f() by A3,FINSEQ_3:25;
hence thesis by A2;
end;
A4: dom f() is finite;
F9 is finite from FRAENKEL:sch 21(A4);
hence thesis by A1;
end;
theorem Th3:
for x1,x2,x3 being Element of REAL n holds
|.x1 - x2.|- |.x2 - x3.| <= |.x1 - x3.|
proof
let x1,x2,x3 be Element of REAL n;
|.x1 - x2.|<= |.x1 - x3.|+|.x3 - x2.| by EUCLID:19;
then |.x1 - x2.|<= |.x1 - x3.|+|.x2 - x3.| by EUCLID:18;
then |.x1 - x2.|- |.x2 - x3.|<= |.x1 - x3.|+|.x2 - x3.|- |.x2 - x3.|
by XREAL_1:9;
hence thesis;
end;
theorem
for x1,x2,x3 being Element of REAL n holds
|.x2 - x1.|- |.x2 - x3.| <= |.x3 - x1.|
proof
let x1,x2,x3 be Element of REAL n;
|.x2 - x1.|=|.x1 - x2.| by EUCLID:18;
then |.x2 - x1.|- |.x2 - x3.| <= |.x1 - x3.| by Th3;
hence thesis by EUCLID:18;
end;
begin
:: Extremal properties of endpoints of line segments in n-dimensional
:: Euclidean space
reserve r,r1,r2,s,s1,s2 for Real;
reserve p,p1,p2,q1,q2 for Point of TOP-REAL n;
theorem Th5:
for u1,u2 being Point of Euclid n, v1,v2 being Element of REAL n
st v1=u1 & v2=u2 holds dist(u1,u2) = |.v1-v2.|
proof
let u1,u2 be Point of Euclid n, v1,v2 be Element of REAL n;
assume v1=u1 & v2=u2;
hence dist(u1,u2) = (Pitag_dist n).(v1,v2) by METRIC_1:def 1
.= |.v1-v2.| by EUCLID:def 6;
end;
theorem
for P being non empty Subset of TOP-REAL n st P is closed & P c= LSeg(
p1,p2) ex s st (1-s)*p1+s*p2 in P & for r st 0<=r & r<=1 & (1-r)*p1+r*p2 in P
holds s<=r
proof
let P be non empty Subset of TOP-REAL n;
set W = {r:0<=r & r<=1 & (1-r)*p1+r*p2 in P};
W c= REAL
proof
let x be object;
assume x in W;
then ex r st r=x & 0<=r & r<=1 & (1-r)*p1+r*p2 in P;
hence thesis by XREAL_0:def 1;
end;
then reconsider W as Subset of REAL;
assume that
A1: P is closed and
A2: P c= LSeg(p1,p2);
take r2 = lower_bound W;
A3: W is bounded_below
proof
take 0;
let r be ExtReal;
assume r in W;
then ex s st s = r & 0<=s & s<=1 & (1-s)*p1+s*p2 in P;
hence thesis;
end;
hereby
set p=(1-r2)*p1+r2*p2;
reconsider u = p as Point of Euclid n by EUCLID:22;
A4: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider Q = P` as Subset of TopSpaceMetr(Euclid n);
P` is open by A1,TOPS_1:3;
then
A5: Q is open by A4,PRE_TOPC:30;
A6: ex r0 being Real st r0 in W
proof
consider v being Element of TOP-REAL n such that
A7: v in P by SUBSET_1:4;
v in LSeg(p1,p2) by A2,A7;
then consider s such that
A8: v = (1-s)*p1+s*p2 & 0<=s & s<=1;
s in {r:0<=r & r<=1 & (1-r)*p1+r*p2 in P} by A7,A8;
hence thesis;
end;
assume
A9: not p in P;
then p in (the carrier of TOP-REAL n)\P by XBOOLE_0:def 5;
then consider r0 being Real such that
A10: r0>0 and
A11: Ball(u,r0) c= Q by A5,TOPMETR:15;
per cases;
suppose
A12: p1<>p2;
reconsider v2 = p2 as Element of REAL n by EUCLID:22;
reconsider v1 = p1 as Element of REAL n by EUCLID:22;
A13: |.v2-v1.|>0 by A12,EUCLID:17;
then r0/|.v2-v1.|>0 by A10,XREAL_1:139;
then consider r4 being Real such that
A14: r4 in W and
A15: r4<r2+r0/|.v2-v1.| by A3,A6,SEQ_4:def 2;
reconsider r4 as Real;
r4+0<r2+r0/|.v2-v1.| by A15;
then
A16: r4-r2<r0/|.v2-v1.|-0 by XREAL_1:21;
set p3=(1-r4)*p1+r4*p2;
reconsider u3 = p3 as Point of Euclid n by EUCLID:22;
reconsider v3=p3, v4=p as Element of REAL n by EUCLID:22;
A17: p3-p = (1-r4)*p1+r4*p2+ (-((1-r2)*p1)-(r2*p2)) by RLVECT_1:30
.= (1-r4)*p1+r4*p2+ -((1-r2)*p1)+-(r2*p2) by RLVECT_1:def 3
.= r4*p2+((1-r4)*p1+ -((1-r2)*p1))+-(r2*p2) by RLVECT_1:def 3
.= ((1-r4)*p1+ -((1-r2)*p1))+r4*p2+(-r2)*p2 by RLVECT_1:79
.= ((1-r4)*p1+ (-(1-r2))*p1)+r4*p2+(-r2)*p2 by RLVECT_1:79
.= ((1-r4)*p1+ (-(1-r2))*p1)+(r4*p2+(-r2)*p2) by RLVECT_1:def 3
.= ((1-r4)*p1+ (-(1-r2))*p1)+(r4+(-r2))*p2 by RLVECT_1:def 6
.= ((1-r4)+ -(1-r2))*p1+(r4-r2)*p2 by RLVECT_1:def 6
.= (-(r4-r2))*p1+(r4-r2)*p2
.= (r4-r2)*p2-((r4-r2)*p1) by RLVECT_1:79
.= (r4-r2)*(p2 -p1) by RLVECT_1:34
.= (r4-r2)*(v2 -v1);
r2<=r4 by A3,A14,SEQ_4:def 2;
then
A18: r4-r2>=0 by XREAL_1:48;
dist(u3,u) = |.v3-v4.| by Th5
.= |.p3-p.|
.=|.(r4-r2)*(v2-v1).| by A17
.=|.r4-r2.|*|.v2-v1.| by EUCLID:11
.=(r4-r2)*|.v2-v1.| by A18,ABSVALUE:def 1;
then dist(u3,u)<(r0/|.v2-v1.|)*|.v2-v1.| by A13,A16,XREAL_1:68;
then dist(u,u3)<r0 by A13,XCMPLX_1:87;
then u3 in {u0 where u0 is Point of Euclid n: dist(u,u0)<r0};
then
A19: u3 in Ball(u,r0) by METRIC_1:17;
ex r st r=r4 & 0<=r & r<=1 & (1-r)*p1+r*p2 in P by A14;
hence contradiction by A11,A19,XBOOLE_0:def 5;
end;
suppose
A20: p1=p2;
then
A21: LSeg(p1,p2)={p1} by RLTOPSP1:70;
A22: ex q1 being Point of TOP-REAL n st q1 in P by SUBSET_1:4;
p = (1-r2+r2)*p1 by A20,RLVECT_1:def 6
.= p1 by RLVECT_1:def 8;
hence contradiction by A2,A9,A21,A22,TARSKI:def 1;
end;
end;
let r;
assume 0<=r & r<=1 & (1-r)*p1+r*p2 in P;
then r in W;
hence thesis by A3,SEQ_4:def 2;
end;
theorem Th7:
for p1,p2,q1,q2 st LSeg(q1,q2) c= LSeg(p1,p2) & p1 in LSeg(q1,q2)
holds p1 = q1 or p1 = q2
proof
let p1,p2,q1,q2;
assume
A1: LSeg(q1,q2) c= LSeg(p1,p2);
q2 in LSeg(q1,q2) by RLTOPSP1:68;
then q2 in LSeg(p1,p2) by A1;
then consider s2 such that
A2: q2=(1-s2)*p1+s2*p2 and
A3: 0<=s2 and
s2<=1;
assume p1 in LSeg(q1,q2);
then consider r1 such that
A4: p1=(1-r1)*q1+r1*q2 and
A5: 0<=r1 & r1<=1;
A6: q1 in LSeg(q1,q2) by RLTOPSP1:68;
then q1 in LSeg(p1,p2) by A1;
then consider s1 such that
A7: q1=(1-s1)*p1+s1*p2 and
A8: 0<=s1 and
s1<=1;
p1 = (1-r1)*((1-s1)*p1+s1*p2)+(r1*((1-s2)*p1)+r1*(s2*p2)) by A4,A7,A2,
RLVECT_1:def 5
.= (1-r1)*((1-s1)*p1)+(1-r1)*(s1*p2)+(r1*((1-s2)*p1)+r1*(s2*p2)) by
RLVECT_1:def 5
.= (1-r1)*((1-s1)*p1)+(1-r1)*(s1*p2)+r1*((1-s2)*p1)+r1*(s2*p2) by
RLVECT_1:def 3
.=((1-r1)*(1-s1))*p1+(1-r1)*(s1*p2)+r1*((1-s2)*p1)+r1*(s2*p2) by
RLVECT_1:def 7
.=((1-r1)*(1-s1))*p1+(1-r1)*s1*p2+r1*((1-s2)*p1)+r1*(s2*p2) by
RLVECT_1:def 7
.=((1-r1)*(1-s1))*p1+(1-r1)*s1*p2+r1*(1-s2)*p1+r1*(s2*p2) by RLVECT_1:def 7
.=((1-r1)*(1-s1))*p1+(1-r1)*s1*p2+r1*(1-s2)*p1+r1*s2*p2 by RLVECT_1:def 7
.=(r1*s2)*p2 + ((1-r1)*s1*p2+(1-r1)*(1-s1)*p1)+r1*(1-s2)*p1 by
RLVECT_1:def 3
.=(r1*s2)*p2 + (1-r1)*s1*p2+(1-r1)*(1-s1)*p1+r1*(1-s2)*p1 by RLVECT_1:def 3
.=((r1*s2) + (1-r1)*s1)*p2+(1-r1)*(1-s1)*p1+r1*(1-s2)*p1 by RLVECT_1:def 6
.=((r1*s2) + (1-r1)*s1)*p2+((1-r1)*(1-s1)*p1+r1*(1-s2)*p1) by
RLVECT_1:def 3
.=(r1*s2+(1-r1)*s1)*p2+((1-r1)*(1-s1)+r1*(1-s2))*p1 by RLVECT_1:def 6;
then 0.TOP-REAL n = (r1*s2+(1-r1)*s1)*p2+((1-r1)*(1-s1)+r1*(1-s2))*p1-p1 by
RLVECT_1:5
.= (r1*s2+(1-r1)*s1)*p2+(((1-r1)*(1-s1)+r1*(1-s2))*p1-p1) by RLVECT_1:def 3
.= (r1*s2+(1-r1)*s1)*p2+(((1-r1)*(1-s1)+r1*(1-s2))*p1-1*p1) by RLVECT_1:def
8
.= (((1-r1)*(1-s1)+r1*(1-s2))-1)*p1+((r1*s2+(1-r1)*s1)*p2) by RLVECT_1:35
.= (((1-r1)*(1-s1)+r1*(1-s2))-1)*p1--((r1*s2+(1-r1)*s1)*p2);
then (((1-r1)*(1-s1)+r1*(1-s2))-1)*p1 = -((r1*s2+(1-r1)*s1)*p2) by
RLVECT_1:21;
then (((1-r1)*(1-s1)+r1*(1-s2))-1)*p1 = (-(r1*s2+(1-r1)*s1))*p2 by
RLVECT_1:79;
then
A9: -(r1*s2+(1-r1)*s1)=-0 or p1=p2 by RLVECT_1:36;
per cases by A9;
suppose
A10: r1*s2+(1-r1)*s1=0;
now
per cases by A5,A8,A3,A10,XREAL_1:170;
suppose
r1=0 & s1=0;
then p1 = 1*q1+0.TOP-REAL n by A4,RLVECT_1:10
.= q1+0.TOP-REAL n by RLVECT_1:def 8
.= q1 by RLVECT_1:4;
hence thesis;
end;
suppose
r1=1 & s2=0;
then p1 = 0.TOP-REAL n +1*q2 by A4,RLVECT_1:10
.= 1*q2 by RLVECT_1:4
.= q2 by RLVECT_1:def 8;
hence thesis;
end;
suppose
s2=0 & s1=0;
then q1 = 1*p1+0.TOP-REAL n by A7,RLVECT_1:10
.= p1+0.TOP-REAL n by RLVECT_1:def 8
.= p1 by RLVECT_1:4;
hence thesis;
end;
end;
hence thesis;
end;
suppose
p1=p2;
then LSeg(q1,q2) c={p1} by A1,RLTOPSP1:70;
hence thesis by A6,TARSKI:def 1;
end;
end;
theorem
for p1,p2,q1,q2 st LSeg(p1,p2) = LSeg(q1,q2) holds
p1 = q1 & p2 = q2 or p1 = q2 & p2 = q1
proof
let p1,p2,q1,q2;
A1: q1 in LSeg(q1,q2) by RLTOPSP1:68;
A2: q2 in LSeg(q1,q2) by RLTOPSP1:68;
assume
A3: LSeg(p1,p2)=LSeg(q1,q2);
per cases by A3,Th7,RLTOPSP1:68;
suppose
A4: p1=q1 & p2=q1;
then LSeg(p1,p2) = {q1} by RLTOPSP1:70;
hence thesis by A3,A2,A4,TARSKI:def 1;
end;
suppose
A5: p1=q2 & p2=q2;
then LSeg(p1,p2) = {q2} by RLTOPSP1:70;
hence thesis by A3,A1,A5,TARSKI:def 1;
end;
suppose
p1=q1 & p2=q2 or p1=q2 & p2=q1;
hence thesis;
end;
end;
registration
let n,p1,p2;
cluster LSeg(p1,p2) -> compact;
coherence
proof
set P = LSeg(p1,p2), T = (TOP-REAL n)|P;
now
per cases;
suppose
p1 = p2;
then P = {p1} by RLTOPSP1:70;
then
A1: { p1 } = [#](T) by PRE_TOPC:def 5
.= the carrier of T;
then Sspace(p1) = T by TEX_2:def 2;
then T = 1TopSp {p1} by A1,TDLAT_3:def 1;
hence T is compact;
end;
suppose
p1 <> p2;
then LSeg(p1,p2) is_an_arc_of p1,p2 by TOPREAL1:9;
then consider f being Function of I[01], T such that
A2: f is being_homeomorphism and
f.0=p1 and
f.1=p2;
A3: I[01] is compact by HEINE:4,TOPMETR:20;
f is continuous & rng f = [#](T) by A2,TOPS_2:def 5;
hence T is compact by A3,COMPTS_1:14;
end;
end;
hence thesis by COMPTS_1:3;
end;
cluster LSeg(p1,p2) -> closed;
coherence by COMPTS_1:7;
end;
definition
let n,p;
let P be Subset of TOP-REAL n;
pred p is_extremal_in P means
p in P & for p1,p2 st p in LSeg(p1,p2) & LSeg(p1,p2) c= P holds p=p1 or p=p2;
end;
theorem
for P,Q being Subset of TOP-REAL n st p is_extremal_in P & Q c= P & p in Q
holds p is_extremal_in Q
proof
let P,Q be Subset of TOP-REAL n;
assume that
A1: p is_extremal_in P and
A2: Q c= P;
assume p in Q;
hence p in Q;
let p1,p2;
assume
A3: p in LSeg(p1,p2);
assume LSeg(p1,p2) c= Q;
then LSeg(p1,p2) c= P by A2;
hence thesis by A1,A3;
end;
theorem
p is_extremal_in {p}
proof
thus p in {p} by TARSKI:def 1;
let p1,p2;
assume that
p in LSeg(p1,p2) and
A1: LSeg(p1,p2) c= {p};
p2 in LSeg(p1,p2) by RLTOPSP1:68;
hence thesis by A1,TARSKI:def 1;
end;
theorem Th11:
p1 is_extremal_in LSeg(p1,p2) by RLTOPSP1:68,Th7;
theorem
p2 is_extremal_in LSeg(p1,p2) by Th11;
theorem
p is_extremal_in LSeg(p1,p2) implies p = p1 or p = p2;
begin
:: Extremal properties of vertices of special polygons
reserve P,Q for Subset of TOP-REAL 2,
f,f1,f2 for FinSequence of the carrier of TOP-REAL 2,
p,p1,p2,p3,q,q3 for Point of TOP-REAL 2;
theorem Th14:
for p1,p2 st p1`1<>p2`1 & p1`2<>p2`2 ex p st p in LSeg(p1,p2) &
p`1<>p1`1 & p`1<>p2`1 & p`2<>p1`2 & p`2<>p2`2
proof
let p1,p2;
assume that
A1: p1`1<>p2`1 and
A2: p1`2<>p2`2;
take p = (1/2)*(p1+p2);
A3: p = (1-1/2)*p1+(1/2)*p2 by RLVECT_1:def 5;
hence p in LSeg(p1,p2);
hereby
assume
A4: p`1=p1`1;
p`1 = ((1-1/2)*p1)`1+((1/2)*p2)`1 by A3,TOPREAL3:2
.= (1-1/2)*(p1`1)+((1/2)*p2)`1 by TOPREAL3:4
.= (1-1/2)*(p`1)+(1/2)*(p2`1) by A4,TOPREAL3:4;
hence contradiction by A1,A4;
end;
hereby
assume
A5: p`1=p2`1;
p`1 = ((1-1/2)*p1)`1+((1/2)*p2)`1 by A3,TOPREAL3:2
.= (1-1/2)*(p1`1)+((1/2)*p2)`1 by TOPREAL3:4
.= (1-1/2)*(p1`1)+(1/2)*(p`1) by A5,TOPREAL3:4;
hence contradiction by A1,A5;
end;
hereby
assume
A6: p`2=p1`2;
p`2 = ((1-1/2)*p1)`2+((1/2)*p2)`2 by A3,TOPREAL3:2
.= (1-1/2)*(p1`2)+((1/2)*p2)`2 by TOPREAL3:4
.= (1-1/2)*(p`2)+(1/2)*(p2`2) by A6,TOPREAL3:4;
hence contradiction by A2,A6;
end;
hereby
assume
A7: p`2=p2`2;
p`2 = ((1-1/2)*p1)`2+((1/2)*p2)`2 by A3,TOPREAL3:2
.= (1-1/2)*(p1`2)+((1/2)*p2)`2 by TOPREAL3:4
.= (1-1/2)*(p1`2)+(1/2)*(p`2) by A7,TOPREAL3:4;
hence contradiction by A2,A7;
end;
end;
definition
let P;
attr P is horizontal means
for p,q st p in P & q in P holds p`2=q`2;
attr P is vertical means
for p,q st p in P & q in P holds p`1=q`1;
end;
Lm1: P is non trivial & P is horizontal implies P is non vertical
proof
assume that
A1: P is non trivial and
A2: ( for p,q st p in P & q in P holds p`2=q`2)& for p,q st p in P & q
in P holds p`1=q`1;
consider p,q such that
A3: p in P & q in P and
A4: p <> q by A1,SUBSET_1:45;
p`2=q`2 & p`1=q`1 by A2,A3;
hence contradiction by A4,TOPREAL3:6;
end;
registration
cluster non trivial horizontal -> non vertical for Subset of TOP-REAL 2;
coherence by Lm1;
cluster non trivial vertical -> non horizontal for Subset of TOP-REAL 2;
coherence;
end;
theorem Th15:
p`2 = q`2 iff LSeg(p,q) is horizontal
proof
set P = LSeg(p,q);
thus p`2=q`2 implies P is horizontal
proof
assume
A1: p`2=q`2;
let p1,p2;
assume
A2: p1 in P;
assume p2 in P;
then
A3: p`2 <= p2`2 & p2`2 <= p`2 by A1,TOPREAL1:4;
p`2 <= p1`2 & p1`2 <= p`2 by A1,A2,TOPREAL1:4;
then p`2 = p1`2 by XXREAL_0:1;
hence thesis by A3,XXREAL_0:1;
end;
p in P & q in P by RLTOPSP1:68;
hence thesis;
end;
theorem Th16:
p`1 = q`1 iff LSeg(p,q) is vertical
proof
set P = LSeg(p,q);
thus p`1=q`1 implies P is vertical
proof
assume
A1: p`1=q`1;
let p1,p2;
assume
A2: p1 in P;
assume p2 in P;
then
A3: p`1 <= p2`1 & p2`1 <= p`1 by A1,TOPREAL1:3;
p`1 <= p1`1 & p1`1 <= p`1 by A1,A2,TOPREAL1:3;
then p`1 = p1`1 by XXREAL_0:1;
hence thesis by A3,XXREAL_0:1;
end;
p in P & q in P by RLTOPSP1:68;
hence thesis;
end;
theorem
p1 in LSeg(p,q) & p2 in LSeg(p,q) & p1`1<>p2`1 & p1`2=p2`2 implies
LSeg(p,q) is horizontal
proof
assume p1 in LSeg(p,q);
then consider r1 such that
A1: p1 = (1-r1)*p+r1*q and
0<=r1 and
r1<=1;
assume p2 in LSeg(p,q);
then consider r2 such that
A2: p2 = (1-r2)*p+r2*q and
0<=r2 and
r2<=1;
assume that
A3: p1`1 <> p2`1 and
A4: p1`2 = p2`2;
p`2-(r1*(p`2)-r1*(q`2))= (1-r1)*(p`2)+r1*(q`2)
.= (1-r1)*(p`2)+(r1*q)`2 by TOPREAL3:4
.= ((1-r1)*p)`2+(r1*q)`2 by TOPREAL3:4
.= p1`2 by A1,TOPREAL3:2
.= ((1-r2)*p)`2+(r2*q)`2 by A2,A4,TOPREAL3:2
.= (1-r2)*(p`2)+(r2*q)`2 by TOPREAL3:4
.= 1*(p`2)-r2*(p`2)+r2*(q`2) by TOPREAL3:4
.= p`2-(r2*(p`2)-r2*(q`2));
then
A5: (r1-r2)*(p`2)=(r1-r2)*(q`2);
r1-r2<>0 by A1,A2,A3;
then p`2 = q`2 by A5,XCMPLX_1:5;
hence thesis by Th15;
end;
theorem
p1 in LSeg(p,q) & p2 in LSeg(p,q) & p1`2<>p2`2 & p1`1=p2`1 implies
LSeg(p,q) is vertical
proof
assume p1 in LSeg(p,q);
then consider r1 such that
A1: p1 = (1-r1)*p+r1*q and
0<=r1 and
r1<=1;
assume p2 in LSeg(p,q);
then consider r2 such that
A2: p2 = (1-r2)*p+r2*q and
0<=r2 and
r2<=1;
assume that
A3: p1`2 <> p2`2 and
A4: p1`1 = p2`1;
p`1-(r1*(p`1)-r1*(q`1))= (1-r1)*(p`1)+r1*(q`1)
.= (1-r1)*(p`1)+(r1*q)`1 by TOPREAL3:4
.= ((1-r1)*p)`1+(r1*q)`1 by TOPREAL3:4
.= p1`1 by A1,TOPREAL3:2
.= ((1-r2)*p)`1+(r2*q)`1 by A2,A4,TOPREAL3:2
.= (1-r2)*(p`1)+(r2*q)`1 by TOPREAL3:4
.= 1*(p`1)-r2*(p`1)+r2*(q`1) by TOPREAL3:4
.= p`1-(r2*(p`1)-r2*(q`1));
then
A5: (r1-r2)*(p`1)=(r1-r2)*(q`1);
r1-r2<>0 by A1,A2,A3;
then p`1 = q`1 by A5,XCMPLX_1:5;
hence thesis by Th16;
end;
registration
let f,i;
cluster LSeg(f,i) -> closed;
coherence
proof
per cases;
suppose
1<=i & i+1<=len f;
then LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by TOPREAL1:def 3;
hence thesis;
end;
suppose
A1: not (1<=i & i+1<=len f);
{} TOP-REAL 2 is closed;
hence thesis by A1,TOPREAL1:def 3;
end;
end;
end;
theorem Th19:
f is special implies LSeg(f,i) is vertical or LSeg(f,i) is horizontal
proof
assume
A1: for j be Nat st 1 <= j & j+1 <= len f holds (f/.j)`1 = (f/.(j+1))`1
or (f/.j)`2 = (f/.(j+1))`2;
set p1=f/.i, p2=f/.(i+1);
per cases;
suppose
A2: 1 <= i & i+1 <= len f;
A3: p1`2=p2`2 implies LSeg(p1,p2) is horizontal by Th15;
p1`1=p2`1 implies LSeg(p1,p2) is vertical by Th16;
hence thesis by A1,A2,A3,TOPREAL1:def 3;
end;
suppose
not (1<=i & i+1<=len f);
then for p,q st p in LSeg(f,i) & q in LSeg(f,i) holds p`2=q`2
by TOPREAL1:def 3;
hence thesis;
end;
end;
theorem Th20:
f is one-to-one & 1 <= i & i+1 <= len f implies LSeg(f,i) is non trivial
proof
assume
A1: f is one-to-one;
A2: i <> i+1;
assume
A3: 1 <= i & i+1 <= len f;
then i in dom f & i+1 in dom f by SEQ_4:134;
then
A4: f/.i<>f/.(i+1) by A1,A2,PARTFUN2:10;
A5: f/.i in LSeg(f/.i,f/.(i+1)) & f/.(i+1) in LSeg(f/.i,f/.(i+1)) by
RLTOPSP1:68;
LSeg(f/.i,f/.(i+1)) = LSeg(f,i) by A3,TOPREAL1:def 3;
hence thesis by A4,A5,ZFMISC_1:def 10;
end;
theorem
f is one-to-one & 1 <= i & i+1 <= len f & LSeg(f,i) is vertical
implies LSeg(f,i) is non horizontal by Lm1,Th20;
theorem Th22:
for f holds {LSeg(f,i): 1<=i & i<=len f} is finite
proof
defpred X[set] means not contradiction;
deffunc U(FinSequence of TOP-REAL 2, Nat) = LSeg($1,$2);
let f;
set Y = {LSeg(f,i): 1<=i & i<=len f};
set X = {U(f,i): 1<=i & i<=len f & X[i]};
A1: for e being object holds e in X iff e in Y
proof
let e be object;
thus e in X implies e in Y
proof
assume e in X;
then ex i being Nat st e = U(f,i) & 1<=i & i<=len f & X[i];
hence thesis;
end;
assume e in Y;
then ex i being Nat st e = LSeg(f,i) & 1<=i & i<=len f;
hence thesis;
end;
X is finite from FinSeqFam9;
hence thesis by A1,TARSKI:2;
end;
theorem Th23:
for f holds {LSeg(f,i): 1<=i & i+1<=len f}
is finite
proof
let f;
set F = {LSeg(f,i): 1<=i & i+1<=len f},
F9 = {LSeg(f,i): 1<=i & i<=len f};
F c= F9
proof
let x be object;
assume x in F;
then consider i being Nat such that
A1: x = LSeg(f,i) & 1<=i and
A2: i+1<=len f;
i <= i + 1 by NAT_1:11;
then i <= len f by A2,XXREAL_0:2;
hence thesis by A1;
end;
hence thesis by Th22,FINSET_1:1;
end;
Lm2: for f,k holds
{LSeg(f,i) : 1<=i & i+1<=len f & i<>k & i<>k+1} is finite
proof
let f,k;
set F = {LSeg(f,i): 1<=i & i+1<=len f & i<>k & i<>k+1};
set F1 = {LSeg(f,i): 1<=i & i+1<=len f};
F c= F1
proof
let x be object;
assume x in F;
then ex i st LSeg(f,i) = x & 1<=i & i+1<=len f & i<>k & i<>k+1;
hence thesis;
end;
hence thesis by Th23,FINSET_1:1;
end;
theorem
for f holds {LSeg(f,i): 1<=i & i<=len f} is Subset-Family of TOP-REAL 2
proof
let f;
set F = {LSeg(f,i): 1<=i & i<=len f};
F c= bool (REAL 2)
proof
let x be object;
assume x in F;
then ex i st LSeg(f,i)=x & 1<=i & i<=len f;
then x is Subset of REAL 2 by EUCLID:22;
hence thesis;
end;
hence thesis by EUCLID:22;
end;
theorem Th25:
for f holds {LSeg(f,i): 1<=i & i+1<=len f} is Subset-Family of TOP-REAL 2
proof
let f;
set F = {LSeg(f,i): 1<=i & i+1<=len f};
F c= bool (REAL 2)
proof
let x be object;
assume x in F;
then ex i st LSeg(f,i)=x & 1<=i & i+1<=len f;
then x is Subset of REAL 2 by EUCLID:22;
hence thesis;
end;
hence thesis by EUCLID:22;
end;
Lm3: for f,k holds {LSeg(f,i): 1<=i & i+1<=len f & i<>k & i<>k+1} is
Subset-Family of TOP-REAL 2
proof
let f,k;
set F = {LSeg(f,i): 1<=i & i+1<=len f & i<>k & i<>k+1};
F c= bool (REAL 2)
proof
let x be object;
assume x in F;
then ex i st LSeg(f,i)=x & 1<=i & i+1<=len f & i<>k & i<>k+ 1;
then x is Subset of REAL 2 by EUCLID:22;
hence thesis;
end;
hence thesis by EUCLID:22;
end;
theorem Th26:
for f st Q = union{LSeg(f,i): 1<=i & i+1<=len f} holds Q is closed
proof
let f;
reconsider F = {LSeg(f,i): 1<=i & i+1<=len f} as Subset-Family of TOP-REAL 2
by Th25;
now
let P;
assume P in F;
then ex i st LSeg(f,i)=P & 1<=i & i+1<=len f;
hence P is closed;
end;
then
A1: F is closed by TOPS_2:def 2;
F is finite by Th23;
hence thesis by A1,TOPS_2:21;
end;
registration
let f;
cluster L~f -> closed;
coherence by Th26;
end;
Lm4: for f,Q,k st Q = union{LSeg(f,i):1<=i & i+1<=len f & i<>k & i<>k+1} holds
Q is closed
proof
let f,Q,k;
reconsider F = {LSeg(f,i): 1<=i & i+1<=len f & i<>k & i<>k+1} as
Subset-Family of TOP-REAL 2 by Lm3;
now
let P;
assume P in F;
then ex i st LSeg(f,i)=P & 1<=i & i+1<=len f & i<>k & i<>k+1;
hence P is closed;
end;
then
A1: F is closed by TOPS_2:def 2;
F is finite by Lm2;
hence thesis by A1,TOPS_2:21;
end;
definition
let IT be FinSequence of TOP-REAL 2;
attr IT is alternating means
for i st 1 <= i & i+2 <= len IT holds (
IT/.i)`1 <> (IT/.(i+2))`1 & (IT/.i)`2 <> (IT/.(i+2))`2;
end;
theorem Th27:
f is special alternating & 1 <= i & i+2 <= len f & (f/.i)`1 = (f
/.(i+1))`1 implies (f/.(i+1))`2 = (f/.(i+2))`2
proof
assume that
A1: f is special and
A2: f is alternating & 1 <= i and
A3: i+2 <= len f;
set p2 = f/.(i+1), p3 = f/.(i+2);
1 <= i+1 & i+1+1 = i+(1+1) by NAT_1:11;
then p2`1 = p3`1 or p2`2 = p3`2 by A1,A3;
hence thesis by A2,A3;
end;
theorem Th28:
f is special alternating & 1 <= i & i+2 <= len f & (f/.i)`2 = (f
/.(i+1))`2 implies (f/.(i+1))`1 = (f/.(i+2))`1
proof
assume that
A1: f is special and
A2: f is alternating & 1 <= i and
A3: i+2 <= len f;
set p2 = f/.(i+1), p3 = f/.(i+2);
1 <= i+1 & i+1+1 = i+(1+1) by NAT_1:11;
then p2`1 = p3`1 or p2`2 = p3`2 by A1,A3;
hence thesis by A2,A3;
end;
theorem Th29:
f is special alternating & 1 <= i & i+2 <= len f & p1 = f/.i &
p2 = f/.(i+1) & p3 = f/.(i+2) implies p1`1 = p2`1 & p3`1 <> p2`1 or p1`2 = p2`2
& p3`2 <> p2`2
proof
assume that
A1: f is special and
A2: f is alternating and
A3: 1 <= i and
A4: i+2 <= len f and
A5: p1 = f/.i and
A6: p2 = f/.(i+1) and
A7: p3 = f/.(i+2);
i+1 <= i+2 by XREAL_1:6;
then i+1 <= len f by A4,XXREAL_0:2;
then p1`1 = p2`1 or p1`2 = p2`2 by A1,A3,A5,A6;
hence thesis by A2,A3,A4,A5,A7;
end;
theorem
f is special alternating & 1 <= i & i+2 <= len f & p1 = f/.i & p2 = f
/.(i+1) & p3 = f/.(i+2) implies p2`1 = p3`1 & p1`1 <> p2`1 or p2`2 = p3`2 & p1
`2 <> p2`2
proof
assume that
A1: f is special and
A2: f is alternating & 1 <= i and
A3: i+2 <= len f and
A4: p1 = f/.i and
A5: p2 = f/.(i+1) and
A6: p3 = f/.(i+2);
1 <= i+1 & i+(1+1) = i+1+1 by NAT_1:11;
then p2`1 = p3`1 or p2`2 = p3`2 by A1,A3,A5,A6;
hence thesis by A2,A3,A4,A6;
end;
Lm5: for f,i,p1,p2 st f is alternating & 1<=i & i+2<=len f & p1=f/.i & p2=f/.(
i+2) ex p st p in LSeg(p1,p2) & p`1<>p1`1 & p`1<>p2`1 & p`2<>p1`2 & p`2<>p2`2
proof
let f,i,p1,p2;
assume f is alternating & 1<=i & i+2<=len f & p1=f/.i & p2=f/.(i+2);
then p1`1<>p2`1 & p1`2<>p2`2;
hence thesis by Th14;
end;
theorem
f is special alternating & 1<=i & i+2<=len f implies not LSeg(f/.i,f/.
(i+2)) c= LSeg(f,i) \/ LSeg(f,i+1)
proof
set p1=f/.i, p2=f/.(i+2);
assume that
A1: f is special and
A2: f is alternating and
A3: 1<=i and
A4: i+2<=len f;
set p0 = f/.(i+1);
i+1 <= i+2 by XREAL_1:6;
then i+1 <= len f by A4,XXREAL_0:2;
then
A5: LSeg(f,i)=LSeg(p1,p0) by A3,TOPREAL1:def 3;
1 <= i+1 & i+(1+1) = i+1+1 by NAT_1:11;
then
A6: LSeg(f,i+1)=LSeg(p0,p2) by A4,TOPREAL1:def 3;
consider p such that
A7: p in LSeg(p1,p2) and
A8: p`1<>p1`1 and
A9: p`1<>p2`1 and
A10: p`2<>p1`2 and
A11: p`2<>p2`2 by A2,A3,A4,Lm5;
assume
A12: LSeg(p1,p2)c= LSeg(f,i) \/ LSeg(f,i+1);
per cases by A7,A5,A6,A12,XBOOLE_0:def 3;
suppose
A13: p in LSeg(p1,p0);
A14: p1 in LSeg(p1,p0) by RLTOPSP1:68;
LSeg(p1,p0) is vertical or LSeg(p1,p0) is horizontal by A1,A5,Th19;
hence contradiction by A8,A10,A13,A14;
end;
suppose
A15: p in LSeg(p0,p2);
A16: p2 in LSeg(p0,p2) by RLTOPSP1:68;
LSeg(p0,p2) is vertical or LSeg(p0,p2) is horizontal by A1,A6,Th19;
hence contradiction by A9,A11,A15,A16;
end;
end;
theorem Th32:
f is special alternating & 1<=i & i+2<=len f & LSeg(f,i) is
vertical implies LSeg(f,i+1) is horizontal
proof
assume that
A1: f is special & f is alternating and
A2: 1<=i and
A3: i+2<=len f and
A4: LSeg(f,i) is vertical;
i+1 <= i+2 by XREAL_1:6;
then i+1 <= len f by A3,XXREAL_0:2;
then LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A2,TOPREAL1:def 3;
then (f/.i)`1 = (f/.(i+1))`1 by A4,Th16;
then (f/.(i+1))`2 = (f/.(i+2))`2 by A1,A2,A3,Th27;
then
A5: LSeg(f/.(i+1),f/.(i+2)) is horizontal by Th15;
1 <= i+1 & i+1+1 = i+(1+1) by NAT_1:11;
hence thesis by A3,A5,TOPREAL1:def 3;
end;
theorem Th33:
f is special alternating & 1<=i & i+2<=len f & LSeg(f,i) is
horizontal implies LSeg(f,i+1) is vertical
proof
assume that
A1: f is special & f is alternating and
A2: 1<=i and
A3: i+2<=len f and
A4: LSeg(f,i) is horizontal;
i+1 <= i+2 by XREAL_1:6;
then i+1 <= len f by A3,XXREAL_0:2;
then LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A2,TOPREAL1:def 3;
then (f/.i)`2 = (f/.(i+1))`2 by A4,Th15;
then (f/.(i+1))`1 = (f/.(i+2))`1 by A1,A2,A3,Th28;
then
A5: LSeg(f/.(i+1),f/.(i+2)) is vertical by Th16;
1 <= i+1 & i+1+1 = i+(1+1) by NAT_1:11;
hence thesis by A3,A5,TOPREAL1:def 3;
end;
theorem
f is special alternating & 1<=i & i+2<=len f implies LSeg(f,i) is
vertical & LSeg(f,i+1) is horizontal or LSeg(f,i) is horizontal & LSeg(f,i+1)
is vertical
by Th32,Th19,Th33;
theorem Th35:
f is special alternating & 1<=i & i+2<=len f & f/.(i+1) in LSeg(
p,q) & LSeg(p,q) c= LSeg(f,i) \/ LSeg(f,i+1) implies f/.(i+1)=p or f/.(i+1)=q
proof
assume that
A1: f is special & f is alternating and
A2: 1<=i and
A3: i+2<=len f;
i+1 <= i+2 by XREAL_1:6;
then
A4: i+1 <= len f by A3,XXREAL_0:2;
set p1=f/.i, p0=f/.(i+1), p2=f/.(i+2);
A5: i+(1+1) = i+1+1 & 1 <= i+1 by NAT_1:11;
assume that
A6: p0 in LSeg(p,q) and
A7: LSeg(p,q)c=LSeg(f,i) \/ LSeg(f,i+1);
A8: p in LSeg(p,q) & q in LSeg(p,q) by RLTOPSP1:68;
now
per cases by A7,A8,XBOOLE_0:def 3;
case
p in LSeg(f,i)& q in LSeg(f,i);
then p in LSeg(p1,p0) & q in LSeg(p1,p0) by A2,A4,TOPREAL1:def 3;
then
A9: LSeg(p,q)c=LSeg(p1,p0) by TOPREAL1:6;
p0 is_extremal_in LSeg(p1,p0) by Th11;
hence thesis by A6,A9;
end;
case
A10: p in LSeg(f,i)& q in LSeg(f,i+1);
then p in LSeg(p1,p0) by A2,A4,TOPREAL1:def 3;
then consider s such that
A11: p=(1-s)*p1+s*p0 and
0<=s and
s<=1;
A12: p`1=((1-s)*p1)`1+(s*p0)`1 by A11,TOPREAL3:2
.=(1-s)*(p1`1)+(s*p0)`1 by TOPREAL3:4
.=(1-s)*(p1`1)+s*(p0`1) by TOPREAL3:4;
q in LSeg(p0,p2) by A3,A5,A10,TOPREAL1:def 3;
then consider s1 such that
A13: q=(1-s1)*p0+s1*p2 and
0<=s1 and
s1<=1;
A14: q`2=((1-s1)*p0)`2+(s1*p2)`2 by A13,TOPREAL3:2
.=(1-s1)*(p0`2)+(s1*p2)`2 by TOPREAL3:4
.=(1-s1)*(p0`2)+s1*(p2`2) by TOPREAL3:4;
A15: p`2=((1-s)*p1)`2+(s*p0)`2 by A11,TOPREAL3:2
.=(1-s)*(p1`2)+(s*p0)`2 by TOPREAL3:4
.=(1-s)*(p1`2)+s*(p0`2) by TOPREAL3:4;
A16: q`1=((1-s1)*p0)`1+(s1*p2)`1 by A13,TOPREAL3:2
.=(1-s1)*(p0`1)+(s1*p2)`1 by TOPREAL3:4
.=(1-s1)*(p0`1)+s1*(p2`1) by TOPREAL3:4;
now
A17: f/.(i+2)=f/.(i+2) & f/.i=f/.i;
per cases by A1,A2,A3,A17,Th29;
case
A18: p1`1=p0`1 & p2`1<>p0`1;
consider r such that
A19: p0=(1-r)*p+r*q and
0<=r and
r<=1 by A6;
p0`1=((1-r)*p)`1+(r*q)`1 by A19,TOPREAL3:2
.=(1-r)*(p`1)+(r*q)`1 by TOPREAL3:4
.=(1-r)*(p0`1)+r*(q`1) by A12,A18,TOPREAL3:4;
then r*(p0`1-q`1)=0;
then
A20: r=0 or p0`1-q`1=0 by XCMPLX_1:6;
now
per cases by A20;
case
r=0;
then p0=(1-0)*p+0.TOP-REAL 2 by A19,RLVECT_1:10
.=1*p by RLVECT_1:4
.=p by RLVECT_1:def 8;
hence thesis;
end;
case
p0`1=q`1;
then s1*(p0`1-p2`1)=0 by A16;
then
A21: s1=0 or p0`1-p2`1=0 by XCMPLX_1:6;
now
per cases by A21;
case
s1=0;
then q=(1-0)*p0+0.TOP-REAL 2 by A13,RLVECT_1:10
.=1*p0 by RLVECT_1:4
.=p0 by RLVECT_1:def 8;
hence thesis;
end;
case
p0`1=p2`1;
hence contradiction by A18;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A22: p1`2=p0`2 & p2`2<>p0`2;
consider r such that
A23: p0=(1-r)*p+r*q and
0<=r and
r<=1 by A6;
p0`2=((1-r)*p)`2+(r*q)`2 by A23,TOPREAL3:2
.=(1-r)*(p`2)+(r*q)`2 by TOPREAL3:4
.=(1-r)*(p0`2)+r*(q`2) by A15,A22,TOPREAL3:4;
then r*(p0`2-q`2)=0;
then
A24: r=0 or p0`2-q`2=0 by XCMPLX_1:6;
now
per cases by A24;
case
r=0;
then p0=(1-0)*p+0.TOP-REAL 2 by A23,RLVECT_1:10
.=1*p by RLVECT_1:4
.=p by RLVECT_1:def 8;
hence thesis;
end;
case
p0`2=q`2;
then s1*(p0`2-p2`2)=0 by A14;
then
A25: s1=0 or p0`2-p2`2=0 by XCMPLX_1:6;
now
per cases by A25;
case
s1=0;
then q=(1-0)*p0+0.TOP-REAL 2 by A13,RLVECT_1:10
.=1*p0 by RLVECT_1:4
.=p0 by RLVECT_1:def 8;
hence thesis;
end;
case
p0`2=p2`2;
hence contradiction by A22;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A26: p in LSeg(f,i+1)& q in LSeg(f,i);
then q in LSeg(p1,p0) by A2,A4,TOPREAL1:def 3;
then consider s such that
A27: q=(1-s)*p1+s*p0 and
0<=s and
s<=1;
A28: q`1=((1-s)*p1)`1+(s*p0)`1 by A27,TOPREAL3:2
.=(1-s)*(p1`1)+(s*p0)`1 by TOPREAL3:4
.=(1-s)*(p1`1)+s*(p0`1) by TOPREAL3:4;
p in LSeg(p0,p2) by A3,A5,A26,TOPREAL1:def 3;
then consider s1 such that
A29: p=(1-s1)*p0+s1*p2 and
0<=s1 and
s1<=1;
A30: p`2=((1-s1)*p0)`2+(s1*p2)`2 by A29,TOPREAL3:2
.=(1-s1)*(p0`2)+(s1*p2)`2 by TOPREAL3:4
.=(1-s1)*(p0`2)+s1*(p2`2) by TOPREAL3:4;
A31: q`2=((1-s)*p1)`2+(s*p0)`2 by A27,TOPREAL3:2
.=(1-s)*(p1`2)+(s*p0)`2 by TOPREAL3:4
.=(1-s)*(p1`2)+s*(p0`2) by TOPREAL3:4;
A32: p`1=((1-s1)*p0)`1+(s1*p2)`1 by A29,TOPREAL3:2
.=(1-s1)*(p0`1)+(s1*p2)`1 by TOPREAL3:4
.=(1-s1)*(p0`1)+s1*(p2`1) by TOPREAL3:4;
now
A33: f/.(i+2)=f/.(i+2) & f/.i=f/.i;
per cases by A1,A2,A3,A33,Th29;
case
A34: p1`1=p0`1 & p2`1<>p0`1;
p0 in LSeg(q,p) by A6;
then consider r such that
A35: p0=(1-r)*q+r*p and
0<=r and
r<=1;
p0`1=((1-r)*q)`1+(r*p)`1 by A35,TOPREAL3:2
.=(1-r)*(q`1)+(r*p)`1 by TOPREAL3:4
.=(1-r)*(p0`1)+r*(p`1) by A28,A34,TOPREAL3:4;
then r*(p0`1-p`1)=0;
then
A36: r=0 or p0`1-p`1=0 by XCMPLX_1:6;
now
per cases by A36;
case
r=0;
then p0=(1-0)*q+0.TOP-REAL 2 by A35,RLVECT_1:10
.=1*q by RLVECT_1:4
.=q by RLVECT_1:def 8;
hence thesis;
end;
case
p0`1=p`1;
then s1*(p0`1-p2`1)=0 by A32;
then
A37: s1=0 or p0`1-p2`1=0 by XCMPLX_1:6;
now
per cases by A37;
case
s1=0;
then p=(1-0)*p0+0.TOP-REAL 2 by A29,RLVECT_1:10
.=1*p0 by RLVECT_1:4
.=p0 by RLVECT_1:def 8;
hence thesis;
end;
case
p0`1=p2`1;
hence contradiction by A34;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
A38: p1`2=p0`2 & p2`2<>p0`2;
p0 in LSeg(q,p) by A6;
then consider r such that
A39: p0=(1-r)*q+r*p and
0<=r and
r<=1;
p0`2=((1-r)*q)`2+(r*p)`2 by A39,TOPREAL3:2
.=(1-r)*(q`2)+(r*p)`2 by TOPREAL3:4
.=(1-r)*(p0`2)+r*(p`2) by A31,A38,TOPREAL3:4;
then r*(p0`2-p`2)=0;
then
A40: r=0 or p0`2-p`2=0 by XCMPLX_1:6;
now
per cases by A40;
case
r=0;
then p0=(1-0)*q+0.TOP-REAL 2 by A39,RLVECT_1:10
.=1*q by RLVECT_1:4
.=q by RLVECT_1:def 8;
hence thesis;
end;
case
p0`2=p`2;
then s1*(p0`2-p2`2)=0 by A30;
then
A41: s1=0 or p0`2-p2`2=0 by XCMPLX_1:6;
now
per cases by A41;
case
s1=0;
then p=(1-0)*p0+0.TOP-REAL 2 by A29,RLVECT_1:10
.=1*p0 by RLVECT_1:4
.=p0 by RLVECT_1:def 8;
hence thesis;
end;
case
p0`2=p2`2;
hence contradiction by A38;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
p in LSeg(f,i+1)& q in LSeg(f,i+1);
then p in LSeg(p0,p2) & q in LSeg(p0,p2) by A3,A5,TOPREAL1:def 3;
then
A42: LSeg(p,q)c=LSeg(p0,p2) by TOPREAL1:6;
p0 is_extremal_in LSeg(p0,p2) by Th11;
hence thesis by A6,A42;
end;
end;
hence thesis;
end;
theorem Th36:
f is special alternating & 1<=i & i+2<=len f implies f/.(i+1)
is_extremal_in LSeg(f,i) \/ LSeg(f,i+1)
proof
assume that
A1: f is special & f is alternating and
A2: 1<=i and
A3: i+2<=len f;
set p2=f/.(i+1);
i+1 <= i+2 by XREAL_1:6;
then i+1 <= len f by A3,XXREAL_0:2;
then LSeg(f,i)=LSeg(f/.i,p2) by A2,TOPREAL1:def 3;
then p2 in LSeg(f,i) by RLTOPSP1:68;
then
A4: p2 in LSeg(f,i) \/ LSeg(f,i+1) by XBOOLE_0:def 3;
for p,q st p2 in LSeg(p,q) & LSeg(p,q) c= LSeg(f,i) \/ LSeg(f,i+1) holds
p2=p or p2=q by A1,A2,A3,Th35;
hence thesis by A4;
end;
theorem Th37:
for u being Point of Euclid 2 st f is special alternating & 1<=i
& i+2<=len f & u = f/.(i+1) & f/.(i+1) in LSeg(p,q) & f/.(i+1)<>q & not p in
LSeg(f,i) \/ LSeg(f,i+1) holds for s st s>0 ex p3 st not p3 in LSeg(f,i) \/
LSeg(f,i+1) & p3 in LSeg(p,q) & p3 in Ball(u,s)
proof
let u be Point of Euclid 2 such that
A1: f is special & f is alternating and
A2: 1<=i and
A3: i+2<=len f and
A4: u = f/.(i+1) and
A5: f/.(i+1) in LSeg(p,q) and
A6: f/.(i+1)<>q and
A7: not p in LSeg(f,i) \/ LSeg(f,i+1);
set p0=f/.(i+1);
i+1 <= i+2 by XREAL_1:6;
then i+1 <= len f by A3,XXREAL_0:2;
then LSeg(f,i)=LSeg(f/.i,p0) by A2,TOPREAL1:def 3;
then
A8: p0 in LSeg(f,i) by RLTOPSP1:68;
let s;
assume
A9: s>0;
per cases;
suppose
p = q;
then f/.(i+1) in {p} by A5,RLTOPSP1:70;
then p in LSeg(f,i) by A8,TARSKI:def 1;
hence thesis by A7,XBOOLE_0:def 3;
end;
suppose
A10: p<>q;
reconsider v2=q as Element of REAL 2 by EUCLID:22;
reconsider v1=p as Element of REAL 2 by EUCLID:22;
A11: |.v2-v1.|>0 by A10,EUCLID:17;
reconsider r0=s/2 as Real;
consider s0 being Real such that
A12: p0=(1-s0)*p+s0*q and
A13: 0<=s0 and
A14: s0<=1 by A5;
set r3 = min(s0+r0/|.v2-v1.|,1), r4=max(s0+(-r0)/|.v2-v1.|,0);
set p4 = (1-r4)*p+r4*q;
set p3 = (1-r3)*p+r3*q;
A15: r0>0 by A9,XREAL_1:139;
then
A16: s0<=s0+r0/|.v2-v1.| by A11,XREAL_1:29,139;
A17: r0/|.v2-v1.|>0 by A15,A11,XREAL_1:139;
then
A18: -(r0/|.v2-v1.|)< -0 by XREAL_1:24;
then
A19: (-r0)/|.v2-v1.|<0 by XCMPLX_1:187;
then
A20: s0+0>s0+(-r0)/|.v2-v1.| by XREAL_1:6;
then
A21: s0+(-r0)/|.v2-v1.|<=1 by A14,XXREAL_0:2;
then 0<=r4 & r4<=1 by XXREAL_0:28,30;
then
A22: p4 in LSeg(p,q);
A23: s0<s0+r0/|.v2-v1.| by A15,A11,XREAL_1:29,139;
not LSeg(p3,p4) c= LSeg(f,i) \/ LSeg(f,i+1)
proof
A24: p0 in LSeg(p3,p4)
proof
s0+(-r0)/|.v2-v1.|<s0+r0/|.v2-v1.| by A9,A19,XREAL_1:6;
then
A25: r4<s0+r0/|.v2-v1.| by A17,A13,XXREAL_0:29;
A26: r4<=1 by A21,XXREAL_0:28;
per cases by A26,XXREAL_0:1;
suppose
r4<1;
then r4<r3 by A25,XXREAL_0:21;
then
A27: r3-r4>0 by XREAL_1:50;
set r5 = (r3-s0)/(r3-r4);
min(s0+r0/|.v2-v1.|,1)>=s0 by A14,A16,XXREAL_0:20;
then
A28: r3-s0>=0 by XREAL_1:48;
max(s0+(-r0)/|.v2-v1.|,0)<=s0 by A13,A20,XXREAL_0:28;
then r3-s0<=r3-r4 by XREAL_1:10;
then (r3-s0)/(r3-r4)<=(r3-r4)/(r3-r4) by A27,XREAL_1:72;
then
A29: r5<=1 by A27,XCMPLX_1:60;
A30: ((1-(r3-s0)/(r3-r4))*r3)+(((r3-s0)/(r3-r4))*r4) = r3-((r3-s0)/(
r3-r4))*(r3-r4)
.= r3-(r3-s0) by A27,XCMPLX_1:87
.= s0;
(1-r5)*p3+r5*p4 = (1-(r3-s0)/(r3-r4))*((1-r3)*p)+(1-(r3-s0)/(r3
-r4))*(r3*q) +((r3-s0)/(r3-r4))*((1-r4)*p+r4*q) by RLVECT_1:def 5
.= (1-(r3-s0)/(r3-r4))*((1-r3)*p)+(1- (r3-s0)/(r3-r4))*(r3*q) +(
((r3-s0)/(r3-r4))*((1-r4)*p)+((r3-s0)/(r3-r4))*(r4*q)) by
RLVECT_1:def 5
.= ((r3-s0)/(r3-r4))*((1-r4)*p)+((1-(r3-s0)/(r3-r4))*((1-r3)*p)
+(1- (r3-s0)/(r3-r4))*(r3*q)+((r3-s0)/(r3-r4))*(r4*q)) by
RLVECT_1:def 3;
then
(1-r5)*p3+r5*p4 = ((r3-s0)/(r3-r4))*((1-r4)*p)+((1-(r3-s0)/(r3-
r4))*((1-r3)*p) +(1- (r3-s0)/(r3-r4))*(r3*q))+((r3-s0)/(r3-r4))*(r4*q) by
RLVECT_1:def 3
.= ((r3-s0)/(r3-r4))*((1-r4)*p)+(1-(r3-s0)/(r3-r4))*((1-r3)*p) +
(1- (r3-s0)/(r3-r4))*(r3*q)+((r3-s0)/(r3-r4))*(r4*q) by
RLVECT_1:def 3
.= (((r3-s0)/(r3-r4)))*(1-r4)*p+(1-(r3-s0)/(r3-r4))*((1-r3)*p) +
(1- (r3-s0)/(r3-r4))*(r3*q)+((r3-s0)/(r3-r4))*(r4*q) by
RLVECT_1:def 7;
then
(1-r5)*p3+r5*p4 = (((r3-s0)/(r3-r4)))*(1-r4)*p+((1-(r3-s0)/(r3-
r4))*(1-r3))*p +(1-(r3-s0)/(r3-r4))*(r3*q)+((r3-s0)/(r3-r4))*(r4*q) by
RLVECT_1:def 7
.= (((r3-s0)/(r3-r4)))*(1-r4)*p+((1-(r3-s0)/(r3-r4))*(1-r3))*p +
((1- (r3-s0)/(r3-r4))*r3)*q+((r3-s0)/(r3-r4))*(r4*q) by
RLVECT_1:def 7;
then
(1-r5)*p3+r5*p4 = (((r3-s0)/(r3-r4)))*(1-r4)*p+((1- (r3-s0)/(r3
-r4))*(1-r3))*p +((1- (r3-s0)/(r3-r4))*r3)*q+(((r3-s0)/(r3-r4))*r4)*q by
RLVECT_1:def 7;
then
(1-r5)*p3+r5*p4 = ((((r3-s0)/(r3-r4)))*(1-r4)+((1- (r3-s0)/(r3-
r4))*(1-r3)))*p +((1- (r3-s0)/(r3-r4))*r3)*q+(((r3-s0)/(r3-r4))*r4)*q by
RLVECT_1:def 6
.= ((((r3-s0)/(r3-r4)))*(1-r4)+((1- (r3-s0)/(r3-r4))*(1-r3)))*p
+(((1- (r3-s0)/(r3-r4))*r3)*q+(((r3-s0)/(r3-r4))*r4)*q) by
RLVECT_1:def 3
.= p0 by A12,A30,RLVECT_1:def 6;
hence thesis by A27,A28,A29;
end;
suppose
r4=1;
then s0+(-r0)/|.v2-v1.|=1 or 0=1 by XXREAL_0:16;
then s0+(-r0)/|.v2-v1.|-s0>=s0-s0 by A14,XREAL_1:9;
hence thesis by A18,XCMPLX_1:187;
end;
end;
A31: p0 is_extremal_in LSeg(f,i) \/ LSeg(f,i+1) by A1,A2,A3,Th36;
assume
A32: LSeg(p3,p4) c= LSeg(f,i) \/ LSeg(f,i+1);
per cases by A32,A24,A31;
suppose
A33: p0=p3;
now
per cases;
suppose
s0 = 1;
then p0 = 0.TOP-REAL 2+1*q by A12,RLVECT_1:10
.= 1*q by RLVECT_1:4
.= q by RLVECT_1:def 8;
hence contradiction by A6;
end;
suppose
A34: s0<>1;
0.TOP-REAL 2 = (1-s0)*p+s0*q-((1-r3)*p+r3*q) by A12,A33,RLVECT_1:5
.= (1-s0)*p+s0*q+(-((1-r3)*p)-(r3*q)) by RLVECT_1:30
.= (1-s0)*p+s0*q+-(r3*q)+-((1-r3)*p) by RLVECT_1:def 3
.= -((1-r3)*p)+((1-s0)*p+(s0*q+-(r3*q))) by RLVECT_1:def 3
.= -((1-r3)*p)+(1-s0)*p+(s0*q+-(r3*q)) by RLVECT_1:def 3
.= (-(1-r3))*p+(1-s0)*p+(s0*q+-(r3*q)) by RLVECT_1:79
.= (-(1-r3)+(1-s0))*p+(s0*q+-(r3*q)) by RLVECT_1:def 6
.= (-(1-r3)+(1-s0))*p+(s0*q+(-r3)*q) by RLVECT_1:79
.= ((-1)*(s0-r3))*p+(s0+-r3)*q by RLVECT_1:def 6
.= (-(s0-r3))*p+(s0+-r3)*q
.= -(s0-r3)*p+(s0+-r3)*q by RLVECT_1:79
.= (s0-r3)*q-((s0-r3)*p);
then (s0-r3)*q = --((s0-r3)*p) by RLVECT_1:6
.= (s0-r3)*p;
then
A35: s0+-r3=0 by A10,RLVECT_1:36;
1>s0 by A14,A34,XXREAL_0:1;
hence contradiction by A23,A35,XXREAL_0:21;
end;
end;
hence contradiction;
end;
suppose
A36: p0=p4;
now
per cases;
suppose
s0 = 0;
then p0 = 1*p+0.TOP-REAL 2 by A12,RLVECT_1:10
.= 1*p by RLVECT_1:4
.= p by RLVECT_1:def 8;
hence contradiction by A7,A8,XBOOLE_0:def 3;
end;
suppose
A37: s0<>0;
0.TOP-REAL 2 = (1-s0)*p+s0*q-((1-r4)*p+r4*q) by A12,A36,RLVECT_1:5
.= (1-s0)*p+s0*q+(-((1-r4)*p)-(r4*q)) by RLVECT_1:30
.= (1-s0)*p+s0*q+-(r4*q)+-((1-r4)*p) by RLVECT_1:def 3
.= -((1-r4)*p)+((1-s0)*p+(s0*q+-(r4*q))) by RLVECT_1:def 3
.= -((1-r4)*p)+(1-s0)*p+(s0*q+-(r4*q)) by RLVECT_1:def 3
.= (-(1-r4))*p+(1-s0)*p+(s0*q+-(r4*q)) by RLVECT_1:79
.= (-(1-r4)+(1-s0))*p+(s0*q+-(r4*q)) by RLVECT_1:def 6
.= (-(1-r4)+(1-s0))*p+(s0*q+(-r4)*q) by RLVECT_1:79
.= ((-1)*(s0-r4))*p+(s0+-r4)*q by RLVECT_1:def 6
.= (-(s0-r4))*p+(s0-r4)*q
.= -(s0-r4)*p+(s0-r4)*q by RLVECT_1:79
.= -((s0-r4)*p)+(s0-r4)*q
.= (s0-r4)*q+-((s0-r4)*p)
.= (s0-r4)*q-((s0-r4)*p);
then (s0-r4)*q = --((s0-r4)*p) by RLVECT_1:6
.= (s0-r4)*p;
then s0+-r4=0 by A10,RLVECT_1:36;
hence contradiction by A13,A20,A37,XXREAL_0:29;
end;
end;
hence contradiction;
end;
end;
then
A38: ex x being object
st x in LSeg(p3,p4) & not x in LSeg(f,i) \/ LSeg(f,i+1);
reconsider u4 = p4 as Point of Euclid 2 by EUCLID:22;
A39: |.v2-v1.|<>0 by A10,EUCLID:17;
reconsider u3 = p3 as Point of Euclid 2 by EUCLID:22;
A40: r3<=1 by XXREAL_0:22;
0<=r3 by A9,A13,XXREAL_0:20;
then p3 in LSeg(p,q) by A40;
then
A41: LSeg(p3,p4)c=LSeg(p,q) by A22,TOPREAL1:6;
reconsider u0=p0 as Point of Euclid 2 by EUCLID:22;
A42: p4-p0 = (1-r4)*p+r4*q+ (-((1-s0)*p)-(s0*q)) by A12,RLVECT_1:30
.= (1-r4)*p+r4*q+ -((1-s0)*p)+-(s0*q) by RLVECT_1:def 3
.= r4*q+((1-r4)*p+ -((1-s0)*p))+-(s0*q) by RLVECT_1:def 3
.= ((1-r4)*p+ -((1-s0)*p))+r4*q+(-s0)*q by RLVECT_1:79
.= ((1-r4)*p+ (-(1-s0))*p)+r4*q+(-s0)*q by RLVECT_1:79
.= ((1-r4)*p+ (-(1-s0))*p)+(r4*q+(-s0)*q) by RLVECT_1:def 3
.= ((1-r4)*p+ (-(1-s0))*p)+(r4+(-s0))*q by RLVECT_1:def 6
.= ((1-r4)+ -(1-s0))*p+(r4-s0)*q by RLVECT_1:def 6
.= (-(r4-s0))*p+(r4-s0)*q
.= (r4-s0)*q -((r4-s0)*p) by RLVECT_1:79
.= (r4-s0)*(q -p) by RLVECT_1:34
.= (r4-s0)*(v2 -v1);
now
per cases;
suppose
s0+(-r0)/|.v2-v1.|<=0;
then
A43: r4=0 by XXREAL_0:def 10;
r4>=s0+(-r0)/|.v2-v1.| by XXREAL_0:25;
then r4+-s0>=s0+(-r0)/|.v2-v1.|+-s0 by XREAL_1:6;
then
A44: -(r4-s0)<=-((-r0)/|.v2-v1.|) by XREAL_1:24;
r0+r0 = s;
then
A45: r0<s by A9,XREAL_1:29;
reconsider v3=p4, v4=p0 as Element of REAL 2 by EUCLID:22;
A46: -((-r0)/|.v2-v1.|) = ((--r0)/|.v2-v1.|) by XCMPLX_1:187
.= r0/|.v2-v1.|;
A47: dist(u4,u0) = |.v3-v4.| by Th5
.= |.p4-p0.|
.= |.r4-s0.|*|.(v2 -v1).| by A42,EUCLID:11;
|.r4-s0.| = |.-(r4-s0).| by COMPLEX1:52
.= -(0-s0) by A13,A43,ABSVALUE:def 1;
then |.r4-s0.|*|.v2 -v1.|<=(r0/|.v2-v1.|)*|.v2 -v1.| by A43,A44,A46,
XREAL_1:64;
then dist(u4,u0)<= r0 by A39,A47,XCMPLX_1:87;
hence dist(u4,u0)<s by A45,XXREAL_0:2;
end;
suppose
not s0+(-r0)/|.v2-v1.|<=0;
then
A48: p4-p0 = (s0+(-r0)/|.v2-v1.|-s0)*(v2-v1) by A42,XXREAL_0:def 10
.= (s0+(-r0)/|.v2-v1.|-s0)*(q-p)
.= ((-r0)/|.v2-v1.|)*(q-p)
.= ((-r0)/|.v2-v1.|)*(v2-v1);
reconsider v3=p4, v4=p0 as Element of REAL 2 by EUCLID:22;
A49: r0+r0 =s;
dist(u4,u0) = |.v3-v4.| by Th5
.= |.p4-p0.|
.= |.(-r0)/|.v2-v1.|.|*|.v2-v1.| by A48,EUCLID:11
.= (|.-r0.|/|.|.v2-v1.|.|)*|.v2-v1.| by COMPLEX1:67
.= (|.-r0.|/|.v2-v1.|)*|.v2-v1.| by ABSVALUE:def 1
.= |.-r0.| by A11,XCMPLX_1:87
.= |.r0.| by COMPLEX1:52
.= r0 by A9,ABSVALUE:def 1;
hence dist(u4,u0)<s by A9,A49,XREAL_1:29;
end;
end;
then u4 in {u7 where u7 is Point of Euclid 2: dist(u0,u7)<s};
then
A50: p4 in Ball(u0,s) by METRIC_1:17;
A51: p3-p0 =(1-r3)*p+r3*q+ (-((1-s0)*p)-(s0*q)) by A12,RLVECT_1:30
.=(1-r3)*p+r3*q+ -((1-s0)*p)+-(s0*q) by RLVECT_1:def 3
.=r3*q+((1-r3)*p+ -((1-s0)*p))+-(s0*q) by RLVECT_1:def 3
.=((1-r3)*p+ -((1-s0)*p))+r3*q+(-s0)*q by RLVECT_1:79
.=((1-r3)*p+ (-(1-s0))*p)+r3*q+(-s0)*q by RLVECT_1:79
.=((1-r3)*p+ (-(1-s0))*p)+(r3*q+(-s0)*q) by RLVECT_1:def 3
.=((1-r3)*p+ (-(1-s0))*p)+(r3+(-s0))*q by RLVECT_1:def 6
.=((1-r3)+ -(1-s0))*p+(r3-s0)*q by RLVECT_1:def 6
.=(-(r3-s0))*p+(r3-s0)*q
.=(r3-s0)*q -((r3-s0)*p) by RLVECT_1:79
.=(r3-s0)*(q-p) by RLVECT_1:34
.=(r3-s0)*(v2-v1);
now
per cases;
suppose
A52: 1<=s0+r0/|.v2-v1.|;
r3<=s0+r0/|.v2-v1.| by XXREAL_0:17;
then
A53: r3+-s0<=s0+r0/|.v2-v1.|+-s0 by XREAL_1:6;
r3=1 by A52,XXREAL_0:def 9;
then r3-s0>=0 by A14,XREAL_1:48;
then |.r3-s0.|<=r0/|.v2-v1.| by A53,ABSVALUE:def 1;
then
A54: |.r3-s0.|*|.v2 -v1.|<=(r0/|.v2-v1.|)*|.v2 -v1.| by XREAL_1:64;
reconsider v3=p3, v4=p0 as Element of REAL 2 by EUCLID:22;
r0+r0 = s;
then
A55: r0<s by A9,XREAL_1:29;
dist(u3,u0) = |.v3-v4.| by Th5
.= |.p3-p0.|
.= |.(r3-s0)*(v2 -v1).| by A51
.= |.r3-s0.|*|.(v2 -v1).| by EUCLID:11;
then dist(u3,u0)<= r0 by A39,A54,XCMPLX_1:87;
hence dist(u3,u0)<s by A55,XXREAL_0:2;
end;
suppose
not 1<=s0+r0/|.v2-v1.|;
then
A56: p3-p0 = (s0+r0/|.v2-v1.|-s0)*(v2-v1) by A51,XXREAL_0:def 9
.= (s0+r0/|.v2-v1.|-s0)*(q-p)
.= (r0/|.v2-v1.|)*(q-p)
.= (r0/|.v2-v1.|)*(v2-v1);
reconsider v3=p3, v4=p0 as Element of REAL 2 by EUCLID:22;
A57: r0+r0 = s;
dist(u3,u0) = |.v3-v4.| by Th5
.= |.p3-p0.|
.= |.r0/|.v2-v1.|.|*|.v2-v1.| by A56,EUCLID:11
.= (|.r0.|/|.|.v2-v1.|.|)*|.v2-v1.| by COMPLEX1:67
.= (|.r0.|/|.v2-v1.|)*|.v2-v1.| by ABSVALUE:def 1
.= |.r0.| by A11,XCMPLX_1:87
.= r0 by A9,ABSVALUE:def 1;
hence dist(u3,u0)<s by A9,A57,XREAL_1:29;
end;
end;
then u3 in {u6 where u6 is Point of Euclid 2: dist(u0,u6)<s};
then p3 in Ball(u0,s) by METRIC_1:17;
then LSeg(p3,p4) c= Ball(u0,s) by A50,TOPREAL3:21;
hence thesis by A4,A38,A41;
end;
end;
definition
let f1,f2,P;
pred f1,f2 are_generators_of P means
f1 is alternating being_S-Seq &
f2 is alternating being_S-Seq & f1/.1 = f2/.1 & f1/.len f1 = f2/.len f2 & <*f1
/.2,f1/.1,f2/.2*> is alternating & <*f1/.(len f1 - 1),f1/.len f1,f2/.(len f2 -
1)*> is alternating & f1/.1 <> f1/.len f1 & L~f1 /\ L~f2 = {f1/.1,f1/.len f1} &
P = L~f1 \/ L~f2;
end;
theorem
f1,f2 are_generators_of P & 1<i & i<len f1 implies f1/.i is_extremal_in P
proof
set p0=f1/.i;
set q1 = f1/.1, q2 = f1/.len f1;
set F1 = {LSeg(f1,k): 1<=k & k+1<=len f1};
set PP = union F1;
reconsider u0 = p0 as Point of Euclid 2 by EUCLID:22;
reconsider F2={LSeg(f2,k): 1<=k & k+1<=len f2} as Subset-Family of TOP-REAL
2 by Th25;
assume that
A1: f1,f2 are_generators_of P and
A2: 1<i and
A3: i<len f1;
set P2 = union F2;
A4: L~f1 /\ L~f2 = {q1,q2} by A1;
reconsider j=i-1 as Element of NAT by A2,INT_1:3,XREAL_1:48;
1+1 <= i by A2,NAT_1:13;
then
A5: 1+1-1 <= j by XREAL_1:9;
reconsider F = {LSeg(f1,k): 1<=k & k+1<=len f1 & k<>j & k<>j+1} as
Subset-Family of TOP-REAL 2 by Lm3;
set P1=union F;
set Q = P1 \/ P2;
A6: j+1=i;
then LSeg(f1,j)=LSeg(f1/.j,p0) by A3,A5,TOPREAL1:def 3;
then
A7: p0 in LSeg(f1,j) by RLTOPSP1:68;
A8: P = L~f1 \/ L~f2 by A1;
A9: f1 is being_S-Seq by A1;
then
A10: f1 is one-to-one;
A11: len f1 >= 1+1 by A9;
A12: i+1<=len f1 by A3,NAT_1:13;
then
A13: LSeg(f1,i) in F1 by A2;
LSeg(f1,i)=LSeg(p0,f1/.(i+1)) by A2,A12,TOPREAL1:def 3;
then
A14: p0 in LSeg(f1,i) by RLTOPSP1:68;
then
A15: p0 in L~f1 by A13,TARSKI:def 4;
not p0 in Q
proof
assume
A16: p0 in Q;
per cases by A16,XBOOLE_0:def 3;
suppose
A17: p0 in P1;
A18: f1 is s.n.c. by A9;
consider Z being set such that
A19: p0 in Z and
A20: Z in F by A17,TARSKI:def 4;
consider k such that
A21: LSeg(f1,k)=Z and
1<=k and
k+1<=len f1 and
A22: k<>i-1 and
A23: k<>i by A20;
k<j+1 or i<k by A23,XXREAL_0:1;
then k<=j or i<k by NAT_1:13;
then
A24: k<j or i<k by A22,XXREAL_0:1;
now
per cases by A24,XREAL_1:50;
suppose
j-k>0;
then 1+(j-k)>1+0 by XREAL_1:6;
then i-k>1;
then k+1<i by XREAL_1:20;
then LSeg(f1,k) misses LSeg(f1,i) by A18;
then LSeg(f1,k) /\ LSeg(f1,i) = {} by XBOOLE_0:def 7;
hence contradiction by A14,A19,A21,XBOOLE_0:def 4;
end;
suppose
k-i>0;
then k-i+1>0+1 by XREAL_1:6;
then k-j>1;
then j+1 < k by XREAL_1:20;
then LSeg(f1,j) misses LSeg(f1,k) by A18;
then LSeg(f1,j) /\ LSeg(f1,k) = {} by XBOOLE_0:def 7;
hence contradiction by A7,A19,A21,XBOOLE_0:def 4;
end;
end;
hence contradiction;
end;
suppose
A25: p0 in P2;
1<=len f1 by A11,XXREAL_0:2;
then 1 in Seg len f1 by FINSEQ_1:1;
then
A26: 1 in dom f1 by FINSEQ_1:def 3;
1<=len f1 by A2,A3,XXREAL_0:2;
then
A27: len f1 in dom f1 by FINSEQ_3:25;
i in Seg len f1 by A2,A3,FINSEQ_1:1;
then
A28: i in dom f1 by FINSEQ_1:def 3;
p0 in {q1,q2} by A4,A15,A25,XBOOLE_0:def 4;
then p0=q1 or p0=q2 by TARSKI:def 2;
hence contradiction by A2,A3,A10,A26,A28,A27,PARTFUN2:10;
end;
end;
then
A29: u0 in Q` by SUBSET_1:29;
A30: f1 is alternating by A1;
A31: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
then reconsider QQ = Q` as Subset of TopSpaceMetr Euclid 2;
A32: f1 is special by A9;
P1 is closed & P2 is closed by Lm4,Th26;
then Q is closed by TOPS_1:9;
then Q` is open by TOPS_1:3;
then QQ is open by A31,PRE_TOPC:30;
then consider r0 being Real such that
A33: r0>0 and
A34: Ball(u0,r0)c=Q` by A29,TOPMETR:15;
reconsider r0 as Real;
A35: j+2 <= len f1 by A12;
now
let y be object;
hereby
assume y in P1 \/ LSeg(f1,j) \/ LSeg(f1,i);
then
A36: y in P1 \/ LSeg(f1,j) or y in LSeg(f1,i) by XBOOLE_0:def 3;
per cases by A36,XBOOLE_0:def 3;
suppose
y in P1;
then consider Z3 being set such that
A37: y in Z3 and
A38: Z3 in F by TARSKI:def 4;
ex k st LSeg(f1,k)=Z3 & 1<=k & k+1<=len f1 & not k=i-1 & not k=i
by A38;
then Z3 in F1;
hence y in PP by A37,TARSKI:def 4;
end;
suppose
A39: y in LSeg(f1,j);
LSeg(f1,j) in F1 by A3,A6,A5;
hence y in PP by A39,TARSKI:def 4;
end;
suppose
y in LSeg(f1,i);
hence y in PP by A13,TARSKI:def 4;
end;
end;
assume y in PP;
then consider Z2 being set such that
A40: y in Z2 and
A41: Z2 in F1 by TARSKI:def 4;
consider k such that
A42: LSeg(f1,k)=Z2 and
A43: 1<=k & k+1<=len f1 by A41;
per cases;
suppose
A44: k=i-1 or k=i;
now
per cases by A44;
suppose
k=i-1;
then y in LSeg(f1,j) \/ LSeg(f1,i) by A40,A42,XBOOLE_0:def 3;
then y in P1 \/ (LSeg(f1,j) \/ LSeg(f1,i)) by XBOOLE_0:def 3;
hence y in P1 \/ LSeg(f1,j) \/ LSeg(f1,i) by XBOOLE_1:4;
end;
suppose
k=i;
hence y in P1 \/ LSeg(f1,j) \/ LSeg(f1,i) by A40,A42,XBOOLE_0:def 3;
end;
end;
hence y in P1 \/ LSeg(f1,j) \/ LSeg(f1,i);
end;
suppose
k<>i-1 & k<>i;
then Z2 in F by A42,A43;
then y in P1 by A40,TARSKI:def 4;
then y in P1 \/ (LSeg(f1,j) \/ LSeg(f1,i)) by XBOOLE_0:def 3;
hence y in P1 \/ LSeg(f1,j) \/ LSeg(f1,i) by XBOOLE_1:4;
end;
end;
then
A45: P1 \/ LSeg(f1,j) \/ LSeg(f1,i) = PP by TARSKI:2;
A46: now
let p,q;
assume that
A47: p0 in LSeg(p,q) and
A48: LSeg(p,q)c=P;
per cases;
suppose
A49: LSeg(p,q) c= LSeg(f1,j)\/ LSeg(f1,i);
p0 is_extremal_in LSeg(f1,j) \/ LSeg(f1,i) by A30,A6,A5,A35,A32,Th36;
hence p0=p or p0=q by A47,A49;
end;
suppose
not LSeg(p,q) c= LSeg(f1,j)\/ LSeg(f1,i);
then consider x being object such that
A50: x in LSeg(p,q) and
A51: not x in LSeg(f1,j)\/ LSeg(f1,i);
reconsider p8 = x as Point of TOP-REAL 2 by A50;
A52: LSeg(p,q) = LSeg(p,p8)\/ LSeg(p8,q) by A50,TOPREAL1:5;
now
per cases by A47,A52,XBOOLE_0:def 3;
suppose
A53: p0 in LSeg(p,p8);
now
assume f1/.i<>p;
then consider q3 such that
A54: not q3 in LSeg(f1,j) \/ LSeg(f1,i) and
A55: q3 in LSeg(p8,p) and
A56: q3 in Ball(u0,r0) by A30,A5,A35,A32,A33,A34,A51,A53,Th37;
A57: not q3 in Q by A34,A56,XBOOLE_0:def 5;
then not q3 in P1 by XBOOLE_0:def 3;
then not q3 in P1 \/ (LSeg(f1,j) \/ LSeg(f1,i)) by A54,
XBOOLE_0:def 3;
then
A58: not q3 in PP by A45,XBOOLE_1:4;
LSeg(p8,p) c= LSeg(p,q) by A52,XBOOLE_1:7;
then
A59: LSeg(p8,p) c= P by A48;
not q3 in L~f2 by A57,XBOOLE_0:def 3;
hence contradiction by A8,A55,A58,A59,XBOOLE_0:def 3;
end;
hence p0=p or p0=q;
end;
suppose
A60: p0 in LSeg(p8,q);
now
assume f1/.i<>q;
then consider q3 such that
A61: not q3 in LSeg(f1,j) \/ LSeg(f1,i) and
A62: q3 in LSeg(p8,q) and
A63: q3 in Ball(u0,r0) by A30,A5,A35,A32,A33,A34,A51,A60,Th37;
A64: not q3 in Q by A34,A63,XBOOLE_0:def 5;
then not q3 in P1 by XBOOLE_0:def 3;
then not q3 in P1 \/ (LSeg(f1,j) \/ LSeg(f1,i)) by A61,
XBOOLE_0:def 3;
then
A65: not q3 in PP by A45,XBOOLE_1:4;
LSeg(p8,q) c= LSeg(p,q) by A52,XBOOLE_1:7;
then
A66: LSeg(p8,q) c= P by A48;
not q3 in L~f2 by A64,XBOOLE_0:def 3;
hence contradiction by A8,A62,A65,A66,XBOOLE_0:def 3;
end;
hence p0=p or p0=q;
end;
end;
hence p0=p or p0=q;
end;
end;
p0 in PP by A14,A13,TARSKI:def 4;
then p0 in P by A8,XBOOLE_0:def 3;
hence thesis by A46;
end;
:: Moved from KURATO_2, AK, 22.02.2006
theorem
for p, q being Point of TOP-REAL n, p9, q9 being Point of Euclid n st
p = p9 & q = q9 holds dist (p9, q9) = |. p - q .| by Th5;
:: Moved from SPRECT_3, AK, 22.02.2006
theorem
for p,q,r being Point of TOP-REAL 2 st LSeg(p,q) is horizontal & r in
LSeg(p,q) holds p`2 = r`2
proof
let p,q,r be Point of TOP-REAL 2;
assume LSeg(p,q) is horizontal;
then
A1: p`2 = q`2 by Th15;
assume r in LSeg(p,q);
then consider t being Real such that
A2: r = (1-t)*p+t*q and
0 <= t and
t <= 1;
thus p`2 = (1-t)*p`2+t*p`2 .= ((1-t)*p)`2+t*q`2 by A1,TOPREAL3:4
.= ((1-t)*p)`2+(t*q)`2 by TOPREAL3:4
.= r`2 by A2,TOPREAL3:2;
end;
theorem
for p,q,r being Point of TOP-REAL 2 st LSeg(p,q) is vertical &
r in LSeg(p,q) holds p`1 = r`1
proof
let p,q,r be Point of TOP-REAL 2;
assume LSeg(p,q) is vertical;
then
A1: p`1 = q`1 by Th16;
assume r in LSeg(p,q);
then consider t being Real such that
A2: r = (1-t)*p+t*q and
0 <= t and
t <= 1;
thus p`1 = (1-t)*p`1+t*p`1 .= ((1-t)*p)`1+t*q`1 by A1,TOPREAL3:4
.= ((1-t)*p)`1+(t*q)`1 by TOPREAL3:4
.= r`1 by A2,TOPREAL3:2;
end;
registration
cluster compact non empty horizontal for Subset of TOP-REAL 2;
existence
proof
take LSeg(|[ 0,0 ]|,|[ 1,0 ]|);
|[ 0,0 ]|`2 = 0 & |[ 1,0 ]|`2 = 0;
hence thesis by Th15;
end;
cluster compact non empty vertical for Subset of TOP-REAL 2;
existence
proof
take LSeg(|[ 0,0 ]|,|[ 0,1 ]|);
|[ 0,0 ]|`1 = 0 & |[ 0,1 ]|`1 = 0;
hence thesis by Th16;
end;
end;