:: Basic Properties of Connecting Points with Line Segments
:: in ${\calE}^2_{\rm T}$
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992-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, PRE_TOPC, EUCLID, FINSEQ_1, SUBSET_1, RELAT_1, ARYTM_3,
MCART_1, ARYTM_1, FUNCT_1, SQUARE_1, BINOP_2, COMPLEX1, RVSUM_1, CARD_3,
NAT_1, STRUCT_0, REAL_1, XXREAL_0, RLTOPSP1, TARSKI, CARD_1, XBOOLE_0,
TOPREAL1, PARTFUN1, ORDINAL4, METRIC_1, FINSEQ_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
SQUARE_1, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1,
BINOP_1, PRE_TOPC, FINSEQ_2, STRUCT_0, METRIC_1, RVSUM_1, RLVECT_1,
RLTOPSP1, EUCLID, TOPREAL1, XXREAL_0;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP,
FINSEQ_4, TOPREAL1, RVSUM_1, RELSET_1, DOMAIN_1, BINOP_1;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, FINSEQ_1,
STRUCT_0, EUCLID, VALUED_0, INT_1, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, TOPREAL1, FUNCT_1, XBOOLE_0;
equalities TOPREAL1, XBOOLE_0, SQUARE_1, EUCLID, RVSUM_1, VALUED_1, ALGSTR_0,
RLTOPSP1;
expansions TOPREAL1, FUNCT_1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, SQUARE_1,
FINSEQ_2, METRIC_1, RVSUM_1, EUCLID, TOPREAL1, FINSEQ_3, FINSEQ_4,
PARTFUN2, TBSP_1, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_0,
COMPLEX1, XREAL_1, BINOP_2, XXREAL_0, ORDINAL1, RLTOPSP1, RLVECT_1;
begin
reserve p,p1,p2,p3,p11,p22,q,q1,q2 for Point of TOP-REAL 2,
f,h for FinSequence of TOP-REAL 2,
r,r1,r2,s,s1,s2 for Real,
u,u1,u2,u5 for Point of Euclid 2,
n,m,i,j,k for Nat,
N for Nat,
x,y,z for set;
begin :: Properties of sets in TOP-REAL 2
::$CT
Th1: for x,y,z being object holds
1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*>
by FINSEQ_1:81;
theorem Th2:
(p1+p2)`1 = p1`1 + p2`1 & (p1+p2)`2 = p1`2 + p2`2
proof
p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2]| by EUCLID:55;
hence thesis;
end;
theorem
(p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2
proof
p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2]| by EUCLID:61;
hence thesis;
end;
theorem Th4:
(r*p)`1 = r*(p`1) & (r*p)`2 = r*(p`2)
proof
r*p = |[r*p`1,r*p`2]| by EUCLID:57;
hence thesis;
end;
theorem Th5:
p1=<*r1,s1*> & p2=<*r2,s2*> implies p1+p2=<*r1+r2,s1+s2*> & p1-
p2=<*r1-r2,s1-s2*>
proof
A1: |[r1,s1]|`1=r1 & |[r1,s1]|`2=s1;
A2: |[r2,s2]|`1=r2 & |[r2,s2]|`2=s2;
assume p1=<*r1,s1*> & p2=<*r2,s2*>;
hence thesis by A1,A2,EUCLID:55,61;
end;
theorem Th6:
p`1 = q`1 & p`2 = q`2 implies p=q
proof
assume p`1 = q`1 & p`2 = q`2;
hence p=|[q`1,q`2]| by EUCLID:53
.= q by EUCLID:53;
end;
theorem Th7:
u1 = p1 & u2 = p2 implies (Pitag_dist 2).(u1,u2) = sqrt ((p1`1 -
p2`1)^2 + (p1`2 - p2`2)^2)
proof
assume that
A1: u1 = p1 and
A2: u2 = p2;
reconsider v1 = u1, v2 = u2 as Element of REAL 2;
reconsider p11 = p1`1, p21 = p2`1, p12 = p1`2, p22 = p2`2 as Element of REAL
by XREAL_0:def 1;
p1 = |[p1`1,p1`2]| & u2 = <* p2`1,p2`2 *> by A2,EUCLID:53;
then v1-v2= <* diffreal.(p11,p21), diffreal.(p12,p22) *> by A1,FINSEQ_2:75
.= <* p1`1 - p2`1, diffreal.(p1`2,p2`2) *> by BINOP_2:def 10
.= <* p1`1 - p2`1,p1`2 - p2`2*> by BINOP_2:def 10;
then abs (v1-v2) = <* absreal.(p1`1-p2`1),absreal.(p1`2-p2`2) *> by
FINSEQ_2:36
.= <* |. p1`1-p2`1 .|,absreal.(p1`2-p2`2) *> by EUCLID:def 2
.= <* |. p1`1-p2`1 .|,|. p1`2-p2`2.| *> by EUCLID:def 2;
then
A3: sqr abs (v1-v2) = <* sqrreal.(|. p1`1 - p2`1 .|),sqrreal.(|. p1`2 -
p2`2 .|) *> by FINSEQ_2:36
.= <* (|. p1`1 - p2`1 .|)^2,sqrreal.(|. p1`2-p2`2 .|) *> by RVSUM_1:def 2
.= <* (|. p1`1 - p2`1 .|)^2,(|.p1`2-p2`2.|)^2 *> by RVSUM_1:def 2
.= <* (p1`1 - p2`1)^2,(|.p1`2-p2`2.|)^2 *> by COMPLEX1:75
.= <* (p1`1-p2`1)^2,(p1`2 - p2`2)^2 *> by COMPLEX1:75;
(Pitag_dist 2).(u1,u2) = |.v1 - v2.| by EUCLID:def 6
.= sqrt Sum sqr abs (v1-v2) by EUCLID:25;
hence thesis by A3,RVSUM_1:77;
end;
theorem Th8:
for n being Nat holds the carrier of TOP-REAL n = the carrier of
Euclid n by EUCLID:22;
reserve lambda for Real;
theorem Th9:
r1 <= s1 implies {p1: p1`1=r & r1<=p1`2 & p1`2<=s1} = LSeg(|[r,
r1]|,|[r,s1]|)
proof
set L = { p3 : p3`1 = r & r1 <= p3`2 & p3`2 <= s1}, p = |[ r,r1 ]|, q = |[ r
,s1 ]|;
A1: p`1 = r;
assume
A2: r1 <= s1;
then
A3: s1 - r1 >= r1 - r1 by XREAL_1:13;
A4: q`2 = s1;
A6: q`1 = r;
thus L c= LSeg(p,q)
proof
per cases by A2,XXREAL_0:1;
suppose
A7: r1 = s1;
L c= {p}
proof
let x be object;
assume x in L;
then consider p2 such that
A8: x = p2 and
A9: p2`1 = r and
A10: r1 <= p2`2 & p2`2 <= s1;
p`2 = p2`2 by A7,A10,XXREAL_0:1;
then p2 = p by A1,A9,Th6;
hence thesis by A8,TARSKI:def 1;
end;
hence thesis by A7,RLTOPSP1:70;
end;
suppose
A11: r1 < s1;
let x be object;
assume x in L;
then consider p2 such that
A12: x = p2 and
A13: p2`1 = r and
A14: r1 <= p2`2 and
A15: p2`2 <= s1;
set t = p2`2, l = (t - r1)/(s1-r1);
A16: s1 - r1 > 0 by A11,XREAL_1:50;
then
A17: 1-l = (1*(s1-r1) -(t-r1))/(s1-r1) by XCMPLX_1:127
.= (s1 - t)/(s1-r1);
t - r1 <= s1 - r1 by A15,XREAL_1:9;
then l <= (s1-r1)/(s1-r1) by A16,XREAL_1:72;
then
A18: l <= 1 by A16,XCMPLX_1:60;
A19: ((1-l)*p + l*q)`1 = ((1-l)*p)`1 + (l*q)`1 by Th2
.= (1-l)* (p`1) + (l*q)`1 by Th4
.= (1-l)*r + l*r by A6,Th4
.= p2`1 by A13;
((1-l)*p + l*q)`2 = ((1-l)*p)`2 + (l*q)`2 by Th2
.= (1-l)* (p`2) + (l*q)`2 by Th4
.= (1-l)*(p`2) + l*(q`2) by Th4
.= (s1-t)*(p`2)/(s1-r1) + l*(q`2) by A17,XCMPLX_1:74
.= (s1-t)*(p`2)/(s1-r1) + (t-r1)*(q`2)/(s1-r1) by XCMPLX_1:74
.= (s1 * r1 - t*r1 + (t-r1)*s1)/(s1-r1) by XCMPLX_1:62
.= t*(s1 - r1)/(s1-r1)
.= t*((s1 - r1)/(s1-r1)) by XCMPLX_1:74
.= t*1 by A16,XCMPLX_1:60
.= p2`2;
then
A20: p2 = (1-l)*p + l*q by A19,Th6;
r1 - r1 <= t - r1 by A14,XREAL_1:9;
hence thesis by A16,A12,A18,A20;
end;
end;
let x be object;
assume x in LSeg(p,q);
then consider lambda such that
A21: (1-lambda)*p + lambda*q = x and
A22: 0 <= lambda and
A23: lambda <= 1;
A24: r1+0<=r1+lambda*(s1-r1) by A3,A22,XREAL_1:7;
lambda*(s1-r1)<= 1*(s1-r1) by A3,A23,XREAL_1:64;
then
A25: r1+lambda*(s1-r1)<=s1-r1+r1 by XREAL_1:7;
set p2 = (1-lambda)*p + lambda*q;
A26: p2 `2 = ((1-lambda)*p)`2 + (lambda*q)`2 by Th2
.= (1-lambda)*(p`2) + (lambda*q)`2 by Th4
.= 1*r1-lambda*r1 + lambda*s1 by A4,Th4
.= r1+lambda*(s1 - r1);
p2 `1 = ((1-lambda)*p)`1 + (lambda*q)`1 by Th2
.= (1-lambda)*(p`1) + (lambda*q)`1 by Th4
.= (1-lambda)*r + lambda*r by A6,Th4
.= 1*r;
hence thesis by A21,A26,A24,A25;
end;
theorem Th10:
r1 <= s1 implies {p1: p1`2=r & r1<=p1`1 & p1`1<=s1} = LSeg(|[r1,
r]|,|[s1,r]|)
proof
set L = {p3 : p3`2 = r & r1 <= p3`1 & p3`1 <= s1}, p = |[ r1,r]|, q = |[ s1,
r]|;
assume
A2: r1 <= s1;
then
A3: s1 - r1 >= r1 - r1 by XREAL_1:13;
A4: q`2 = r;
A5: p`2 = r;
A6: q`1 = s1;
thus L c= LSeg(p,q)
proof
per cases by A2,XXREAL_0:1;
suppose
A7: r1 = s1;
L c= {p}
proof
let x be object;
assume x in L;
then consider p2 such that
A8: x = p2 and
A9: p2`2 = r and
A10: r1 <= p2`1 & p2`1 <= s1;
p`1 = p2`1 by A7,A10,XXREAL_0:1;
then p2 = p by A5,A9,Th6;
hence thesis by A8,TARSKI:def 1;
end;
hence thesis by A7,RLTOPSP1:70;
end;
suppose
A11: r1 < s1;
let x be object;
assume x in L;
then consider p2 such that
A12: x = p2 and
A13: p2`2 = r and
A14: r1 <= p2`1 and
A15: p2`1 <= s1;
set t = p2`1, l = (t - r1)/(s1-r1);
A16: s1 - r1 > 0 by A11,XREAL_1:50;
then
A17: 1-l = (1*(s1-r1) -(t-r1))/(s1-r1) by XCMPLX_1:127
.= (s1 - t)/(s1-r1);
t - r1 <= s1 - r1 by A15,XREAL_1:9;
then l <= (s1-r1)/(s1-r1) by A16,XREAL_1:72;
then
A18: l <= 1 by A16,XCMPLX_1:60;
A19: ((1-l)*p + l*q)`2 = ((1-l)*p)`2 + (l*q)`2 by Th2
.= (1-l)* (p`2) + (l*q)`2 by Th4
.= (1-l)*r + l*r by A4,Th4
.= p2`2 by A13;
((1-l)*p + l*q)`1 = ((1-l)*p)`1 + (l*q)`1 by Th2
.= (1-l)* (p`1) + (l*q)`1 by Th4
.= (1-l)*(p`1) + l*(q`1) by Th4
.= (s1-t)*(p`1)/(s1-r1) + l*(q`1) by A17,XCMPLX_1:74
.= (s1-t)*(p`1)/(s1-r1) + (t-r1)*(q`1)/(s1-r1) by XCMPLX_1:74
.= (s1 * r1 - t*r1 + (t-r1)*s1)/(s1-r1) by XCMPLX_1:62
.= t*(s1 - r1)/(s1-r1)
.= t*((s1 - r1)/(s1-r1)) by XCMPLX_1:74
.= t*1 by A16,XCMPLX_1:60
.= p2`1;
then
A20: p2 = (1-l)*p + l*q by A19,Th6;
r1 - r1 <= t - r1 by A14,XREAL_1:9;
hence thesis by A16,A12,A18,A20;
end;
end;
let x be object;
assume x in LSeg(p,q);
then consider lambda such that
A21: (1-lambda)*p + lambda*q = x and
A22: 0 <= lambda and
A23: lambda <= 1;
A24: r1+0<=r1+lambda*(s1-r1) by A3,A22,XREAL_1:7;
lambda*(s1-r1)<= 1*(s1-r1) by A3,A23,XREAL_1:64;
then
A25: r1+lambda*(s1-r1)<=s1-r1+r1 by XREAL_1:7;
set p2 = (1-lambda)*p + lambda*q;
A26: p2 `1 = ((1-lambda)*p)`1 + (lambda*q)`1 by Th2
.= (1-lambda)*(p`1) + (lambda*q)`1 by Th4
.= 1*r1-lambda*r1 + lambda*s1 by A6,Th4
.= r1+lambda*(s1 - r1);
p2 `2 = ((1-lambda)*p)`2 + (lambda*q)`2 by Th2
.= (1-lambda)*(p`2) + (lambda*q)`2 by Th4
.= (1-lambda)*r + lambda*r by A4,Th4
.= r;
hence thesis by A21,A26,A24,A25;
end;
theorem
p in LSeg(|[r,r1]|,|[r,s1]|) implies p`1 = r
proof
assume
A1: p in LSeg(|[r,r1]|,|[r,s1]|);
per cases by XXREAL_0:1;
suppose
r1<s1;
then LSeg(|[r,r1]|,|[r,s1]|) = {q: q`1 = r & r1<=q`2 & q`2<=s1} by Th9;
then ex p1 st p1=p & p1`1 = r & r1<=p1`2 & p1`2<=s1 by A1;
hence thesis;
end;
suppose
r1=s1;
then p in {|[r,r1]|} by A1,RLTOPSP1:70;
then p = |[r,r1]| by TARSKI:def 1;
hence thesis;
end;
suppose
r1>s1;
then LSeg(|[r,r1]|,|[r,s1]|) = {q: q`1 = r & s1<=q`2 & q`2<=r1} by Th9;
then ex p1 st p1=p & p1`1 = r & s1<=p1`2 & p1`2<=r1 by A1;
hence thesis;
end;
end;
theorem
p in LSeg(|[r1,r]|,|[s1,r]|) implies p`2 = r
proof
assume
A1: p in LSeg(|[r1,r]|,|[s1,r]|);
per cases by XXREAL_0:1;
suppose
r1<s1;
then LSeg(|[r1,r]|,|[s1,r]|) = {q: q`2 = r & r1<=q`1 & q`1<=s1} by Th10;
then ex p1 st p1=p & p1`2 = r & r1<=p1`1 & p1`1<=s1 by A1;
hence thesis;
end;
suppose
r1=s1;
then p in {|[r1,r]|} by A1,RLTOPSP1:70;
then p = |[r1,r]| by TARSKI:def 1;
hence thesis;
end;
suppose
r1>s1;
then LSeg(|[r1,r]|,|[s1,r]|) = {q: q`2 = r & s1<=q`1 & q`1<=r1} by Th10;
then ex p1 st p1=p & p1`2 = r & s1<=p1`1 & p1`1<=r1 by A1;
hence thesis;
end;
end;
theorem
p`1 <> q`1 & p`2 = q`2 implies |[(p`1+q`1)/2,p`2]| in LSeg(p,q)
proof
set p1 = |[(p`1+q`1)/2,p`2]|;
assume that
A1: p`1 <> q`1 and
A2: p`2 = q`2;
A3: p = |[p`1,p`2]| & q = |[q`1,p`2]| by A2,EUCLID:53;
A4: p1`1 = (p`1+q`1)/2 & p1`2 = p`2;
per cases by A1,XXREAL_0:1;
suppose
A5: p`1 < q`1;
then p`1 <= (p`1+q`1)/2 & (p`1+q`1)/2 <= q`1 by XREAL_1:226;
then p1 in {p2: p2`2 = p`2 & p`1 <= p2`1 & p2`1 <= q`1} by A4;
hence thesis by A3,A5,Th10;
end;
suppose
A6: p`1 > q`1;
then q`1 <= (p`1+q`1)/2 & (p`1+q`1)/2 <= p`1 by XREAL_1:226;
then p1 in {p2: p2`2 = p`2 & q`1 <= p2`1 & p2`1 <= p`1} by A4;
hence thesis by A3,A6,Th10;
end;
end;
theorem
p`1 = q`1 & p`2 <> q`2 implies |[p`1,(p`2+q`2)/2]| in LSeg(p,q)
proof
set p1 = |[p`1,(p`2+q`2)/2]|;
assume that
A1: p`1 = q`1 and
A2: p`2 <> q`2;
A3: p = |[p`1,p`2]| & q = |[p`1,q`2]| by A1,EUCLID:53;
A4: p1`1 = p`1 & p1`2 = (p`2+q`2)/2;
per cases by A2,XXREAL_0:1;
suppose
A5: p`2 < q`2;
then p`2 <= (p`2+q`2)/2 & (p`2+q`2)/2 <= q`2 by XREAL_1:226;
then p1 in {p2: p2`1 = p`1 & p`2 <= p2`2 & p2`2 <= q`2} by A4;
hence thesis by A3,A5,Th9;
end;
suppose
A6: p`2 > q`2;
then q`2 <= (p`2+q`2)/2 & (p`2+q`2)/2 <= p`2 by XREAL_1:226;
then p1 in {p2: p2`1 = p`1 & q`2 <= p2`2 & p2`2 <= p`2} by A4;
hence thesis by A3,A6,Th9;
end;
end;
theorem Th15:
for i,j be Nat holds f = <* p,p1,q *> & i<>0 & j>i+1 implies LSeg(f,j) = {}
proof
let i,j be Nat;
assume that
A1: f = <* p,p1,q *> and
A2: i<>0 and
A3: j>i+1;
i>=0+1 by A2,NAT_1:13;
then 1+i>=1+1 by XREAL_1:7;
then j>2 by A3,XXREAL_0:2;
then j>=2+1 by NAT_1:13;
then
A4: j+1 > 3 by NAT_1:13;
len f = 3 by A1,FINSEQ_1:45;
hence thesis by A4,TOPREAL1:def 3;
end;
theorem
f = <* p1,p2,p3 *> implies L~f = LSeg(p1,p2) \/ LSeg(p2,p3)
proof
set M = {LSeg(f,i) : 1 <= i & i+1 <= len f };
assume
A1: f = <* p1,p2,p3 *>;
then
A2: len f = 2+1 by FINSEQ_1:45;
A3: f/.3=p3 by A1,FINSEQ_4:18;
A4: f/.1=p1 by A1,FINSEQ_4:18;
A5: f/.2=p2 by A1,FINSEQ_4:18;
A6: 1+1 in dom f by A1,Th1;
M = {LSeg(p1,p2),LSeg(p2,p3)}
proof
thus M c= {LSeg(p1,p2),LSeg(p2,p3)}
proof
let x be object;
assume x in M;
then consider j such that
A7: x = LSeg(f,j) and
A8: 1<=j and
A9: j+1<=len f;
j <= 2 by A2,A9,XREAL_1:6;
then j = 0 or ... or j = 2;
then per cases by A8;
suppose
j=1;
then x = LSeg(p1,p2) by A4,A5,A7,A9,TOPREAL1:def 3;
hence thesis by TARSKI:def 2;
end;
suppose
j=2;
then x = LSeg(p2,p3) by A2,A5,A3,A7,TOPREAL1:def 3;
hence thesis by TARSKI:def 2;
end;
end;
let x be object such that
A10: x in {LSeg(p1,p2),LSeg(p2,p3)};
per cases by A10,TARSKI:def 2;
suppose
A11: x = LSeg(p1,p2);
A12: 1+1 <= len f by A2;
x=LSeg(f,1) by A2,A4,A5,A6,A11,TOPREAL1:def 3;
hence thesis by A12;
end;
suppose
x = LSeg(p2,p3);
then x=LSeg(f,2) by A2,A5,A3,TOPREAL1:def 3;
hence thesis by A2;
end;
end;
hence thesis by ZFMISC_1:75;
end;
theorem Th17:
j in dom(f|i) & j+1 in dom(f|i) implies LSeg(f,j) = LSeg(f|i,j)
proof
assume that
A1: j in dom(f|i) and
A2: j+1 in dom(f|i);
A3: 1 <= j & j+1 <= len(f|i) by A1,A2,FINSEQ_3:25;
set p1 = (f|i)/.j, p2 = (f|i)/.(j+1);
A4: f|i = f| (Seg i) by FINSEQ_1:def 16;
then j in dom f /\ (Seg i) by A1,RELAT_1:61;
then j in dom f by XBOOLE_0:def 4;
then
A5: 1 <= j by FINSEQ_3:25;
j+1 in dom f /\ (Seg i) by A2,A4,RELAT_1:61;
then j+1 in dom f by XBOOLE_0:def 4;
then
A6: j+1 <= len f by FINSEQ_3:25;
p1 = f/.j & p2 = f/.(j+1) by A1,A2,FINSEQ_4:70;
then LSeg(f,j) = LSeg(p1,p2) by A5,A6,TOPREAL1:def 3;
hence thesis by A3,TOPREAL1:def 3;
end;
theorem
j in dom f & j+1 in dom f implies LSeg(f^h,j) = LSeg(f,j)
proof
assume that
A1: j in dom f and
A2: j+1 in dom f;
A3: 1 <= j & j+1 <= len f by A1,A2,FINSEQ_3:25;
dom f c= dom(f^h) by FINSEQ_1:26;
then
A4: j+1 <= len(f^h) by A2,FINSEQ_3:25;
set p1 = f/.j, p2 = f/.(j+1);
A5: 1 <= j by A1,FINSEQ_3:25;
p1 = (f^h)/.j & p2 = (f^h)/.(j+1) by A1,A2,FINSEQ_4:68;
then LSeg(f^h,j) = LSeg(p1,p2) by A5,A4,TOPREAL1:def 3;
hence thesis by A3,TOPREAL1:def 3;
end;
theorem Th19:
for f being FinSequence of TOP-REAL n,i being Nat holds LSeg(f,i ) c= L~f
proof
let f be FinSequence of TOP-REAL n,i be Nat;
let x be object such that
A1: x in LSeg(f,i);
now
per cases;
case
i < 1;
hence contradiction by A1,TOPREAL1:def 3;
end;
case
A2: i >= 1;
now
per cases;
case
i+1 > len f;
hence contradiction by A1,TOPREAL1:def 3;
end;
case
A3: i+1 <= len f;
set M = {LSeg(f,j) : 1<=j & j+1<=len f};
LSeg(f,i) in M by A2,A3;
hence thesis by A1,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
L~(f|i) c= L~f
proof
set h = f|i, Mh = {LSeg(h,n) : 1<=n & n+1<=len h}, Mf = {LSeg(f,m) : 1<=m &
m+1<=len f};
let x be object;
A1: h = f|Seg i by FINSEQ_1:def 16;
A2: dom f = Seg len f by FINSEQ_1:def 3;
assume
A3: x in L~h;
then consider X be set such that
A4: x in X and
A5: X in Mh by TARSKI:def 4;
consider k such that
A6: X = LSeg(h,k) and
A7: 1<=k and
A8: k+1<=len h by A5;
per cases;
suppose
A9: i in dom f;
A10: dom h=dom f /\ Seg i by A1,RELAT_1:61;
A11: i in NAT by ORDINAL1:def 12;
A12: i<=len f by A9,FINSEQ_3:25;
then Seg i c= dom f by A2,FINSEQ_1:5;
then dom h = Seg i by A10,XBOOLE_1:28;
then len h <= len f by A12,A11,FINSEQ_1:def 3;
then
A13: k+1<=len f by A8,XXREAL_0:2;
k <= k+1 by NAT_1:12;
then k <= len h by A8,XXREAL_0:2;
then
A14: k in dom h by A7,FINSEQ_3:25;
1<=k+1 by NAT_1:12;
then k+1 in dom h by A8,FINSEQ_3:25;
then X = LSeg(f,k) by A6,A14,Th17;
then X in Mf by A7,A13;
hence thesis by A4,TARSKI:def 4;
end;
suppose
A15: not i in dom f;
now
per cases by A15,FINSEQ_3:25;
case
i<1;
then i<0+1;
then i<=0 by NAT_1:13;
then Seg i = {};
then dom h = dom f /\ {} by A1,RELAT_1:61;
then dom h = {};
then Seg len h = {} by FINSEQ_1:def 3;
then len h = 0;
hence contradiction by A3,TOPREAL1:22;
end;
case
len f<i;
then Seg len f c= Seg i by FINSEQ_1:5;
then dom f c= Seg i by FINSEQ_1:def 3;
then
A16: dom f = dom f /\ (Seg i) by XBOOLE_1:28;
for x being object st x in dom h holds h.x = f.x by A1,FUNCT_1:47;
then h = f by A1,A16,RELAT_1:61;
hence thesis by A4,A5,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
theorem Th21:
for p1,p2 being Point of TOP-REAL N, u being Point of Euclid N
st p1 in Ball(u,r) & p2 in Ball(u,r) holds LSeg(p1,p2) c= Ball(u,r)
proof
let p1,p2 be Point of TOP-REAL N, u be Point of Euclid N;
assume that
A1: p1 in Ball(u,r) and
A2: p2 in Ball(u,r);
reconsider p9=p1 as Point of Euclid N by A1;
A3: dist(p9,u)<r by A1,METRIC_1:11;
thus LSeg(p1,p2) c= Ball(u,r)
proof
p2 in {u4 where u4 is Point of Euclid N : dist(u,u4)<r} by A2,METRIC_1:17;
then
A4: ex u4 be Point of Euclid N st u4=p2 & dist(u,u4)<r;
reconsider q29=u as Element of REAL N;
let a be object;
reconsider q2=q29 as Point of TOP-REAL N by EUCLID:22;
assume a in LSeg(p1,p2);
then consider lambda such that
A5: (1-lambda)*p1 + lambda*p2=a and
A6: 0 <= lambda and
A7: lambda <= 1;
A8: lambda=|.lambda.| by A6,ABSVALUE:def 1;
set p = (1-lambda)*p1 + lambda*p2;
reconsider p9=p,p19=p1,p29=p2 as Element of REAL N by EUCLID:22;
reconsider u5=(1-lambda)*p1 + lambda*p2 as Point of Euclid N by EUCLID:22;
A9: (Pitag_dist N).(q29,p9)=|.q29-p9.| & (Pitag_dist N).(u,u5)=dist(u,u5)
by EUCLID:def 6,METRIC_1:def 1;
(Pitag_dist N).(q29,p29)=|.q29-p29.| by EUCLID:def 6;
then
A10: |.q29+-p29.| < r by A4,METRIC_1:def 1;
A11: 0 <= 1-lambda by A7,XREAL_1:48;
then
A12: 1-lambda= |.1-lambda.| by ABSVALUE:def 1;
consider u3 being Point of Euclid N such that
A13: u3=p1 and
A14: dist(u,u3)<r by A3;
A15: (Pitag_dist N).(q29,p19)=|.q29-p19.| by EUCLID:def 6;
then
A16: dist(u,u3) = |.q29-p19.| by A13,METRIC_1:def 1;
|.1-lambda.|*|.q29+-p19.| < (1-lambda)*r & |.lambda.|*|.q29 + -p29
.| <= lambda*r or |.1-lambda.|*|.q29+-p19.| <= (1-lambda)*r & |.lambda.|*|.
q29 + -p29.| < lambda*r
proof
per cases by A6;
suppose
lambda=0;
hence thesis by A13,A14,A15,A12,A8,METRIC_1:def 1;
end;
suppose
lambda>0;
hence thesis by A14,A16,A10,A11,A12,A8,XREAL_1:64,68;
end;
end;
then
A17: |.1-lambda.|*|.q29+-p19.| + |.lambda.|*|.q29 + -p29.| < (1-lambda)*
r + lambda*r by XREAL_1:8;
q29-p19 = q2-p1 by EUCLID:69;
then
A18: q29-p9 = q2-p & (1-lambda)*(q29-p19) = (1-lambda)*(q2-p1) by EUCLID:65,69;
q29-p29 = q2-p2 by EUCLID:69;
then
A19: lambda*(q29 -p29) = lambda*(q2 -p2) by EUCLID:65;
q2 - p = (1-lambda+lambda)*q2-((1-lambda)*p1 + lambda*p2) by RLVECT_1:def 8
.= (1-lambda)*q2+lambda*q2-((1-lambda)*p1 + lambda*p2) by RLVECT_1:def 6
.= (1-lambda)*q2+lambda*q2+-((1-lambda)*p1 + lambda*p2)
.= (1-lambda)*q2+lambda*q2+(-(1-lambda)*p1 - lambda*p2) by RLVECT_1:30
.= (1-lambda)*q2+lambda*q2+-(1-lambda)*p1 + -lambda*p2 by RLVECT_1:def 3
.= (1-lambda)*q2+-(1-lambda)*p1+lambda*q2 + -lambda*p2 by RLVECT_1:def 3
.= (1-lambda)*q2+(1-lambda)*(-p1)+lambda*q2 + -lambda*p2 by RLVECT_1:25
.= (1-lambda)*(q2+-p1)+lambda*q2 + -lambda*p2 by RLVECT_1:def 5
.= (1-lambda)*(q2+-p1)+(lambda*q2 + -lambda*p2) by RLVECT_1:def 3
.= (1-lambda)*(q2+-p1)+(lambda*q2 + lambda*(-p2)) by RLVECT_1:25
.= (1-lambda)*(q2-p1)+(lambda*(q2 -p2)) by RLVECT_1:def 5;
then q29-p9 = (1-lambda)*(q29-p19) + lambda*(q29 -p29) by A18,A19,EUCLID:64
;
then
A20: |. q29-p9 .| <= |.(1-lambda)*(q29-p19).| + |.lambda*(q29 -p29).| by
EUCLID:12;
|.(1-lambda)*(q29+-p19).| + |.lambda*(q29 + -p29).| = |.1-lambda.|*
|.q29+-p19.| + |.lambda*(q29 + -p29).| by EUCLID:11
.= |.1-lambda.|*|.q29+-p19.| + |.lambda.|*|.q29 + -p29.| by EUCLID:11;
then |.q29-p9.| < r by A20,A17,XXREAL_0:2;
then a in {u6 where u6 is Element of Euclid N:dist(u,u6)<r} by A5,A9;
hence thesis by METRIC_1:17;
end;
end;
theorem
u=p1 & p1=|[r1,s1]| & p2=|[r2,s2]| & p=|[r2,s1]| & p2 in Ball(u,r)
implies p in Ball(u,r)
proof
assume that
A1: u=p1 and
A2: p1=|[r1,s1]| and
A3: p2=|[r2,s2]| and
A4: p=|[r2,s1]| and
A5: p2 in Ball(u,r);
reconsider p19= p1, p29= p2,p9=p as Element of REAL 2 by EUCLID:22;
reconsider r1,s1,r2,s2 as Real;
A6: (Pitag_dist 2).(p19,p29)=|.p19-p29.| by EUCLID:def 6;
p2 in {u6 where u6 is Element of Euclid 2:dist(u,u6)<r} by A5,METRIC_1:17;
then ex u5 st u5 = p2 & dist(u,u5)<r;
then
A7: |.p19-p29.| < r by A1,A6,METRIC_1:def 1;
reconsider up=p as Point of Euclid 2 by EUCLID:22;
(Pitag_dist 2).(p19,p9)=|.p19-p9.| by EUCLID:def 6;
then
A8: dist(u,up)=|.p19-p9.| by A1,METRIC_1:def 1;
(s1-s2)^2 >= 0 by XREAL_1:63;
then sqrreal.(s1-s2) >= 0 by RVSUM_1:def 2;
then
A9: sqrreal.(r1-r2)+0 <= sqrreal.(r1-r2) + sqrreal.(s1-s2) by XREAL_1:7;
p19-p9 = p1-p by EUCLID:69;
then (p19-p9)=<*r1-r2,s1-s1*> by A2,A4,Th5;
then sqr (p19-p9) = <* sqrreal.(r1-r2),sqrreal.(s1-s1)*> by FINSEQ_2:36;
then
A10: Sum sqr (p19-p9) = sqrreal.(r1-r2) + sqrreal.0 by RVSUM_1:77
.= sqrreal.(r1-r2) + 0^2 by RVSUM_1:def 2
.= sqrreal.(r1-r2);
p19-p29 = p1-p2 by EUCLID:69;
then (p19-p29)=<*r1-r2,s1-s2*> by A2,A3,Th5;
then sqr (p19-p29) = <* sqrreal.(r1-r2),sqrreal.(s1-s2)*> by FINSEQ_2:36;
then
A11: |.p19-p29.| = sqrt (sqrreal.(r1-r2) + sqrreal.(s1-s2)) by RVSUM_1:77;
(r1-r2)^2 >= 0 by XREAL_1:63;
then sqrreal.(r1-r2) >= 0 by RVSUM_1:def 2;
then |.p19-p9.| <= sqrt(sqrreal.(r1-r2) + sqrreal.(s1-s2)) by A10,A9,
SQUARE_1:26;
then |.p19-p9.| < r by A7,A11,XXREAL_0:2;
then p in {u6 where u6 is Element of Euclid 2:dist(u,u6)<r} by A8;
hence thesis by METRIC_1:17;
end;
theorem
|[s,r1]| in Ball(u,r) & |[s,s1]| in Ball(u,r) implies |[s,(r1+s1)/2]|
in Ball(u,r)
proof
set p = |[s,r1]|, q = |[s,s1]|, p3 = |[s,(r1+s1)/2]|;
assume |[s,r1]| in Ball(u,r) & |[s,s1]| in Ball(u,r);
then
A1: LSeg(|[s,r1]|,|[s,s1]|) c= Ball(u,r) by Th21;
A2: p3`2 = (1 - 1/2)*(p`2) + (1/2)*(q`2)
.= ((1 - 1/2)*p)`2 + (1/2)*(q`2) by Th4
.= ((1 - 1/2)*p)`2 + ((1/2)*q)`2 by Th4
.= ((1 - 1/2)*p + (1/2)*q)`2 by Th2;
p3`1 = (1 - 1/2)*(p`1) + (1/2)*(q`1)
.= ((1 - 1/2)*p)`1 + (1/2)*(q`1) by Th4
.= ((1 - 1/2)*p)`1 + ((1/2)*q)`1 by Th4
.= ((1 - 1/2)*p + (1/2)*q)`1 by Th2;
then p3 = (1 - 1/2)*p + (1/2)*q by A2,Th6;
then p3 in {(1-lambda)*p + lambda*q: 0<=lambda & lambda<=1 };
hence thesis by A1;
end;
theorem
|[r1,s]| in Ball(u,r) & |[s1,s]| in Ball(u,r) implies |[(r1+s1)/2,s]|
in Ball(u,r)
proof
set p = |[r1,s]|, q = |[s1,s]|, p3 = |[(r1+s1)/2,s]|;
assume |[r1,s]| in Ball(u,r) & |[s1,s]| in Ball(u,r);
then
A1: LSeg(|[r1,s]|,|[s1,s]|) c= Ball(u,r) by Th21;
A2: p3`1 = (1 - 1/2)*(p`1) + (1/2)*(q`1)
.= ((1 - 1/2)*p)`1 + (1/2)*(q`1) by Th4
.= ((1 - 1/2)*p)`1 + ((1/2)*q)`1 by Th4
.= ((1 - 1/2)*p + (1/2)*q)`1 by Th2;
p3`2 = (1 - 1/2)*(p`2) + (1/2)*(q`2)
.= ((1 - 1/2)*p)`2 + (1/2)*(q`2) by Th4
.= ((1 - 1/2)*p)`2 + ((1/2)*q)`2 by Th4
.= ((1 - 1/2)*p + (1/2)*q)`2 by Th2;
then p3 = (1 - 1/2)*p + (1/2)*q by A2,Th6;
then p3 in {(1-lambda)*p + lambda*q: 0<=lambda & lambda<=1 };
hence thesis by A1;
end;
theorem
|[r1,r2]| in Ball(u,r) & |[s1,s2]| in Ball(u,r) implies |[r1,s2]| in
Ball(u,r) or |[s1,r2]| in Ball(u,r)
proof
assume that
A1: |[r1,r2]| in Ball(u,r) and
A2: |[s1,s2]| in Ball(u,r);
A3: r > 0 by A1,TBSP_1:12;
per cases;
suppose
|[r1,s2]| in Ball(u,r);
hence thesis;
end;
suppose
A4: not |[r1,s2]| in Ball(u,r);
reconsider p = u as Point of TOP-REAL 2 by EUCLID:22;
set p1 = |[r1,s2]|, p2 = |[s1,r2]|, p3 = |[s1,s2]|, p4 = |[r1,r2]|;
reconsider u1 = p1, u2 = p2, u3 = p3, u4 = p4 as Point of Euclid 2 by
EUCLID:22;
set a = (p`1 - p1`1)^2 + (p`2 - p1`2)^2, b = (p`1 - p4`1)^2 + (p`2 - p4`2)
^2, c = (p`1 - p3`1)^2 + (p`2 - p3`2)^2, d = (p`1 - p2`1)^2 + (p`2 - p2`2)^2;
(Pitag_dist 2).(u,u1) = dist(u,u1) & r <= dist(u,u1) by A4,METRIC_1:11
,def 1;
then r <= sqrt a by Th7;
then
A5: r * r <= (sqrt a)^2 by A3,XREAL_1:66;
(p`1 - p1`1)^2 >= 0 & (p`2 - p1`2)^2 >= 0 by XREAL_1:63;
then
A6: r^2 <= a by A5,SQUARE_1:def 2;
(Pitag_dist 2).(u,u3) = dist(u,u3) & dist(u,u3) < r by A2,METRIC_1:11,def 1
;
then
A10: sqrt c < r by Th7;
A11: (p`1 - p3`1)^2 >= 0 & (p`2 - p3`2)^2 >= 0 by XREAL_1:63;
then 0<=sqrt c by SQUARE_1:def 2;
then (sqrt c)^2 < r*r by A10,XREAL_1:96;
then
A12: c < r*r by A11,SQUARE_1:def 2;
(Pitag_dist 2).(u,u4) = dist(u,u4) & dist(u,u4) < r by A1,METRIC_1:11,def 1
;
then
A13: sqrt b < r by Th7;
c + b = a + d;
then
A14: r^2+d <= c + b by A6,XREAL_1:6;
A15: (p`1 - p4`1)^2 >= 0 & (p`2 - p4`2)^2 >= 0 by XREAL_1:63;
then 0<=sqrt b by SQUARE_1:def 2;
then (sqrt b)^2 < r*r by A13,XREAL_1:96;
then b < r^2 by A15,SQUARE_1:def 2;
then c+b <r^2 + r^2 by A12,XREAL_1:8;
then r^2+d < r^2+r^2 by A14,XXREAL_0:2;
then
A16: d < r^2+r^2 - r^2 by XREAL_1:20;
(p`1 - p2`1)^2 >= 0 & (p`2 - p2`2)^2 >= 0 by XREAL_1:63;
then sqrt d < sqrt(r^2) by A16,SQUARE_1:27;
then
A17: sqrt d < r by A3,SQUARE_1:22;
dist(u,u2) = (Pitag_dist 2).(u,u2) by METRIC_1:def 1
.= sqrt d by Th7;
hence thesis by A17,METRIC_1:11;
end;
end;
theorem
not f/.1 in Ball(u,r) & 1<=m & m<=len f - 1 & (for i st 1<=i & i<=len
f - 1 & LSeg(f,i) /\ Ball(u,r) <> {} holds m<=i) implies not f/.m in Ball(u,r)
proof
assume that
A1: not f/.1 in Ball(u,r) and
A2: 1<=m and
A3: m<=len f - 1 and
A4: for i st 1<=i & i<=len f - 1 & LSeg(f,i) /\ Ball(u,r) <> {} holds m <=i;
assume
A5: f/.m in Ball(u,r);
per cases by A2,XXREAL_0:1;
suppose
1=m;
hence contradiction by A1,A5;
end;
suppose
A6: 1<m;
reconsider k=m-1 as Element of NAT by A6,INT_1:5;
1+1<=m by A6,NAT_1:13;
then
A7: 1<=m-1 by XREAL_1:19;
m-1<=m by XREAL_1:43;
then
A8: k<=len f - 1 by A3,XXREAL_0:2;
then k+1<=len f by XREAL_1:19;
then f/.(k+1) in LSeg(f,k) by A7,TOPREAL1:21;
then LSeg(f,k) /\ Ball(u,r) <> {} by A5,XBOOLE_0:def 4;
then m<=k by A4,A7,A8;
then m+1<=m by XREAL_1:19;
hence contradiction by NAT_1:13;
end;
end;
theorem
for q,p2,p st q`2 = p2`2 & p`2 <> p2`2 holds (LSeg(p2,|[p2`1,p`2]|) \/
LSeg(|[p2`1,p`2]|,p)) /\ LSeg(q,p2) = {p2}
proof
let q,p2,p such that
A1: q`2 = p2`2 and
A2: p`2 <> p2`2;
set p3 = |[(p2)`1,p`2]|;
set l23 = LSeg(p2,p3), l3 = LSeg(p3,p), l = LSeg(q,p2);
A3: l3 /\ l = {}
proof
set x = the Element of l3 /\ l;
assume
A4: l3 /\ l <> {};
then x in l3 by XBOOLE_0:def 4;
then consider s1 being Real such that
A5: x = (1-s1)*p3 + s1*p and
0 <= s1 and
s1 <= 1;
x in l by A4,XBOOLE_0:def 4;
then consider s2 being Real such that
A6: x = (1-s2)*q + s2*p2 and
0 <= s2 and
s2 <= 1;
A7: ((1-s1)*p3 + s1*p)`2 = ((1-s1)*p3) `2 + (s1*p) `2 by Th2
.= (1-s1)*(p3 `2) + (s1*p) `2 by Th4
.= (1-s1)*(p3 `2) + s1*(p `2) by Th4
.= (1-s1)*(p `2) + s1*(p `2)
.= p `2;
((1-s2)*q + s2*p2) `2 = ((1-s2)*q) `2 + (s2*p2) `2 by Th2
.= (1-s2)*(q`2) + (s2*p2) `2 by Th4
.= (1-s2)*(q `2) + s2*(p2 `2) by Th4
.= p2 `2 by A1;
hence contradiction by A2,A5,A7,A6;
end;
A8: l23 /\ l = {p2}
proof
thus l23 /\ l c= {p2}
proof
let x be object;
assume
A9: x in l23 /\ l;
then x in l23 by XBOOLE_0:def 4;
then consider s1 being Real such that
A10: (1-s1)*p2 + s1*p3=x and
0<=s1 and
s1<=1;
x in l by A9,XBOOLE_0:def 4;
then consider s2 being Real such that
A11: (1-s2)*q + s2*p2=x and
0 <= s2 and
s2 <= 1;
A12: ((1-s2)*q + s2*p2) `2 = ((1-s2)*q) `2 + (s2*p2) `2 by Th2
.= (1-s2)*(q`2) + (s2*p2) `2 by Th4
.= (1-s2)*(q `2) + s2*(p2 `2) by Th4
.= p2 `2 by A1;
set t = (1-s1)*p2 + s1*p3;
A13: t`1 = ((1-s1)*p2) `1 + (s1*p3) `1 by Th2
.= (1-s1)*(p2 `1) + (s1*p3) `1 by Th4
.= (1-s1)*(p2 `1) + s1*(p3 `1) by Th4
.= (1-s1)*(p2 `1) + s1*(p2 `1)
.= p2 `1;
t = |[t`1, t`2]| by EUCLID:53
.= p2 by A10,A13,A11,A12,EUCLID:53;
hence thesis by A10,TARSKI:def 1;
end;
let x be object;
assume x in {p2};
then
A14: x=p2 by TARSKI:def 1;
p2 in l23 & p2 in l by RLTOPSP1:68;
hence thesis by A14,XBOOLE_0:def 4;
end;
thus (l23 \/ l3) /\ l = l23 /\ l \/ l3 /\ l by XBOOLE_1:23
.= {p2} by A8,A3;
end;
theorem
for q,p2,p st q`1 = p2`1 & p`1 <> p2`1 holds (LSeg(p2,|[p`1,p2`2]|) \/
LSeg(|[p`1,p2`2]|,p)) /\ LSeg(q,p2) = {p2}
proof
let q,p2,p such that
A1: q`1 = (p2)`1 and
A2: p`1 <> (p2)`1;
set p3 = |[p`1,(p2)`2]|;
set l23 = LSeg(p2,p3), l3 = LSeg(p3,p), l = LSeg(q,p2);
A3: l3 /\ l = {}
proof
set x = the Element of l3 /\ l;
assume
A4: l3 /\ l <> {};
then x in l3 by XBOOLE_0:def 4;
then consider d1 be Real such that
A5: x = (1-d1)*p3 + d1*p and
0 <= d1 and
d1 <= 1;
x in l by A4,XBOOLE_0:def 4;
then consider d2 be Real such that
A6: x = (1-d2)*q + d2*p2 and
0 <= d2 and
d2 <= 1;
A7: ((1-d1)*p3 + d1*p)`1 = ((1-d1)*p3) `1 + (d1*p) `1 by Th2
.= (1-d1)*(p3 `1) + (d1*p) `1 by Th4
.= (1-d1)*(p3 `1) + d1*(p `1) by Th4
.= (1-d1)*(p `1) + d1*(p `1)
.= p `1;
((1-d2)*q + d2*p2) `1 = ((1-d2)*q) `1 + (d2*p2) `1 by Th2
.= (1-d2)*(q`1) + (d2*p2) `1 by Th4
.= (1-d2)*(q `1) + d2*(p2 `1) by Th4
.= p2 `1 by A1;
hence contradiction by A2,A5,A7,A6;
end;
A8: l23 /\ l = {p2}
proof
thus l23 /\ l c= {p2}
proof
let x be object;
assume
A9: x in l23 /\ l;
then x in l23 by XBOOLE_0:def 4;
then consider s1 being Real such that
A10: x = (1-s1)*p2 + s1*p3 and
0 <= s1 and
s1 <= 1;
x in l by A9,XBOOLE_0:def 4;
then consider s2 being Real such that
A11: x = (1-s2)*q + s2*p2 and
0 <= s2 and
s2 <= 1;
A12: ((1-s2)*q + s2*p2) `1 = ((1-s2)*q) `1 + (s2*p2) `1 by Th2
.= (1-s2)*(q`1) + (s2*p2) `1 by Th4
.= (1-s2)*(q `1) + s2*(p2 `1) by Th4
.= p2 `1 by A1;
set t = (1-s1)*p2 + s1*p3;
A13: t`2 = ((1-s1)*p2) `2 + (s1*p3) `2 by Th2
.= (1-s1)*(p2 `2) + (s1*p3) `2 by Th4
.= (1-s1)*(p2 `2) + s1*(p3 `2) by Th4
.= (1-s1)*(p2 `2) + s1*(p2 `2)
.= p2 `2;
t = |[t`1, t`2]| by EUCLID:53
.= p2 by A10,A13,A11,A12,EUCLID:53;
hence thesis by A10,TARSKI:def 1;
end;
let x be object;
assume x in {p2};
then
A14: x=p2 by TARSKI:def 1;
p2 in l23 & p2 in l by RLTOPSP1:68;
hence thesis by A14,XBOOLE_0:def 4;
end;
thus (l23 \/ l3) /\ l = l23 /\ l \/ l3 /\ l by XBOOLE_1:23
.= {p2} by A8,A3;
end;
theorem Th29:
LSeg(p,|[p`1,q`2]|) /\ LSeg(|[p`1,q`2]|,q) ={|[p`1,q`2]|}
proof
set p3 = |[p`1,q`2]|;
set l23 = LSeg(p,p3), l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof
let x be object;
assume
A1: x in l23 /\ l;
then x in l23 by XBOOLE_0:def 4;
then consider d1 be Real such that
A2: x = (1-d1)*p + d1*p3 and
0 <= d1 and
d1 <= 1;
x in l by A1,XBOOLE_0:def 4;
then consider d2 be Real such that
A3: x = (1-d2)*p3 + d2*q and
0 <= d2 and
d2 <= 1;
set t = (1-d1)*p + d1*p3;
A4: t`1 = ((1-d1)*p) `1 + (d1*p3) `1 by Th2
.= (1-d1)*(p `1) + (d1*p3) `1 by Th4
.= (1-d1)*(p `1) + d1*(p3 `1) by Th4
.= (1-d1)*(p `1) + d1*(p `1)
.= p3 `1;
t`2 = ((1-d2)*p3) `2 + (d2*q) `2 by A2,A3,Th2
.= (1-d2)*(p3 `2) + (d2*q) `2 by Th4
.= (1-d2)*(p3 `2) + d2*(q`2) by Th4
.= (1-d2)*(q`2) + d2*(q`2)
.= p3 `2;
then t = p3 by A4,Th6;
hence thesis by A2,TARSKI:def 1;
end;
let x be object;
assume x in {p3};
then
A5: x=p3 by TARSKI:def 1;
p3 in l23 & p3 in l by RLTOPSP1:68;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th30:
LSeg(p,|[q`1,p`2]|) /\ LSeg(|[q`1,p`2]|,q) ={|[q`1,p`2]|}
proof
set p3 = |[q`1,p`2]|;
set l23 = LSeg(p,p3), l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof
let x be object;
assume
A1: x in l23 /\ l;
then x in l23 by XBOOLE_0:def 4;
then consider d1 be Real such that
A2: x = (1-d1)*p + d1*p3 and
0 <= d1 and
d1 <= 1;
x in l by A1,XBOOLE_0:def 4;
then consider d2 be Real such that
A3: x = (1-d2)*p3 + d2*q and
0 <= d2 and
d2 <= 1;
set t = (1-d1)*p + d1*p3;
A4: t`2 = ((1-d1)*p) `2 + (d1*p3) `2 by Th2
.= (1-d1)*(p `2) + (d1*p3) `2 by Th4
.= (1-d1)*(p `2) + d1*(p3 `2) by Th4
.= (1-d1)*(p3 `2) + d1*(p3 `2)
.= p3 `2;
t`1 = ((1-d2)*p3) `1 + (d2*q) `1 by A2,A3,Th2
.= (1-d2)*(p3 `1) + (d2*q) `1 by Th4
.= (1-d2)*(p3 `1) + d2*(q`1) by Th4
.= (1-d2)*(p3`1) + d2*(p3`1)
.= p3`1;
then t = p3 by A4,Th6;
hence thesis by A2,TARSKI:def 1;
end;
let x be object;
assume x in {p3};
then
A5: x=p3 by TARSKI:def 1;
p3 in l23 & p3 in l by RLTOPSP1:68;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th31:
p`1 = q`1 & p`2 <> q`2 implies LSeg(p,|[p`1,(p`2+q`2)/2]|) /\
LSeg(|[p`1,(p`2+q`2)/2]|,q)={|[p`1,(p`2+q`2)/2]|}
proof
assume that
A1: p`1 = q`1 and
A2: p`2 <> q`2;
set p3 = |[p`1,(p`2+q`2)/2]|;
set l23 = LSeg(p,p3), l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof
let x be object;
A3: l23 = LSeg(|[p`1,p`2]|,|[p`1,(p`2+q`2)/2]|) by EUCLID:53;
assume
A4: x in l23 /\ l;
then
A5: x in l by XBOOLE_0:def 4;
A6: l = LSeg(|[q`1,(p`2+q`2)/2]|,|[q`1,q`2]|) by A1,EUCLID:53;
A7: x in l23 by A4,XBOOLE_0:def 4;
now
per cases by A2,XXREAL_0:1;
suppose
A8: p`2 < q`2;
then p`2 < (p`2+q`2)/2 by XREAL_1:226;
then x in {p1: p1 `1 = p`1 & p`2 <= p1 `2 & p1 `2 <= (p`2+q`2)/2} by A7
,A3,Th9;
then consider t1 be Point of TOP-REAL 2 such that
A9: t1 = x and
A10: t1 `1 = p`1 and
p`2 <= t1 `2 and
A11: t1 `2 <= (p`2+q`2)/2;
A12: t1`2 <= p3 `2 by A11;
(p`2+q`2)/2 < q`2 by A8,XREAL_1:226;
then x in {p2: p2 `1 = q`1 & (p`2+q`2)/2 <= p2 `2 & p2 `2 <= q`2} by A5
,A6,Th9;
then
ex t2 be Point of TOP-REAL 2 st t2 = x & t2 `1 = q`1 & (p`2+q`2)/
2 <= t2 `2 & t2 `2 <= q`2;
then t1`2 >= p3 `2 by A9;
then
A13: t1`2 = p3 `2 by A12,XXREAL_0:1;
t1 `1 = p3 `1 by A10;
hence x=p3 by A9,A13,Th6;
end;
suppose
A14: p`2 > q`2;
then p`2 > (p`2+q`2)/2 by XREAL_1:226;
then x in {p11: p11 `1 = p`1 & (p`2+q`2)/2<=p11 `2 & p11 `2<= p`2} by
A7,A3,Th9;
then consider t1 be Point of TOP-REAL 2 such that
A15: t1 = x and
A16: t1 `1 = p`1 and
A17: (p`2+q`2)/2 <= t1 `2 and
t1 `2 <= p`2;
A18: p3 `2 <= t1 `2 by A17;
q`2 < (p`2+q`2)/2 by A14,XREAL_1:226;
then
x in {p22: p22 `1=q`1 & q`2<=p22 `2 & p22 `2<=(p`2+q`2)/2} by A5,A6,Th9
;
then ex t2 be Point of TOP-REAL 2 st t2 = x & t2 `1 = q`1 & q`2 <= t2
`2 & t2 `2 <= (p`2+q`2)/2;
then t1`2 <= p3 `2 by A15;
then
A19: t1`2 = p3 `2 by A18,XXREAL_0:1;
t1 `1 = p3 `1 by A16;
hence x=p3 by A15,A19,Th6;
end;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {p3};
then
A20: x=p3 by TARSKI:def 1;
p3 in l23 & p3 in l by RLTOPSP1:68;
hence thesis by A20,XBOOLE_0:def 4;
end;
theorem Th32:
p`1 <> q`1 & p`2 = q`2 implies LSeg(p,|[(p`1+q`1)/2,p`2]|) /\
LSeg(|[(p`1+q`1)/2,p`2]|,q)={|[(p`1+q`1)/2,p`2]|}
proof
assume that
A1: p`1 <> q`1 and
A2: p`2 = q`2;
set p3 = |[(p`1+q`1)/2,p`2]|;
set l23 = LSeg(p,p3), l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof
let x be object;
A3: l23 = LSeg(|[p`1,p`2]|,|[(p`1+q`1)/2,p`2]|) by EUCLID:53;
assume
A4: x in l23 /\ l;
then
A5: x in l by XBOOLE_0:def 4;
A6: l = LSeg(|[(p`1+q`1)/2,q`2]|,|[q`1,q`2]|) by A2,EUCLID:53;
A7: x in l23 by A4,XBOOLE_0:def 4;
now
per cases by A1,XXREAL_0:1;
suppose
A8: p`1 < q`1;
then p`1 < (p`1+q`1)/2 by XREAL_1:226;
then x in {p1: p1 `2 = p`2 & p`1 <= p1 `1 & p1 `1 <= (p`1+q`1)/2} by A7
,A3,Th10;
then consider t1 be Point of TOP-REAL 2 such that
A9: t1 = x and
A10: t1 `2 = p`2 and
p`1 <= t1 `1 and
A11: t1 `1 <= (p`1+q`1)/2;
A12: t1`1 <= p3 `1 by A11;
(p`1+q`1)/2 < q`1 by A8,XREAL_1:226;
then x in {p2: p2 `2 = q`2 & (p`1+q`1)/2 <= p2 `1 & p2 `1 <= q`1} by A5
,A6,Th10;
then
ex t2 be Point of TOP-REAL 2 st t2 = x & t2 `2 = q`2 & (p`1+q`1)/
2 <= t2 `1 & t2 `1 <= q`1;
then t1`1 >= p3 `1 by A9;
then
A13: t1 `1 = p3 `1 by A12,XXREAL_0:1;
t1`2 = p3 `2 by A10;
hence x=p3 by A9,A13,Th6;
end;
suppose
A14: p`1 > q`1;
then p`1 > (p`1+q`1)/2 by XREAL_1:226;
then x in {p11: p11 `2 = p`2 & (p`1+q`1)/2 <= p11 `1 & p11 `1 <= p`1}
by A7,A3,Th10;
then consider t1 be Point of TOP-REAL 2 such that
A15: t1 = x and
A16: t1 `2 = p`2 and
A17: (p`1+q`1)/2 <= t1 `1 and
t1 `1 <= p`1;
A18: p3 `1 <= t1 `1 by A17;
q`1 < (p`1+q`1)/2 by A14,XREAL_1:226;
then x in {p22: p22 `2 = q`2 & q`1<=p22 `1 & p22 `1<= (p`1+q`1)/2} by
A5,A6,Th10;
then ex t2 be Point of TOP-REAL 2 st t2 = x & t2 `2 = q`2 & q`1 <= t2
`1 & t2 `1 <= (p`1+q`1)/2;
then t1`1 <= p3 `1 by A15;
then
A19: t1 `1 = p3 `1 by A18,XXREAL_0:1;
t1`2 = p3 `2 by A16;
hence x=p3 by A15,A19,Th6;
end;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {p3};
then
A20: x=p3 by TARSKI:def 1;
p3 in l23 & p3 in l by RLTOPSP1:68;
hence thesis by A20,XBOOLE_0:def 4;
end;
theorem
i>2 & i in dom f & f is being_S-Seq implies f|i is being_S-Seq
proof
assume that
A1: i>2 and
A2: i in dom f and
A3: f is being_S-Seq;
A4: f|i = f|Seg i by FINSEQ_1:def 16;
then
A5: dom(f|i)=dom f /\ Seg i by RELAT_1:61;
thus f|i is one-to-one
proof
A6: f is one-to-one by A3;
let x,y be object;
assume that
A7: x in dom (f|i) and
A8: y in dom (f|i) and
A9: (f|i).x = (f|i).y;
A10: x in dom f & y in dom f by A5,A7,A8,XBOOLE_0:def 4;
f.x = (f|i).x by A4,A7,FUNCT_1:47
.= f.y by A4,A8,A9,FUNCT_1:47;
hence thesis by A6,A10;
end;
A11: i<=len f by A2,FINSEQ_3:25;
A12: i in NAT by ORDINAL1:def 12;
Seg len f = dom f by FINSEQ_1:def 3;
then Seg i c= dom f by A11,FINSEQ_1:5;
then
A13: dom (f|i) = Seg i by A5,XBOOLE_1:28;
hence len (f|i) >= 2 by A1,A12,FINSEQ_1:def 3;
A14: f is unfolded by A3;
thus f|i is unfolded
proof
let j be Nat such that
A15: 1 <= j and
A16: j + 2 <= len (f|i);
j + 1 <= j + 2 by XREAL_1:6;
then
A17: j+1 <= len(f|i) by A16,XXREAL_0:2;
len(f|i) <= len f by A11,A13,A12,FINSEQ_1:def 3;
then
A18: j + 2 <= len f by A16,XXREAL_0:2;
1<=j+1 by NAT_1:12;
then
A19: j+1 in dom(f|i) by A17,FINSEQ_3:25;
1<=j+1+1 by NAT_1:12;
then j+1+1 in dom(f|i) by A16,FINSEQ_3:25;
then
A20: LSeg(f,j+1) = LSeg(f|i,j+1) by A19,Th17;
j <= j+2 by NAT_1:11;
then j <= len(f|i) by A16,XXREAL_0:2;
then j in dom(f|i) by A15,FINSEQ_3:25;
then LSeg(f,j) = LSeg(f|i,j) by A19,Th17;
then LSeg(f|i,j) /\ LSeg(f|i,j+1) = {f/.(j+1)} by A14,A15,A18,A20;
hence thesis by A19,FINSEQ_4:70;
end;
A21: f is s.n.c. by A3;
thus f|i is s.n.c.
proof
let n,k be Nat;
A22: k+1 >= 1 by NAT_1:11;
A23: n+1 >= 1 by NAT_1:11;
assume n+1 < k;
then LSeg(f,n) misses LSeg(f,k) by A21;
then
A24: LSeg(f,n) /\ LSeg(f,k) = {};
A25: k+1 >= k by NAT_1:11;
A26: n+1 >= n by NAT_1:11;
per cases;
suppose
A27: n in dom(f|i);
now
per cases;
suppose
n+1 in dom(f|i);
then
A28: LSeg(f,n)=LSeg(f|i,n) by A27,Th17;
now
per cases;
suppose
A29: k in dom (f|i);
now
per cases;
suppose
k+1 in dom(f|i);
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {} by A24,A28,A29,Th17;
end;
suppose
not k+1 in dom(f|i);
then k+1 > len(f|i) by A22,FINSEQ_3:25;
then LSeg(f|i,k) = {} by TOPREAL1:def 3;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
end;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
suppose
not k in dom (f|i);
then k < 1 or k > len(f|i) by FINSEQ_3:25;
then k < 1 or k+1 > len(f|i) by A25,XXREAL_0:2;
then LSeg(f|i,k) = {} by TOPREAL1:def 3;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
end;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
suppose
not n+1 in dom(f|i);
then n+1 > len(f|i) by A23,FINSEQ_3:25;
then LSeg(f|i,n) = {} by TOPREAL1:def 3;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
end;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
suppose
not n in dom(f|i);
then n < 1 or n > len(f|i) by FINSEQ_3:25;
then n < 1 or n+1 > len(f|i) by A26,XXREAL_0:2;
then LSeg(f|i,n) = {} by TOPREAL1:def 3;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
end;
let j be Nat such that
A30: 1 <= j and
A31: j + 1 <= len (f|i);
len(f|i) <= len f by A11,A13,A12,FINSEQ_1:def 3;
then
A32: j + 1 <= len f by A31,XXREAL_0:2;
j <= j + 1 by NAT_1:11;
then j <= len(f|i) by A31,XXREAL_0:2;
then j in dom (f|i) by A30,FINSEQ_3:25;
then
A33: (f|i)/.j=f/.j by FINSEQ_4:70;
1<=j+1 by NAT_1:12;
then j+1 in dom(f|i) by A31,FINSEQ_3:25;
then
A34: (f|i)/.(j+1)=f/.(j+1) by FINSEQ_4:70;
f is special by A3;
hence thesis by A30,A32,A33,A34;
end;
theorem
p`1 <> q`1 & p`2 <> q`2 & f = <* p,|[p`1,q`2]|,q *> implies f/.1 = p &
f/.len f = q & f is being_S-Seq
proof
set p1 = |[p`1,q`2]|;
assume that
A1: p`1 <> q`1 and
A2: p`2 <> q`2 and
A3: f = <* p,p1,q *>;
A4: len f = 1 + 2 by A3,FINSEQ_1:45;
hence f/.1 = p & f/.len f = q by A3,FINSEQ_4:18;
p<>p1 & q<>p1 by A1,A2;
hence f is one-to-one & len f>=2 by A1,A3,A4,FINSEQ_3:95;
A5: f/.2 = p1 by A3,FINSEQ_4:18;
A6: f/.3 = q by A3,FINSEQ_4:18;
A7: f/.1 = p by A3,FINSEQ_4:18;
thus f is unfolded
proof
let i be Nat;
assume that
A8: 1 <= i and
A9: i + 2 <= len f;
i <= 1 by A4,A9,XREAL_1:6;
then
A10: i = 1 by A8,XXREAL_0:1;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2) by A4,A7,A5,
TOPREAL1:def 3
.= LSeg(p,p1) /\ LSeg(p1,q) by A4,A5,A6,TOPREAL1:def 3
.= {f/.(i+1)} by A5,A10,Th29;
end;
thus f is s.n.c.
proof
let i,j be Nat such that
A11: i+1 < j;
now
per cases;
suppose
i=0;
then LSeg(f,i)={} by TOPREAL1:def 3;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
suppose
i<>0;
then LSeg(f,j)={} by A3,A11,Th15;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
end;
hence thesis;
end;
let i be Nat such that
A12: 1 <= i and
A13: i + 1 <= len f;
i <= 2 by A4,A13,XREAL_1:6;
then i = 0 or ... or i = 2;
then per cases by A12;
suppose i=1;
hence thesis by A7,A5;
end;
suppose i=2;
hence thesis by A5,A6;
end;
end;
theorem
p`1 <> q`1 & p`2 <> q`2 & f = <* p,|[q`1,p`2]|,q *> implies f/.1 = p &
f/.len f = q & f is being_S-Seq
proof
set p1 = |[q`1,p`2]|;
assume that
A1: p`1 <> q`1 and
A2: p`2 <> q`2 and
A3: f = <* p,p1,q *>;
A4: len f = 1 + 2 by A3,FINSEQ_1:45;
hence f/.1 = p & f/.len f = q by A3,FINSEQ_4:18;
p<>p1 & q<>p1 by A1,A2;
hence f is one-to-one & len f >= 2 by A1,A3,A4,FINSEQ_3:95;
A5: f/.2 = p1 by A3,FINSEQ_4:18;
A6: f/.3 = q by A3,FINSEQ_4:18;
A7: f/.1 = p by A3,FINSEQ_4:18;
thus f is unfolded
proof
let i be Nat;
assume that
A8: 1 <= i and
A9: i + 2 <= len f;
i <= 1 by A4,A9,XREAL_1:6;
then
A10: i = 1 by A8,XXREAL_0:1;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2) by A4,A7,A5,
TOPREAL1:def 3
.= LSeg(p,p1) /\ LSeg(p1,q) by A4,A5,A6,TOPREAL1:def 3
.= {f/.(i+1)} by A5,A10,Th30;
end;
thus f is s.n.c.
proof
let i,j be Nat such that
A11: i+1 < j;
now
per cases;
suppose
i=0;
then LSeg(f,i)={} by TOPREAL1:def 3;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
suppose
i<>0;
then LSeg(f,j)={} by A3,A11,Th15;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
end;
hence thesis;
end;
let i be Nat such that
A12: 1 <= i and
A13: i + 1 <= len f;
i <= 2 by A4,A13,XREAL_1:6;
then i = 0 or ... or i = 2;
then per cases by A12;
suppose i=1;
hence thesis by A7,A5;
end;
suppose i=2;
hence thesis by A5,A6;
end;
end;
theorem
p`1 = q`1 & p`2 <> q`2 & f = <* p,|[p`1,(p`2 + q`2)/2]|,q *> implies f
/.1 = p & f/.len f = q & f is being_S-Seq
proof
set p1 = |[p`1,(p`2 + q`2)/2]|;
assume that
A1: p`1 = q`1 and
A2: p`2 <> q`2 and
A3: f = <* p,p1,q *>;
A4: p1`2 = (p`2+q`2)/2;
A5: len f = 1 + 2 by A3,FINSEQ_1:45;
hence f/.1 = p & f/.len f = q by A3,FINSEQ_4:18;
p`2 <> (p`2+q`2)/2 & q`2 <> (p`2+q`2)/2 by A2;
hence f is one-to-one & len f >= 2 by A2,A3,A5,A4,FINSEQ_3:95;
A6: f/.2 = p1 by A3,FINSEQ_4:18;
A7: f/.3 = q by A3,FINSEQ_4:18;
A8: f/.1 = p by A3,FINSEQ_4:18;
thus f is unfolded
proof
let i be Nat;
assume that
A9: 1 <= i and
A10: i + 2 <= len f;
i <= 1 by A5,A10,XREAL_1:6;
then
A11: i = 1 by A9,XXREAL_0:1;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2) by A5,A8,A6,
TOPREAL1:def 3
.= LSeg(p,p1) /\ LSeg(p1,q) by A5,A6,A7,TOPREAL1:def 3
.= {f/.(i+1)} by A1,A2,A6,A11,Th31;
end;
thus f is s.n.c.
proof
let i,j be Nat such that
A12: i+1 < j;
now
per cases;
suppose
i=0;
then LSeg(f,i)={} by TOPREAL1:def 3;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
suppose
i<>0;
then LSeg(f,j)={} by A3,A12,Th15;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
end;
hence thesis;
end;
let i be Nat such that
A13: 1 <= i and
A14: i + 1 <= len f;
i <= 2 by A5,A14,XREAL_1:6;
then i = 0 or ... or i = 2;
then per cases by A13;
suppose i=1;
hence thesis by A8,A6;
end;
suppose i=2;
hence thesis by A1,A6,A7;
end;
end;
theorem
p`1 <> q`1 & p`2 = q`2 & f = <* p,|[(p`1 + q`1)/2,p`2]|,q *> implies f
/.1 = p & f/.len f = q & f is being_S-Seq
proof
set p1 = |[(p`1 + q`1)/2,p`2]|;
assume that
A1: p`1 <> q`1 and
A2: p`2 = q`2 and
A3: f = <* p,p1,q *>;
A4: p1`1 = (p`1 + q`1)/2;
A5: len f = 1 + 2 by A3,FINSEQ_1:45;
hence f/.1 = p & f/.len f = q by A3,FINSEQ_4:18;
p`1 <> (p`1 + q`1)/2 & q`1 <> (p`1 + q`1)/2 by A1;
hence f is one-to-one & len f >= 2 by A1,A3,A5,A4,FINSEQ_3:95;
A6: f/.2 = p1 by A3,FINSEQ_4:18;
A7: f/.3 = q by A3,FINSEQ_4:18;
A8: f/.1 = p by A3,FINSEQ_4:18;
thus f is unfolded
proof
let i be Nat;
assume that
A9: 1 <= i and
A10: i + 2 <= len f;
i <= 1 by A5,A10,XREAL_1:6;
then
A11: i = 1 by A9,XXREAL_0:1;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2) by A5,A8,A6,
TOPREAL1:def 3
.= LSeg(p,p1) /\ LSeg(p1,q) by A5,A6,A7,TOPREAL1:def 3
.= {f/.(i+1)} by A1,A2,A6,A11,Th32;
end;
thus f is s.n.c.
proof
let i,j be Nat such that
A12: i+1 < j;
now
per cases;
suppose
i=0;
then LSeg(f,i)={} by TOPREAL1:def 3;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
suppose
i<>0;
then LSeg(f,j)={} by A3,A12,Th15;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis;
end;
end;
hence thesis;
end;
let i be Nat such that
A13: 1 <= i and
A14: i + 1 <= len f;
i <= 2 by A5,A14,XREAL_1:6;
then i = 0 or ... or i = 2;
then per cases by A13;
suppose i=1;
hence thesis by A8,A6;
end;
suppose i=2;
hence thesis by A2,A6,A7;
end;
end;
theorem
i in dom f & i+1 in dom f implies L~(f| (i+1)) = L~(f|i) \/ LSeg(f/.i,f
/.(i+1))
proof
set M1={LSeg(f| (i+1),k): 1<=k & k+1<=len(f| (i+1))}, Mi={LSeg(f|i,n): 1<=n &
n+1<=len(f|i)};
assume that
A1: i in dom f and
A2: i+1 in dom f;
set p = f/.i, q= f/.(i+1);
A3: i+1<=len f by A2,FINSEQ_3:25;
then Seg(i+1) c= Seg len f by FINSEQ_1:5;
then Seg(i+1) c= dom f by FINSEQ_1:def 3;
then Seg(i+1) = dom f /\ Seg(i+1) by XBOOLE_1:28;
then
A4: f| (i+1) = f|Seg(i+1) & Seg(i+1)=dom(f|Seg(i+1)) by FINSEQ_1:def 16
,RELAT_1:61;
then
A5: i+1=len(f| (i+1)) by FINSEQ_1:def 3;
A6: 1<=i by A1,FINSEQ_3:25;
then
A7: LSeg(f,i) = LSeg(p,q) by A3,TOPREAL1:def 3;
1<=i+1 by A2,FINSEQ_3:25;
then
A8: i+1 in dom(f| (i+1)) by A5,FINSEQ_3:25;
A9: i<=i+1 by NAT_1:11;
then i in dom(f| (i+1)) by A6,A5,FINSEQ_3:25;
then
A10: LSeg(f| (i+1),i) = LSeg(p,q) by A7,A8,Th17;
then
A11: LSeg(p,q) c= L~(f| (i+1)) by Th19;
A12: i in NAT by ORDINAL1:def 12;
i<=len f by A1,FINSEQ_3:25;
then Seg i c= Seg len f by FINSEQ_1:5;
then Seg i c= dom f by FINSEQ_1:def 3;
then dom f /\ Seg i = Seg i by XBOOLE_1:28;
then
A13: f|i = f|Seg i & dom(f| (Seg i))=Seg i by FINSEQ_1:def 16,RELAT_1:61;
then
A14: i=len(f|i) by A12,FINSEQ_1:def 3;
A15: Seg len(f| (i+1)) = dom(f| (i+1)) by FINSEQ_1:def 3;
thus L~(f| (i+1)) c= L~(f|i) \/ LSeg(p,q)
proof
let x be object;
assume x in L~(f| (i+1));
then consider X be set such that
A16: x in X and
A17: X in M1 by TARSKI:def 4;
consider m such that
A18: X=LSeg(f| (i+1),m) and
A19: 1<=m and
A20: m+1<=len(f| (i+1)) by A17;
A21: m <= i by A5,A20,XREAL_1:6;
per cases by A21,XXREAL_0:1;
suppose
m = i;
then X c= L~(f|i) \/ LSeg(p,q) by A10,A18,XBOOLE_1:7;
hence thesis by A16;
end;
suppose
A22: m < i;
then m<=i+1 by NAT_1:13;
then
A23: m in dom(f| (i+1)) by A4,A19,FINSEQ_1:1;
A24: m in dom(f|i) by A13,A19,A22,FINSEQ_1:1;
A25: 1<=m+1 by A19,NAT_1:13;
A26: m+1<=i by A22,NAT_1:13;
then
A27: m+1 in dom(f|i) by A13,A25,FINSEQ_1:1;
m+1 in dom(f| (i+1)) by A15,A20,A25,FINSEQ_1:1;
then X = LSeg(f,m) by A18,A23,Th17
.= LSeg(f|i,m) by A24,A27,Th17;
then X in Mi by A14,A19,A26;
then x in union Mi by A16,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object such that
A28: x in L~(f|i) \/ LSeg(p,q);
per cases by A28,XBOOLE_0:def 3;
suppose
x in L~(f|i);
then consider X be set such that
A29: x in X and
A30: X in Mi by TARSKI:def 4;
consider m such that
A31: X=LSeg(f|i,m) and
A32: 1<=m and
A33: m+1<=len(f|i) by A30;
A34: 1<=m+1 by NAT_1:11;
then
A35: m+1 in dom(f|i) by A33,FINSEQ_3:25;
m<=m+1 by NAT_1:11;
then
A36: m<=len(f|i) by A33,XXREAL_0:2;
then m<=len(f| (i+1)) by A5,A14,A9,XXREAL_0:2;
then
A37: m in dom(f| (i+1)) by A32,FINSEQ_3:25;
A38: m+1<=len(f| (i+1)) by A5,A14,A9,A33,XXREAL_0:2;
then
A39: m+1 in dom(f| (i+1)) by A34,FINSEQ_3:25;
m in dom(f|i) by A32,A36,FINSEQ_3:25;
then X = LSeg(f,m) by A31,A35,Th17
.= LSeg(f| (i+1),m) by A37,A39,Th17;
then X in M1 by A32,A38;
hence thesis by A29,TARSKI:def 4;
end;
suppose
x in LSeg(p,q);
hence thesis by A11;
end;
end;
theorem
len f>=2 & not p in L~f implies for n st 1<=n & n<=len f holds f/.n<>p
proof
assume that
A1: len f>=2 and
A2: not p in L~f;
set Mf={LSeg(f,k): 1<=k & k+1<=len f};
given n such that
A3: 1<=n and
A4: n<=len f and
A5: f/.n=p;
per cases by A4,XXREAL_0:1;
suppose
A6: n=len f;
reconsider j = len f - 1 as Element of NAT by A1,INT_1:5,XXREAL_0:2;
1+1<=len f by A1;
then
A7: 1<=j by XREAL_1:19;
then
A8: f/.(j+1) in LSeg(f,j) by TOPREAL1:21;
j+1<=len f;
then LSeg(f,j) in Mf by A7;
hence contradiction by A2,A5,A6,A8,TARSKI:def 4;
end;
suppose
A9: n<len f;
then n+1<=len f by NAT_1:13;
then
A10: f/.n in LSeg(f,n) by A3,TOPREAL1:21;
n+1<=len f by A9,NAT_1:13;
then LSeg(f,n) in Mf by A3;
hence contradiction by A2,A5,A10,TARSKI:def 4;
end;
end;
theorem
q<>p & LSeg(q,p) /\ L~f = {q} implies not p in L~f
proof
assume that
A1: q<>p and
A2: LSeg(q,p) /\ L~f = {q} & p in L~f;
p in LSeg(q,p) by RLTOPSP1:68;
then p in {q} by A2,XBOOLE_0:def 4;
hence contradiction by A1,TARSKI:def 1;
end;
theorem
f is being_S-Seq & f/.len f in LSeg(f,m) & 1<=m & m + 1 <=len f
implies m + 1 = len f
proof
assume that
A1: f is being_S-Seq and
A2: f/.len f in LSeg(f,m) and
A3: 1<=m and
A4: m + 1 <= len f;
A5: f is s.n.c. by A1;
A6: f is one-to-one by A1;
A7: f is unfolded by A1;
set q= f/.len f;
A8: m+1+1=m+(1+1);
A9: len f >=2 by A1;
then reconsider k = len f - 1 as Element of NAT by INT_1:5,XXREAL_0:2;
A10: k+1 = len f;
assume m + 1 <> len f;
then
A11: m+1<=k by A4,A10,NAT_1:8;
1<=len f by A9,XXREAL_0:2;
then
A12: len f in dom f by FINSEQ_3:25;
per cases by A11,XXREAL_0:1;
suppose
A13: m+1=k;
A14: 1<=m+1 by NAT_1:11;
m+1+1<=len f by A13;
then
A15: f/.(m+2) in LSeg(f,m+1) by A14,TOPREAL1:21;
LSeg(f,m) /\ LSeg(f,m+1) = {f/.(m+1)} by A3,A7,A8,A13;
then q in {f/.(m+1)} by A2,A13,A15,XBOOLE_0:def 4;
then
A16: f/.len f=f/.(m+1) by TARSKI:def 1;
m+1<=len f by A10,A13,NAT_1:11;
then m+1 in dom f by A14,FINSEQ_3:25;
then len f= len f -1 by A6,A12,A13,A16,PARTFUN2:10;
hence contradiction;
end;
suppose
A17: m+1<k;
(1+1)-1 = 1;
then k+1 = len f & 1<=k by A9,XREAL_1:13;
then
A18: q in LSeg(f,k) by TOPREAL1:21;
LSeg(f,m) misses LSeg(f,k) by A5,A17;
then LSeg(f,m) /\ LSeg(f,k) = {};
hence contradiction by A2,A18,XBOOLE_0:def 4;
end;
end;
theorem
not p1 in Ball(u,r) & q in Ball(u,r) & p in Ball(u,r) & not p in LSeg(
p1,q ) & ( q`1=p`1 & q`2<>p`2 or q`1<>p`1 & q`2=p`2 ) & (p1`1=q`1 or p1`2=q`2)
implies LSeg(p1,q) /\ LSeg(q,p) = {q}
proof
assume that
A1: not p1 in Ball(u,r) and
A2: q in Ball(u,r) and
A3: p in Ball(u,r) and
A4: not p in LSeg(p1,q);
assume
A5: q`1=p`1 & q`2<>p`2 or q`1<>p`1 & q`2=p`2;
assume
A6: p1`1=q`1 or p1`2=q`2;
A7: now
per cases by A6;
suppose
p1`1=q`1;
hence p1`1=q`1 & p1`2<>q`2 or p1`1<>q`1 & p1`2=q`2 by A1,A2,Th6;
end;
suppose
p1`2=q`2;
hence p1`1=q`1 & p1`2<>q`2 or p1`1<>q`1 & p1`2=q`2 by A1,A2,Th6;
end;
end;
A8: p=|[p`1,p`2]| by EUCLID:53;
A9: p1=|[p1`1,p1`2]| by EUCLID:53;
A10: q=|[q`1,q`2]| by EUCLID:53;
A11: LSeg(p,q) c= Ball(u,r) by A2,A3,Th21;
now
per cases by A5;
suppose
A12: q`1=p`1 & q`2<>p`2;
set r = p`1, pq = {p2: p2`1=r & p`2<=p2`2 & p2`2<=q`2}, qp = {p3: p3`1=r
& q`2<=p3`2 & p3`2<=p`2}, pp1 = {p11: p11`1=r & p`2<=p11`2 & p11`2<=p1`2}, p1p
= {p22: p22`1=r & p1`2<=p22`2 & p22`2<=p`2}, qp1 = {q1: q1`1=r & q`2<=q1`2 & q1
`2<=p1`2}, p1q = {q2: q2`1=r & p1`2<=q2`2 & q2`2<=q`2};
now
per cases by A12,XXREAL_0:1;
suppose
A13: q`2>p`2;
now
per cases by A7;
suppose
A14: p1`1=q`1 & p1`2<>q`2;
now
per cases by A14,XXREAL_0:1;
case
A15: p1`2>q`2;
then q in pp1 by A12,A13;
then q in LSeg(p,p1) by A8,A9,A12,A13,A14,A15,Th9,XXREAL_0:2;
hence thesis by TOPREAL1:8;
end;
case
A16: p1`2<q`2;
now
per cases by XXREAL_0:1;
suppose
A17: p1`2>p`2;
then p1 in pq by A12,A14,A16;
then p1 in LSeg(p,q) by A8,A10,A12,A16,A17,Th9,XXREAL_0:2
;
hence contradiction by A1,A11;
end;
suppose
p1`2=p`2;
hence contradiction by A1,A3,A12,A14,Th6;
end;
suppose
p1`2<p`2;
then p in p1q by A13;
hence contradiction by A4,A9,A10,A12,A14,A16,Th9;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
suppose
p1`1<>q`1 & p1`2=q`2;
hence thesis by A10,A12,Th30;
end;
end;
hence thesis;
end;
suppose
A18: q`2<p`2;
now
per cases by A7;
suppose
A19: p1`1=q`1 & p1`2<>q`2;
now
per cases by A19,XXREAL_0:1;
case
A20: p1`2>q`2;
now
per cases by XXREAL_0:1;
suppose
p1`2>p`2;
then p in qp1 by A18;
hence contradiction by A4,A9,A10,A12,A19,A20,Th9;
end;
suppose
p1`2=p`2;
hence contradiction by A1,A3,A12,A19,Th6;
end;
suppose
p1`2<p`2;
then p1 in qp by A12,A19,A20;
then p1 in LSeg(p,q) by A8,A10,A12,A18,Th9;
hence contradiction by A1,A11;
end;
end;
hence contradiction;
end;
case
A21: p1`2<q`2;
then q in p1p by A12,A18;
then q in LSeg(p1,p) by A8,A9,A12,A18,A19,A21,Th9,XXREAL_0:2;
hence thesis by TOPREAL1:8;
end;
end;
hence thesis;
end;
suppose
p1`1<>q`1 & p1`2=q`2;
hence thesis by A10,A12,Th30;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A22: q`1<>p`1 & q`2=p`2;
set r = p`2, pq = {p2: p2`2=r & p`1<=p2`1 & p2`1<=q`1}, qp = {p3: p3`2=r
& q`1<=p3`1 & p3`1<=p`1}, pp1 = {p11: p11`2=r & p`1<=p11`1 & p11`1<=p1`1}, p1p
= {p22: p22`2=r & p1`1<=p22`1 & p22`1<=p`1}, qp1 = {q1: q1`2=r & q`1<=q1`1 & q1
`1<=p1`1}, p1q = {q2: q2`2=r & p1`1<=q2`1 & q2`1<=q`1};
now
per cases by A22,XXREAL_0:1;
suppose
A23: q`1>p`1;
now
per cases by A7;
suppose
p1`1=q`1 & p1`2<>q`2;
hence thesis by A10,A22,Th29;
end;
suppose
A24: p1`1<>q`1 & p1`2=q`2;
now
per cases by A24,XXREAL_0:1;
case
A25: p1`1>q`1;
then q in pp1 by A22,A23;
then q in LSeg(p,p1) by A8,A9,A22,A23,A24,A25,Th10,XXREAL_0:2
;
hence thesis by TOPREAL1:8;
end;
case
A26: p1`1<q`1;
now
per cases by XXREAL_0:1;
suppose
A27: p1`1>p`1;
then p1 in pq by A22,A24,A26;
then p1 in LSeg(p,q) by A8,A10,A22,A26,A27,Th10,
XXREAL_0:2;
hence contradiction by A1,A11;
end;
suppose
p1`1=p`1;
hence contradiction by A1,A3,A22,A24,Th6;
end;
suppose
p1`1<p`1;
then p in p1q by A23;
hence contradiction by A4,A9,A10,A22,A24,A26,Th10;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A28: q`1<p`1;
now
per cases by A7;
suppose
p1`1=q`1 & p1`2<>q`2;
hence thesis by A10,A22,Th29;
end;
suppose
A29: p1`1<>q`1 & p1`2=q`2;
now
per cases by A29,XXREAL_0:1;
case
A30: p1`1>q`1;
now
per cases by XXREAL_0:1;
suppose
p1`1>p`1;
then p in qp1 by A28;
hence contradiction by A4,A9,A10,A22,A29,A30,Th10;
end;
suppose
p1`1=p`1;
hence contradiction by A1,A3,A22,A29,Th6;
end;
suppose
p1`1<p`1;
then p1 in qp by A22,A29,A30;
then p1 in LSeg(p,q) by A8,A10,A22,A28,Th10;
hence contradiction by A1,A11;
end;
end;
hence contradiction;
end;
case
A31: p1`1<q`1;
then q in p1p by A22,A28;
then q in LSeg(p1,p) by A8,A9,A22,A28,A29,A31,Th10,XXREAL_0:2
;
hence thesis by TOPREAL1:8;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem
not p1 in Ball(u,r) & p in Ball(u,r) & |[p`1,q`2]| in Ball(u,r) & not
|[p`1,q`2]| in LSeg(p1,p) & p1`1 = p`1 & p`1<>q`1 & p`2<>q`2 implies (LSeg(p,|[
p`1,q`2]|) \/ LSeg(|[p`1,q`2]|,q)) /\ LSeg(p1,p) = {p}
proof
set v = |[p`1,q`2]|;
assume that
A1: not p1 in Ball(u,r) and
A2: p in Ball(u,r) and
A3: v in Ball(u,r) and
A4: not v in LSeg(p1,p) and
A5: p1`1=p`1 and
A6: p`1<>q`1 and
A7: p`2<>q`2;
A8: LSeg(p,v) c= Ball(u,r) by A2,A3,Th21;
p in LSeg(p,v) by RLTOPSP1:68;
then p in LSeg(p1,p) & p in LSeg(p,v) \/ LSeg(v,q) by RLTOPSP1:68
,XBOOLE_0:def 3;
then p in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by XBOOLE_0:def 4;
then
A9: {p} c= (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by ZFMISC_1:31;
A10: (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) = LSeg(p,v) /\ LSeg(p1,p) \/
LSeg(v,q) /\ LSeg(p1,p) by XBOOLE_1:23;
A11: p1=|[p`1,p1`2]| by A5,EUCLID:53;
A12: q=|[q`1,q`2]| by EUCLID:53;
A13: p=|[p`1,p`2]| by EUCLID:53;
A14: v`1=p`1;
A15: v`2=q`2;
per cases;
suppose
p1`2=p`2;
hence thesis by A1,A2,A5,Th6;
end;
suppose
A16: p1`2<>p`2;
now
per cases by A16,XXREAL_0:1;
suppose
A17: p1`2>p`2;
now
per cases by A6,XXREAL_0:1;
suppose
A18: p`1>q`1;
now
per cases by A7,XXREAL_0:1;
case
A19: p`2>q`2;
then
A20: p`2>=v`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A21: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A10,A21,XBOOLE_0:def 3;
case
A22: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`1=p`1 & v`2<=q1`2 & q1`2<=p1`2} by A17,A20;
then p in LSeg(p1,v) by A11,A17,A19,Th9,XXREAL_0:2;
hence thesis by A22,TOPREAL1:8;
end;
case
A23: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(v,q) by XBOOLE_0:def 4;
then
x in {p2: p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1} by A12,A18
,Th10;
then
A24: ex p2 st p2=x & p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1;
x in LSeg(p1, p) by A23,XBOOLE_0:def 4;
then
x in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2} by A11,A13
,A17,Th9;
then
ex q2 st q2=x & q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2;
hence contradiction by A19,A24;
end;
end;
hence thesis;
end;
hence thesis by A9;
end;
case
A25: p`2<q`2;
now
per cases by XXREAL_0:1;
suppose
A26: q`2>p1`2;
then p1 in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=v`2} by A5,A17
;
then p1 in LSeg(p,v) by A13,A17,A26,Th9,XXREAL_0:2;
hence contradiction by A1,A8;
end;
suppose
q`2=p1`2;
hence contradiction by A1,A3,A5,EUCLID:53;
end;
suppose
A27: q`2<p1`2;
then v in {p2: p2`1=p`1 & p`2<=p2`2 & p2`2<=p1`2} by A14
,A15,A25;
hence contradiction by A4,A11,A13,A25,A27,Th9,XXREAL_0:2;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
suppose
A28: p`1<q`1;
now
per cases by A7,XXREAL_0:1;
case
A29: p`2>q`2;
then
A30: p`2>=v`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A31: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A10,A31,XBOOLE_0:def 3;
case
A32: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`1=p`1 & v`2<=q1`2 & q1`2<=p1`2} by A17,A30;
then p in LSeg(p1,v) by A11,A17,A29,Th9,XXREAL_0:2;
hence thesis by A32,TOPREAL1:8;
end;
case
A33: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(v,q) by XBOOLE_0:def 4;
then
x in {p2: p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1} by A12,A28
,Th10;
then
A34: ex p2 st p2=x & p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1;
x in LSeg(p1, p) by A33,XBOOLE_0:def 4;
then
x in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2} by A11,A13
,A17,Th9;
then ex q2 st q2=x & q2`1=p`1 & p`2 <=q2`2 & q2`2<=p1`2;
hence contradiction by A29,A34;
end;
end;
hence thesis;
end;
hence thesis by A9;
end;
case
A35: p`2<q`2;
now
per cases by XXREAL_0:1;
suppose
A36: q`2>p1`2;
then p1 in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=v`2} by A5,A17
;
then p1 in LSeg(p,v) by A13,A17,A36,Th9,XXREAL_0:2;
hence contradiction by A1,A8;
end;
suppose
q`2=p1`2;
hence contradiction by A1,A3,A5,EUCLID:53;
end;
suppose
A37: q`2<p1`2;
then v in {p2: p2`1=p`1 & p`2<=p2`2 & p2`2<=p1`2} by A14
,A15,A35;
hence contradiction by A4,A11,A13,A35,A37,Th9,XXREAL_0:2;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A38: p1`2<p`2;
now
per cases by A6,XXREAL_0:1;
suppose
A39: p`1>q`1;
now
per cases by A7,XXREAL_0:1;
case
A40: p`2>q`2;
now
per cases by XXREAL_0:1;
suppose
A41: q`2>p1`2;
then v in {p2: p2`1=p`1 & p1`2<=p2`2 & p2`2<=p`2} by A14
,A15,A40;
hence contradiction by A4,A11,A13,A40,A41,Th9,XXREAL_0:2;
end;
suppose
q`2=p1`2;
hence contradiction by A1,A3,A5,EUCLID:53;
end;
suppose
A42: q`2<p1`2;
then p1 in {q2: q2`1=p`1 & v`2<=q2`2 & q2`2<=p`2} by A5,A38
;
then p1 in LSeg(p,v) by A13,A38,A42,Th9,XXREAL_0:2;
hence contradiction by A1,A8;
end;
end;
hence contradiction;
end;
case
A43: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A44: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A10,A44,XBOOLE_0:def 3;
case
A45: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`1=p`1 & p1`2<=q1`2 & q1`2<=v`2} by A38
,A43;
then p in LSeg(p1,v) by A11,A38,A43,Th9,XXREAL_0:2;
hence thesis by A45,TOPREAL1:8;
end;
case
A46: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(v,q) by XBOOLE_0:def 4;
then
x in {p2: p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1} by A12,A39
,Th10;
then
A47: ex p2 st p2=x & p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1;
x in LSeg(p1, p) by A46,XBOOLE_0:def 4;
then
x in {q2: q2`1=p`1 & p1`2<=q2`2 & q2`2<=p`2} by A11,A13
,A38,Th9;
then ex q2 st q2=x & q2`1=p`1 & p1 `2<=q2`2 & q2`2<=p`2;
hence contradiction by A43,A47;
end;
end;
hence thesis;
end;
hence thesis by A9;
end;
end;
hence thesis;
end;
suppose
A48: p`1<q`1;
now
per cases by A7,XXREAL_0:1;
case
A49: p`2>q`2;
now
per cases by XXREAL_0:1;
suppose
A50: q`2>p1`2;
then v in {p2: p2`1=p`1 & p1`2<=p2`2 & p2`2<=p`2} by A14
,A15,A49;
hence contradiction by A4,A11,A13,A49,A50,Th9,XXREAL_0:2;
end;
suppose
q`2=p1`2;
hence contradiction by A1,A3,A5,EUCLID:53;
end;
suppose
A51: q`2<p1`2;
then p1 in {q2: q2`1=p`1 & v`2<=q2`2 & q2`2<=p`2} by A5,A38
;
then p1 in LSeg(p,v) by A13,A38,A51,Th9,XXREAL_0:2;
hence contradiction by A1,A8;
end;
end;
hence contradiction;
end;
case
A52: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A53: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A10,A53,XBOOLE_0:def 3;
case
A54: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`1=p`1 & p1`2<=q1`2 & q1`2<=v`2} by A38
,A52;
then p in LSeg(p1,v) by A11,A38,A52,Th9,XXREAL_0:2;
hence thesis by A54,TOPREAL1:8;
end;
case
A55: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(v,q) by XBOOLE_0:def 4;
then x in {p2: p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1} by A12
,A48,Th10;
then
A56: ex p2 st p2=x & p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1;
x in LSeg(p1, p) by A55,XBOOLE_0:def 4;
then x in {q2: q2`1=p`1 & p1`2<=q2`2 & q2`2<=p`2} by A11
,A13,A38,Th9;
then ex q2 st q2=x & q2`1=p`1 & p1 `2<=q2`2 & q2`2<=p`2;
hence contradiction by A52,A56;
end;
end;
hence thesis;
end;
hence thesis by A9;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
theorem
not p1 in Ball(u,r) & p in Ball(u,r) & |[q`1,p`2]| in Ball(u,r) & not
|[q`1,p`2]| in LSeg(p1,p) & p1`2 = p`2 & p`1<>q`1 & p`2<>q`2 implies (LSeg(p,|[
q`1,p`2]|) \/ LSeg(|[q`1,p`2]|,q)) /\ LSeg(p1,p) = {p}
proof
set v = |[q`1,p`2]|;
assume that
A1: not p1 in Ball(u,r) and
A2: p in Ball(u,r) and
A3: v in Ball(u,r) and
A4: not v in LSeg(p1,p) and
A5: p1`2=p`2 and
A6: p`1<>q`1 and
A7: p`2<>q`2;
A8: LSeg(p,v) c= Ball(u,r) by A2,A3,Th21;
A9: p1=|[p1`1,p`2]| by A5,EUCLID:53;
p in LSeg(p,v) by RLTOPSP1:68;
then p in LSeg(p1,p) & p in LSeg(p,v) \/ LSeg(v,q) by RLTOPSP1:68
,XBOOLE_0:def 3;
then p in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by XBOOLE_0:def 4;
then
A10: {p} c= (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by ZFMISC_1:31;
A11: (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) = LSeg(p,v) /\ LSeg(p1,p) \/
LSeg(v,q) /\ LSeg(p1,p) by XBOOLE_1:23;
A12: q=|[q`1,q`2]| by EUCLID:53;
A13: p=|[p`1,p`2]| by EUCLID:53;
A14: v`2=p`2;
A15: v`1=q`1;
per cases;
suppose
p1`1=p`1;
hence thesis by A1,A2,A5,Th6;
end;
suppose
A16: p1`1<>p`1;
now
per cases by A16,XXREAL_0:1;
suppose
A17: p1`1>p`1;
now
per cases by A6,XXREAL_0:1;
case
A18: p`1>q`1;
then
A19: p`1>=v`1;
now
per cases by A7,XXREAL_0:1;
suppose
A20: p`2>q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A21: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A11,A21,XBOOLE_0:def 3;
case
A22: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`2=p`2 & v`1<=q1`1 & q1`1<=p1`1} by A17,A19;
then p in LSeg(p1,v) by A9,A17,A18,Th10,XXREAL_0:2;
hence thesis by A22,TOPREAL1:8;
end;
case
A23: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(q,v) by XBOOLE_0:def 4;
then
x in {p2: p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2} by A12,A20
,Th9;
then
A24: ex p2 st p2=x & p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2;
x in LSeg(p, p1) by A23,XBOOLE_0:def 4;
then
x in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=p1`1} by A9,A13
,A17,Th10;
then ex q2 st q2=x & q2`2=p`2 & p`1 <=q2`1 & q2`1<=p1`1;
hence contradiction by A18,A24;
end;
end;
hence thesis;
end;
hence thesis by A10;
end;
suppose
A25: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A26: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A11,A26,XBOOLE_0:def 3;
case
A27: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`2=p`2 & v`1<=q1`1 & q1`1<=p1`1} by A17,A19;
then p in LSeg(p1,v) by A9,A17,A18,Th10,XXREAL_0:2;
hence thesis by A27,TOPREAL1:8;
end;
case
A28: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(p1, p) by XBOOLE_0:def 4;
then
x in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=p1`1} by A9,A13
,A17,Th10;
then
A29: ex q2 st q2=x & q2`2=p`2 & p`1 <=q2`1 & q2`1<=p1`1;
x in LSeg(v,q) by A28,XBOOLE_0:def 4;
then
x in {p2: p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2} by A12,A25,
Th9;
then ex p2 st p2=x & p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2;
hence contradiction by A18,A29;
end;
end;
hence thesis;
end;
hence thesis by A10;
end;
end;
hence thesis;
end;
case
A30: p`1<q`1;
now
per cases by XXREAL_0:1;
suppose
A31: q`1>p1`1;
then p1 in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=v`1} by A5,A17
;
then p1 in LSeg(p,v) by A13,A17,A31,Th10,XXREAL_0:2;
hence contradiction by A1,A8;
end;
suppose
q`1=p1`1;
hence contradiction by A1,A3,A5,EUCLID:53;
end;
suppose
q`1<p1`1;
then
v in {p2: p2`2=p`2 & p`1<=p2`1 & p2`1<=p1`1} by A15,A14,A30;
hence contradiction by A4,A9,A13,A17,Th10;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
suppose
A32: p1`1<p`1;
now
per cases by A6,XXREAL_0:1;
case
A33: p`1>q`1;
now
per cases by XXREAL_0:1;
suppose
q`1>p1`1;
then
v in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A15,A14,A33;
hence contradiction by A4,A9,A13,A32,Th10;
end;
suppose
q`1=p1`1;
hence contradiction by A1,A3,A5,EUCLID:53;
end;
suppose
A34: q`1<p1`1;
then p1 in {p2: p2`2=p`2 & v`1<=p2`1 & p2`1<=p`1} by A5,A32
;
then p1 in LSeg(p,v) by A13,A32,A34,Th10,XXREAL_0:2;
hence contradiction by A1,A8;
end;
end;
hence contradiction;
end;
case
A35: p`1<q`1;
then
A36: p`1<=v`1;
now
per cases by A7,XXREAL_0:1;
suppose
A37: p`2>q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A38: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A11,A38,XBOOLE_0:def 3;
case
A39: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`2=p`2 & p1`1<=q1`1 & q1`1<=v`1} by A32,A36;
then p in LSeg(p1,v) by A9,A32,A35,Th10,XXREAL_0:2;
hence thesis by A39,TOPREAL1:8;
end;
case
A40: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(v,q) by XBOOLE_0:def 4;
then
x in {p2: p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2} by A12,A37
,Th9;
then
A41: ex p2 st p2=x & p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2;
x in LSeg(p1, p) by A40,XBOOLE_0:def 4;
then
x in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A9,A13
,A32,Th10;
then ex q2 st q2=x & q2`2=p`2 & p1 `1<=q2`1 & q2`1<=p`1;
hence contradiction by A35,A41;
end;
end;
hence thesis;
end;
hence thesis by A10;
end;
suppose
A42: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof
let x be object such that
A43: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now
per cases by A11,A43,XBOOLE_0:def 3;
case
A44: x in LSeg(p,v) /\ LSeg(p1,p);
p in {q1: q1`2=p`2 & p1`1<=q1`1 & q1`1<=v`1} by A32,A36;
then p in LSeg(p1,v) by A9,A32,A35,Th10,XXREAL_0:2;
hence thesis by A44,TOPREAL1:8;
end;
case
A45: x in LSeg(v,q) /\ LSeg(p1,p);
then x in LSeg(p1, p) by XBOOLE_0:def 4;
then x in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A9
,A13,A32,Th10;
then
A46: ex q2 st q2=x & q2`2=p`2 & p1 `1<=q2`1 & q2`1<=p`1;
x in LSeg(v,q) by A45,XBOOLE_0:def 4;
then x in {p2: p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2} by A12
,A42,Th9;
then ex p2 st p2=x & p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2;
hence contradiction by A35,A46;
end;
end;
hence thesis;
end;
hence thesis by A10;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
reserve f for FinSequence of REAL;
theorem Th45:
len f = n implies f in the carrier of Euclid n
proof
f in REAL* & n-tuples_on REAL = { s where s is Element of REAL*: len s =
n } by FINSEQ_1:def 11,FINSEQ_2:def 4;
hence thesis;
end;
theorem
len f = n implies f in the carrier of TOP-REAL n
proof
assume len f = n;
then f in the carrier of Euclid n by Th45;
hence thesis by Th8;
end;