:: The Topological Space ${\calE}^2_{\rm T}$.
:: Arcs, Line Segments and Special Polygonal Arcs
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991-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, REAL_1, NAT_1, XBOOLE_0, SUBSET_1, PRE_TOPC, EUCLID,
FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, CARD_1, STRUCT_0, XXREAL_1, RLTOPSP1,
TARSKI, ARYTM_1, ARYTM_3, XXREAL_0, MCART_1, SUPINF_2, RCOMP_1, PCOMPS_1,
CONNSP_2, TOPMETR, METRIC_1, TOPS_1, COMPLEX1, ORDINAL2, FINSEQ_1,
PARTFUN1, ZFMISC_1, SETFAM_1, TOPREAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
BINOP_1, TOPS_1, TOPS_2, CONNSP_2, COMPTS_1, RCOMP_1, FINSEQ_1, FINSEQ_4,
STRUCT_0, METRIC_1, TOPMETR, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID,
PRE_TOPC, XXREAL_0;
constructors SETFAM_1, REAL_1, NAT_1, COMPLEX1, FINSEQOP, RCOMP_1, FINSEQ_4,
TOPS_1, TOPS_2, COMPTS_1, EUCLID, TOPMETR, RVSUM_1, VALUED_1, FUNCSDOM,
RLTOPSP1, CONVEX1, BINOP_2, PCOMPS_1, RUSUB_4;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, EUCLID,
TOPMETR, VALUED_0, RLTOPSP1, FUNCT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, PRE_TOPC;
equalities EUCLID, STRUCT_0, RLTOPSP1, RLVECT_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, PRE_TOPC;
theorems BORSUK_1, COMPTS_1, CONNSP_2, ENUMSET1, EUCLID, FINSEQ_1, FUNCT_1,
FUNCT_2, HEINE, METRIC_1, NAT_1, PCOMPS_1, PRE_TOPC, RCOMP_1, TARSKI,
TOPMETR, TOPMETR2, TOPS_1, TOPS_2, ZFMISC_1, FINSEQ_3, FINSEQ_4, TBSP_1,
PARTFUN2, RELSET_1, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_0,
XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, XXREAL_1, RLTOPSP1, RLVECT_1;
schemes NAT_1, CLASSES1, XBOOLE_0;
begin
reserve r,lambda for Real,
i,j,n for Nat;
:: PRELIMINARIES
scheme
FraenkelAlt {A() -> non empty set, P[set], Q[set]}: {v where v is Element of
A(): P[v] or Q[v]} = {v1 where v1 is Element of A(): P[v1]} \/ {v2 where v2 is
Element of A(): Q[v2]} proof
set X = {v where v is Element of A(): P[v] or Q[v]}, Y = {v1 where v1 is
Element of A(): P[v1]}, Z = {v2 where v2 is Element of A(): Q[v2]};
now
let x be object;
thus for x being object holds x in X implies x in Y \/ Z
proof let x be object;
assume x in X;
then consider v being Element of A() such that
A1: x = v and
A2: P[v] or Q[v];
per cases by A2;
suppose
P[v];
then x in Y by A1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
Q[v];
then x in Z by A1;
hence thesis by XBOOLE_0:def 3;
end;
end;
assume
A3: x in Y \/ Z;
per cases by A3,XBOOLE_0:def 3;
suppose
x in Y;
then ex v being Element of A() st x = v & P[v];
hence x in X;
end;
suppose
x in Z;
then ex v being Element of A() st x = v & Q[v];
hence x in X;
end;
end;
hence thesis by TARSKI:2;
end;
:: PROPER TEXT
reserve p,p1,p2,q1,q2 for Point of TOP-REAL 2,
P, P1 for Subset of TOP-REAL 2;
reserve T for TopSpace;
definition
let T;
let p1, p2 be Point of T, P be Subset of T;
pred P is_an_arc_of p1,p2 means
ex f being Function of I[01], T|P st
f is being_homeomorphism & f.0 = p1 & f.1 = p2;
end;
theorem Th1:
for P being Subset of T, p1,p2 being Point of T st P is_an_arc_of
p1,p2 holds p1 in P & p2 in P
proof
let P be Subset of T, p1,p2 be Point of T;
assume P is_an_arc_of p1,p2;
then consider f being Function of I[01], T|P such that
A1: f is being_homeomorphism and
A2: f.0 = p1 and
A3: f.1 = p2;
A4: dom f = [#]I[01] by A1,TOPS_2:def 5
.= the carrier of I[01];
1 in [.0,1.] by XXREAL_1:1;
then
A5: p2 in rng f by A3,A4,BORSUK_1:40,FUNCT_1:def 3;
A6: rng f = [#](T|P) by A1,TOPS_2:def 5;
0 in [.0,1.] by XXREAL_1:1;
then p1 in rng f by A2,A4,BORSUK_1:40,FUNCT_1:def 3;
hence thesis by A5,A6,PRE_TOPC:def 5;
end;
theorem Th2:
for T being T_2 TopSpace for P,Q being Subset of T, p1,p2,q1
being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2}
holds P \/ Q is_an_arc_of p1,q1
by TOPMETR2:3;
definition
func R^2-unit_square -> Subset of TOP-REAL 2 equals
( LSeg(|[0,0]|,|[0,1]|)
\/ LSeg(|[0,1]|,|[1,1]|) ) \/ ( LSeg(|[1,1]|,|[1,0]|) \/ LSeg(|[1,0]|,|[0,0]|)
);
coherence;
end;
Lm1: for p,p1,p2 being Point of TOP-REAL n st p in LSeg(p1,p2) holds LSeg(p1,p
) c= LSeg(p1,p2)
proof
let p,p1,p2 be Point of TOP-REAL n;
assume p in LSeg(p1,p2);
then consider r such that
A1: p = (1-r)*p1 + r*p2 and
A2: 0 <= r and
A3: r <= 1;
let q be object;
assume q in LSeg(p1,p);
then consider b being Real such that
A4: q = (1-b)*p1 + b*p and
A5: 0 <= b and
A6: b <= 1;
A7: q = (1-b)*p1 + (b*((1-r)*p1) + b*(r*p2)) by A1,A4,RLVECT_1:def 5
.= (1-b)*p1 + b*((1-r)*p1) + b*(r*p2) by RLVECT_1:def 3
.= (1-b)*p1 + b*(1-r)*p1 + b*(r*p2) by RLVECT_1:def 7
.= (1-b + b*(1-r))*p1 + b*(r*p2) by RLVECT_1:def 6
.= (1-b*r)*p1 + b*r*p2 by RLVECT_1:def 7;
b*r <= 1 by A2,A3,A6,XREAL_1:160;
hence thesis by A2,A5,A7;
end;
theorem
p1`1 <= p2`1 & p in LSeg(p1,p2) implies p1`1 <= p`1 & p`1 <= p2`1
proof
assume that
A1: p1`1 <= p2`1 and
A2: p in LSeg(p1,p2);
consider lambda such that
A3: p = (1-lambda)*p1 + lambda*p2 and
A4: 0 <= lambda and
A5: lambda <= 1 by A2;
A6: ((1-lambda)*p1)`1 = |[(1-lambda)*p1`1, (1-lambda)*p1`2]|`1 by EUCLID:57
.= (1-lambda)*p1`1 by EUCLID:52;
A7: (lambda*p2)`1 = |[lambda*p2`1, lambda*p2`2]|`1 by EUCLID:57
.= lambda*p2`1 by EUCLID:52;
A8: p`1 = |[((1-lambda)*p1)`1 + (lambda*p2)`1, ((1-lambda)*p1)`2 + (lambda*
p2)`2]|`1 by A3,EUCLID:55
.= (1-lambda)*p1`1 + lambda*p2`1 by A6,A7,EUCLID:52;
lambda*p1`1 <= lambda*p2`1 by A1,A4,XREAL_1:64;
then (1-lambda)*p1`1 + lambda*p1`1 <= p`1 by A8,XREAL_1:7;
hence p1`1 <= p`1;
0 <= 1-lambda by A5,XREAL_1:48;
then (1-lambda)*p1`1 <= (1-lambda)*p2`1 by A1,XREAL_1:64;
then p`1 <= (1-lambda)*p2`1 + lambda*p2`1 by A8,XREAL_1:6;
hence thesis;
end;
theorem
p1`2 <= p2`2 & p in LSeg(p1,p2) implies p1`2 <= p`2 & p`2 <= p2`2
proof
assume that
A1: p1`2 <= p2`2 and
A2: p in LSeg(p1,p2);
consider lambda such that
A3: p = (1-lambda)*p1 + lambda*p2 and
A4: 0 <= lambda and
A5: lambda <= 1 by A2;
A6: ((1-lambda)*p1)`2 = |[(1-lambda)*p1`1, (1-lambda)*p1`2]|`2 by EUCLID:57
.= (1-lambda)*p1`2 by EUCLID:52;
A7: (lambda*p2)`2 = |[lambda*p2`1, lambda*p2`2]|`2 by EUCLID:57
.= lambda*p2`2 by EUCLID:52;
A8: p`2 = |[((1-lambda)*p1)`1 + (lambda*p2)`1, ((1-lambda)*p1)`2 + (lambda*
p2)`2]|`2 by A3,EUCLID:55
.= (1-lambda)*p1`2 + lambda*p2`2 by A6,A7,EUCLID:52;
lambda*p1`2 <= lambda*p2`2 by A1,A4,XREAL_1:64;
then (1-lambda)*p1`2 + lambda*p1`2 <= p`2 by A8,XREAL_1:7;
hence p1`2 <= p`2;
0 <= 1-lambda by A5,XREAL_1:48;
then (1-lambda)*p1`2 <= (1-lambda)*p2`2 by A1,XREAL_1:64;
then p`2 <= (1-lambda)*p2`2 + lambda*p2`2 by A8,XREAL_1:6;
hence thesis;
end;
theorem Th5:
for p,p1,p2 being Point of TOP-REAL n st p in LSeg(p1,p2) holds
LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,p2)
proof
let p,p1,p2 be Point of TOP-REAL n;
now
assume
A1: p in LSeg(p1,p2);
then consider r such that
A2: p = (1-r)*p1 + r*p2 and
A3: 0 <= r and
A4: r <= 1;
now
per cases;
suppose
A5: 0 <> r & r <> 1;
now
let q be object;
assume q in LSeg(p1,p2);
then consider b being Real such that
A6: q = (1-b)*p1 + b*p2 and
A7: 0 <= b and
A8: b <= 1;
now
per cases;
suppose
A9: b <= r;
set x = b*(1/r);
x <= r*(1/r) by A3,A9,XREAL_1:64;
then
A10: x <= 1 by A5,XCMPLX_1:106;
(1-x)*p1 + x*p = (1-x)*p1 + (x*((1-r)*p1) + x*(r*p2)) by A2,
RLVECT_1:def 5
.= (1-x)*p1 + x*((1-r)*p1) + x*(r*p2) by RLVECT_1:def 3
.= (1-x)*p1 + x*(1-r)*p1 + x*(r*p2) by RLVECT_1:def 7
.= (1-x)*p1 + x*(1-r)*p1 + x*r*p2 by RLVECT_1:def 7
.= ((1-x) + x*(1-r))*p1 + x*r*p2 by RLVECT_1:def 6
.= (1 -x*r)*p1 + b*p2 by A5,XCMPLX_1:109
.= q by A5,A6,XCMPLX_1:109;
then
q in { (1-lambda)*p1 + lambda*p : 0 <= lambda & lambda <= 1
} by A3,A7,A10;
hence q in LSeg(p1,p) \/ LSeg(p,p2) by XBOOLE_0:def 3;
end;
suppose
A11: not b <= r;
set bp =1-b,rp=1-r;
set x=bp*(1/rp);
A12: 0 <> rp by A5;
r-r=0;
then
A13: 0 <= rp by A4,XREAL_1:9;
bp <= rp by A11,XREAL_1:10;
then x <= rp*(1/rp) by A13,XREAL_1:64;
then
A14: x <= 1 by A12,XCMPLX_1:106;
A15: 0 <= bp by A8,XREAL_1:48;
A16: 1-0=1;
(1-x)*p2 + x*p = (1-x)*p2 + (x*((1-rp)*p2) + x*(rp*p1)) by A2,
RLVECT_1:def 5
.= (1-x)*p2 + x*((1-rp)*p2) + x*(rp*p1) by RLVECT_1:def 3
.= (1-x)*p2 + x*(1-rp)*p2 + x*(rp*p1) by RLVECT_1:def 7
.= (1-x)*p2 + x*(1-rp)*p2 + x*rp*p1 by RLVECT_1:def 7
.= ((1-x) + x*(1-rp))*p2 + x*rp*p1 by RLVECT_1:def 6
.= (1 -x*rp)*p2 + bp*p1 by A5,A16,XCMPLX_1:109
.= (1-bp)*p2 + bp*p1 by A12,XCMPLX_1:109
.= q by A6;
then q in { (1-lambda)*p2 + lambda*p: 0 <= lambda & lambda <= 1
} by A15,A13,A14;
then q in LSeg(p,p2) by RLTOPSP1:def 2;
hence q in LSeg(p1,p) \/ LSeg(p,p2) by XBOOLE_0:def 3;
end;
end;
hence q in LSeg(p1,p) \/ LSeg(p,p2);
end;
then
A17: LSeg(p1,p2) c= LSeg(p1,p) \/ LSeg(p,p2);
A18: LSeg(p,p2) c= LSeg(p1,p2) by A1,Lm1;
LSeg(p1,p) c= LSeg(p1,p2) by A1,Lm1;
then LSeg(p1,p) \/ LSeg(p,p2) c= LSeg(p1,p2) by A18,XBOOLE_1:8;
hence thesis by A17;
end;
suppose
A19: not (0<>r & r<>1);
now
per cases by A19;
suppose
A20: r = 0;
A21: p in LSeg(p,p2) by RLTOPSP1:68;
A22: p = 1*p1 + 0.TOP-REAL n by A2,A20,RLVECT_1:10
.= p1 + 0.TOP-REAL n by RLVECT_1:def 8
.= p1 by RLVECT_1:4;
then LSeg(p1,p) = {p} by RLTOPSP1:70;
then LSeg(p1,p) c= LSeg(p,p2) by A21,ZFMISC_1:31;
hence LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,p2) by A22,XBOOLE_1:12;
end;
suppose
A23: r = 1;
A24: p in LSeg(p1,p) by RLTOPSP1:68;
A25: p = 0.TOP-REAL n + 1*p2 by A2,A23,RLVECT_1:10
.= 0.TOP-REAL n + p2 by RLVECT_1:def 8
.= p2 by RLVECT_1:4;
then LSeg(p,p2) = {p} by RLTOPSP1:70;
then LSeg(p,p2) c= LSeg(p1,p) by A24,ZFMISC_1:31;
hence LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,p2) by A25,XBOOLE_1:12;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th6:
for p1,p2,q1,q2 being Point of TOP-REAL n st q1 in LSeg(p1,p2) &
q2 in LSeg(p1,p2) holds LSeg(q1,q2) c= LSeg(p1,p2)
proof
let p1,p2,q1,q2 be Point of TOP-REAL n;
assume that
A1: q1 in LSeg(p1,p2) and
A2: q2 in LSeg(p1,p2);
A3: LSeg(p1,p2) = LSeg(p1,q1) \/ LSeg(q1,p2) by A1,Th5;
now
per cases by A2,A3,XBOOLE_0:def 3;
suppose
A4: q2 in LSeg(p1,q1);
A5: LSeg(p1,q1) c= LSeg(p1,p2) by A1,Lm1;
LSeg(q2,q1) c= LSeg(p1,q1) by A4,Lm1;
hence thesis by A5;
end;
suppose
A6: q2 in LSeg(q1,p2);
A7: LSeg(q1,p2) c= LSeg(p1,p2) by A1,Lm1;
LSeg(q1,q2) c= LSeg(q1,p2) by A6,Lm1;
hence thesis by A7;
end;
end;
hence thesis;
end;
theorem
for p,q,p1,p2 being Point of TOP-REAL n st p in LSeg(p1,p2) & q in
LSeg(p1,p2) holds LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,q) \/ LSeg(q,p2)
proof
let p,q,p1,p2 be Point of TOP-REAL n;
assume that
A1: p in LSeg(p1,p2) and
A2: q in LSeg(p1,p2);
A3: LSeg(p,q) c= LSeg(p1,p2) by A1,A2,Th6;
A4: LSeg(p1,p2) = LSeg(p1,q) \/ LSeg(q,p2) by A2,Th5;
A5: now
per cases;
suppose
p in LSeg(p1,q);
hence LSeg(p1,p2) c= LSeg(p1,p) \/ LSeg(p,q) \/ LSeg(q,p2) by A4,Th5;
end;
suppose
not p in LSeg(p1,q);
then p in LSeg(q,p2) by A1,A4,XBOOLE_0:def 3;
then
A6: LSeg(q,p2) = LSeg(q,p) \/ LSeg(p,p2) by Th5;
LSeg(p1,p2) = LSeg(p1,p) \/ LSeg(p,p2) by A1,Th5;
then
A7: LSeg(p1,p2) c= LSeg(p1,p) \/ LSeg(q,p2) by A6,XBOOLE_1:7,9;
A8: LSeg(p1,p) \/ LSeg(q,p2) \/ LSeg(p,q) = LSeg(p1,p) \/ LSeg(p,q) \/
LSeg(q,p2) by XBOOLE_1:4;
LSeg(p1,p) \/ LSeg(q,p2) c= LSeg(p1,p) \/ LSeg(q,p2) \/ LSeg(p,q)
by XBOOLE_1:7;
hence LSeg(p1,p2) c= LSeg(p1,p) \/ LSeg(p,q) \/ LSeg(q,p2) by A7,A8;
end;
end;
p1 in LSeg(p1,p2) by RLTOPSP1:68;
then LSeg(p1,p) c= LSeg(p1,p2) by A1,Th6;
then
A9: LSeg(p1,p) \/ LSeg(p,q) c= LSeg(p1,p2) by A3,XBOOLE_1:8;
p2 in LSeg(p1,p2) by RLTOPSP1:68;
then LSeg(q,p2) c= LSeg(p1,p2) by A2,Th6;
then LSeg(p1,p) \/ LSeg(p,q) \/ LSeg(q,p2) c= LSeg(p1,p2) by A9,XBOOLE_1:8;
hence thesis by A5;
end;
theorem
for p, p1, p2 being Point of TOP-REAL n st p in LSeg(p1,p2) holds LSeg
(p1,p) /\ LSeg(p,p2) = {p}
proof
let p, p1, p2 be Point of TOP-REAL n;
A1: p in LSeg(p,p2) by RLTOPSP1:68;
assume
A2: p in LSeg(p1,p2);
A3: now
assume not LSeg(p1,p) /\ LSeg(p,p2) c= {p};
then consider y being object such that
A4: y in LSeg(p1,p) /\ LSeg(p,p2) and
A5: not y in {p};
reconsider q=y as Point of TOP-REAL n by A4;
A6: q in LSeg(p1,p) by A4,XBOOLE_0:def 4;
then consider d being Real such that
A7: q=(1-d)*p1+d*p and
0<=d and
A8: d<=1;
q in LSeg(p,p2) by A4,XBOOLE_0:def 4;
then consider e being Real such that
A9: q=(1-e)*p+e*p2 and
A10: 0<=e and
e<=1;
consider a being Real such that
A11: p=(1-a)*p1+a*p2 and
A12: 0<=a and
A13: a<=1 by A2;
A14: 1-a>=0 by A13,XREAL_1:48;
now
assume d=1;
then q=(1-1)*p1+p by A7,RLVECT_1:def 8
.=(0.TOP-REAL n) +p by RLVECT_1:10
.=p by RLVECT_1:4;
hence contradiction by A5,TARSKI:def 1;
end;
then d<1 by A8,XXREAL_0:1;
then
A15: 1-d>0 by XREAL_1:50;
now
assume a=0;
then p=(1-0)*p1+0.TOP-REAL n by A11,RLVECT_1:10
.=(1-0)*p1 by RLVECT_1:4
.=p1 by RLVECT_1:def 8;
hence contradiction by A5,A6,RLTOPSP1:70;
end;
then
A16: (1-d)*a>0 by A12,A15,XREAL_1:129;
set f=(1-e)*a+e;
q=(1-e)*((1-a)*p1)+(1-e)*(a*p2)+e*p2 by A11,A9,RLVECT_1:def 5
.=(1-e)*(1-a)*p1+(1-e)*(a*p2)+e*p2 by RLVECT_1:def 7
.=(1-e)*(1-a)*p1+(1-e)*a*p2+e*p2 by RLVECT_1:def 7
.=(1-e)*(1-a)*p1+((1-e)*a*p2+e*p2) by RLVECT_1:def 3
.=(1-e)*(1-a)*p1+((1-e)*a+e)*p2 by RLVECT_1:def 6;
then
A17: p-q=(1-a)*p1 +a*p2 -(1-f)*p1-f*p2 by A11,RLVECT_1:27
.=(1-a)*p1-(1-f)*p1 +a*p2-f*p2 by RLVECT_1:def 3
.=(1-a-(1-f))*p1+a*p2-f*p2 by RLVECT_1:35
.=(f-a)*p1-f*p2+a*p2 by RLVECT_1:def 3
.=(f-a)*p1-(f*p2-a*p2) by RLVECT_1:29
.=(f-a)*p1-(f-a)*p2 by RLVECT_1:35
.=(f-a)*(p1-p2) by RLVECT_1:34;
q=(1-d)*p1+(d*((1-a)*p1)+d*(a*p2)) by A11,A7,RLVECT_1:def 5
.=(1-d)*p1+d*((1-a)*p1) +d*(a*p2) by RLVECT_1:def 3
.=(1-d)*p1+d*(1-a)*p1 +d*(a*p2) by RLVECT_1:def 7
.=(1-d+d*(1-a))*p1+d*(a*p2) by RLVECT_1:def 6
.=(1-d*a)*p1+d*a*p2 by RLVECT_1:def 7;
then p-q=(1-a)*p1 +a*p2 -(1-d*a)*p1-d*a*p2 by A11,RLVECT_1:27
.=(1-a)*p1-(1-d*a)*p1 +a*p2-d*a*p2 by RLVECT_1:def 3
.=(1-a-(1-d*a))*p1+a*p2-d*a*p2 by RLVECT_1:35
.=(d*a-a)*p1-d*a*p2+a*p2 by RLVECT_1:def 3
.=(d*a-a)*p1-(d*a*p2-a*p2) by RLVECT_1:29
.=(d*a-a)*p1-(d*a-a)*p2 by RLVECT_1:35
.=(d*a-a)*(p1-p2) by RLVECT_1:34;
then (f-a)*(p1-p2)-(d*a-a)*(p1-p2)=0.TOP-REAL n by A17,RLVECT_1:5;
then (f-a-(d*a-a))*(p1-p2)=0.TOP-REAL n by RLVECT_1:35;
then
A18: f-d*a=0 or p1-p2=0.TOP-REAL n by RLVECT_1:11;
((1-e)*a+e)-d*a=(1-d)*a+(e*(1-a));
then p1=p2 by A10,A18,A16,A14,RLVECT_1:21;
then p in {p1} by A2,RLTOPSP1:70;
then p=p1 by TARSKI:def 1;
hence contradiction by A5,A6,RLTOPSP1:70;
end;
p in LSeg(p1,p) by RLTOPSP1:68;
then p in LSeg(p1,p) /\ LSeg(p,p2) by A1,XBOOLE_0:def 4;
then {p} c= LSeg(p1,p) /\ LSeg(p,p2) by ZFMISC_1:31;
hence thesis by A3;
end;
Lm2: for T being TopSpace holds T is T_2 iff the TopStruct of T is T_2
proof
let T be TopSpace;
thus T is T_2 implies the TopStruct of T is T_2
proof
assume
A1: T is T_2;
let p, q being Point of the TopStruct of T such that
A2: p <> q;
reconsider pp=p, qq=q as Point of T;
consider G1,G2 being Subset of T such that
A3: G1 is open and
A4: G2 is open and
A5: pp in G1 and
A6: qq in G2 and
A7: G1 misses G2 by A1,A2;
reconsider H1=G1, H2=G2 as Subset of the TopStruct of T;
take H1,H2;
thus H1 is open & H2 is open by A3,A4;
thus p in H1 & q in H2 & H1 misses H2 by A5,A6,A7;
end;
assume
A8: the TopStruct of T is T_2;
let p, q being Point of T such that
A9: p <> q;
reconsider pp=p, qq=q as Point of the TopStruct of T;
consider G1,G2 being Subset of the TopStruct of T such that
A10: G1 is open and
A11: G2 is open and
A12: pp in G1 and
A13: qq in G2 and
A14: G1 misses G2 by A8,A9;
reconsider H1=G1, H2=G2 as Subset of T;
take H1,H2;
thus H1 is open & H2 is open by A10,A11;
thus p in H1 & q in H2 & H1 misses H2 by A12,A13,A14;
end;
registration
let n;
cluster the carrier of TOP-REAL n -> functional;
coherence
by EUCLID:23;
end;
theorem Th9:
for p1,p2 being Point of TOP-REAL n st p1 <> p2 holds
LSeg(p1,p2) is_an_arc_of p1,p2
proof
let p1,p2 be Point of TOP-REAL n;
set P = LSeg(p1,p2);
reconsider PP = P as Subset of Euclid n by EUCLID:67;
PP is non empty;
then reconsider PP = P as non empty Subset of Euclid n;
reconsider p19 = p1, p29 = p2 as Element of REAL n by EUCLID:22;
defpred X[object,object] means
for x being Real st x = $1 holds $2 = (1-x)*p1 + x*
p2;
A1: for a being object st a in [.0,1.] ex u being object st X[a,u]
proof
let a be object;
assume a in [.0,1.];
then reconsider x = a as Real;
take (1-x)*p1 + x*p2;
thus thesis;
end;
consider f being Function such that
A2: dom f = [.0,1.] and
A3: for a being object st a in [.0,1.] holds X[a,f.a] from CLASSES1:sch 1(
A1);
A4: rng f c= the carrier of (TOP-REAL n)|P
proof
let y be object;
assume y in rng f;
then consider x being object such that
A5: x in dom f and
A6: y = f.x by FUNCT_1:def 3;
x in {r: 0 <= r & r <= 1} by A2,A5,RCOMP_1:def 1;
then consider r such that
A7: r = x and
A8: 0 <= r and
A9: r <= 1;
y = (1-r)*p1 + r*p2 by A2,A3,A5,A6,A7;
then y in { (1-lambda)*p1 + lambda*p2: 0 <= lambda & lambda <= 1 } by A8
,A9;
then y in [#]((TOP-REAL n)|P) by PRE_TOPC:def 5;
hence thesis;
end;
then reconsider f as Function of I[01], (TOP-REAL n)|P by A2,BORSUK_1:40
,FUNCT_2:def 1,RELSET_1:4;
A10: I[01] is compact by HEINE:4,TOPMETR:20;
assume
A11: p1 <> p2;
now
let x1,x2 be object;
assume that
A12: x1 in dom f and
A13: x2 in dom f and
A14: f.x1 = f.x2;
x2 in {r: 0 <= r & r <= 1} by A2,A13,RCOMP_1:def 1;
then consider r2 being Real such that
A15: r2 = x2 and
0 <= r2 and
r2 <= 1;
A16: f.x2 = (1-r2)*p1 + r2*p2 by A2,A3,A13,A15;
x1 in {r: 0 <= r & r <= 1} by A2,A12,RCOMP_1:def 1;
then consider r1 being Real such that
A17: r1 = x1 and
0 <= r1 and
r1 <= 1;
f.x1 = (1-r1)*p1 + r1*p2 by A2,A3,A12,A17;
then
(1-r1)*p1 + r1*p2 + (-r1)*p2 = (1-r2)*p1 + (r2*p2 + (-r1)*p2) by A14,A16,
RLVECT_1:def 3;
then (1-r1)*p1 + r1*p2 + (-r1)*p2 = (1-r2)*p1 + (r2+(-r1))*p2 by
RLVECT_1:def 6;
then (1-r1)*p1 + (r1*p2 + (-r1)*p2) = (1-r2)*p1 + (r2-r1)*p2 by
RLVECT_1:def 3;
then (1-r1)*p1 + (r1+(-r1))*p2 = (1-r2)*p1 + (r2-r1)*p2 by RLVECT_1:def 6;
then (1-r1)*p1 + 0.TOP-REAL n = (1-r2)*p1 + (r2-r1)*p2 by RLVECT_1:10;
then
(-(1-r2))*p1 + (1-r1)*p1 = (-(1-r2))*p1 + ((1-r2)*p1 + (r2-r1)*p2) by
RLVECT_1:4;
then
(-(1-r2))*p1 + (1-r1)*p1 = ((-(1-r2))*p1 + (1-r2)*p1) + (r2-r1)*p2 by
RLVECT_1:def 3;
then (-(1-r2))*p1 + (1-r1)*p1 = (-(1-r2)+ (1-r2))*p1 + (r2-r1)*p2 by
RLVECT_1:def 6;
then (-(1-r2))*p1 + (1-r1)*p1 = 0.TOP-REAL n + (r2-r1)*p2 by RLVECT_1:10;
then (-(1-r2))*p1 + (1-r1)*p1 = (r2-r1)*p2 by RLVECT_1:4;
then ((r2-1)+(1-r1))*p1 = (r2-r1)*p2 by RLVECT_1:def 6;
then r2-r1 = 0 by A11,RLVECT_1:36;
hence x1 = x2 by A17,A15;
end;
then
A18: f is one-to-one;
[#]((TOP-REAL n)|P) c= rng f
proof
let a be object;
assume a in [#]((TOP-REAL n)|P);
then a in P by PRE_TOPC:def 5;
then consider lambda such that
A19: a = (1-lambda)*p1 + lambda*p2 and
A20: 0 <= lambda and
A21: lambda <= 1;
lambda in { r: 0 <= r & r <= 1} by A20,A21;
then
A22: lambda in dom f by A2,RCOMP_1:def 1;
then a = f.lambda by A2,A3,A19;
hence thesis by A22,FUNCT_1:def 3;
end;
then
A23: rng f = [#]((TOP-REAL n)|P) by A4;
A24: TopSpaceMetr(Euclid n) is T_2 by PCOMPS_1:34;
A25: (TOP-REAL n)|P = TopSpaceMetr((Euclid n)|PP) by EUCLID:63;
for W being Point of I[01], G being a_neighborhood of f.W ex H being
a_neighborhood of W st f.:H c= G
proof
reconsider p11=p1,p22=p2 as Point of Euclid n by EUCLID:67;
let W be Point of I[01], G be a_neighborhood of f.W;
reconsider W9 = W as Point of Closed-Interval-MSpace(0,1) by BORSUK_1:40
,TOPMETR:10;
A26: (Pitag_dist n).(p19,p29) = dist(p11,p22) by METRIC_1:def 1;
[#]((TOP-REAL n)|P) = P by PRE_TOPC:def 5;
then reconsider Y = f.W as Point of (Euclid n)|PP by TOPMETR:def 2;
A27: dist(p11,p22) >= 0 by METRIC_1:5;
reconsider W1 = W as Real;
P = the carrier of (Euclid n)|PP by TOPMETR:def 2;
then reconsider WW9 = Y as Point of Euclid n by TARSKI:def 3;
f.W in Int G by CONNSP_2:def 1;
then consider Q being Subset of (TOP-REAL n)|P such that
A28: Q is open and
A29: Q c= G and
A30: f.W in Q by TOPS_1:22;
consider r being Real such that
A31: r > 0 and
A32: Ball(Y,r) c= Q by A25,A28,A30,TOPMETR:15;
reconsider r as Element of REAL by XREAL_0:def 1;
set delta = r/(Pitag_dist n).(p19,p29);
reconsider H = Ball(W9,delta) as Subset of I[01] by BORSUK_1:40,TOPMETR:10;
Closed-Interval-TSpace(0,1) = TopSpaceMetr(Closed-Interval-MSpace(0,1
)) by TOPMETR:def 7;
then
A33: H is open by TOPMETR:14,20;
A34: dist(p11,p22) <> 0 by A11,METRIC_1:2;
then W in H by A31,A26,A27,TBSP_1:11,XREAL_1:139;
then W in Int H by A33,TOPS_1:23;
then reconsider H as a_neighborhood of W by CONNSP_2:def 1;
take H;
A35: delta > 0 by A31,A26,A27,A34,XREAL_1:139;
f.:H c= Ball(Y,r)
proof
reconsider WW1 = WW9 as Element of REAL n;
let a be object;
A36: rng f c= the carrier of (TOP-REAL n)|P by RELAT_1:def 19;
assume a in f.:H;
then consider u being object such that
A37: u in dom f and
A38: u in H and
A39: a = f.u by FUNCT_1:def 6;
reconsider u1 = u as Real by A2,A37;
A40: [#] ((TOP-REAL n)|P) = P by PRE_TOPC:def 5;
reconsider u9 = u as Point of Closed-Interval-MSpace(0,1) by A38;
reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR:8;
A41: dist(W9,u9) = (the distance of Closed-Interval-MSpace(0,1)).(W9,u9
) by METRIC_1:def 1
.= (the distance of RealSpace).(W99,u99) by TOPMETR:def 1
.= dist(W99,u99) by METRIC_1:def 1;
dist(W9,u9) < delta by A38,METRIC_1:11;
then |.W1-u1.| < delta by A41,TOPMETR:11;
then |.-(u1-W1).| < delta;
then
A42: |.u1-W1.| < delta by COMPLEX1:52;
A43: delta <> 0 by A31,A26,A27,A34,XREAL_1:139;
then (Pitag_dist n).(p19,p29) = r/delta by XCMPLX_1:54;
then
A44: |.p19 - p29.| = r/delta by EUCLID:def 6;
f.u in rng f by A37,FUNCT_1:def 3;
then reconsider aa = a as Point of (Euclid n)|PP by A39,A36,A40,
TOPMETR:def 2;
P = the carrier of (Euclid n)|PP by TOPMETR:def 2;
then reconsider aa9 = aa as Point of Euclid n by TARSKI:def 3;
reconsider aa1 = aa9 as Element of REAL n;
A45: p19 - p29 = p1 - p2 by EUCLID:69;
A46: WW1 = (1-W1)*p1 + W1*p2 by A3,BORSUK_1:40;
aa1 = ((1-u1)*p1 + u1*p2) by A2,A3,A37,A39;
then WW1 - aa1 = (1-W1)*p1 + W1*p2 - ((1-u1)*p1 + u1*p2) by A46,EUCLID:69
.= W1*p2 + (1-W1)*p1 - (1-u1)*p1 - u1*p2 by RLVECT_1:27
.= W1*p2 + ((1-W1)*p1 - (1-u1)*p1) - u1*p2 by RLVECT_1:def 3
.= W1*p2 + ((1-W1)-(1-u1))*p1 - u1*p2 by RLVECT_1:35
.= (u1-W1)*p1 + (W1*p2 - u1*p2) by RLVECT_1:def 3
.= (u1-W1)*p1 + (W1-u1)*p2 by RLVECT_1:35
.= (u1-W1)*p1 + (-(u1-W1))*p2
.= (u1-W1)*p1 + -(u1-W1)*p2 by RLVECT_1:79
.= (u1-W1)*p1 - (u1-W1)*p2
.= (u1-W1)*(p1 - p2) by RLVECT_1:34
.= (u1-W1)*(p19 - p29) by A45,EUCLID:65;
then
A47: |. WW1 -aa1 .| = |.u1-W1.|*|.p19 - p29.| by EUCLID:11;
r/delta > 0 by A31,A35,XREAL_1:139;
then |. WW1 - aa1.| < delta*(r/delta) by A47,A42,A44,XREAL_1:68;
then |. WW1 - aa1 .| < r by A43,XCMPLX_1:87;
then (the distance of Euclid n).(WW9,aa9) < r by EUCLID:def 6;
then (the distance of (Euclid n)|PP).(Y,aa) < r by TOPMETR:def 1;
then dist(Y,aa) < r by METRIC_1:def 1;
hence thesis by METRIC_1:11;
end;
then f.:H c= Q by A32;
hence thesis by A29;
end;
then
A48: f is continuous by BORSUK_1:def 1;
take f;
A49: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8;
then reconsider PP = P as Subset of TopSpaceMetr(Euclid n);
(TopSpaceMetr(Euclid n))|PP = (TOP-REAL n)|P by A49,PRE_TOPC:36;
then (TOP-REAL n)|P is T_2 by A24,TOPMETR:2;
hence f is being_homeomorphism by A23,A18,A48,A10,COMPTS_1:17;
0 in [.0,1.] by XXREAL_1:1;
hence f.0 = (1-0)*p1 + 0 * p2 by A3
.= p1 + 0 * p2 by RLVECT_1:def 8
.= p1 + 0.TOP-REAL n by RLVECT_1:10
.= p1 by RLVECT_1:4;
1 in [.0,1.] by XXREAL_1:1;
hence f.1 = (1-1)*p1 + 1*p2 by A3
.= 0.TOP-REAL n + 1*p2 by RLVECT_1:10
.= 1*p2 by RLVECT_1:4
.= p2 by RLVECT_1:def 8;
end;
registration
let n;
cluster TOP-REAL n -> T_2;
coherence
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then the TopStruct of TOP-REAL n is T_2 by PCOMPS_1:34;
hence thesis by Lm2;
end;
end;
theorem Th10:
for P being Subset of TOP-REAL n, p1,p2,q1 being Point of
TOP-REAL n st P is_an_arc_of p1,p2 & P /\ LSeg(p2,q1) = {p2} holds P \/ LSeg(p2
,q1) is_an_arc_of p1,q1
proof
let P be Subset of TOP-REAL n, p1,p2,q1 be Point of TOP-REAL n;
assume that
A1: P is_an_arc_of p1,p2 and
A2: P /\ LSeg(p2,q1) = {p2};
per cases;
suppose
p2 <> q1;
then LSeg(p2,q1) is_an_arc_of p2,q1 by Th9;
hence thesis by A1,A2,Th2;
end;
suppose
A3: p2 = q1;
then
A4: LSeg(p2,q1) = {q1} by RLTOPSP1:70;
q1 in P by A1,A3,Th1;
hence thesis by A1,A3,A4,ZFMISC_1:40;
end;
end;
theorem Th11:
for P being Subset of TOP-REAL n, p1,p2,q1 being Point of
TOP-REAL n st P is_an_arc_of p2,p1 & LSeg(q1,p2) /\ P = {p2} holds LSeg(q1,p2)
\/ P is_an_arc_of q1,p1
proof
let P be Subset of TOP-REAL n, p1,p2,q1 be Point of TOP-REAL n;
assume that
A1: P is_an_arc_of p2,p1 and
A2: LSeg(q1,p2) /\ P = {p2};
per cases;
suppose
p2 <> q1;
then LSeg(q1,p2) is_an_arc_of q1,p2 by Th9;
hence thesis by A1,A2,Th2;
end;
suppose
A3: p2 = q1;
then
A4: LSeg(q1,p2) = {q1} by RLTOPSP1:70;
q1 in P by A1,A3,Th1;
hence thesis by A1,A3,A4,ZFMISC_1:40;
end;
end;
theorem
for p1,p2,q1 being Point of TOP-REAL n st (p1 <> p2 or p2 <> q1) &
LSeg(p1,p2) /\ LSeg(p2,q1) = {p2} holds LSeg(p1,p2) \/ LSeg(p2,q1) is_an_arc_of
p1,q1
proof
let p1,p2,q1 be Point of TOP-REAL n;
assume that
A1: p1 <> p2 or p2 <> q1 and
A2: LSeg(p1,p2) /\ LSeg(p2,q1) = {p2};
per cases by A1;
suppose
p1 <> p2;
hence thesis by A2,Th9,Th10;
end;
suppose
p2 <> q1;
hence thesis by A2,Th9,Th11;
end;
end;
theorem Th13:
LSeg(|[ 0,0 ]|, |[ 0,1 ]|) = { p1 : p1`1 = 0 & p1`2 <= 1 & p1`2
>= 0} & LSeg(|[ 0,1 ]|, |[ 1,1 ]|) = { p2 : p2`1 <= 1 & p2`1 >= 0 & p2`2 = 1} &
LSeg(|[ 0,0 ]|, |[ 1,0 ]|) = { q1 : q1`1 <= 1 & q1`1 >= 0 & q1`2 = 0} & LSeg(|[
1,0 ]|, |[ 1,1 ]|) = { q2 : q2`1 = 1 & q2`2 <= 1 & q2`2 >= 0}
proof
set p0 = |[ 0,0 ]|, p01 = |[ 0,1 ]|, p10 = |[ 1,0 ]|, p1 = |[ 1,1 ]|;
set L1 = { p : p`1 = 0 & p`2 <= 1 & p`2 >= 0}, L2 = { p : p`1 <= 1 & p`1 >=
0 & p`2 = 1}, L3 = { p : p`1 <= 1 & p`1 >= 0 & p`2 = 0}, L4 = { p : p`1 = 1 & p
`2 <= 1 & p`2 >= 0};
A1: p01`2 = 1 by EUCLID:52;
A2: p01`1 = 0 by EUCLID:52;
A3: LSeg(p0,p01) c= L1
proof
let a be object;
assume a in LSeg(p0,p01);
then consider lambda such that
A4: a = (1-lambda)*p0 + lambda*p01 and
A5: 0 <= lambda and
A6: lambda <= 1;
set q = (1-lambda)*p0 + lambda*p01;
A7: (1-lambda)*p0 + lambda*p01 = 0.TOP-REAL 2 + lambda*p01 by EUCLID:54
,RLVECT_1:10
.= lambda*p01 by RLVECT_1:4
.= |[lambda*(p01`1), lambda*(p01`2) ]| by EUCLID:57
.= |[ 0, lambda ]| by A2,A1;
then
A8: q`2 >= 0 by A5,EUCLID:52;
A9: q`1 = 0 by A7,EUCLID:52;
q`2 <= 1 by A6,A7,EUCLID:52;
hence thesis by A4,A9,A8;
end;
L1 c= LSeg(p0,p01)
proof
let a be object;
assume a in L1;
then consider p such that
A10: a = p and
A11: p`1 = 0 and
A12: p`2 <= 1 and
A13: p`2 >= 0;
set lambda = p`2;
(1-lambda)*p0 + lambda*p01 = 0.TOP-REAL 2 + lambda*p01 by EUCLID:54
,RLVECT_1:10
.= lambda*p01 by RLVECT_1:4
.= |[lambda*p01`1, lambda*p01`2 ]| by EUCLID:57
.= p by A2,A1,A11,EUCLID:53;
hence thesis by A10,A12,A13;
end;
hence L1 = LSeg(p0,p01) by A3;
A14: p1`2 = 1 by EUCLID:52;
A15: p1`1 = 1 by EUCLID:52;
A16: LSeg(p01,p1) c= L2
proof
let a be object;
assume a in LSeg(p01,p1);
then consider lambda such that
A17: a = (1-lambda)*p01 + lambda*p1 and
A18: 0 <= lambda and
A19: lambda <= 1;
set q = (1-lambda)*p01 + lambda*p1;
A20: (1-lambda)*p01 + lambda*p1 = |[(1-lambda)*0, (1-lambda)*p01`2]| +
lambda*p1 by A2,EUCLID:57
.= |[0, 1-lambda]| + |[lambda, lambda*1]| by A1,A15,A14,EUCLID:57
.= |[0+lambda, 1-lambda+lambda]| by EUCLID:56
.= |[lambda, 1]|;
then
A21: q`1 >= 0 by A18,EUCLID:52;
A22: q`2 = 1 by A20,EUCLID:52;
q`1 <= 1 by A19,A20,EUCLID:52;
hence thesis by A17,A21,A22;
end;
L2 c= LSeg(p01,p1)
proof
let a be object;
assume a in L2;
then consider p such that
A23: a = p and
A24: p`1 <= 1 and
A25: p`1 >= 0 and
A26: p`2 = 1;
set lambda = p`1;
(1-lambda)*p01 + lambda*p1 = |[(1-lambda)*0, (1-lambda)*p01`2]| +
lambda*p1 by A2,EUCLID:57
.= |[0, 1-lambda]| + |[lambda*1, lambda]| by A1,A15,A14,EUCLID:57
.= |[0+lambda, 1-lambda+lambda]| by EUCLID:56
.= p by A26,EUCLID:53;
hence thesis by A23,A24,A25;
end;
hence L2 = LSeg(p01,p1) by A16;
A27: p10`2 = 0 by EUCLID:52;
A28: p10`1 = 1 by EUCLID:52;
A29: LSeg(p0,p10) c= L3
proof
let a be object;
assume a in LSeg(p0,p10);
then consider lambda such that
A30: a = (1-lambda)*p0 + lambda*p10 and
A31: 0 <= lambda and
A32: lambda <= 1;
set q =(1-lambda)*p0 + lambda*p10;
A33: (1-lambda)*p0 + lambda*p10 = 0.TOP-REAL 2 + lambda*p10 by EUCLID:54
,RLVECT_1:10
.= lambda*p10 by RLVECT_1:4
.= |[ lambda*(p10`1), lambda*(p10`2) ]| by EUCLID:57
.= |[ lambda, 0 ]| by A28,A27;
then
A34: q`1 >= 0 by A31,EUCLID:52;
A35: q`2 = 0 by A33,EUCLID:52;
q`1 <= 1 by A32,A33,EUCLID:52;
hence thesis by A30,A34,A35;
end;
A36: LSeg(p10,p1) c= L4
proof
let a be object;
assume a in LSeg(p10,p1);
then consider lambda such that
A37: a = (1-lambda)*p10 + lambda*p1 and
A38: 0 <= lambda and
A39: lambda <= 1;
set q = (1-lambda)*p10 + lambda*p1;
A40: (1-lambda)*p10 + lambda*p1 = |[(1-lambda)*1, (1-lambda)*p10`2]| +
lambda*p1 by A28,EUCLID:57
.= |[(1-lambda), 0]| + |[lambda, lambda*1]| by A15,A14,A27,EUCLID:57
.= |[1-lambda+lambda, 0+lambda]| by EUCLID:56
.= |[1, lambda]|;
then
A41: q`2 >= 0 by A38,EUCLID:52;
A42: q`1 = 1 by A40,EUCLID:52;
q`2 <= 1 by A39,A40,EUCLID:52;
hence thesis by A37,A42,A41;
end;
L3 c= LSeg(p0,p10)
proof
let a be object;
assume a in L3;
then consider p such that
A43: a = p and
A44: p`1 <= 1 and
A45: p`1 >= 0 and
A46: p`2 = 0;
set lambda = p`1;
(1-lambda)*p0 + lambda*p10 = 0.TOP-REAL 2 + lambda*p10 by EUCLID:54
,RLVECT_1:10
.= lambda*p10 by RLVECT_1:4
.= |[lambda*p10`1, lambda*p10`2 ]| by EUCLID:57
.= p by A28,A27,A46,EUCLID:53;
hence thesis by A43,A44,A45;
end;
hence L3 = LSeg(p0,p10) by A29;
L4 c= LSeg(p10,p1)
proof
let a be object;
assume a in L4;
then consider p such that
A47: a = p and
A48: p`1 = 1 and
A49: p`2 <= 1 and
A50: p`2 >= 0;
set lambda = p`2;
(1-lambda)*p10 + lambda*p1 = |[(1-lambda)*1, (1-lambda)*p10`2]| +
lambda*p1 by A28,EUCLID:57
.= |[(1-lambda), 0]| + |[lambda*1, lambda]| by A15,A14,A27,EUCLID:57
.= |[1-lambda+lambda, 0+lambda]| by EUCLID:56
.= p by A48,EUCLID:53;
hence thesis by A47,A49,A50;
end;
hence L4 = LSeg(p10,p1) by A36;
end;
theorem
R^2-unit_square ={ p : p`1 = 0 & p`2 <= 1 & p`2 >= 0 or p`1 <= 1 & p`1
>= 0 & p`2 = 1 or p`1 <= 1 & p`1 >= 0 & p`2 = 0 or p`1 = 1 & p`2 <= 1 & p`2 >=
0}
proof
defpred X4[Point of TOP-REAL 2] means $1`1 = 1 & $1`2 <= 1 & $1`2 >= 0;
defpred X3[Point of TOP-REAL 2] means $1`1 <= 1 & $1`1 >= 0 & $1`2 = 0;
defpred X2[Point of TOP-REAL 2] means $1`1 <= 1 & $1`1 >= 0 & $1`2 = 1;
defpred X1[Point of TOP-REAL 2] means $1`1 = 0 & $1`2 <= 1 & $1`2 >= 0;
defpred X34[Point of TOP-REAL 2] means $1`1 <= 1 & $1`1 >= 0 & $1`2 = 0 or
$1`1 = 1 & $1`2 <= 1 & $1`2 >= 0;
defpred X12[Point of TOP-REAL 2] means $1`1 = 0 & $1`2 <= 1 & $1`2 >= 0 or
$1`1 <= 1 & $1`1 >= 0 & $1`2 = 1;
set L1 = { p : X1[p]}, L2 = { p : X2[p]}, L3 = { p : X3[p]}, L4 = { p : X4[p
]};
A1: { p2 : X12[p2] or X34[p2] } = { p : X12[p] } \/ { q1: X34[q1] } from
FraenkelAlt;
A2: { q1: X3[q1] or X4[q1] } = L3 \/ L4 from FraenkelAlt
.= LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by Th13;
{ p : X1[p] or X2[p] } = L1 \/ L2 from FraenkelAlt
.= LSeg(|[0,0]|,|[0,1]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|) by Th13;
hence thesis by A1,A2;
end;
registration
cluster R^2-unit_square -> non empty;
coherence;
end;
theorem
LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,1]|,|[1,1]|) = {|[0,1]|}
proof
for a being object holds a in LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,1]|,|[1,1]|
) iff a = |[0,1]|
proof
set p00 = |[0,0]|, p01 = |[0,1]|, p11 = |[1,1]|;
let a be object;
thus a in LSeg(p00,p01) /\ LSeg(p01,p11) implies a = p01
proof
assume
A1: a in LSeg(p00,p01) /\ LSeg(p01,p11);
then a in {p2 : p2`1 <= 1 & p2`1 >= 0 & p2`2 = 1} by Th13,XBOOLE_0:def 4;
then
A2: ex p2 st p2=a & p2`1<=1 & p2`1>=0 & p2`2=1;
a in {p : p`1 = 0 & p`2 <= 1 & p`2 >= 0} by A1,Th13,XBOOLE_0:def 4;
then ex p st p = a & p`1 = 0 & p`2 <= 1 & p`2 >= 0;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = p01;
then
A4: a in LSeg(p01,p11) by RLTOPSP1:68;
a in LSeg(p00,p01) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
LSeg(|[0,0]|,|[1,0]|) /\ LSeg(|[1,0]|,|[1,1]|) = {|[1,0]|}
proof
for a being object holds a in LSeg(|[0,0]|,|[1,0]|) /\ LSeg(|[1,0]|,|[1,1]|
) iff a = |[1,0]|
proof
set p00 = |[0,0]|, p10 = |[1,0]|, p11 = |[1,1]|;
let a be object;
thus a in LSeg(p00,p10) /\ LSeg(p10,p11) implies a = p10
proof
assume
A1: a in LSeg(p00,p10) /\ LSeg(p10,p11);
then a in { p : p`1 <= 1 & p`1 >= 0 & p`2 = 0} by Th13,XBOOLE_0:def 4;
then
A2: ex p st p = a & p`1 <= 1 & p`1 >= 0 & p`2 = 0;
a in LSeg(p10,p11) by A1,XBOOLE_0:def 4;
then ex p2 st p2=a & p2`1 = 1 & p2`2 <= 1 & p2`2 >= 0 by Th13;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = |[1,0]|;
then
A4: a in LSeg(p10,p11) by RLTOPSP1:68;
a in LSeg(p00,p10) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th17:
LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,0]|,|[1,0]|) = {|[0,0]|}
proof
for a being object holds a in LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,0]|,|[1,0]|
) iff a = |[0,0]|
proof
let a be object;
thus a in LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,0]|,|[1,0]|) implies a = |[0,0
]|
proof
assume
A1: a in LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[0,0]|,|[1,0]|);
then a in { p2 : p2`1 <= 1 & p2`1 >= 0 & p2`2 = 0 } by Th13,
XBOOLE_0:def 4;
then
A2: ex p2 st p2 = a & p2`1 <= 1 & p2`1 >= 0 & p2`2 = 0;
a in LSeg(|[0,0]|,|[0,1]|) by A1,XBOOLE_0:def 4;
then ex p st p = a & p`1 = 0 & p`2 <= 1 & p`2 >= 0 by Th13;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = |[0,0]|;
then
A4: a in LSeg(|[0,0]|,|[1,0]|) by RLTOPSP1:68;
a in LSeg(|[0,0]|,|[0,1]|) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th18:
LSeg(|[0,1]|,|[1,1]|) /\ LSeg(|[1,0]|,|[1,1]|) = {|[1,1]|}
proof
for a being object holds a in LSeg(|[0,1]|,|[1,1]|) /\ LSeg(|[1,0]|,|[1,1]|
) iff a = |[1,1]|
proof
let a be object;
thus a in LSeg(|[0,1]|,|[1,1]|) /\ LSeg(|[1,0]|,|[1,1]|) implies a = |[1,1
]|
proof
assume
A1: a in LSeg(|[0,1]|,|[1,1]|) /\ LSeg(|[1,0]|,|[1,1]|);
then a in { p : p`1 <= 1 & p`1 >= 0 & p`2 = 1} by Th13,XBOOLE_0:def 4;
then
A2: ex p st p = a & p`1 <= 1 & p`1 >= 0 & p`2 = 1;
a in LSeg(|[1,0]|,|[1,1]|) by A1,XBOOLE_0:def 4;
then ex p2 st p2 = a & p2`1 = 1 & p2`2 <= 1 & p2`2 >= 0 by Th13;
hence thesis by A2,EUCLID:53;
end;
assume
A3: a = |[1,1]|;
then
A4: a in LSeg(|[1,0]|,|[1,1]|) by RLTOPSP1:68;
a in LSeg(|[0,1]|,|[1,1]|) by A3,RLTOPSP1:68;
hence thesis by A4,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
LSeg(|[0,0]|,|[1,0]|) misses LSeg(|[0,1]|,|[1,1]|)
proof
set x = the Element of LSeg(|[0,0]|,|[1,0]|) /\ LSeg(|[0,1]|,|[1,1]|);
assume
A1: LSeg(|[0,0]|,|[1,0]|) /\ LSeg(|[0,1]|,|[1,1]|) <> {};
then x in LSeg(|[0,1]|,|[1,1]|) by XBOOLE_0:def 4;
then
A2: ex p st p = x & p`1 <= 1 & p`1 >= 0 & p`2 = 1 by Th13;
x in LSeg(|[0,0]|,|[1,0]|) by A1,XBOOLE_0:def 4;
then ex p2 st p2 = x & p2`1 <= 1 & p2`1 >= 0 & p2`2 = 0 by Th13;
hence contradiction by A2;
end;
theorem Th20:
LSeg(|[0,0]|,|[0,1]|) misses LSeg(|[1,0]|,|[1,1]|)
proof
set x = the Element of LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[1,0]|,|[1,1]|);
assume
A1: LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[1,0]|,|[1,1]|) <> {};
then x in LSeg(|[0,0]|,|[0,1]|) by XBOOLE_0:def 4;
then
A2: ex p st p = x & p`1 = 0 & p`2 <= 1 & p`2 >= 0 by Th13;
x in LSeg(|[1,0]|,|[1,1]|) by A1,XBOOLE_0:def 4;
then ex p2 st p2 = x & p2`1 = 1 & p2`2 <= 1 & p2`2 >= 0 by Th13;
hence contradiction by A2;
end;
definition
let n;
let f be FinSequence of TOP-REAL n;
let i;
func LSeg(f,i) -> Subset of TOP-REAL n equals
:Def3:
LSeg(f/.i,f/.(i+1)) if
1 <= i & i+1 <= len f otherwise {};
coherence
proof
thus 1 <= i & i+1 <= len f implies LSeg(f/.i,f/.(i+1)) is Subset of
TOP-REAL n;
assume i < 1 or len f < i+1;
{}(TOP-REAL n) is Subset of TOP-REAL n;
hence thesis;
end;
correctness;
end;
theorem Th21:
for f being FinSequence of TOP-REAL n st 1 <= i & i+1 <= len f
holds f/.i in LSeg(f,i) & f/.(i+1) in LSeg(f,i)
proof
let f be FinSequence of TOP-REAL n;
assume that
A1: 1 <= i and
A2: i+1 <= len f;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,Def3;
hence thesis by RLTOPSP1:68;
end;
definition
let n;
let f be FinSequence of TOP-REAL n;
func L~f -> Subset of TOP-REAL n equals
union { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f };
coherence
proof
set F = { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f };
F c= bool the carrier of TOP-REAL n
proof
let a be object;
assume a in F;
then ex i be Nat st a = LSeg(f,i) & 1 <= i & i+1 <= len f;
hence thesis;
end;
then reconsider F as Subset-Family of TOP-REAL n;
union F is Subset of TOP-REAL n;
hence thesis;
end;
end;
theorem Th22:
for f being FinSequence of TOP-REAL n holds len f = 0 or len f =
1 iff L~f = {}
proof
let f be FinSequence of TOP-REAL n;
thus (len f = 0 or len f = 1) implies L~f = {}
proof
set L = { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f };
set x = the Element of L;
assume
A1: len f = 0 or len f = 1;
now
per cases by A1;
suppose
A2: len f = 0;
now
assume L <> {};
then x in L;
then
ex i being Nat st x = LSeg(f,i) & 1 <= i & i+1 <= len f;
hence contradiction by A2;
end;
hence thesis by ZFMISC_1:2;
end;
suppose
A3: len f = 0+1;
now
assume L <> {};
then x in L;
then ex i being Nat st x = LSeg(f,i) & 1 <= i & i+1 <=
len f;
hence contradiction by A3,XREAL_1:6;
end;
hence thesis by ZFMISC_1:2;
end;
end;
hence thesis;
end;
set L = { LSeg(f,i) where i is Nat : 1 <= i & i+1 <= len f };
assume
A4: L~f = {};
assume that
A5: len f <> 0 and
A6: len f <> 1;
now
assume len f <= 1;
then len f < 0+1 by A6,XXREAL_0:1;
hence contradiction by A5,NAT_1:13;
end;
then
A7: len f >= 1+1 by NAT_1:13;
then LSeg(f,1) in L;
then LSeg(f,1) = {} by A4,XBOOLE_1:3,ZFMISC_1:74;
hence contradiction by A7,Th21;
end;
theorem Th23:
for f being FinSequence of TOP-REAL n holds len f >= 2 implies L~f <> {}
proof
let f be FinSequence of TOP-REAL n;
assume
A1: len f >= 2;
then not len f = 1;
hence thesis by A1,Th22;
end;
definition
let IT be FinSequence of TOP-REAL 2;
attr IT is special means
for i st 1 <= i & i+1 <= len IT holds (IT/.i)`1 = (
IT/.(i+1))`1 or (IT/.i)`2 = (IT/.(i+1))`2;
attr IT is unfolded means
for i st 1 <= i & i + 2 <= len IT holds
LSeg(IT,i) /\ LSeg(IT,i+1) = {IT/.(i+1)};
attr IT is s.n.c. means
for i,j st i+1 < j holds LSeg(IT,i) misses LSeg(IT,j);
end;
reserve f,f1,f2,h for FinSequence of TOP-REAL 2;
definition
let f;
attr f is being_S-Seq means
f is one-to-one & len f >= 2 & f is unfolded s.n.c. special;
end;
theorem Th24:
ex f1,f2 st f1 is being_S-Seq & f2 is being_S-Seq &
R^2-unit_square = L~f1 \/ L~f2 & L~f1 /\ L~f2 = {|[ 0,0 ]|, |[ 1,1 ]|} & f1/.1
= |[0,0]| & f1/.len f1=|[1,1]| & f2/.1 = |[0,0]| & f2/.len f2 = |[1,1]|
proof
set p0 = |[ 0,0 ]|, p01 = |[ 0,1 ]|, p10 = |[ 1,0 ]|, p1 = |[ 1,1 ]|;
set L4 = { p : p`1 = 1 & p`2 <= 1 & p`2 >= 0};
set L3 = { p : p`1 <= 1 & p`1 >= 0 & p`2 = 0};
set L2 = { p : p`1 <= 1 & p`1 >= 0 & p`2 = 1};
set L1 = { p : p`1 = 0 & p`2 <= 1 & p`2 >= 0};
A1: p1`1 = 1 by EUCLID:52;
reconsider f2 = <* p0,p10,p1 *> as FinSequence of TOP-REAL 2;
reconsider f1 = <* p0,p01,p1 *> as FinSequence of TOP-REAL 2;
A2: p0`1 = 0 by EUCLID:52;
take f1,f2;
A3: f1/.2 = p01 by FINSEQ_4:18;
now
assume L2 meets L3;
then consider x being object such that
A4: x in L2 and
A5: x in L3 by XBOOLE_0:3;
A6: ex p2 st p2 = x & p2`1 <= 1 & p2`1 >= 0 & p2`2 = 0 by A5;
ex p st p = x & p`1 <= 1 & p`1 >= 0 & p`2 = 1 by A4;
hence contradiction by A6;
end;
then
A7: L2 /\ L3 = {};
A8: p10`2 = 0 by EUCLID:52;
A9: p10`1 = 1 by EUCLID:52;
A10: len f2 = 1 + 2 by FINSEQ_1:45;
then
A11: 1+1 <= len f2;
A12: f1/.3 = p1 by FINSEQ_4:18;
A13: f1/.1 = p0 by FINSEQ_4:18;
A14: {LSeg(f1,i) where i is Nat: 1 <= i & i+1 <= len f1} c= {LSeg
(p0,p01),LSeg(p01,p1)}
proof
let a be object;
assume a in {LSeg(f1,i) where i is Nat: 1 <= i & i+1 <= len f1};
then consider i being Nat such that
A15: a = LSeg(f1,i) and
A16: 1<=i and
A17: i+1<=len f1;
i+1 <= 2 + 1 by A17,FINSEQ_1:45;
then i <= 1 + 1 by XREAL_1:6;
then i = 1 or i = 2 by A16,NAT_1:9;
then a = LSeg(p0,p01) or a = LSeg(p01,p1) by A13,A3,A12,A15,A17,Def3;
hence thesis by TARSKI:def 2;
end;
A18: len f1 = 1 + 2 by FINSEQ_1:45;
then
A19: 1+1 <= len f1;
1+1 in Seg len f1 by A18,FINSEQ_1:1;
then LSeg(p0,p01) = LSeg(f1,1) by A18,A13,A3,Def3;
then
A20: LSeg(p0,p01) in {LSeg(f1,i) where i is Nat: 1 <= i & i+1 <=
len f1} by A19;
A21: f2/.3 = p1 by FINSEQ_4:18;
A22: p0`2 = 0 by EUCLID:52;
thus f1 is being_S-Seq
proof
A23: p01 <> p1 by A1,EUCLID:52;
p0 <> p01 by A22,EUCLID:52;
hence f1 is one-to-one by A1,A2,A23,FINSEQ_3:95;
thus len f1 >= 2 by A18;
thus f1 is unfolded
proof
A24: for x being object holds x in LSeg(p0,p01) /\ LSeg(p01,p1) iff x = p01
proof
let x be object;
thus x in LSeg(p0,p01) /\ LSeg(p01,p1) implies x = p01
proof
assume
A25: x in LSeg(p0,p01) /\ LSeg(p01,p1);
then x in {p2 : p2`1 <= 1 & p2`1 >= 0 & p2`2 = 1} by Th13,
XBOOLE_0:def 4;
then
A26: ex p2 st p2=x & p2`1<=1 & p2`1>=0 & p2`2=1;
x in {p : p`1 = 0 & p`2 <= 1 & p`2 >= 0} by A25,Th13,XBOOLE_0:def 4;
then ex p st p = x & p`1 = 0 & p`2 <= 1 & p`2 >= 0;
hence thesis by A26,EUCLID:53;
end;
assume
A27: x = p01;
then
A28: x in LSeg(p01,p1) by RLTOPSP1:68;
x in LSeg(p0,p01) by A27,RLTOPSP1:68;
hence thesis by A28,XBOOLE_0:def 4;
end;
let i;
assume that
A29: 1 <= i and
A30: i + 2 <= len f1;
i <= 1 by A18,A30,XREAL_1:6;
then
A31: i = 1 by A29,XXREAL_0:1;
1+1 in Seg len f1 by A18,FINSEQ_1:1;
then
A32: LSeg(f1,1) = LSeg(p0,p01) by A18,A13,A3,Def3;
LSeg(f1,1+1) = LSeg(p01,p1) by A18,A3,A12,Def3;
hence thesis by A3,A31,A32,A24,TARSKI:def 1;
end;
thus f1 is s.n.c.
proof
let i,j such that
A33: i+1 < j;
now
per cases;
suppose
1 <= i;
then
A34: 1+1 <= i+1 by XREAL_1:6;
now
per cases;
case
1 <= j & j+1 <= len f1;
then j <= 2 by A18,XREAL_1:6;
hence contradiction by A33,A34,XXREAL_0:2;
end;
case
not (1 <= j & j+1 <= len f1);
then LSeg(f1,j) = {} by Def3;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
end;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
suppose
not (1 <= i & i+1 <= len f1);
then LSeg(f1,i) = {} by Def3;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
end;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
let i;
assume that
A35: 1 <= i and
A36: i + 1 <= len f1;
A37: i <= 1 + 1 by A18,A36,XREAL_1:6;
per cases by A35,A37,NAT_1:9;
suppose
A38: i = 1;
then (f1/.i)`1 = p0`1 by FINSEQ_4:18
.= 0 by EUCLID:52
.= (f1/.(i+1))`1 by A3,A38,EUCLID:52;
hence thesis;
end;
suppose
A39: i = 2;
then (f1/.i)`2 = p01`2 by FINSEQ_4:18
.= 1 by EUCLID:52
.= (f1/.(i+1))`2 by A12,A39,EUCLID:52;
hence thesis;
end;
end;
A40: f2/.2 = p10 by FINSEQ_4:18;
A41: f2/.1 = p0 by FINSEQ_4:18;
A42: {LSeg(f2,i) where i is Nat: 1 <= i & i+1 <= len f2} c= {
LSeg(p0,p10),LSeg(p10,p1)}
proof
let a be object;
assume a in {LSeg(f2,i) where i is Nat: 1 <= i & i+1 <= len f2};
then consider i being Nat such that
A43: a = LSeg(f2,i) and
A44: 1<=i and
A45: i+1<=len f2;
i+1 <= 2 + 1 by A45,FINSEQ_1:45;
then i <= 1 + 1 by XREAL_1:6;
then i = 1 or i = 2 by A44,NAT_1:9;
then a = LSeg(p0,p10) or a = LSeg(p10,p1) by A41,A40,A21,A43,A45,Def3;
hence thesis by TARSKI:def 2;
end;
1+1 in Seg len f2 by A10,FINSEQ_1:1;
then LSeg(p0,p10) = LSeg(f2,1) by A10,A41,A40,Def3;
then
A46: LSeg(p0,p10) in {LSeg(f2,i) where i is Nat: 1 <= i & i+1 <=
len f2} by A11;
LSeg(p10,p1) = LSeg(f2,2) by A10,A40,A21,Def3;
then LSeg(p10,p1) in {LSeg(f2,i) where i is Nat: 1 <= i & i+1 <=
len f2} by A10;
then {LSeg(p0,p10),LSeg(p10,p1)} c= {LSeg(f2,i) where i is Nat:1
<=i & i+1<=len f2} by A46,ZFMISC_1:32;
then
A47: L~f2 = union {LSeg(p0,p10),LSeg(p10,p1)} by A42,XBOOLE_0:def 10;
A48: p1`2 = 1 by EUCLID:52;
thus f2 is being_S-Seq
proof
thus f2 is one-to-one by A1,A48,A9,A8,A2,FINSEQ_3:95;
thus len f2 >= 2 by A10;
thus f2 is unfolded
proof
A49: for x being object holds x in LSeg(p0,p10) /\ LSeg(p10,p1) iff x = p10
proof
let x be object;
thus x in LSeg(p0,p10) /\ LSeg(p10,p1) implies x = p10
proof
assume
A50: x in LSeg(p0,p10) /\ LSeg(p10,p1);
then x in { p2 : p2`1 = 1 & p2`2 <= 1 & p2`2 >= 0} by Th13,
XBOOLE_0:def 4;
then
A51: ex p2 st p2=x & p2`1=1 & p2`2<=1 & p2`2>=0;
x in { p : p`1 <= 1 & p`1 >= 0 & p`2 = 0} by A50,Th13,XBOOLE_0:def 4;
then ex p st p = x & p`1 <= 1 & p`1 >= 0 & p`2 = 0;
hence thesis by A51,EUCLID:53;
end;
assume
A52: x = p10;
then
A53: x in LSeg(p10,p1) by RLTOPSP1:68;
x in LSeg(p0,p10) by A52,RLTOPSP1:68;
hence thesis by A53,XBOOLE_0:def 4;
end;
let i;
assume that
A54: 1 <= i and
A55: i + 2 <= len f2;
i <= 1 by A10,A55,XREAL_1:6;
then
A56: i = 1 by A54,XXREAL_0:1;
1+1 in Seg len f2 by A10,FINSEQ_1:1;
then
A57: LSeg(f2,1) = LSeg(p0,p10) by A10,A41,A40,Def3;
LSeg(f2,1+1) = LSeg(p10,p1) by A10,A40,A21,Def3;
hence thesis by A40,A56,A57,A49,TARSKI:def 1;
end;
thus f2 is s.n.c.
proof
let i,j such that
A58: i+1 < j;
per cases;
suppose
1 <= i;
then
A59: 1+1 <= i+1 by XREAL_1:6;
now
per cases;
case
1 <= j & j+1 <= len f2;
then j <= 2 by A10,XREAL_1:6;
hence contradiction by A58,A59,XXREAL_0:2;
end;
case
not (1 <= j & j+1 <= len f2);
then LSeg(f2,j) = {} by Def3;
hence LSeg(f2,i) /\ LSeg(f2,j) = {};
end;
end;
hence LSeg(f2,i) /\ LSeg(f2,j) = {};
end;
suppose
not (1 <= i & i+1 <= len f2);
then LSeg(f2,i) = {} by Def3;
hence LSeg(f2,i) /\ LSeg(f2,j) = {};
end;
end;
let i;
assume that
A60: 1 <= i and
A61: i + 1 <= len f2;
A62: i <= 1 + 1 by A10,A61,XREAL_1:6;
per cases by A60,A62,NAT_1:9;
suppose
A63: i = 1;
then (f2/.i)`2 = p0`2 by FINSEQ_4:18
.= 0 by EUCLID:52
.= (f2/.(i+1))`2 by A40,A63,EUCLID:52;
hence thesis;
end;
suppose
A64: i = 2;
then (f2/.i)`1 = p10`1 by FINSEQ_4:18
.= 1 by EUCLID:52
.= (f2/.(i+1))`1 by A21,A64,EUCLID:52;
hence thesis;
end;
end;
A65: LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[1,0]|,|[1,1]|) = {} by Th20;
LSeg(p01,p1) = LSeg(f1,2) by A18,A3,A12,Def3;
then LSeg(p01,p1) in {LSeg(f1,i) where i is Nat: 1 <= i & i+1 <=
len f1} by A18;
then {LSeg(p0,p01),LSeg(p01,p1)} c= {LSeg(f1,i) where i is Nat:1
<=i & i+1<=len f1} by A20,ZFMISC_1:32;
then
A66: L~f1 = union {LSeg(p0,p01),LSeg(p01,p1)} by A14,XBOOLE_0:def 10;
then L~f1 = (LSeg(p0,p01) \/ LSeg(p01,p1)) by ZFMISC_1:75;
hence R^2-unit_square = L~f1 \/ L~f2 by A47,ZFMISC_1:75;
L~f2 = (LSeg(p0,p10) \/ LSeg(p10,p1)) by A47,ZFMISC_1:75;
hence L~f1 /\ L~f2 = (L1 \/ L2) /\ (L3 \/ L4) by A66,Th13,ZFMISC_1:75
.= (L1 \/ L2) /\ L3 \/ (L1 \/ L2) /\ L4 by XBOOLE_1:23
.= L1 /\ L3 \/ L2 /\ L3 \/ (L1 \/ L2) /\ L4 by XBOOLE_1:23
.= L1 /\ L3 \/ L2 /\ L3 \/ (L1 /\ L4 \/ L2 /\ L4) by XBOOLE_1:23
.= {|[ 0,0 ]|, |[ 1,1 ]|} by A7,A65,Th13,Th17,Th18,ENUMSET1:1;
thus thesis by A18,A10,FINSEQ_4:18;
end;
theorem Th25:
h is being_S-Seq implies L~h is_an_arc_of h/.1,h/.len h
proof
set P = L~h;
set p1 = h/.1;
deffunc Q(Nat) = L~(h|($1+2));
defpred ARC[Nat] means 1 <= $1 + 2 & $1 + 2 <= len h implies ex NE be non
empty Subset of TOP-REAL 2 st NE = Q($1) & ex f being Function of I[01], (
TOP-REAL 2)|NE st f is being_homeomorphism & f.0 = p1 & f.1 = h/.($1+2);
set p2 = h/.(1+1);
assume
A1: h is being_S-Seq;
then
A2: len h >= 1+1;
then 1 <= len h by XXREAL_0:2;
then
A3: 1 in Seg len h by FINSEQ_1:1;
A4: h is one-to-one by A1;
A5: for n st ARC[n] holds ARC[n+1]
proof
let n;
assume
A6: ARC[n];
set pn = h/.(n+2), pn1 = h/.(n+2+1);
A7: n + 1 +1 <> n + 2 + 1;
reconsider NE1 = Q(n) \/ LSeg(pn,pn1) as non empty Subset of TOP-REAL 2;
assume that
A8: 1 <= n + 1 + 2 and
A9: n + 1 + 2 <= len h;
A10: n + 2 + 1 in dom h by A8,A9,FINSEQ_3:25;
A11: n + 1 + 1 <= n + 2 + 1 by NAT_1:11;
then consider NE being non empty Subset of TOP-REAL 2 such that
A12: NE = Q(n) and
A13: ex f being Function of I[01], (TOP-REAL 2)|NE st f is
being_homeomorphism & f.0 = p1 & f.1 = h/.(n+2) by A6,A9,NAT_1:11
,XXREAL_0:2;
A14: n + 1 + 1 = n + (1 + 1);
now
let x be object such that
A15: x in Q(n) \/ LSeg(h,n+2);
now
per cases by A15,XBOOLE_0:def 3;
suppose
A16: x in Q(n);
A17: n+1 <= n+(1+1) by XREAL_1:6;
consider X being set such that
A18: x in X and
A19: X in {LSeg(h|(n+2),i) where i is Nat: 1 <= i &
i+1 <= len(h|(n+2))} by A16,TARSKI:def 4;
consider i being Nat such that
A20: X = LSeg(h|(n+2),i) and
A21: 1 <= i and
A22: i+1 <= len(h|(n+2)) by A19;
i+1 <= n + 1 + 1 by A9,A11,A22,FINSEQ_1:59,XXREAL_0:2;
then i <= n + 1 by XREAL_1:6;
then
A23: i <= n+2 by A17,XXREAL_0:2;
len(h|(n+2)) = n + 2 by A9,A11,FINSEQ_1:59,XXREAL_0:2;
then i in Seg len(h|(n+2)) by A21,A23,FINSEQ_1:1;
then
A24: i in dom(h|(n+2)) by FINSEQ_1:def 3;
set p19 = (h|(n+2))/.i, p29 = (h|(n+2))/.(i+1);
A25: n+2 <= n+2+1 by NAT_1:11;
then i <= n+1+2 by A23,XXREAL_0:2;
then i in Seg(n+1+2) by A21,FINSEQ_1:1;
then i in Seg len(h|(n+1+2)) by A9,FINSEQ_1:59;
then i in dom(h|(n+1+2)) by FINSEQ_1:def 3;
then
A26: (h|(n+1+2))/.i = h/.i by FINSEQ_4:70
.= p19 by A24,FINSEQ_4:70;
i+1 <= n+2 by A9,A11,A22,FINSEQ_1:59,XXREAL_0:2;
then
A27: i+1 <= n+1+2 by A25,XXREAL_0:2;
A28: len(h|(n+1+2)) = n+1+2 by A9,FINSEQ_1:59;
A29: len(h|(n+1+2)) = n+(1+2) by A9,FINSEQ_1:59;
A30: n+2 <= n + 3 by XREAL_1:6;
1 <= i+1 by NAT_1:11;
then i+1 in Seg len(h|(n+2)) by A22,FINSEQ_1:1;
then
A31: i+1 in dom(h|(n+2)) by FINSEQ_1:def 3;
1 <= 1+i by NAT_1:11;
then i+1 in Seg(n+1+2) by A27,FINSEQ_1:1;
then i+1 in Seg len(h|(n+1+2) ) by A9,FINSEQ_1:59;
then i+1 in dom(h|(n+1+2)) by FINSEQ_1:def 3;
then
A32: (h|(n+1+2))/.(i+1) = h/.(i+1) by FINSEQ_4:70
.= p29 by A31,FINSEQ_4:70;
i+1 <= n + (1 + 1) by A9,A11,A22,FINSEQ_1:59,XXREAL_0:2;
then
A33: i+1 <= len(h|(n+1+2)) by A29,A30,XXREAL_0:2;
X = LSeg(p19,p29) by A20,A21,A22,Def3
.= LSeg(h|(n+1+2),i) by A21,A27,A28,A26,A32,Def3;
then X in {LSeg(h|(n+1+2),j) where j is Nat: 1 <= j & j+
1 <= len(h|(n+1+2))} by A21,A33;
hence x in Q(n+1) by A18,TARSKI:def 4;
end;
suppose
A34: x in LSeg(h,n+2);
A35: 1 <= n+2 by A14,NAT_1:11;
A36: len(h|(n+1+2)) = n+1+2 by A9,FINSEQ_1:59;
then n + 2 + 1 in Seg len(h|(n+1+2)) by A8,FINSEQ_1:1;
then
A37: n + 2 + 1 in dom(h|(n+1+ 2)) by FINSEQ_1:def 3;
then
A38: n+2+1 <= len(h|(n+1+2)) by FINSEQ_3:25;
n+2 <= n+2+1 by NAT_1:11;
then n + 2 in Seg len(h|(n+1+2)) by A36,A35,FINSEQ_1:1;
then
A39: n + 2 in dom(h|(n+1+2)) by FINSEQ_1:def 3;
then
A40: 1 <= n+2 by FINSEQ_3:25;
A41: pn1 = (h|(n+1+2))/.(n+2+1) by A37,FINSEQ_4:70;
A42: pn = (h|(n+1+2))/.(n+2) by A39,FINSEQ_4:70;
LSeg(h,n+2) = LSeg(pn,pn1) by A9,A35,Def3
.= LSeg(h|(n+1+2),n+2) by A36,A35,A42,A41,Def3;
then LSeg(h,n+2) in {LSeg(h|(n+1+2),i) where i is Nat: 1
<= i & i+1 <= len(h|(n+1+2))} by A40,A38;
hence x in Q(n+1) by A34,TARSKI:def 4;
end;
end;
hence x in Q(n+1);
end;
then
A43: Q(n) \/ LSeg(h,n+2) c= Q(n+1);
take NE1;
A44: 1 <= n + 1 + 1 by NAT_1:11;
now
let x be object;
A45: n+(1+1) = n+1+1;
A46: len(h|(n+1+2))-1 = n+1+2-1 by A9,FINSEQ_1:59
.= n+(1+1);
assume x in Q(n+1);
then consider X being set such that
A47: x in X and
A48: X in {LSeg(h|(n+1+2),i) where i is Nat: 1 <= i & i+1
<= len(h|(n+1+2))} by TARSKI:def 4;
consider i being Nat such that
A49: X = LSeg(h|(n+1+2),i) and
A50: 1 <= i and
A51: i+1 <= len(h|(n+1+2)) by A48;
i + 1 - 1 = i;
then
A52: i <= len(h|(n+1+2)) - 1 by A51,XREAL_1:9;
now
per cases by A52,A46,A45,NAT_1:8;
suppose
A53: i = n+2;
A54: len(h|(n+1+2)) = n+1+2 by A9,FINSEQ_1:59;
1<=n+2+1 by NAT_1:11;
then n + 2 + 1 in Seg len(h|(n+1+2)) by A54,FINSEQ_1:1;
then n + 2 + 1 in dom(h|(n+1+ 2)) by FINSEQ_1:def 3;
then
A55: (h|(n+1+2))/.(n+2+1) = h/.(n+(2+1)) by FINSEQ_4:70;
A56: 1 <= n+2 by A14,NAT_1:11;
n+1+2 = n+2+1;
then n+2<=n+1+2 by NAT_1:11;
then n + 2 in Seg len(h|(n+1+2)) by A54,A56,FINSEQ_1:1;
then n + 2 in dom(h|(n+1+2)) by FINSEQ_1:def 3;
then (h|(n+1+2))/.(n+2) = h/.(n+2) by FINSEQ_4:70;
then LSeg(h|(n+1+2),n+2) = LSeg(pn,pn1) by A54,A56,A55,Def3
.= LSeg(h,n+2) by A9,A44,Def3;
hence x in Q(n) \/ LSeg(h,n+2) by A47,A49,A53,XBOOLE_0:def 3;
end;
suppose
A57: i <= n+1;
then i+1 <= n+1+1 by XREAL_1:6;
then i+1 <= len(h|(n+2)) by A9,A11,FINSEQ_1:59,XXREAL_0:2;
then
A58: LSeg(h|(n+2),i) in {LSeg(h|(n+2),j) where j is Nat:
1 <= j & j+1 <= len(h|(n+2))} by A50;
set p19 = (h|(n+2))/.i, p29 = (h|(n+2))/.(i+1);
A59: 1 <= 1+i by NAT_1:11;
A60: len(h|(n+2)) = n + (1 + 1) by A9,A11,FINSEQ_1:59,XXREAL_0:2;
n+1 <= n+1+1 by NAT_1:11;
then
A61: i <= n+2 by A57,XXREAL_0:2;
then i in Seg len (h|(n+2)) by A50,A60,FINSEQ_1:1;
then
A62: i in dom(h|(n+2)) by FINSEQ_1:def 3;
A63: i+1 <= n+1+1 by A57,XREAL_1:7;
then i+1 in Seg len(h|(n+2)) by A60,A59,FINSEQ_1:1;
then
A64: i+1 in dom(h|(n+2)) by FINSEQ_1:def 3;
n+2 <= n+2+1 by NAT_1:11;
then i <= n+1+2 by A61,XXREAL_0:2;
then i in Seg(n+1+2) by A50,FINSEQ_1:1;
then i in Seg len(h|(n+1+2)) by A9,FINSEQ_1:59;
then i in dom(h|(n+1+2)) by FINSEQ_1:def 3;
then
A65: (h|(n+1+2))/.i = h/.i by FINSEQ_4:70
.= p19 by A62,FINSEQ_4:70;
i+1 <= n+1+2 by A57,XREAL_1:7;
then i+1 in Seg(n+1+2) by A59,FINSEQ_1:1;
then i+1 in Seg len(h|(n+1+2)) by A9,FINSEQ_1:59;
then i+1 in dom(h|(n+1+2)) by FINSEQ_1:def 3;
then
A66: (h|(n+1+2))/.(i+1) = h/.(i+1) by FINSEQ_4:70
.= p29 by A64,FINSEQ_4:70;
LSeg(h|(n+2),i) = LSeg(p19,p29) by A50,A60,A63,Def3
.= LSeg(h|(n+1+2),i) by A50,A51,A65,A66,Def3;
then x in union {LSeg(h|(n+2),j) where j is Nat: 1 <= j
& j+1 <= len(h|(n+2))} by A47,A49,A58,TARSKI:def 4;
hence x in Q(n) \/ LSeg(h,n+2) by XBOOLE_0:def 3;
end;
end;
hence x in Q(n) \/ LSeg(h,n+2);
end;
then Q(n+1) c= Q(n) \/ LSeg(h,n+2);
then Q(n+1) = Q(n) \/ LSeg(h,n+2) by A43;
hence NE1 = Q(n+1) by A9,A44,Def3;
A67: n + 1 + 1 <= len h by A9,A11,XXREAL_0:2;
then n + 1 +1 in dom h by A44,FINSEQ_3:25;
then LSeg(pn,pn1) is_an_arc_of pn,pn1 by A4,A7,A10,Th9,PARTFUN2:10;
then consider
f1 being Function of I[01], (TOP-REAL 2)|LSeg(pn,pn1) such that
A68: f1 is being_homeomorphism and
A69: f1.0 = pn and
A70: f1.1 = pn1;
consider f being Function of I[01], (TOP-REAL 2)|NE such that
f is being_homeomorphism and
A71: f.0 = p1 and
f.1 = h/.(n+2) by A13;
for x being object holds x in Q(n) /\ LSeg(pn,pn1) iff x = pn
proof
let x be object;
A72: 1 <= n+1 by NAT_1:11;
thus x in Q(n) /\ LSeg(pn,pn1) implies x = pn
proof
A73: 1 <= n+1 by NAT_1:11;
h is unfolded by A1;
then
A74: LSeg(h,n+1) /\ LSeg(h,n+1+1) = {h/.(n+1+1)} by A9,A73;
A75: n+1+1 <= len h by A9,A11,XXREAL_0:2;
assume
A76: x in Q(n) /\ LSeg(pn,pn1);
then
A77: x in LSeg(pn,pn1) by XBOOLE_0:def 4;
A78: LSeg(pn,pn1) = LSeg(h,n+1+1) by A9,A44,Def3;
set p19 = h/.(n+1), p29 = h/.(n+1+1);
A79: 1 <= 1+n by NAT_1:11;
x in Q(n) by A76,XBOOLE_0:def 4;
then consider X being set such that
A80: x in X and
A81: X in {LSeg(h|(n+2),i) where i is Nat: 1 <= i & i+
1 <= len(h|(n+2))} by TARSKI:def 4;
consider i being Nat such that
A82: X = LSeg(h|(n+2),i) and
A83: 1 <= i and
A84: i+1 <= len(h|(n+2)) by A81;
A85: len(h|(n+2)) = n+(1+1) by A9,A11,FINSEQ_1:59,XXREAL_0:2;
n+1 <= n+1+1 by NAT_1:11;
then n+1 in Seg len(h|(n+2)) by A85,A79,FINSEQ_1:1;
then n+1 in dom(h|(n+2)) by FINSEQ_1:def 3;
then
A86: (h|(n+2))/.(n+1) = p19 by FINSEQ_4:70;
1 <= 1+(n+1) by NAT_1:11;
then n+1+1 in Seg len(h|(n+2)) by A85,FINSEQ_1:1;
then n+1+1 in dom(h|(n+2)) by FINSEQ_1:def 3;
then
A87: (h|(n+2))/.(n+1+1) = p29 by FINSEQ_4:70;
A88: len(h|(n+2)) = n+1+1 by A9,A11,FINSEQ_1:59,XXREAL_0:2;
then
A89: i <= n+1 by A84,XREAL_1:6;
then 1 <= n+1 by A83,XXREAL_0:2;
then
A90: LSeg(h,n+1) = LSeg(p19,p29) by A75,Def3
.= LSeg(h|(n+2),n+1) by A85,A79,A86,A87,Def3;
A91: h is s.n.c. by A1;
now
set p19 = h/.i, p29 = h/.(i+1);
assume
A92: i < n+1;
then
A93: i+1 < n+1+1 by XREAL_1:6;
n+1 <= n+1+1 by NAT_1:11;
then i <= n+2 by A92,XXREAL_0:2;
then i in Seg len(h|(n+2)) by A83,A85,FINSEQ_1:1;
then i in dom(h|(n+2)) by FINSEQ_1:def 3;
then
A94: (h|(n+2))/.i = p19 by FINSEQ_4:70;
A95: LSeg(h,n+2) = LSeg(pn,pn1) by A9,A44,Def3;
1 <= 1+i by NAT_1:11;
then i+1 in Seg len(h|(n+2)) by A84,FINSEQ_1:1;
then i+1 in dom(h|(n+2)) by FINSEQ_1:def 3;
then
A96: (h|(n+2))/.(i+1) = p29 by FINSEQ_4:70;
i+1 <= len h by A67,A84,A88,XXREAL_0:2;
then LSeg(h,i) = LSeg(p19,p29) by A83,Def3
.= LSeg(h|(n+2),i) by A83,A84,A94,A96,Def3;
then LSeg(h|(n+2),i) misses LSeg(pn,pn1) by A91,A93,A95;
hence contradiction by A77,A80,A82,XBOOLE_0:3;
end;
then i = n + 1 by A89,XXREAL_0:1;
then x in LSeg(h,n+1) /\ LSeg(h,n+1+1) by A77,A80,A82,A90,A78,
XBOOLE_0:def 4;
hence thesis by A74,TARSKI:def 1;
end;
assume
A97: x = pn;
A98: 1 <= n+1 by NAT_1:11;
n+1+1 <= len(h|(n+2)) by A9,A11,FINSEQ_1:59,XXREAL_0:2;
then
A99: LSeg(h|(n+2),n+1) in {LSeg(h|(n+2),i) where i is Nat: 1
<= i & i+1 <= len(h|(n+2))} by A98;
A100: n + 2 in Seg(n+2) by A44,FINSEQ_1:1;
A101: len(h|(n+2)) = n+2 by A9,A11,FINSEQ_1:59,XXREAL_0:2;
then dom(h|(n+2)) = Seg(n+2) by FINSEQ_1:def 3;
then x = (h|(n+2))/.(n+1+1) by A97,A100,FINSEQ_4:70;
then x in LSeg(h|(n+2),n+1) by A101,A72,Th21;
then
A102: x in union {LSeg(h|(n+2),i) where i is Nat: 1 <= i & i+
1 <= len(h|(n+2))} by A99,TARSKI:def 4;
x in LSeg(pn,pn1) by A97,RLTOPSP1:68;
hence thesis by A102,XBOOLE_0:def 4;
end;
then Q(n) /\ LSeg(pn,pn1) = {pn} by TARSKI:def 1;
then consider hh being Function of I[01], (TOP-REAL 2)|NE1 such that
A103: hh is being_homeomorphism and
A104: hh.0 = f.0 and
A105: hh.1 = f1.1 by A12,A13,A71,A68,A69,TOPMETR2:3;
take hh;
thus hh is being_homeomorphism & hh.0 = p1 & hh.1 = h/.(n+1+2) by A71,A70
,A103,A104,A105;
end;
h|2 = h|(Seg 2) by FINSEQ_1:def 16;
then
A106: dom (h|2) = dom h /\ Seg 2 by RELAT_1:61
.= Seg len h /\ Seg 2 by FINSEQ_1:def 3
.= Seg 2 by A2,FINSEQ_1:7;
then
A107: len(h|2) = 1+1 by FINSEQ_1:def 3;
then
A108: 2 in Seg len (h|2) by FINSEQ_1:1;
A109: 1 in Seg len (h|2) by A107,FINSEQ_1:1;
now
let x be object;
A110: p2 = (h|2)/.2 by A106,A107,A108,FINSEQ_4:70;
thus x in {LSeg(h|2,i) where i is Nat: 1 <= i & i+1 <= len(h|2)
} implies x = LSeg(h,1)
proof
assume
x in {LSeg(h|2,i) where i is Nat: 1 <= i & i+1 <= len(h|2) };
then consider i being Nat such that
A111: x = LSeg(h|2,i) and
A112: 1 <= i and
A113: i+1 <= len(h|2);
i+1 <= (1 + 1) by A106,A113,FINSEQ_1:def 3;
then i <= 1 by XREAL_1:6;
then
A114: 1 = i by A112,XXREAL_0:1;
A115: (h|2)/.(1+1) = h/.(1+1) by A106,A107,A108,FINSEQ_4:70;
(h|2)/.1 = h/.1 by A106,A107,A109,FINSEQ_4:70;
hence x = LSeg(p1,p2) by A107,A111,A114,A115,Def3
.= LSeg(h,1) by A2,Def3;
end;
assume x = LSeg(h,1);
then
A116: x = LSeg(p1,p2) by A2,Def3;
p1 = (h|2)/.1 by A106,A107,A109,FINSEQ_4:70;
then x = LSeg(h|2,1) by A107,A116,A110,Def3;
hence
x in {LSeg(h|2,i) where i is Nat: 1 <= i & i+1 <= len(h|2)
} by A107;
end;
then {LSeg(h|2,i) where i is Nat: 1 <= i & i+1 <= len(h|2) } = {
LSeg (h,1)} by TARSKI:def 1;
then
A117: Q(0) = LSeg(h,1) by ZFMISC_1:25
.= LSeg(p1,p2) by A2,Def3;
A118: 1+1 in Seg len h by A2,FINSEQ_1:1;
1 <= 0 + 2 & 0 + 2 <= len h implies ex f being Function of I[01], (
TOP-REAL 2)|(LSeg(p1,p2)) st f is being_homeomorphism & f.0 = p1 & f.1 = h/.(0+
2)
proof
assume that
1 <= 0 + 2 and
0 + 2 <= len h;
A119: 2 in dom h by A118,FINSEQ_1:def 3;
1 in dom h by A3,FINSEQ_1:def 3;
then LSeg(p1,p2) is_an_arc_of p1,p2 by A4,A119,Th9,PARTFUN2:10;
hence thesis;
end;
then
A120: ARC[0] by A117;
A121: for n holds ARC[n] from NAT_1:sch 2(A120,A5);
len h - 2 in NAT by A2,INT_1:5;
then reconsider h1 = len h - 2 as Nat;
1 <= h1 + 2 by NAT_1:12;
then consider NE being non empty Subset of TOP-REAL 2 such that
A122: NE = Q(h1) and
A123: ex f being Function of I[01], (TOP-REAL 2)|NE st f is
being_homeomorphism & f.0 = p1 & f.1 = h/.(h1+2) by A121;
consider f being Function of I[01], (TOP-REAL 2)|NE such that
A124: f is being_homeomorphism and
A125: f.0 = p1 and
A126: f.1 = h/.(h1+2) by A123;
A127: h|(len h) = h|(Seg len h) by FINSEQ_1:def 16
.= h|(dom h) by FINSEQ_1:def 3
.= h by RELAT_1:68;
then reconsider f as Function of I[01], (TOP-REAL 2)|P by A122;
take f;
thus f is being_homeomorphism by A122,A124,A127;
thus thesis by A125,A126;
end;
definition
let P be Subset of TOP-REAL 2;
attr P is being_S-P_arc means
ex f st f is being_S-Seq & P = L~f;
end;
theorem Th26:
P1 is being_S-P_arc implies P1 <> {}
proof
assume P1 is being_S-P_arc;
then consider f such that
A1: f is being_S-Seq and
A2: P1 = L~f;
len f >= 2 by A1;
hence thesis by A2,Th23;
end;
registration
cluster being_S-P_arc -> non empty for Subset of TOP-REAL 2;
coherence by Th26;
end;
theorem
ex P1, P2 being non empty Subset of TOP-REAL 2 st P1 is being_S-P_arc
& P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[ 0,0 ]|, |[
1,1 ]|}
proof
consider f1,f2 such that
A1: f1 is being_S-Seq and
A2: f2 is being_S-Seq and
A3: R^2-unit_square = L~f1 \/ L~f2 and
A4: L~f1 /\ L~f2 = {|[ 0,0 ]|, |[ 1,1 ]|} and
f1/.1=|[0,0]| and
f1/.len f1=|[1,1]| and
f2/.1=|[0,0]| and
f2/.len f2=|[1,1]| by Th24;
reconsider P1 = L~f1, P2 = L~f2 as non empty Subset of TOP-REAL 2 by A4;
take P1, P2;
thus thesis by A1,A2,A3,A4;
end;
theorem Th28:
P is being_S-P_arc implies ex p1,p2 st P is_an_arc_of p1,p2
proof
assume P is being_S-P_arc;
then consider h such that
A1: h is being_S-Seq and
A2: P = L~h;
take h/.1, h/.len h;
thus thesis by A1,A2,Th25;
end;
theorem
P is being_S-P_arc implies ex f being Function of I[01], (TOP-REAL 2)|
P st f is being_homeomorphism
proof
assume P is being_S-P_arc;
then consider p1,p2 such that
A1: P is_an_arc_of p1,p2 by Th28;
ex f being Function of I[01], (TOP-REAL 2)|P st f is being_homeomorphism
& f.0 = p1 & f.1 = p2 by A1;
hence thesis;
end;
:: Moved from JORDAN1A, AK, 23.02.2006
scheme
TRSubsetEx { n() -> Nat, P[object] } :
ex A being Subset of TOP-REAL n() st for
p being Point of TOP-REAL n() holds p in A iff P[p] proof
consider A being set such that
A1: for x being object holds x in A iff x in the carrier of TOP-REAL n() &
P[x] from XBOOLE_0:sch 1;
A c= the carrier of TOP-REAL n()
by A1;
then reconsider A as Subset of TOP-REAL n();
take A;
thus thesis by A1;
end;
scheme
TRSubsetUniq { n() -> Nat, P[object] } :
for A, B being Subset of TOP-REAL n()
st (for p being Point of TOP-REAL n() holds p in A iff P[p]) & (for p being
Point of TOP-REAL n() holds p in B iff P[p]) holds A = B proof
let A, B be Subset of TOP-REAL n() such that
A1: for p being Point of TOP-REAL n() holds p in A iff P[p] and
A2: for p being Point of TOP-REAL n() holds p in B iff P[p];
thus for x being object st x in A holds x in B by A2,A1;
let x be object;
assume
A3: x in B;
then P[x] by A2;
hence thesis by A1,A3;
end;
definition
let p be Point of TOP-REAL 2;
func north_halfline p -> Subset of TOP-REAL 2 means
:Def10:
for x being Point of TOP-REAL 2 holds x in it iff x`1 = p`1 & x`2 >= p`2;
existence
proof
defpred P[Point of TOP-REAL 2] means $1`1 = p`1 & $1`2 >= p`2;
thus ex IT being Subset of TOP-REAL 2 st for x being Point of TOP-REAL 2
holds x in IT iff P[x] from TRSubsetEx;
end;
uniqueness
proof
defpred P[Point of TOP-REAL 2] means $1`1 = p`1 & $1`2 >= p`2;
thus for a,b being Subset of TOP-REAL 2 st (for x being Point of TOP-REAL
2 holds x in a iff P[x]) & (for x being Point of TOP-REAL 2 holds x in b iff P[
x]) holds a=b from TRSubsetUniq;
end;
func east_halfline p -> Subset of TOP-REAL 2 means
:Def11:
for x being Point of TOP-REAL 2 holds x in it iff x`1 >= p`1 & x`2 = p`2;
existence
proof
defpred P[Point of TOP-REAL 2] means $1`1 >= p`1 & $1`2 = p`2;
thus ex IT being Subset of TOP-REAL 2 st for x being Point of TOP-REAL 2
holds x in IT iff P[x] from TRSubsetEx;
end;
uniqueness
proof
defpred P[Point of TOP-REAL 2] means $1`1 >= p`1 & $1`2 = p`2;
thus for a,b being Subset of TOP-REAL 2 st (for x being Point of TOP-REAL
2 holds x in a iff P[x]) & (for x being Point of TOP-REAL 2 holds x in b iff P[
x]) holds a=b from TRSubsetUniq;
end;
func south_halfline p -> Subset of TOP-REAL 2 means
:Def12:
for x being Point of TOP-REAL 2 holds x in it iff x`1 = p`1 & x`2 <= p`2;
existence
proof
defpred P[Point of TOP-REAL 2] means $1`1 = p`1 & $1`2 <= p`2;
thus ex IT being Subset of TOP-REAL 2 st for x being Point of TOP-REAL 2
holds x in IT iff P[x] from TRSubsetEx;
end;
uniqueness
proof
defpred P[Point of TOP-REAL 2] means $1`1 = p`1 & $1`2 <= p`2;
thus for a,b being Subset of TOP-REAL 2 st (for x being Point of TOP-REAL
2 holds x in a iff P[x]) & (for x being Point of TOP-REAL 2 holds x in b iff P[
x]) holds a=b from TRSubsetUniq;
end;
func west_halfline p -> Subset of TOP-REAL 2 means
:Def13:
for x being Point of TOP-REAL 2 holds x in it iff x`1 <= p`1 & x`2 = p`2;
existence
proof
defpred P[Point of TOP-REAL 2] means $1`1 <= p`1 & $1`2 = p`2;
thus ex IT being Subset of TOP-REAL 2 st for x being Point of TOP-REAL 2
holds x in IT iff P[x] from TRSubsetEx;
end;
uniqueness
proof
defpred P[Point of TOP-REAL 2] means $1`1 <= p`1 & $1`2 = p`2;
thus for a,b being Subset of TOP-REAL 2 st (for x being Point of TOP-REAL
2 holds x in a iff P[x]) & (for x being Point of TOP-REAL 2 holds x in b iff P[
x]) holds a=b from TRSubsetUniq;
end;
end;
theorem
north_halfline p = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 >= p`2}
proof
set A = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 >= p`2};
hereby
let x be object;
assume
A1: x in north_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 >= p`2 by A1,Def10;
q`1 = p`1 by A1,Def10;
hence x in A by A2;
end;
let x be object;
assume x in A;
then ex q being Point of TOP-REAL 2 st x = q & q`1 = p`1 & q`2 >= p`2;
hence thesis by Def10;
end;
theorem Th31:
north_halfline p = { |[ p`1,r ]| where r is Real: r >= p`2 }
proof
set A = {|[ p`1,r ]| where r is Real: r >= p`2};
hereby
let x be object;
assume
A1: x in north_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 >= p`2 by A1,Def10;
A3: q = |[q`1, q`2]| by EUCLID:53;
q`1 = p`1 by A1,Def10;
hence x in A by A2,A3;
end;
let x be object;
assume x in A;
then consider r being Real such that
A4: x = |[p`1,r]| and
A5: r >= p`2;
reconsider q = x as Point of TOP-REAL 2 by A4;
A6: q`2 = r by A4,EUCLID:52;
q`1 = p`1 by A4,EUCLID:52;
hence thesis by A5,A6,Def10;
end;
theorem
east_halfline p = {q where q is Point of TOP-REAL 2: q`1 >= p`1 & q`2 = p`2}
proof
set A = {q where q is Point of TOP-REAL 2: q`1 >= p`1 & q`2 = p`2};
hereby
let x be object;
assume
A1: x in east_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 = p`2 by A1,Def11;
q`1 >= p`1 by A1,Def11;
hence x in A by A2;
end;
let x be object;
assume x in A;
then ex q being Point of TOP-REAL 2 st x = q & q`1 >= p`1 & q`2 = p`2;
hence thesis by Def11;
end;
theorem Th33:
east_halfline p = { |[ r,p`2 ]| where r is Real: r >= p`1 }
proof
set A = {|[ r,p`2 ]| where r is Real: r >= p`1};
hereby
let x be object;
assume
A1: x in east_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 = p`2 by A1,Def11;
A3: q = |[q`1, q`2]| by EUCLID:53;
q`1 >= p`1 by A1,Def11;
hence x in A by A2,A3;
end;
let x be object;
assume x in A;
then consider r being Real such that
A4: x = |[r,p`2]| and
A5: r >= p`1;
reconsider q = x as Point of TOP-REAL 2 by A4;
A6: q`2 = p`2 by A4,EUCLID:52;
q`1 = r by A4,EUCLID:52;
hence thesis by A5,A6,Def11;
end;
theorem
south_halfline p = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 <= p`2}
proof
set A = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 <= p`2};
hereby
let x be object;
assume
A1: x in south_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 <= p`2 by A1,Def12;
q`1 = p`1 by A1,Def12;
hence x in A by A2;
end;
let x be object;
assume x in A;
then ex q being Point of TOP-REAL 2 st x = q & q`1 = p`1 & q`2 <= p`2;
hence thesis by Def12;
end;
theorem Th35:
south_halfline p = { |[ p`1,r ]| where r is Real: r <= p`2 }
proof
set A = {|[ p`1,r ]| where r is Real: r <= p`2};
hereby
let x be object;
assume
A1: x in south_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 <= p`2 by A1,Def12;
A3: q = |[q`1, q`2]| by EUCLID:53;
q`1 = p`1 by A1,Def12;
hence x in A by A2,A3;
end;
let x be object;
assume x in A;
then consider r being Real such that
A4: x = |[p`1,r]| and
A5: r <= p`2;
reconsider q = x as Point of TOP-REAL 2 by A4;
A6: q`2 = r by A4,EUCLID:52;
q`1 = p`1 by A4,EUCLID:52;
hence thesis by A5,A6,Def12;
end;
theorem
west_halfline p = {q where q is Point of TOP-REAL 2: q`1 <= p`1 & q`2 = p`2}
proof
set A = {q where q is Point of TOP-REAL 2: q`1 <= p`1 & q`2 = p`2};
hereby
let x be object;
assume
A1: x in west_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 = p`2 by A1,Def13;
q`1 <= p`1 by A1,Def13;
hence x in A by A2;
end;
let x be object;
assume x in A;
then ex q being Point of TOP-REAL 2 st x = q & q`1 <= p`1 & q`2 = p`2;
hence thesis by Def13;
end;
theorem Th37:
west_halfline p = { |[ r,p`2 ]| where r is Real: r <= p`1 }
proof
set A = {|[ r,p`2 ]| where r is Real: r <= p`1};
hereby
let x be object;
assume
A1: x in west_halfline p;
then reconsider q = x as Point of TOP-REAL 2;
A2: q`2 = p`2 by A1,Def13;
A3: q = |[q`1, q`2]| by EUCLID:53;
q`1 <= p`1 by A1,Def13;
hence x in A by A2,A3;
end;
let x be object;
assume x in A;
then consider r being Real such that
A4: x = |[r,p`2]| and
A5: r <= p`1;
reconsider q = x as Point of TOP-REAL 2 by A4;
A6: q`2 = p`2 by A4,EUCLID:52;
q`1 = r by A4,EUCLID:52;
hence thesis by A5,A6,Def13;
end;
registration
let p be Point of TOP-REAL 2;
cluster north_halfline p -> non empty;
coherence
proof
north_halfline p = { |[ p`1,r ]| where r is Real: r >= p`2
} by Th31;
then |[p`1,p`2]| in north_halfline p;
hence thesis;
end;
cluster east_halfline p -> non empty;
coherence
proof
east_halfline p = { |[ r,p`2 ]| where r is Real: r >= p`1 }
by Th33;
then |[p`1,p`2]| in east_halfline p;
hence thesis;
end;
cluster south_halfline p -> non empty;
coherence
proof
south_halfline p = { |[ p`1,r ]| where r is Real: r <= p`2
} by Th35;
then |[p`1,p`2]| in south_halfline p;
hence thesis;
end;
cluster west_halfline p -> non empty;
coherence
proof
west_halfline p = { |[ r,p`2 ]| where r is Real: r <= p`1
} by Th37;
then |[p`1,p`2]| in west_halfline p;
hence thesis;
end;
end;
:: Moved from JORDAN1C, AK, 23.02.2006
theorem
p in west_halfline p & p in east_halfline p & p in north_halfline p &
p in south_halfline p
proof
A1: p`2 = p`2;
p`1 <= p`1;
hence thesis by A1,Def10,Def11,Def12,Def13;
end;