:: On the Decompositions of Intervals and Simple Closed Curves
:: by Adam Grabowski
::
:: Received August 7, 2002
:: Copyright (c) 2002-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, ZFMISC_1, TOPREAL2, PRE_TOPC, EUCLID, XBOOLE_0,
SUBSET_1, TARSKI, STRUCT_0, FUNCT_1, RELAT_1, FUNCT_4, PARTFUN1,
TOPREAL1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, BORSUK_1, XXREAL_1,
TOPMETR, CONNSP_1, REAL_1, RELAT_2, RCOMP_1, XXREAL_2, ORDINAL2, SEQ_4,
T_0TOPSP, TOPS_2, RLTOPSP1, TREAL_1, VALUED_1, BORSUK_4, FUNCT_2,
MEASURE5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_2, XREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
DOMAIN_1, RCOMP_1, FUNCT_4, XXREAL_0, STRUCT_0, MEASURE6, PRE_TOPC,
COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, SEQ_4, TREAL_1, CONNSP_1,
BORSUK_1, BORSUK_3, TSEP_1, TOPMETR, MEASURE5, TOPS_2;
constructors FUNCT_4, CONNSP_1, TOPS_2, COMPTS_1, TSEP_1, TOPREAL1, TOPREAL2,
TREAL_1, MEASURE6, BORSUK_3, INTEGRA1, SEQ_4, BINOP_2;
registrations XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED,
RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, EUCLID,
TOPREAL1, TOPREAL2, BORSUK_2, REVROT_1, TOPREAL6, XXREAL_2, TOPMETR,
SUBSET_1, MEASURE5, JORDAN2C, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, CONNSP_1, PARTFUN1, STRUCT_0;
equalities SUBSET_1, STRUCT_0, RELAT_1;
expansions TARSKI, PARTFUN1, SUBSET_1;
theorems TOPS_2, T_0TOPSP, BORSUK_1, PRE_TOPC, COMPTS_1, TARSKI, TOPMETR,
TOPREAL1, RCOMP_1, CONNSP_1, ZFMISC_1, JORDAN5A, TOPREAL6, MEASURE6,
TREAL_1, XBOOLE_0, XBOOLE_1, JORDAN6, SEQ_4, INTEGRA1, INTEGRA2, TSEP_1,
TOPREAL2, JORDAN5B, FUNCT_2, FUNCT_1, GOBOARD9, RELAT_1, RFUNCT_2,
BORSUK_3, FUNCT_4, JGRAPH_2, TOPMETR2, XREAL_1, FRECHET, ENUMSET1,
XXREAL_0, XXREAL_1, XXREAL_2, SUBSET_1, MEASURE5, RLTOPSP1;
begin :: Preliminaries
registration
cluster -> non trivial for Simple_closed_curve;
coherence
proof
let D be Simple_closed_curve;
ex p1,p2 being Point of TOP-REAL 2 st p1 <> p2 & p1 in D & p2 in D by
TOPREAL2:5;
hence thesis;
end;
end;
::$CT 3
theorem Th1:
for f, g being Function, a being set st f is one-to-one & g is
one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } holds f +* g is
one-to-one
proof
let f, g be Function, a be set;
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: dom f /\ dom g = { a } and
A4: rng f /\ rng g = { f.a };
for x1,x2 being set st x1 in dom g & x2 in dom f \ dom g holds g.x1 <> f .x2
proof
{ a } c= dom g by A3,XBOOLE_1:17;
then
A5: a in dom g by ZFMISC_1:31;
{ a } c= dom f by A3,XBOOLE_1:17;
then
A6: a in dom f by ZFMISC_1:31;
let x1,x2 be set;
assume that
A7: x1 in dom g and
A8: x2 in dom f \ dom g;
A9: f.x2 in rng f by A8,FUNCT_1:3;
assume
A10: g.x1 = f.x2;
g.x1 in rng g by A7,FUNCT_1:3;
then f.x2 in rng f /\ rng g by A9,A10,XBOOLE_0:def 4;
then f.x2 = f.a by A4,TARSKI:def 1;
then x2 = a by A1,A8,A6,FUNCT_1:def 4;
then dom g meets (dom f \ dom g) by A8,A5,XBOOLE_0:3;
hence thesis by XBOOLE_1:79;
end;
hence thesis by A1,A2,TOPMETR2:1;
end;
theorem Th2:
for f, g being Function, a being set st f is one-to-one & g is
one-to-one & dom f /\ dom g = { a } & rng f /\ rng g = { f.a } & f.a = g.a
holds (f +* g)" = f" +* g"
proof
let f, g be Function, a be set;
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: dom f /\ dom g = { a } and
A4: rng f /\ rng g = { f.a } and
A5: f.a = g.a;
A6: dom (g") = rng g by A2,FUNCT_1:33;
A7: dom (f") = rng f by A1,FUNCT_1:33;
for x being object st x in dom (f") /\ dom (g") holds f".x = g".x
proof
let x be object;
{ a } c= dom f by A3,XBOOLE_1:17;
then
A8: a in dom f by ZFMISC_1:31;
assume
A9: x in dom (f") /\ dom (g");
then x = f.a by A4,A7,A6,TARSKI:def 1;
then
A10: a = f".x by A1,A8,FUNCT_1:32;
{ a } c= dom g by A3,XBOOLE_1:17;
then
A11: a in dom g by ZFMISC_1:31;
x = g.a by A4,A5,A7,A6,A9,TARSKI:def 1;
hence thesis by A2,A11,A10,FUNCT_1:32;
end;
then
A12: f" tolerates g";
set gf = f" +* g", F = f +* g;
for x being object st x in dom f /\ dom g holds f.x = g.x
proof
let x be object;
assume x in dom f /\ dom g;
then x = a by A3,TARSKI:def 1;
hence thesis by A5;
end;
then
A13: f tolerates g;
dom gf = (dom (f")) \/ (dom (g")) by FUNCT_4:def 1
.= (rng f) \/ (dom (g")) by A1,FUNCT_1:33
.= (rng f) \/ (rng g) by A2,FUNCT_1:33;
then
A14: dom gf = rng F by A13,FRECHET:35;
A15: dom F = (dom f) \/ (dom g) by FUNCT_4:def 1;
then
A16: dom f c= dom F by XBOOLE_1:7;
A17: dom g c= dom F by A15,XBOOLE_1:7;
A18: rng F = (rng f) \/ (rng g) by A13,FRECHET:35;
A19: for y,x being object
holds y in rng F & x = gf.y iff x in dom F & y = F.x
proof
let y,x be object;
hereby
assume that
A20: y in rng F and
A21: x = gf.y;
per cases by A14,A20,FUNCT_4:12;
suppose
A22: y in dom (f");
then
A23: y in rng f by A1,FUNCT_1:33;
A24: x = f".y by A12,A21,A22,FUNCT_4:15;
then
A25: y = f.x by A1,A23,FUNCT_1:32;
x in dom f by A1,A23,A24,FUNCT_1:32;
hence x in dom F & y = F.x by A13,A16,A25,FUNCT_4:15;
end;
suppose
A26: y in dom (g");
then
A27: x = g".y by A21,FUNCT_4:13;
A28: y in rng g by A2,A26,FUNCT_1:33;
then
A29: y = g.x by A2,A27,FUNCT_1:32;
x in dom g by A2,A28,A27,FUNCT_1:32;
hence x in dom F & y = F.x by A17,A29,FUNCT_4:13;
end;
end;
assume that
A30: x in dom F and
A31: y = F.x;
per cases by A30,FUNCT_4:12;
suppose
A32: x in dom f;
then
A33: y = f.x by A13,A31,FUNCT_4:15;
then
A34: x = f".y by A1,A32,FUNCT_1:32;
rng F = (rng f) \/ (rng g) by A13,FRECHET:35;
then
A35: rng f c= rng F by XBOOLE_1:7;
A36: y in rng f by A32,A33,FUNCT_1:3;
then y in dom (f") by A1,FUNCT_1:33;
hence thesis by A12,A34,A36,A35,FUNCT_4:15;
end;
suppose
A37: x in dom g;
then
A38: y = g.x by A31,FUNCT_4:13;
then
A39: x = g".y by A2,A37,FUNCT_1:32;
A40: rng g c= rng F by A18,XBOOLE_1:7;
A41: y in rng g by A37,A38,FUNCT_1:3;
then y in dom (g") by A2,FUNCT_1:33;
hence thesis by A39,A41,A40,FUNCT_4:13;
end;
end;
F is one-to-one by A1,A2,A3,A4,Th1;
hence thesis by A14,A19,FUNCT_1:32;
end;
theorem Th3:
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n st A is_an_arc_of p, q holds A \ {p} is non empty
proof
let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
TOP-REAL n;
assume A is_an_arc_of p, q;
then
A1: A \ { p, q } <> {} by JORDAN6:43;
{ p } c= { p, q } by ZFMISC_1:7;
hence thesis by A1,XBOOLE_1:3,34;
end;
theorem
for s1, s3, s4, l being Real st s1 <= s3 & s1 < s4 & 0 <= l & l
<= 1 holds s1 <= (1-l) * s3+l*s4
proof
let s1, s3, s4, l be Real;
assume that
A1: s1 <= s3 and
A2: s1 < s4 and
A3: 0 <= l and
A4: l <= 1;
now
per cases;
suppose
l=0;
hence thesis by A1;
end;
suppose
l=1;
hence thesis by A2;
end;
suppose
A5: not(l=0 or l=1);
then l<1 by A4,XXREAL_0:1;
then 1-l>0 by XREAL_1:50;
then
A6: (1-l)*s1<=(1-l)*s3 by A1,XREAL_1:64;
A7: (1-l)*s1+l*s1=1 * s1;
l*s1<l*s4 by A2,A3,A5,XREAL_1:68;
hence thesis by A6,A7,XREAL_1:8;
end;
end;
hence thesis;
end;
theorem Th5:
for A being Subset of I[01], a, b being Real st a < b & A
= ].a,b.[ holds [.a,b.] c= the carrier of I[01]
proof
let A be Subset of I[01], a, b be Real;
assume
A1: a < b;
assume
A2: A = ].a,b.[;
then
A3: b <= 1 by A1,BORSUK_1:40,XXREAL_1:51;
0 <= a by A1,A2,BORSUK_1:40,XXREAL_1:51;
hence thesis by A3,BORSUK_1:40,XXREAL_1:34;
end;
theorem Th6:
for A being Subset of I[01], a, b being Real st a < b & A
= ].a,b.] holds [.a,b.] c= the carrier of I[01]
proof
let A be Subset of I[01], a, b be Real;
assume
A1: a < b;
A2: ].a,b.[ c= ]. a,b .] by XXREAL_1:21;
assume A = ].a,b.];
then
A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:40,XBOOLE_1:1;
then
A4: b <= 1 by A1,XXREAL_1:51;
0 <= a by A1,A3,XXREAL_1:51;
hence thesis by A4,BORSUK_1:40,XXREAL_1:34;
end;
theorem Th7:
for A being Subset of I[01], a, b being Real st a < b & A
= [.a,b.[ holds [.a,b.] c= the carrier of I[01]
proof
let A be Subset of I[01], a, b be Real;
assume
A1: a < b;
A2: ].a,b.[ c= [. a,b .[ by XXREAL_1:22;
assume A = [.a,b.[;
then
A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:40,XBOOLE_1:1;
then
A4: b <= 1 by A1,XXREAL_1:51;
0 <= a by A1,A3,XXREAL_1:51;
hence thesis by A4,BORSUK_1:40,XXREAL_1:34;
end;
theorem Th8:
for a, b being Real st a <> b holds Cl ].a,b.] = [.a,b.]
proof
let a, b be Real;
A1: Cl ].a,b.] c= [.a,b.] by MEASURE6:57,XXREAL_1:23;
A2: Cl ].a,b.[ c= Cl ].a,b.] by MEASURE6:62,XXREAL_1:21;
assume a <> b;
then [.a,b.] c= Cl ].a,b.] by A2,JORDAN5A:26;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th9:
for a, b being Real st a <> b holds Cl [.a,b.[ = [.a,b.]
proof
let a, b be Real;
A1: Cl [.a,b.[ c= [.a,b.] by MEASURE6:57,XXREAL_1:24;
A2: Cl ].a,b.[ c= Cl [.a,b.[ by MEASURE6:62,XXREAL_1:22;
assume a <> b;
then [.a,b.] c= Cl [.a,b.[ by A2,JORDAN5A:26;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
for A being Subset of I[01], a, b being Real st a < b & A = ].a
,b.[ holds Cl A = [.a,b.]
proof
let A be Subset of I[01], a, b be Real;
assume that
A1: a < b and
A2: A = ].a,b.[;
reconsider A1 = ].a,b.[ as Subset of R^1 by TOPMETR:17;
A3: Cl ].a,b.[ = [.a,b.] by A1,JORDAN5A:26;
Cl A = (Cl A1) /\ [#]I[01] by A2,PRE_TOPC:17
.= [.a,b.] /\ [#]I[01] by A3,JORDAN5A:24
.= [.a,b.] by A1,A2,Th5,XBOOLE_1:28;
hence thesis;
end;
theorem Th11:
for A being Subset of I[01], a, b being Real st a < b & A
= ].a,b.] holds Cl A = [.a,b.]
proof
let A be Subset of I[01], a, b be Real;
assume that
A1: a < b and
A2: A = ].a,b.];
reconsider A1 = ].a,b.] as Subset of R^1 by TOPMETR:17;
A3: Cl ].a,b.] = [.a,b.] by A1,Th8;
Cl A = (Cl A1) /\ [#]I[01] by A2,PRE_TOPC:17
.= [.a,b.] /\ [#]I[01] by A3,JORDAN5A:24
.= [.a,b.] by A1,A2,Th6,XBOOLE_1:28;
hence thesis;
end;
theorem Th12:
for A being Subset of I[01], a, b being Real st a < b & A
= [.a,b.[ holds Cl A = [.a,b.]
proof
let A be Subset of I[01], a, b be Real;
assume that
A1: a < b and
A2: A = [.a,b.[;
reconsider A1 = [.a,b.[ as Subset of R^1 by TOPMETR:17;
A3: Cl [.a,b.[ = [.a,b.] by A1,Th9;
Cl A = (Cl A1) /\ [#]I[01] by A2,PRE_TOPC:17
.= [.a,b.] /\ [#]I[01] by A3,JORDAN5A:24
.= [.a,b.] by A1,A2,Th7,XBOOLE_1:28;
hence thesis;
end;
theorem Th13:
for A being Subset of I[01], a, b being Real st a <= b &
A = [.a,b.] holds 0 <= a & b <= 1
proof
let A be Subset of I[01], a, b be Real;
assume that
A1: a <= b and
A2: A = [.a,b.];
A3: b in A by A1,A2,XXREAL_1:1;
a in A by A1,A2,XXREAL_1:1;
hence thesis by A3,BORSUK_1:43;
end;
theorem Th14:
for A, B being Subset of I[01], a, b, c being Real st a <
b & b < c & A = [.a,b.[ & B = ].b,c.] holds A, B are_separated
proof
let A, B be Subset of I[01], a, b, c be Real;
assume that
A1: a < b and
A2: b < c and
A3: A = [.a,b.[ and
A4: B = ].b,c.];
Cl A = [.a,b.] by A1,A3,Th12;
hence Cl A misses B by A4,XXREAL_1:90;
Cl B = [.b,c.] by A2,A4,Th11;
hence thesis by A3,XXREAL_1:95;
end;
theorem
for p1, p2 being Point of I[01] holds [. p1, p2 .] is Subset of I[01]
by BORSUK_1:40,XXREAL_2:def 12;
theorem Th16:
for a, b being Point of I[01] holds ]. a, b .[ is Subset of I[01]
proof
let a, b be Point of I[01];
A1: [. a,b .] is Subset of I[01] by BORSUK_1:40,XXREAL_2:def 12;
]. a,b .[ c= [. a,b .] by XXREAL_1:25;
hence thesis by A1,XBOOLE_1:1;
end;
begin :: Decompositions of Intervals
theorem
for p being Real holds {p} is non empty closed_interval Subset of REAL
proof
let p be Real;
A1: {p} = [.p,p.] by XXREAL_1:17;
thus thesis by A1,MEASURE5:14;
end;
theorem Th18:
for A being non empty connected Subset of I[01], a, b, c being
Point of I[01] st a <= b & b <= c & a in A & c in A holds b in A
proof
let A be non empty connected Subset of I[01], a, b, c be Point of I[01];
assume that
A1: a <= b and
A2: b <= c and
A3: a in A and
A4: c in A;
per cases by A1,A2,A3,A4,XXREAL_0:1;
suppose
a = b or b = c;
hence thesis by A3,A4;
end;
suppose
A5: a < b & b < c & a in A & c in A;
A6: ].b,1 .] c= [.b,1 .] by XXREAL_1:23;
A7: [.0,b.[ c= [.0,b.] by XXREAL_1:24;
A8: 0 <= a by BORSUK_1:43;
A9: c <= 1 by BORSUK_1:43;
then
A10: b < 1 by A5,XXREAL_0:2;
then
A11: b in [. 0,1 .] by A5,A8,XXREAL_1:1;
1 in [.0,1 .] by XXREAL_1:1;
then
A12: [. b,1 .] c= [.0,1 .] by A11,XXREAL_2:def 12;
0 in [.0,1 .] by XXREAL_1:1;
then [.0,b.] c= [. 0,1 .] by A11,XXREAL_2:def 12;
then reconsider
B = [.0,b.[, C = ].b,1 .] as non empty Subset of I[01] by A5,A8,A9,A7,A6
,A12,BORSUK_1:40,XBOOLE_1:1,XXREAL_1:2,3;
assume not b in A;
then A c= [. 0,1 .] \ {b} by BORSUK_1:40,ZFMISC_1:34;
then
A13: A c= [. 0,b .[ \/ ]. b,1 .] by A5,A8,A10,XXREAL_1:201;
now
per cases by A5,A8,A10,A13,Th14,CONNSP_1:16;
suppose
A c= B;
hence contradiction by A5,XXREAL_1:3;
end;
suppose
A c= C;
hence contradiction by A5,XXREAL_1:2;
end;
end;
hence thesis;
end;
end;
theorem Th19:
for A being non empty connected Subset of I[01], a, b being Real
st a in A & b in A holds [.a,b.] c= A
proof
let A be non empty connected Subset of I[01], a, b be Real;
assume that
A1: a in A and
A2: b in A;
let x be object;
assume x in [.a,b.];
then x in { y where y is Real: a <= y & y <= b } by RCOMP_1:def 1;
then consider z being Real such that
A3: z = x and
A4: a <= z and
A5: z <= b;
A6: 0 <= z by A1,A4,BORSUK_1:43;
b <= 1 by A2,BORSUK_1:43;
then z <= 1 by A5,XXREAL_0:2;
then reconsider z as Point of I[01] by A6,BORSUK_1:43;
z in A by A1,A2,A4,A5,Th18;
hence thesis by A3;
end;
theorem Th20:
for a, b being Real, A being Subset of I[01] st A = [.a,b
.] holds A is closed
proof
let a, b be Real, A be Subset of I[01];
assume
A1: A = [.a,b.];
per cases;
suppose
A2: a <= b;
then
A3: b <= 1 by A1,Th13;
0 <= a by A1,A2,Th13;
then
A4: Closed-Interval-TSpace(a,b) is closed SubSpace of
Closed-Interval-TSpace(0,1) by A2,A3,TREAL_1:3;
then reconsider
BA = the carrier of Closed-Interval-TSpace(a,b) as Subset of
Closed-Interval-TSpace(0,1) by BORSUK_1:1;
BA is closed by A4,BORSUK_1:def 11;
hence thesis by A1,A2,TOPMETR:18,20;
end;
suppose
a > b;
then A = {}I[01] by A1,XXREAL_1:29;
hence thesis;
end;
end;
theorem Th21:
for p1, p2 being Point of I[01] st p1 <= p2 holds [. p1, p2 .]
is non empty compact connected Subset of I[01]
proof
let p1, p2 be Point of I[01];
A1: p2 <= 1 by BORSUK_1:43;
set S = [. p1, p2 .];
reconsider S as Subset of I[01] by BORSUK_1:40,XXREAL_2:def 12;
assume
A2: p1 <= p2;
then
A3: Closed-Interval-TSpace(p1,p2) is connected by TREAL_1:20;
A4: S is closed by Th20;
0 <= p1 by BORSUK_1:43;
then I[01] | S = Closed-Interval-TSpace(p1,p2) by A2,A1,TOPMETR:24;
hence thesis by A4,A3,COMPTS_1:8,CONNSP_1:def 3;
end;
theorem Th22:
for X being Subset of I[01], X9 being Subset of REAL st X9 = X
holds X9 is bounded_above bounded_below
proof
let X be Subset of I[01], X9 be Subset of REAL;
assume
A1: X9 = X;
then for r being ExtReal st r in X9 holds r <= 1 by BORSUK_1:43;
then 1 is UpperBound of X9 by XXREAL_2:def 1;
hence X9 is bounded_above by XXREAL_2:def 10;
for r being ExtReal st r in X9 holds 0 <= r by A1,BORSUK_1:43;
then 0 is LowerBound of X9 by XXREAL_2:def 2;
hence thesis by XXREAL_2:def 9;
end;
theorem Th23:
for X being Subset of I[01], X9 being Subset of REAL, x being
Real st x in X9 & X9 = X holds lower_bound X9 <= x &
x <= upper_bound X9
proof
let X be Subset of I[01], X9 be Subset of REAL, x be Real;
assume that
A1: x in X9 and
A2: X9 = X;
X9 is bounded_above bounded_below by A2,Th22;
hence thesis by A1,SEQ_4:def 1,def 2;
end;
Lm1: I[01] is closed SubSpace of R^1 by TOPMETR:20,TREAL_1:2;
theorem Th24:
for A being Subset of REAL, B being Subset of I[01] st A = B
holds A is closed iff B is closed
proof
reconsider Z = the carrier of I[01] as Subset of R^1 by BORSUK_1:1;
let A be Subset of REAL, B be Subset of I[01];
assume
A1: A = B;
the carrier of I[01] c= the carrier of R^1 by BORSUK_1:1;
then reconsider C = A as Subset of R^1 by A1,XBOOLE_1:1;
hereby
assume A is closed;
then
A2: C is closed by JORDAN5A:23;
C /\ [#] I[01] = B by A1,XBOOLE_1:28;
hence B is closed by A2,PRE_TOPC:13;
end;
assume
A3: B is closed;
Z is closed by Lm1,BORSUK_1:def 11;
then B is closed iff C is closed by A1,TSEP_1:8;
hence thesis by A3,JORDAN5A:23;
end;
theorem Th25:
for C being non empty closed_interval Subset of REAL
holds lower_bound C <= upper_bound C
proof
let C be non empty closed_interval Subset of REAL;
set c = the Element of C;
A1: c <= upper_bound C by INTEGRA2:1;
lower_bound C <= c by INTEGRA2:1;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th26:
for C being non empty compact connected Subset of I[01], C9
being Subset of REAL st C = C9 &
[. lower_bound C9, upper_bound C9 .] c= C9 holds [. lower_bound C9,
upper_bound C9 .] = C9
proof
let C be non empty compact connected Subset of I[01], C9 be Subset of REAL;
assume that
A1: C = C9 and
A2: [. lower_bound C9, upper_bound C9 .] c= C9;
assume [. lower_bound C9, upper_bound C9 .] <> C9;
then not C9 c= [. lower_bound C9, upper_bound C9 .] by A2,XBOOLE_0:def 10;
then consider c being object such that
A3: c in C9 and
A4: not c in [. lower_bound C9, upper_bound C9 .];
reconsider c as Real by A3;
A5: c <= upper_bound C9 by A1,A3,Th23;
lower_bound C9 <= c by A1,A3,Th23;
hence thesis by A4,A5,XXREAL_1:1;
end;
theorem Th27:
for C being non empty compact connected Subset of I[01] holds C
is non empty closed_interval Subset of REAL
proof
let C be non empty compact connected Subset of I[01];
reconsider C9 = C as Subset of REAL by BORSUK_1:40,XBOOLE_1:1;
C9 is bounded_below bounded_above by Th22;
then
A1: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
A2: C9 is closed by Th24;
then
A3: upper_bound C9 in C9 by Th22,RCOMP_1:12;
lower_bound C9 in C9 by A2,Th22,RCOMP_1:13;
then [. lower_bound C9, upper_bound C9 .] = C9 by A3,Th19,Th26;
hence thesis by A1,MEASURE5:14;
end;
theorem Th28:
for C being non empty compact connected Subset of I[01] ex p1,
p2 being Point of I[01] st p1 <= p2 & C = [. p1, p2 .]
proof
let C be non empty compact connected Subset of I[01];
reconsider C9 = C as non empty closed_interval Subset of REAL by Th27;
A1: C9 = [. lower_bound C9, upper_bound C9 .] by INTEGRA1:4;
A2: lower_bound C9 <= upper_bound C9 by Th25;
then
A3: upper_bound C9 in C by A1,XXREAL_1:1;
lower_bound C9 in C by A1,A2,XXREAL_1:1;
then reconsider p1 = lower_bound C9, p2 = upper_bound C9 as Point of I[01]
by A3;
take p1, p2;
thus p1 <= p2 by Th25;
thus thesis by INTEGRA1:4;
end;
begin :: Decompositions of Simple Closed Curves
definition
func I(01) -> strict SubSpace of I[01] means
:Def1:
the carrier of it = ]. 0,1 .[;
existence
proof
reconsider E = ]. 0,1 .[ as Subset of I[01] by BORSUK_1:40,XXREAL_1:25;
take I[01] | E;
thus thesis by PRE_TOPC:8;
end;
uniqueness by TSEP_1:5;
end;
registration
cluster I(01) -> non empty;
coherence
proof
the carrier of I(01) = ]. 0,1 .[ by Def1;
hence the carrier of I(01) is non empty by XXREAL_1:33;
end;
end;
theorem
for A being Subset of I[01] st A = the carrier of I(01) holds
I(01) = I[01] | A by PRE_TOPC:8,TSEP_1:5;
theorem Th30:
the carrier of I(01) = (the carrier of I[01]) \ {0,1}
proof
A1: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128;
the carrier of I(01) = ]. 0,1 .[ by Def1;
hence thesis by A1,BORSUK_1:40,XBOOLE_1:88,XXREAL_1:86;
end;
registration
cluster I(01) -> open;
coherence by Th30,JORDAN6:34,TSEP_1:def 1;
end;
theorem
I(01) is open;
theorem Th32:
for r being Real holds r in the carrier of I(01) iff 0 < r & r < 1
proof
let r be Real;
hereby
assume r in the carrier of I(01);
then r in ]. 0, 1 .[ by Def1;
hence 0 < r & r < 1 by XXREAL_1:4;
end;
assume that
A1: 0 < r and
A2: r < 1;
r in ]. 0, 1 .[ by A1,A2,XXREAL_1:4;
hence thesis by Def1;
end;
theorem Th33:
for a, b being Point of I[01] st a < b & b <> 1 holds ]. a, b .]
is non empty Subset of I(01)
proof
let a, b be Point of I[01];
assume that
A1: a < b and
A2: b <> 1;
b <= 1 by BORSUK_1:43;
then
A3: b < 1 by A2,XXREAL_0:1;
]. a, b .] c= the carrier of I(01)
proof
let x be object;
assume x in ]. a, b .];
then x in { r where r is Real: a < r & r <= b } by RCOMP_1:def 8;
then consider r being Real such that
A4: x = r and
A5: a < r and
A6: r <= b;
A7: 0 < r by A5,BORSUK_1:43;
r < 1 by A3,A6,XXREAL_0:2;
hence thesis by A4,A7,Th32;
end;
hence thesis by A1,XXREAL_1:2;
end;
theorem Th34:
for a, b being Point of I[01] st a < b & a <> 0 holds [. a, b .[
is non empty Subset of I(01)
proof
let a, b be Point of I[01];
assume that
A1: a < b and
A2: a <> 0;
A3: b <= 1 by BORSUK_1:43;
[. a, b .[ c= the carrier of I(01)
proof
let x be object;
assume x in [. a, b .[;
then x in { r where r is Real : a <= r & r < b } by RCOMP_1:def 7;
then consider r being Real such that
A4: x = r and
A5: a <= r and
A6: r < b;
A7: r < 1 by A3,A6,XXREAL_0:2;
0 < r by A2,A5,BORSUK_1:43;
hence thesis by A4,A7,Th32;
end;
hence thesis by A1,XXREAL_1:3;
end;
theorem
for D being Simple_closed_curve holds (TOP-REAL 2) | R^2-unit_square,
(TOP-REAL 2) | D are_homeomorphic
proof
let D be Simple_closed_curve;
ex f being Function of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|D st f
is being_homeomorphism by TOPREAL2:def 1;
hence thesis by T_0TOPSP:def 1;
end;
theorem
for n being Element of NAT, D being non empty Subset of TOP-REAL n, p1
, p2 being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I(01), (TOP-REAL
n) | (D \ {p1,p2}) are_homeomorphic
proof
reconsider K0 = the carrier of I(01) as Subset of I[01] by BORSUK_1:1;
let n be Element of NAT, D be non empty Subset of TOP-REAL n, p1, p2 be
Point of TOP-REAL n;
assume
A1: D is_an_arc_of p1, p2;
then consider f being Function of I[01], (TOP-REAL n)|D such that
A2: f is being_homeomorphism and
A3: f.0 = p1 and
A4: f.1 = p2 by TOPREAL1:def 1;
A5: rng f = [#] ((TOP-REAL n)|D) by A2,TOPS_2:def 5
.= D by PRE_TOPC:8;
A6: dom f = the carrier of I[01] by FUNCT_2:def 1;
then
A7: 0 in dom f by BORSUK_1:43;
A8: 1 in dom f by A6,BORSUK_1:43;
A9: f is continuous one-to-one by A2,TOPS_2:def 5;
then
A10: f .: the carrier of I(01) = f .: (the carrier of I[01]) \ f .: {0,1} by
Th30,FUNCT_1:64
.= D \ f .: {0,1} by A6,A5,RELAT_1:113
.= D \ {p1,p2} by A3,A4,A7,A8,FUNCT_1:60;
A11: D \ {p1,p2} c= D by XBOOLE_1:36;
then reconsider D0 = D \ {p1,p2} as Subset of (TOP-REAL n)|D by PRE_TOPC:8;
reconsider D1 = D \ {p1,p2} as non empty Subset of TOP-REAL n by A1,
JORDAN6:43;
A12: (TOP-REAL n)|D1 = ((TOP-REAL n)|D)|D0 by GOBOARD9:2;
set g = (f") | D1;
A13: D1 = the carrier of (TOP-REAL n)|D1 by PRE_TOPC:8;
D1 c= the carrier of (TOP-REAL n)|D by A11,PRE_TOPC:8;
then reconsider ff = g as Function of (TOP-REAL n)|D1, I[01] by A13,
FUNCT_2:32;
f" is continuous by A2,TOPS_2:def 5;
then
A14: ff is continuous by A12,TOPMETR:7;
set fD = f | the carrier of I(01);
A15: I(01) = I[01] | K0 by PRE_TOPC:8,TSEP_1:5;
then reconsider fD1 = fD as Function of I[01]|K0, (TOP-REAL n)|D by
FUNCT_2:32;
A16: dom fD = the carrier of I(01) by A6,BORSUK_1:1,RELAT_1:62;
rng f = [#]((TOP-REAL n)|D) by A2,TOPS_2:def 5;
then f is onto by FUNCT_2:def 3;
then
A17: f" = (f qua Function)" by A9,TOPS_2:def 4;
A18: rng fD = f .: the carrier of I(01) by RELAT_1:115;
then
A19: rng fD = the carrier of ((TOP-REAL n)|(D \ {p1,p2})) by A10,PRE_TOPC:8;
then reconsider fD as Function of I(01), (TOP-REAL n)|(D \ {p1,p2}) by A16,
FUNCT_2:1;
A20: dom fD = [#]I(01) by A6,BORSUK_1:1,RELAT_1:62;
A21: fD is onto by A19,FUNCT_2:def 3;
f is one-to-one by A2,TOPS_2:def 5;
then
A22: fD is one-to-one by FUNCT_1:52;
then fD" = (fD qua Function)" by A21,TOPS_2:def 4;
then
A23: fD" is continuous by A9,A10,A15,A14,A17,RFUNCT_2:17,TOPMETR:6;
fD1 is continuous by A9,TOPMETR:7;
then
A24: fD is continuous by A15,A12,TOPMETR:6;
rng fD = [#]((TOP-REAL n)|(D \ {p1,p2})) by A10,A18,PRE_TOPC:8;
then fD is being_homeomorphism by A20,A22,A24,A23,TOPS_2:def 5;
hence thesis by T_0TOPSP:def 1;
end;
theorem Th37:
for n being Element of NAT, D being Subset of TOP-REAL n, p1, p2
being Point of TOP-REAL n st D is_an_arc_of p1, p2 holds I[01], (TOP-REAL n) |
D are_homeomorphic
proof
let n be Element of NAT, D be Subset of TOP-REAL n, p1, p2 be Point of
TOP-REAL n;
assume D is_an_arc_of p1, p2;
then
ex f being Function of I[01], (TOP-REAL n)|D st f is being_homeomorphism
& f.0 = p1 & f.1 = p2 by TOPREAL1:def 1;
hence thesis by T_0TOPSP:def 1;
end;
theorem
for n being Element of NAT, p1, p2 being Point of TOP-REAL n st p1 <>
p2 holds I[01], (TOP-REAL n) | LSeg (p1, p2) are_homeomorphic by Th37,
TOPREAL1:9;
theorem Th39:
for E being Subset of I(01) st (ex p1, p2 being Point of I[01]
st p1 < p2 & E = [. p1,p2 .]) holds I[01], I(01)|E are_homeomorphic
proof
let E be Subset of I(01);
given p1, p2 being Point of I[01] such that
A1: p1 < p2 and
A2: E = [. p1,p2 .];
A3: p2 <= 1 by BORSUK_1:43;
0 <= p1 by BORSUK_1:43;
then reconsider
S = Closed-Interval-TSpace(p1,p2) as SubSpace of I[01] by A1,A3,TOPMETR:20
,TREAL_1:3;
reconsider T = I(01)|E as SubSpace of I[01] by TSEP_1:7;
the carrier of S = E by A1,A2,TOPMETR:18;
then
A4: S = T by PRE_TOPC:8,TSEP_1:5;
set f = L[01]((#)(p1,p2), (p1,p2)(#));
f is being_homeomorphism by A1,TREAL_1:17;
hence thesis by A4,TOPMETR:20,T_0TOPSP:def 1;
end;
theorem Th40:
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b ex E being non empty Subset of I[01], f being Function of I[01]|E, (
TOP-REAL n)|A st E = [. a, b .] & f is being_homeomorphism & f.a = p & f.b = q
proof
A1: 0 = (#)(0,1) by TREAL_1:def 1;
let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
TOP-REAL n, a, b be Point of I[01];
assume that
A2: A is_an_arc_of p, q and
A3: a < b;
reconsider E = [. a, b .] as non empty Subset of I[01] by A3,Th21;
A4: b <= 1 by BORSUK_1:43;
0 <= a by BORSUK_1:43;
then
A5: I[01]|E = Closed-Interval-TSpace(a,b) by A3,A4,TOPMETR:24;
then reconsider
e = P[01](a,b,(#)(0,1),(0,1)(#)) as Function of I[01]|E, I[01] by TOPMETR:20;
take E;
A6: a = (#)(a,b) by A3,TREAL_1:def 1;
reconsider B = A as non empty Subset of TOP-REAL n by A2,TOPREAL1:1;
consider f being Function of I[01], (TOP-REAL n)|B such that
A7: f is being_homeomorphism and
A8: f.0 = p and
A9: f.1 = q by A2,TOPREAL1:def 1;
set g = f * e;
reconsider g as Function of I[01]|E, (TOP-REAL n)|A;
take g;
thus E = [. a, b .];
e is being_homeomorphism by A3,A5,TOPMETR:20,TREAL_1:17;
hence g is being_homeomorphism by A7,TOPS_2:57;
a in E by A3,XXREAL_1:1;
then a in the carrier of I[01]|E by PRE_TOPC:8;
hence g.a = f.(e.a) by FUNCT_2:15
.= p by A3,A8,A1,A6,TREAL_1:13;
A10: 1 = (0,1)(#) by TREAL_1:def 2;
A11: b = (a,b)(#) by A3,TREAL_1:def 2;
b in E by A3,XXREAL_1:1;
then b in the carrier of I[01]|E by PRE_TOPC:8;
hence g.b = f.(e.b) by FUNCT_2:15
.= q by A3,A9,A10,A11,TREAL_1:13;
end;
theorem Th41:
for A being TopSpace, B being non empty TopSpace, f being
Function of A, B, C being TopSpace, X being Subset of A st f is continuous & C
is SubSpace of B holds for h being Function of A|X, C st h = f|X holds h is
continuous
proof
let A be TopSpace, B be non empty TopSpace;
let f be Function of A,B;
let C be TopSpace, X be Subset of A;
assume that
A1: f is continuous and
A2: C is SubSpace of B;
the carrier of A|X = X by PRE_TOPC:8;
then reconsider g = f|X as Function of A|X, B by FUNCT_2:32;
let h be Function of A|X, C;
assume
A3: h = f|X;
g is continuous by A1,TOPMETR:7;
hence thesis by A2,A3,PRE_TOPC:27;
end;
theorem Th42:
for X being Subset of I[01], a, b being Point of I[01] st X = ].
a, b .[ holds X is open
proof
let X be Subset of I[01], a, b be Point of I[01];
A1: 0 <= a by BORSUK_1:43;
1 in the carrier of I[01] by BORSUK_1:43;
then reconsider B = [. b, 1 .] as Subset of I[01] by BORSUK_1:40
,XXREAL_2:def 12;
0 in the carrier of I[01] by BORSUK_1:43;
then reconsider A = [. 0, a .] as Subset of I[01] by BORSUK_1:40
,XXREAL_2:def 12;
A2: b <= 1 by BORSUK_1:43;
A3: B is closed by Th20;
A4: A is closed by Th20;
assume X = ]. a, b .[;
then X = (A \/ B)` by A1,A2,BORSUK_1:40,XXREAL_1:200;
hence thesis by A4,A3;
end;
theorem Th43:
for X being Subset of I(01), a, b being Point of I[01] st X = ].
a, b .[ holds X is open
proof
let X be Subset of I(01), a, b be Point of I[01];
assume
A1: X = ]. a, b .[;
then reconsider X9 = X as Subset of I[01] by Th16;
X9 is open by A1,Th42;
hence thesis by TSEP_1:17;
end;
theorem Th44:
for X being Subset of I(01), a being Point of I[01] st X = ]. 0,
a .] holds X is closed
proof
let X be Subset of I(01), a be Point of I[01];
assume
A1: X = ]. 0, a .];
per cases;
suppose
A2: 0 < a;
[#] I(01) = ]. 0, 1 .[ by Def1;
then
A3: [#] I(01) \ X = ]. a, 1 .[ by A1,A2,XXREAL_1:187;
1 in the carrier of I[01] by BORSUK_1:43;
then [#] I(01) \ X is open by A3,Th43;
hence thesis by PRE_TOPC:def 3;
end;
suppose
0 >= a;
then X = {}I(01) by A1,XXREAL_1:26;
hence thesis;
end;
end;
theorem Th45:
for X being Subset of I(01), a being Point of I[01] st X = [. a,
1 .[ holds X is closed
proof
A1: 0 in the carrier of I[01] by BORSUK_1:43;
let X be Subset of I(01), a be Point of I[01];
assume
A2: X = [. a, 1 .[;
per cases;
suppose
A3: X is non empty;
A4: a <= 1 by BORSUK_1:43;
a <> 1 by A2,A3,XXREAL_1:18;
then
A5: a < 1 by A4,XXREAL_0:1;
[#] I(01) = ]. 0, 1 .[ by Def1;
then [#] I(01) \ X = ]. 0, a .[ by A2,A5,XXREAL_1:195;
then [#] I(01) \ X is open by A1,Th43;
hence thesis by PRE_TOPC:def 3;
end;
suppose
X is empty;
hence thesis;
end;
end;
theorem Th46:
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & b <> 1 ex E being non empty Subset of I(01), f being Function of I(01)|E,
(TOP-REAL n)|(A \ {p}) st E = ]. a, b .] & f is being_homeomorphism & f.b = q
proof
let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
TOP-REAL n, a, b be Point of I[01];
assume that
A1: A is_an_arc_of p, q and
A2: a < b and
A3: b <> 1;
reconsider B = A as non empty Subset of TOP-REAL n by A1,TOPREAL1:1;
consider F being non empty Subset of I[01], s being Function of I[01]|F, (
TOP-REAL n)|B such that
A4: F = [. a, b .] and
A5: s is being_homeomorphism and
A6: s.a = p and
A7: s.b = q by A1,A2,Th40;
A8: dom s = [#] (I[01]|F) by A5,TOPS_2:def 5
.= F by PRE_TOPC:def 5;
then
A9: a in dom s by A2,A4,XXREAL_1:1;
reconsider E = ]. a, b .] as non empty Subset of I(01) by A2,A3,Th33;
set X = E;
A10: I(01)|X is SubSpace of I[01] by TSEP_1:7;
set sX = s|E;
A11: s is continuous one-to-one by A5,TOPS_2:def 5;
A12: s" is continuous by A5,TOPS_2:def 5;
A13: the carrier of (TOP-REAL n)|A = A by PRE_TOPC:8;
then reconsider Ap = A \ {p} as Subset of (TOP-REAL n)|A by XBOOLE_1:36;
the carrier of (TOP-REAL n)|(A \ {p}) = A \ {p} by PRE_TOPC:8;
then the carrier of (TOP-REAL n)|(A \ {p}) c= the carrier of (TOP-REAL n)|A
by A13,XBOOLE_1:36;
then
A14: (TOP-REAL n)|(A \ {p}) is SubSpace of (TOP-REAL n)|A by TSEP_1:4;
A15: E c= F by A4,XXREAL_1:23;
then reconsider X9 = E as Subset of I[01]|F by PRE_TOPC:8;
A16: I[01]|F|X9 is SubSpace of I[01] by TSEP_1:7;
the carrier of I(01)|E = E by PRE_TOPC:8;
then the carrier of I(01)|X c= the carrier of I[01]|F by A15,PRE_TOPC:8;
then
A17: I(01)|X is SubSpace of I[01]|F by A10,TSEP_1:4;
A18: ((TOP-REAL n)|A)|Ap = (TOP-REAL n)|(A \ {p}) by PRE_TOPC:7,XBOOLE_1:36;
A19: dom sX = X by A4,A8,RELAT_1:62,XXREAL_1:23
.= [#] (I(01)|X) by PRE_TOPC:def 5;
A20: rng s = [#] ((TOP-REAL n)|A) by A5,TOPS_2:def 5;
then
A21: rng s = A by PRE_TOPC:def 5;
X = F \ {a} by A2,A4,XXREAL_1:134;
then
A22: s.:X = s.:F \ Im(s,a) by A11,FUNCT_1:64
.= s.:F \ {s.a} by A9,FUNCT_1:59
.= rng s \ {p} by A6,A8,RELAT_1:113
.= [#] ((TOP-REAL n)|(A \ {p})) by A21,PRE_TOPC:def 5;
then
A23: [#] ((TOP-REAL n)|(A \ {p})) = rng sX by RELAT_1:115;
rng (s|E) = the carrier of (TOP-REAL n)|(A \ {p}) by A22,RELAT_1:115;
then reconsider sX as Function of I(01)|E, (TOP-REAL n)|(A \ {p}) by A19,
FUNCT_2:1;
A24: s is onto by A20,FUNCT_2:def 3;
A25: sX is onto by A23,FUNCT_2:def 3;
b in X by A2,XXREAL_1:2;
then
A26: sX.b = q by A7,FUNCT_1:49;
the carrier of I(01)|X = X by PRE_TOPC:8;
then I(01)|X = I[01]|F|X9 by A10,A16,PRE_TOPC:8,TSEP_1:5;
then
A27: sX is continuous by A11,A14,Th41;
A28: sX is one-to-one by A11,FUNCT_1:52;
then sX" = (sX qua Function)" by A25,TOPS_2:def 4
.= (s qua Function)" | (s.:X) by A11,RFUNCT_2:17
.= s" | [#] ((TOP-REAL n)|(A \ {p})) by A24,A11,A22,TOPS_2:def 4
.= s" | Ap by PRE_TOPC:def 5;
then sX" is continuous by A12,A17,A18,Th41;
then sX is being_homeomorphism by A23,A19,A27,A28,TOPS_2:def 5;
hence thesis by A26;
end;
theorem Th47:
for n being Element of NAT, A being Subset of TOP-REAL n, p, q
being Point of TOP-REAL n, a, b being Point of I[01] st A is_an_arc_of p, q & a
< b & a <> 0 ex E being non empty Subset of I(01), f being Function of I(01)|E,
(TOP-REAL n)|(A \ {q}) st E = [. a, b .[ & f is being_homeomorphism & f.a = p
proof
let n be Element of NAT, A be Subset of TOP-REAL n, p, q be Point of
TOP-REAL n, a, b be Point of I[01];
assume that
A1: A is_an_arc_of p, q and
A2: a < b and
A3: a <> 0;
reconsider B = A as non empty Subset of TOP-REAL n by A1,TOPREAL1:1;
consider F being non empty Subset of I[01], s being Function of I[01]|F, (
TOP-REAL n)|B such that
A4: F = [. a, b .] and
A5: s is being_homeomorphism and
A6: s.a = p and
A7: s.b = q by A1,A2,Th40;
A8: dom s = [#] (I[01]|F) by A5,TOPS_2:def 5
.= F by PRE_TOPC:def 5;
then
A9: b in dom s by A2,A4,XXREAL_1:1;
reconsider E = [. a, b .[ as non empty Subset of I(01) by A2,A3,Th34;
set X = E;
A10: I(01)|X is SubSpace of I[01] by TSEP_1:7;
set sX = s|E;
A11: s is continuous one-to-one by A5,TOPS_2:def 5;
A12: s" is continuous by A5,TOPS_2:def 5;
A13: the carrier of (TOP-REAL n)|A = A by PRE_TOPC:8;
then reconsider Ap = A \ {q} as Subset of (TOP-REAL n)|A by XBOOLE_1:36;
the carrier of (TOP-REAL n)|(A \ {q}) = A \ {q} by PRE_TOPC:8;
then the carrier of (TOP-REAL n)|(A \ {q}) c= the carrier of (TOP-REAL n)|A
by A13,XBOOLE_1:36;
then
A14: (TOP-REAL n)|(A \ {q}) is SubSpace of (TOP-REAL n)|A by TSEP_1:4;
A15: E c= F by A4,XXREAL_1:24;
then reconsider X9 = E as Subset of I[01]|F by PRE_TOPC:8;
A16: I[01]|F|X9 is SubSpace of I[01] by TSEP_1:7;
the carrier of I(01)|E = E by PRE_TOPC:8;
then the carrier of I(01)|X c= the carrier of I[01]|F by A15,PRE_TOPC:8;
then
A17: I(01)|X is SubSpace of I[01]|F by A10,TSEP_1:4;
A18: ((TOP-REAL n)|A)|Ap = (TOP-REAL n)|(A \ {q}) by PRE_TOPC:7,XBOOLE_1:36;
A19: dom sX = X by A4,A8,RELAT_1:62,XXREAL_1:24
.= [#] (I(01)|X) by PRE_TOPC:def 5;
A20: rng s = [#] ((TOP-REAL n)|A) by A5,TOPS_2:def 5;
then
A21: rng s = A by PRE_TOPC:def 5;
X = F \ {b} by A2,A4,XXREAL_1:135;
then
A22: s.:X = s.:F \ Im(s,b) by A11,FUNCT_1:64
.= s.:F \ {s.b} by A9,FUNCT_1:59
.= rng s \ {q} by A7,A8,RELAT_1:113
.= [#] ((TOP-REAL n)|(A \ {q})) by A21,PRE_TOPC:def 5;
then
A23: [#] ((TOP-REAL n)|(A \ {q})) = rng sX by RELAT_1:115;
rng (s|E) = the carrier of (TOP-REAL n)|(A \ {q}) by A22,RELAT_1:115;
then reconsider sX as Function of I(01)|E, (TOP-REAL n)|(A \ {q}) by A19,
FUNCT_2:1;
A24:sX is onto by A23,FUNCT_2:def 3;
A25:s is onto by A20,FUNCT_2:def 3;
a in X by A2,XXREAL_1:3;
then
A26: sX.a = p by A6,FUNCT_1:49;
the carrier of I(01)|X = X by PRE_TOPC:8;
then I(01)|X = I[01]|F|X9 by A10,A16,PRE_TOPC:8,TSEP_1:5;
then
A27: sX is continuous by A11,A14,Th41;
A28: sX is one-to-one by A11,FUNCT_1:52;
then sX" = (sX qua Function)" by A24,TOPS_2:def 4
.= (s qua Function)" | (s.:X) by A11,RFUNCT_2:17
.= s" | [#] ((TOP-REAL n)|(A \ {q})) by A25,A11,A22,TOPS_2:def 4
.= s" | Ap by PRE_TOPC:def 5;
then sX" is continuous by A12,A17,A18,Th41;
then sX is being_homeomorphism by A23,A19,A27,A28,TOPS_2:def 5;
hence thesis by A26;
end;
theorem Th48:
for n being Element of NAT, A, B being Subset of TOP-REAL n, p,
q being Point of TOP-REAL n st A is_an_arc_of p, q & B is_an_arc_of q, p & A /\
B = { p, q } & p <> q holds I(01), (TOP-REAL n) | ((A \ {p}) \/ (B \ {p}))
are_homeomorphic
proof
reconsider a = 0, b = 1/2, c = 1 as Point of I[01] by BORSUK_1:43;
let n be Element of NAT, A, B be Subset of TOP-REAL n, p, q be Point of
TOP-REAL n;
assume that
A1: A is_an_arc_of p, q and
A2: B is_an_arc_of q, p and
A3: A /\ B = { p, q } and
A4: p <> q;
consider E2 being non empty Subset of I(01), ty being Function of I(01)|E2,
(TOP-REAL n)|(B \ {p}) such that
A5: E2 = [. b, c .[ and
A6: ty is being_homeomorphism and
A7: ty.b = q by A2,Th47;
consider E1 being non empty Subset of I(01), sx being Function of I(01)|E1,
(TOP-REAL n)|(A \ {p}) such that
A8: E1 = ]. a, b .] and
A9: sx is being_homeomorphism and
A10: sx.b = q by A1,Th46;
set T1 = I(01)|E1, T2 = I(01)|E2, T = I(01), S = (TOP-REAL n) | ((A \ {p})
\/ (B \ {p})), U1 = (TOP-REAL n) | (A \ {p}), U2 = (TOP-REAL n)|(B \ {p});
A11: A \ {p} is non empty by A1,Th3;
then reconsider S as non empty SubSpace of TOP-REAL n;
B \ {p} is non empty by A2,Th3,JORDAN5B:14;
then reconsider U1, U2 as non empty SubSpace of TOP-REAL n by A11;
A12: the carrier of S = (A \ {p}) \/ (B \ {p}) by PRE_TOPC:8;
the carrier of U2 = B \ {p} by PRE_TOPC:8;
then
A13: the carrier of U2 c= the carrier of S by A12,XBOOLE_1:7;
then reconsider ty9 = ty as Function of T2, S by FUNCT_2:7;
A14: U2 is SubSpace of S by A13,TSEP_1:4;
ty is continuous by A6,TOPS_2:def 5;
then
A15: ty9 is continuous by A14,PRE_TOPC:26;
reconsider F1 = [#] T1, F2 = [#] T2 as non empty Subset of T by
PRE_TOPC:def 5;
A16: F2 = [. 1/2, 1 .[ by A5,PRE_TOPC:def 5;
the carrier of U1 = A \ {p} by PRE_TOPC:8;
then
A17: the carrier of U1 c= the carrier of S by A12,XBOOLE_1:7;
then reconsider sx9 = sx as Function of T1, S by FUNCT_2:7;
A18: U1 is SubSpace of S by A17,TSEP_1:4;
A19: rng ty = [#] ((TOP-REAL n)|(B \ {p})) by A6,TOPS_2:def 5;
then
A20: rng ty = B \ {p} by PRE_TOPC:def 5;
A21: ty is onto by A19,FUNCT_2:def 3;
A22: rng sx = [#] ((TOP-REAL n)|(A \ {p})) by A9,TOPS_2:def 5;
then
A23: rng sx = A \ {p} by PRE_TOPC:def 5;
then
A24: rng sx9 /\ rng ty9 = ((A \ {p}) /\ B) \ {p} by A20,XBOOLE_1:49
.= ((A /\ B) \ {p}) \ {p} by XBOOLE_1:49
.= (A /\ B) \ ({p} \/ {p}) by XBOOLE_1:41
.= { sx9.b } by A3,A4,A10,ZFMISC_1:17;
sx is continuous by A9,TOPS_2:def 5;
then
A25: sx9 is continuous by A18,PRE_TOPC:26;
A26: 1/2 in the carrier of I[01] by BORSUK_1:43;
then
A27: F2 is closed by A16,Th45;
A28: F1 = ]. 0, 1/2 .] by A8,PRE_TOPC:def 5;
then
A29: ([#] T1) \/ ([#] T2) = ]. 0, 1 .[ by A16,XXREAL_1:172
.= [#] T by Def1;
A30: ([#] T1) /\ ([#] T2) = { 1/2 } by A28,A16,XXREAL_1:138;
A31: for d be object st d in ([#] T1) /\ ([#] T2) holds sx.d = ty.d
proof
let d be object;
assume d in ([#] T1) /\ ([#] T2);
then d = b by A30,TARSKI:def 1;
hence thesis by A10,A7;
end;
F1 is closed by A26,A28,Th44;
then consider F being Function of T,S such that
A32: F = sx9+*ty and
A33: F is continuous by A25,A15,A27,A29,A31,JGRAPH_2:1;
A34: [#] U2 = B \ {p} by PRE_TOPC:def 5;
then
A35: [#] U2 c= (A \ {p}) \/ (B \ {p}) by XBOOLE_1:7;
the carrier of T2 c= the carrier of T by BORSUK_1:1;
then reconsider g = ty" as Function of U2, T by FUNCT_2:7;
the carrier of T1 c= the carrier of T by BORSUK_1:1;
then reconsider f = sx" as Function of U1, T by FUNCT_2:7;
A36: dom ty9 = [#] T2 by FUNCT_2:def 1;
A37: [#] U1 = A \ {p} by PRE_TOPC:def 5;
then [#] U1 c= (A \ {p}) \/ (B \ {p}) by XBOOLE_1:7;
then reconsider V1 = [#] U1, V2 = [#] U2 as Subset of S by A35,PRE_TOPC:8;
A38: dom F = [#] I(01) by FUNCT_2:def 1;
A39: V2 is closed
proof
reconsider B9 = B as Subset of TOP-REAL n;
A40: B9 is closed by A2,COMPTS_1:7,JORDAN5A:1;
A41: not p in {q} by A4,TARSKI:def 1;
q in B by A2,TOPREAL1:1;
then
A42: {q} c= B by ZFMISC_1:31;
A43: B /\ (A \ {p}) = B /\ A \ {p} by XBOOLE_1:49
.= {q} by A3,A4,ZFMISC_1:17;
B9 /\ [#] S = B9 /\ ((A \ {p}) \/ (B \ {p})) by PRE_TOPC:def 5
.= (B /\ (A \ {p})) \/ (B /\ (B \ {p})) by XBOOLE_1:23
.= (B /\ (A \ {p})) \/ (B \ {p}) by XBOOLE_1:28,36
.= B \ {p} by A41,A42,A43,XBOOLE_1:12,ZFMISC_1:34
.= V2 by PRE_TOPC:def 5;
hence thesis by A40,PRE_TOPC:13;
end;
A44: V1 is closed
proof
reconsider A9 = A as Subset of TOP-REAL n;
A45: A9 is closed by A1,COMPTS_1:7,JORDAN5A:1;
A46: not p in {q} by A4,TARSKI:def 1;
q in A by A1,TOPREAL1:1;
then
A47: {q} c= A by ZFMISC_1:31;
A48: A /\ (B \ {p}) = A /\ B \ {p} by XBOOLE_1:49
.= {q} by A3,A4,ZFMISC_1:17;
A9 /\ [#] S = A9 /\ ((A \ {p}) \/ (B \ {p})) by PRE_TOPC:def 5
.= (A /\ (A \ {p})) \/ (A /\ (B \ {p})) by XBOOLE_1:23
.= (A \ {p}) \/ (A /\ (B \ {p})) by XBOOLE_1:28,36
.= A \ {p} by A46,A47,A48,XBOOLE_1:12,ZFMISC_1:34
.= V1 by PRE_TOPC:def 5;
hence thesis by A45,PRE_TOPC:13;
end;
ty" is continuous by A6,TOPS_2:def 5;
then
A49: g is continuous by PRE_TOPC:26;
sx" is continuous by A9,TOPS_2:def 5;
then
A50: f is continuous by PRE_TOPC:26;
A51: ty9 is one-to-one by A6,TOPS_2:def 5;
then
A52: ty" = (ty qua Function)" by A21,TOPS_2:def 4;
A53: dom sx9 = [#] T1 by FUNCT_2:def 1;
then
A54: dom sx9 /\ dom ty9 = { b } by A28,A16,A36,XXREAL_1:138;
sx9 tolerates ty9
proof
let t be object;
assume t in dom sx9 /\ dom ty9;
then t = b by A54,TARSKI:def 1;
hence thesis by A10,A7;
end;
then
A55: rng F = rng sx9 \/ rng ty9 by A32,FRECHET:35
.= [#] S by A23,A20,PRE_TOPC:def 5;
A56: sx is onto by A22,FUNCT_2:def 3;
A57: sx9 is one-to-one by A9,TOPS_2:def 5;
then
A58: sx" = (sx qua Function)" by A56,TOPS_2:def 4;
A59: for r being object st r in ([#] U1) /\ ([#] U2) holds f.r = g.r
proof
let r be object;
b in E2 by A5,XXREAL_1:3;
then
A60: b in dom ty by A36,PRE_TOPC:def 5;
b in E1 by A8,XXREAL_1:2;
then b in dom sx by A53,PRE_TOPC:def 5;
then
A61: f.q = b by A10,A57,A58,FUNCT_1:34;
assume r in ([#] U1) /\ ([#] U2);
then r = q by A10,A22,A19,A24,TARSKI:def 1;
hence thesis by A7,A51,A52,A60,A61,FUNCT_1:34;
end;
([#] U1) \/ ([#] U2) = [#] S by A37,A34,PRE_TOPC:def 5;
then
A62: ex h being Function of S,T st h = f+*g & h is continuous by A18,A14,A44
,A39,A50,A49,A59,JGRAPH_2:1;
A63: F is onto by A55,FUNCT_2:def 3;
A64: F is one-to-one by A32,A57,A51,A54,A24,Th1;
then F" = (F qua Function)" by A63,TOPS_2:def 4;
then F" = sx" +* ty" by A10,A7,A32,A57,A51,A54,A24,A58,A52,Th2;
then F is being_homeomorphism by A33,A38,A64,A55,A62,TOPS_2:def 5;
hence thesis by T_0TOPSP:def 1;
end;
theorem Th49:
for D being Simple_closed_curve, p being Point of TOP-REAL 2 st
p in D holds (TOP-REAL 2) | (D \ {p}), I(01) are_homeomorphic
proof
let D be Simple_closed_curve, p be Point of TOP-REAL 2;
consider q being Point of TOP-REAL 2 such that
A1: q in D and
A2: p <> q by SUBSET_1:51;
not q in {p} by A2,TARSKI:def 1;
then reconsider R2p = D \ {p} as non empty Subset of TOP-REAL 2 by A1,
XBOOLE_0:def 5;
assume p in D;
then consider P1, P2 being non empty Subset of TOP-REAL 2 such that
A3: P1 is_an_arc_of p,q and
A4: P2 is_an_arc_of p,q and
A5: D = P1 \/ P2 and
A6: P1 /\ P2 = {p,q} by A1,A2,TOPREAL2:5;
A7: P2 is_an_arc_of q, p by A4,JORDAN5B:14;
D \ {p} = (P1 \ {p}) \/ (P2 \ {p}) by A5,XBOOLE_1:42;
then (TOP-REAL 2) | R2p, I(01) are_homeomorphic by A2,A3,A6,A7,Th48;
hence thesis;
end;
theorem
for D being Simple_closed_curve, p, q being Point of TOP-REAL 2 st p
in D & q in D holds (TOP-REAL 2) | (D \ {p}), (TOP-REAL 2) | (D \ {q})
are_homeomorphic
proof
let D be Simple_closed_curve, p, q be Point of TOP-REAL 2;
assume that
A1: p in D and
A2: q in D;
per cases;
suppose
p = q;
hence thesis;
end;
suppose
p <> q;
then reconsider
Dp = D \ {p}, Dq = D \ {q} as non empty Subset of TOP-REAL 2 by A1,A2,
ZFMISC_1:56;
A3: (TOP-REAL 2) | Dq, I(01) are_homeomorphic by A2,Th49;
(TOP-REAL 2) | Dp, I(01) are_homeomorphic by A1,Th49;
hence thesis by A3,BORSUK_3:3;
end;
end;
theorem Th51:
for n being Element of NAT, C being non empty Subset of TOP-REAL
n, E being Subset of I(01) st (ex p1, p2 being Point of I[01] st p1 < p2 & E =
[. p1,p2 .]) & I(01)|E, (TOP-REAL n)|C are_homeomorphic holds ex s1, s2 being
Point of TOP-REAL n st C is_an_arc_of s1,s2
proof
let n be Element of NAT, C be non empty Subset of TOP-REAL n, E be Subset of
I(01);
given p1, p2 being Point of I[01] such that
A1: p1 < p2 and
A2: E = [. p1,p2 .];
A3: I[01], I(01)|E are_homeomorphic by A1,A2,Th39;
assume
A4: I(01)|E, (TOP-REAL n)|C are_homeomorphic;
E is non empty by A1,A2,Th21;
then I[01], (TOP-REAL n)|C are_homeomorphic by A4,A3,BORSUK_3:3;
then consider g being Function of I[01], (TOP-REAL n)|C such that
A5: g is being_homeomorphism by T_0TOPSP:def 1;
set s1 = g.0, s2 = g.1;
0 in the carrier of I[01] by BORSUK_1:43;
then
A6: g.0 in the carrier of (TOP-REAL n)|C by FUNCT_2:5;
1 in the carrier of I[01] by BORSUK_1:43;
then
A7: g.1 in the carrier of (TOP-REAL n)|C by FUNCT_2:5;
the carrier of (TOP-REAL n)|C c= the carrier of TOP-REAL n by BORSUK_1:1;
then reconsider s1, s2 as Point of TOP-REAL n by A6,A7;
C is_an_arc_of s1, s2 by A5,TOPREAL1:def 1;
hence thesis;
end;
theorem Th52:
for Dp being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2) | Dp, I(01), C being non empty Subset of TOP-REAL 2 st f is
being_homeomorphism & C c= Dp & (ex p1, p2 being Point of I[01] st p1 < p2 & f
.:C = [. p1,p2 .]) holds ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of
s1,s2
proof
let Dp be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2) | Dp
, I(01), C be non empty Subset of TOP-REAL 2;
assume that
A1: f is being_homeomorphism and
A2: C c= Dp;
reconsider C9 = C as Subset of (TOP-REAL 2) | Dp by A2,PRE_TOPC:8;
A3: the carrier of (TOP-REAL 2)|Dp = Dp by PRE_TOPC:8;
dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
then C c= dom f by A2,PRE_TOPC:8;
then
A4: C c= f"(f.:C) by FUNCT_1:76;
given p1, p2 being Point of I[01] such that
A5: p1 < p2 and
A6: f.:C = [. p1,p2 .];
reconsider E = [. p1,p2 .] as Subset of I(01) by A6;
A7: rng f = [#] I(01) by A1,TOPS_2:def 5;
A8: f is continuous one-to-one by A1,TOPS_2:def 5;
then f"(f.:C) c= C by FUNCT_1:82;
then f"(f.:C) = C by A4,XBOOLE_0:def 10;
then
A9: f".:E = C by A6,A8,A7,TOPS_2:55;
the carrier of (TOP-REAL 2)|C = C by PRE_TOPC:8;
then
A10: (TOP-REAL 2)|C is SubSpace of (TOP-REAL 2) | Dp by A2,A3,TOPMETR:3;
set g = f"| E;
the carrier of (I(01)|E) = E by PRE_TOPC:8;
then
A11: g is Function of the carrier of I(01)|E, the carrier of (TOP-REAL 2)|Dp
by FUNCT_2:32;
A12: rng g = f".:E by RELAT_1:115
.= [#] ((TOP-REAL 2)|C) by A9,PRE_TOPC:8;
then reconsider g as Function of I(01)|E, (TOP-REAL 2)|C by A11,FUNCT_2:6;
f" is being_homeomorphism by A1,TOPS_2:56;
then
A13: f" is one-to-one by TOPS_2:def 5;
then
A14: g is one-to-one by FUNCT_1:52;
A15: f is onto by A7,FUNCT_2:def 3;
g is onto by A12,FUNCT_2:def 3;
then
A16: g" = (g qua Function)" by A14,TOPS_2:def 4
.= ((f" qua Function)")|((f").:E) by A13,RFUNCT_2:17
.= ((f qua Function)"")|((f").:E) by A8,A15,TOPS_2:def 4
.= f|C by A8,A9,FUNCT_1:43;
then reconsider t = f|C as Function of (TOP-REAL 2) | C, I(01)|E;
dom (f") = the carrier of I(01) by FUNCT_2:def 1;
then dom g = E by RELAT_1:62
.= the carrier of (I(01)|E) by PRE_TOPC:8;
then
A17: dom g = [#] (I(01)|E);
f" is continuous by A1,TOPS_2:def 5;
then
A18: g is continuous by A10,Th41;
((TOP-REAL 2) | Dp)|C9 = (TOP-REAL 2) | C by A2,PRE_TOPC:7;
then t is continuous by A8,Th41;
then g is being_homeomorphism by A12,A17,A14,A18,A16,TOPS_2:def 5;
then I(01)|E, (TOP-REAL 2)|C are_homeomorphic by T_0TOPSP:def 1;
hence thesis by A5,Th51;
end;
theorem
for D being Simple_closed_curve, C being non empty compact connected
Subset of TOP-REAL 2 st C c= D holds C = D or (ex p1, p2 being Point of
TOP-REAL 2 st C is_an_arc_of p1,p2) or ex p being Point of TOP-REAL 2 st C = {p
}
proof
let D be Simple_closed_curve, C be non empty compact connected Subset of
TOP-REAL 2;
assume
A1: C c= D;
assume
A2: C <> D;
per cases;
suppose
C is trivial;
hence thesis by SUBSET_1:47;
end;
suppose
A3: C is non trivial;
C c< D by A1,A2,XBOOLE_0:def 8;
then consider p being Point of TOP-REAL 2 such that
A4: p in D and
A5: C c= D \ {p} by SUBSET_1:44;
consider d1,d2 being Point of TOP-REAL 2 such that
A6: d1 in C and
A7: d2 in C and
A8: d1 <> d2 by A3,SUBSET_1:45;
reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2 by A5;
(TOP-REAL 2) | Dp, I(01) are_homeomorphic by A4,Th49;
then consider f being Function of (TOP-REAL 2) | Dp, I(01) such that
A9: f is being_homeomorphism by T_0TOPSP:def 1;
reconsider C9 = C as Subset of (TOP-REAL 2) | Dp by A5,PRE_TOPC:8;
C c= [#] ((TOP-REAL 2) | Dp) by A5,PRE_TOPC:8;
then
A10: C9 is compact by COMPTS_1:2;
set fC = f.:C9;
A11: C9 is connected by CONNSP_1:23;
A12: rng f = [#] I(01) by A9,TOPS_2:def 5;
f is continuous by A9,TOPS_2:def 5;
then reconsider fC as compact connected Subset of I(01) by A10,A11,A12,
COMPTS_1:15,TOPS_2:61;
reconsider fC9 = fC as Subset of I[01] by PRE_TOPC:11;
A13: fC9 c= [#] I(01);
A14: for P being Subset of I(01) st P=fC9 holds P is compact;
d1 in D \ {p} by A6,A5;
then d1 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:8;
then
A15: d1 in dom f by FUNCT_2:def 1;
A16: f is one-to-one by A9,TOPS_2:def 5;
d2 in D \ {p} by A7,A5;
then d2 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:8;
then
A17: d2 in dom f by FUNCT_2:def 1;
A18: f.d2 in f.:C9 by A7,FUNCT_2:35;
then reconsider
fC9 as non empty compact connected Subset of I[01] by A13,A14,COMPTS_1:2
,CONNSP_1:23;
consider p1, p2 being Point of I[01] such that
A19: p1 <= p2 and
A20: fC9 = [. p1,p2 .] by Th28;
A21: f.d1 in f.:C9 by A6,FUNCT_2:35;
p1 <> p2
proof
assume p1 = p2;
then
A22: fC9 = {p1} by A20,XXREAL_1:17;
then
A23: f.d2 = p1 by A18,TARSKI:def 1;
f.d1 = p1 by A21,A22,TARSKI:def 1;
hence thesis by A8,A15,A17,A16,A23,FUNCT_1:def 4;
end;
then p1 < p2 by A19,XXREAL_0:1;
hence thesis by A5,A9,A20,Th52;
end;
end;
begin :: Addenda
theorem Th54:
for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex D being non empty closed_interval Subset of REAL
st C c= D & D c= ].0,1.[ &
lower_bound C = lower_bound D & upper_bound C = upper_bound D
proof
let C be non empty compact Subset of I[01];
assume
A1: C c= ].0,1.[;
reconsider C9 = C as Subset of REAL by BORSUK_1:40,XBOOLE_1:1;
reconsider D = [. lower_bound C9, upper_bound C9 .] as Subset of REAL;
A2: C9 is bounded_below bounded_above by Th22;
then
A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11;
A4: C c= D
proof
let x be object;
assume
A5: x in C;
then x in the carrier of I[01];
then reconsider x9 = x as Real;
A6: x9 <= upper_bound C9 by A5,Th23;
lower_bound C9 <= x9 by A5,Th23;
hence thesis by A6,XXREAL_1:1;
end;
A7: C9 is closed by Th24;
then
A8: lower_bound C9 in C9 by Th22,RCOMP_1:13;
A9: upper_bound C9 in C9 by A7,Th22,RCOMP_1:12;
then
A10: D is non empty compact connected Subset of I[01] by A2,A8,Th21,SEQ_4:11;
then
A11: D is non empty closed_interval Subset of REAL by Th27;
then
A12: D = [. lower_bound D, upper_bound D .] by INTEGRA1:4;
then
A13: upper_bound C9 = upper_bound D by A3,XXREAL_1:66;
A14: not 1 in D
proof
assume 1 in D;
then upper_bound D >= 1 by A11,INTEGRA2:1;
hence thesis by A1,A9,A13,XXREAL_1:4;
end;
A15: lower_bound C9 = lower_bound D by A3,A12,XXREAL_1:66;
A16: not 0 in D
proof
assume 0 in D;
then lower_bound D <= 0 by A11,INTEGRA2:1;
hence thesis by A1,A8,A15,XXREAL_1:4;
end;
A17: D c= ].0,1.[
by A10,A16,A14,BORSUK_1:40,XXREAL_1:5;
reconsider D as non empty closed_interval Subset of REAL
by A3,MEASURE5:14;
take D;
thus thesis by A4,A3,A12,A17,XXREAL_1:66;
end;
theorem Th55:
for C being non empty compact Subset of I[01] st C c= ].0,1.[
holds ex p1, p2 being Point of I[01] st p1 <= p2 & C c= [. p1, p2 .] & [.p1,p2
.] c= ]. 0, 1 .[
proof
let C be non empty compact Subset of I[01];
assume C c= ].0,1.[;
then consider D being non empty closed_interval Subset of REAL such that
A1: C c= D and
A2: D c= ].0,1.[ and
lower_bound C = lower_bound D and
upper_bound C = upper_bound D by Th54;
consider p1,p2 being Real such that
A3: p1 <= p2 and
A4: D = [.p1,p2.] by MEASURE5:14;
p1 in D by A3,A4,XXREAL_1:1;
then
A5: p1 in ].0,1.[ by A2;
p2 in D by A3,A4,XXREAL_1:1;
then
A6: p2 in ].0,1.[ by A2;
].0,1.[ c= [.0,1.] by XXREAL_1:25;
then reconsider p1, p2 as Point of I[01] by A5,A6,BORSUK_1:40;
take p1, p2;
thus p1 <= p2 by A3;
thus thesis by A1,A2,A4;
end;
theorem
for D being Simple_closed_curve, C being closed Subset of TOP-REAL 2
st C c< D ex p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2 st B
is_an_arc_of p1,p2 & C c= B & B c= D
proof
let D be Simple_closed_curve, C be closed Subset of TOP-REAL 2;
assume
A1: C c< D;
then
A2: C c= D by XBOOLE_0:def 8;
A3: for C being compact Subset of TOP-REAL 2 st C is non trivial & C c< D ex
p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2 st B is_an_arc_of
p1,p2 & C c= B & B c= D
proof
let C be compact Subset of TOP-REAL 2;
assume C is non trivial;
then consider d1,d2 being Point of TOP-REAL 2 such that
A4: d1 in C and
A5: d2 in C and
A6: d1 <> d2 by SUBSET_1:45;
assume C c< D;
then consider p being Point of TOP-REAL 2 such that
A7: p in D and
A8: C c= D \ {p} by A4,SUBSET_1:44;
reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2 by A4,A8;
(TOP-REAL 2) | Dp, I(01) are_homeomorphic by A7,Th49;
then consider f being Function of (TOP-REAL 2) | Dp, I(01) such that
A9: f is being_homeomorphism by T_0TOPSP:def 1;
d2 in D \ {p} by A5,A8;
then d2 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:8;
then
A10: d2 in dom f by FUNCT_2:def 1;
d1 in D \ {p} by A4,A8;
then d1 in the carrier of (TOP-REAL 2) | Dp by PRE_TOPC:8;
then
A11: d1 in dom f by FUNCT_2:def 1;
A12: f is one-to-one by A9,TOPS_2:def 5;
C c= the carrier of (TOP-REAL 2) | Dp by A8,PRE_TOPC:8;
then
A13: C c= dom f by FUNCT_2:def 1;
dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
then
A14: dom f c= the carrier of TOP-REAL 2 by BORSUK_1:1;
dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
then
A15: dom f = Dp by PRE_TOPC:8;
reconsider C9 = C as Subset of (TOP-REAL 2) | Dp by A8,PRE_TOPC:8;
C c= [#] ((TOP-REAL 2) | Dp) by A8,PRE_TOPC:8;
then
A16: C9 is compact by COMPTS_1:2;
set fC = f.:C9;
A17: rng f = [#] I(01) by A9,TOPS_2:def 5;
f is continuous by A9,TOPS_2:def 5;
then reconsider fC as compact Subset of I(01) by A16,A17,COMPTS_1:15;
reconsider fC9 = fC as Subset of I[01] by PRE_TOPC:11;
A18: fC9 c= [#] I(01);
A19: for P being Subset of I(01) st P=fC9 holds P is compact;
fC9 c= the carrier of I(01);
then
A20: fC9 c= ].0,1.[ by Def1;
A21: f.d2 in f.:C9 by A5,FUNCT_2:35;
then reconsider fC9 as non empty compact Subset of I[01] by A18,A19,
COMPTS_1:2;
consider p1, p2 being Point of I[01] such that
A22: p1 <= p2 and
A23: fC9 c= [. p1,p2 .] and
A24: [.p1,p2.] c= ].0,1.[ by A20,Th55;
reconsider E = [.p1,p2.] as non empty compact connected Subset of I[01] by
A22,Th21;
A25: f " E c= dom f by RELAT_1:132;
A26: f.d1 in f.:C9 by A4,FUNCT_2:35;
p1 <> p2
proof
assume p1 = p2;
then
A27: fC9 c= {p1} by A23,XXREAL_1:17;
then
A28: f.d2 = p1 by A21,TARSKI:def 1;
f.d1 = p1 by A26,A27,TARSKI:def 1;
hence thesis by A6,A11,A10,A12,A28,FUNCT_1:def 4;
end;
then
A29: p1 < p2 by A22,XXREAL_0:1;
E c= rng f by A17,A24,Def1;
then reconsider B = f " E as non empty Subset of TOP-REAL 2 by A25,A14,
RELAT_1:139,XBOOLE_1:1;
rng f = ].0,1.[ by A17,Def1;
then f.: (f"E) = E by A24,FUNCT_1:77;
then consider s1, s2 being Point of TOP-REAL 2 such that
A30: B is_an_arc_of s1,s2 by A9,A29,A15,Th52,RELAT_1:132;
take s1, s2, B;
thus B is_an_arc_of s1,s2 by A30;
Dp c= D by XBOOLE_1:36;
hence thesis by A23,A25,A15,A13,FUNCT_1:93;
end;
A31: C is compact by A2,RLTOPSP1:42,TOPREAL6:79;
per cases;
suppose
A32: C is trivial;
per cases;
suppose
A33: C = {};
consider p,q being Point of TOP-REAL 2 such that
A34: p <> q and
A35: p in D and
A36: q in D by TOPREAL2:4;
reconsider CC = {p,q} as Subset of TOP-REAL 2;
A37: q in CC by TARSKI:def 2;
p in CC by TARSKI:def 2;
then
A38: CC is non trivial by A34,A37;
reconsider pp = {p}, qq = {q} as Subset of TOP-REAL 2;
CC = pp \/ qq by ENUMSET1:1;
then
A39: CC is compact by COMPTS_1:10;
A40: CC <> D
proof
assume CC = D;
then D \ CC = {} by XBOOLE_1:37;
then not {}((TOP-REAL 2)|D) is connected by A34,A35,A36,JORDAN6:47;
hence thesis;
end;
CC c= D by A35,A36,ZFMISC_1:32;
then CC c< D by A40,XBOOLE_0:def 8;
then consider
p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2
such that
A41: B is_an_arc_of p1,p2 and
CC c= B and
A42: B c= D by A3,A38,A39;
take p1, p2, B;
thus B is_an_arc_of p1,p2 by A41;
thus C c= B by A33;
thus thesis by A42;
end;
suppose
C <> {};
then consider x being Element of TOP-REAL 2 such that
A43: C = {x} by A32,SUBSET_1:47;
consider y being Element of D such that
A44: x <> y by SUBSET_1:50;
reconsider y9 = y as Element of TOP-REAL 2;
reconsider Y = {y9} as compact non empty Subset of TOP-REAL 2;
reconsider Cy = C \/ Y as non empty compact Subset of TOP-REAL 2 by A31,
COMPTS_1:10;
A45: x in C by A43,TARSKI:def 1;
A46: Cy <> D
proof
assume Cy = D;
then
A47: D \ Cy = {} by XBOOLE_1:37;
Cy = {x,y} by A43,ENUMSET1:1;
then not {}((TOP-REAL 2)|D) is connected by A2,A45,A44,A47,JORDAN6:47;
hence thesis;
end;
{y} c= D;
then Cy c= D by A2,XBOOLE_1:8;
then
A48: Cy c< D by A46,XBOOLE_0:def 8;
A49: C c= Cy by XBOOLE_1:7;
y in Y by TARSKI:def 1;
then y in Cy by XBOOLE_0:def 3;
then Cy is non trivial by A45,A44,A49;
then consider
p1,p2 being Point of TOP-REAL 2, B being Subset of TOP-REAL 2
such that
A50: B is_an_arc_of p1,p2 and
A51: Cy c= B and
A52: B c= D by A3,A48;
take p1, p2, B;
thus B is_an_arc_of p1,p2 by A50;
thus C c= B by A49,A51;
thus thesis by A52;
end;
end;
suppose
C is non trivial;
hence thesis by A1,A31,A3;
end;
end;