Copyright (c) 2002 Association of Mizar Users
environ
vocabulary BOOLE, TOPREAL1, EUCLID, ARYTM_1, PRE_TOPC, COMPTS_1, SEQ_1,
TOPREAL2, RELAT_2, BORSUK_1, SUBSET_1, RCOMP_1, TOPS_2, TOPMETR,
CONNSP_1, ARYTM_3, SQUARE_1, RELAT_1, ORDINAL2, LATTICES, T_0TOPSP,
SEQ_2, INTEGRA1, REALSET1, FUNCT_1, BORSUK_4, PARTFUN1, TREAL_1, FUNCT_4,
ARYTM, JORDAN1;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, REALSET1, FUNCT_2,
STRUCT_0, PRE_TOPC, COMPTS_1, FUNCT_4, RCOMP_1, EUCLID, TOPREAL1,
TOPREAL2, SEQ_4, T_0TOPSP, TREAL_1, CONNSP_1, BORSUK_1, BORSUK_3, TSEP_1,
RCOMP_2, JORDAN1, TOPMETR, PSCOMP_1, INTEGRA1, TOPS_2;
constructors REALSET1, JORDAN2C, TOPS_2, TOPREAL2, TOPREAL1, CONNSP_1,
RCOMP_2, PSCOMP_1, INTEGRA1, TMAP_1, BORSUK_3, COMPTS_1, YELLOW_8,
PARTFUN1, LIMFUNC1, SPPOL_1, TOPGRP_1, TREAL_1, DOMAIN_1, XCMPLX_0,
MEMBERED, JORDAN1;
clusters XREAL_0, RELSET_1, REVROT_1, TOPREAL6, STRUCT_0, PRE_TOPC, BORSUK_2,
REALSET1, INTEGRA1, TEX_1, TEX_2, JORDAN1B, YELLOW13, EUCLID, MEMBERED,
ZFMISC_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, TARSKI, CONNSP_1, PARTFUN1, JORDAN1;
theorems TOPS_2, T_0TOPSP, BORSUK_1, RCOMP_2, PRE_TOPC, COMPTS_1, TARSKI,
TOPREAL5, TOPMETR, TOPREAL1, RCOMP_1, SPPOL_1, CONNSP_1, ZFMISC_1,
JORDAN5A, AXIOMS, XREAL_0, STRUCT_0, SQUARE_1, REAL_1, TOPREAL6,
PSCOMP_1, TREAL_1, XBOOLE_0, XBOOLE_1, JORDAN6, JORDAN1, SEQ_4, JGRAPH_5,
INTEGRA1, INTEGRA2, TSEP_1, TOPREAL2, JORDAN5B, REALSET1, FUNCT_2,
FUNCT_1, GOBOARD9, RELAT_1, PARTFUN1, RFUNCT_2, BORSUK_3, FUNCT_4,
TOPS_1, JGRAPH_2, CIRCCMB2, TOPMETR2, TEX_2, SUBSET_1, XCMPLX_1;
begin :: Preliminaries
definition
cluster -> non trivial Simple_closed_curve;
coherence
proof
let D be Simple_closed_curve;
consider p1,p2 being Point of TOP-REAL 2 such that
A1: p1 <> p2 & p1 in D & p2 in D by TOPREAL2:5;
thus thesis by A1,SPPOL_1:3;
end;
end;
definition let T be non empty TopSpace;
cluster non empty compact connected Subset of T;
existence
proof
consider t being Element of T;
reconsider E = {t} as Subset of T;
take E;
thus thesis by CONNSP_1:29;
end;
end;
definition
cluster -> real Element of I[01];
coherence
proof
let a be Element of I[01];
a in [. 0, 1 .] by BORSUK_1:83;
hence thesis by XREAL_0:def 1;
end;
end;
theorem Th1:
for X being non empty set,
A, B being non empty Subset of X st A c< B holds
ex p being Element of X st p in B & A c= B \ {p}
proof
let X be non empty set,
A, B be non empty Subset of X;
assume
A1: A c< B;
then B \ A <> {} by XBOOLE_1:105;
then consider p being set such that
A2: p in B \ A by XBOOLE_0:def 1;
A3: p in B & not p in A by A2,XBOOLE_0:def 4;
reconsider p as Element of X by A2;
take p;
A c= B by A1,XBOOLE_0:def 8;
hence thesis by A3,ZFMISC_1:40;
end;
theorem Th2:
for X being non empty set,
A being non empty Subset of X holds
A is trivial iff ex x being Element of X st A = {x}
proof
let X be non empty set,
A be non empty Subset of X;
hereby assume A is trivial;
then consider s being Element of A such that
A1: A = {s} by TEX_2:def 1;
thus ex x being Element of X st A = {x} by A1;
end;
given x being Element of X such that
A2: A = {x};
thus thesis by A2;
end;
definition let T be non trivial 1-sorted;
cluster non trivial Subset of T;
existence
proof
consider x, y being Element of T such that
A1: x <> y by REALSET1:def 20;
take X = {x, y};
x in X & y in X by TARSKI:def 2;
hence thesis by A1,SPPOL_1:4;
end;
end;
theorem
for X being non trivial set,
p being set
ex q being Element of X st q <> p
proof
let X be non trivial set,
p be set;
X \ { p } is non empty by REALSET1:32;
then consider q being set such that
A1: q in X \ { p } by XBOOLE_0:def 1;
reconsider q as Element of X by A1,XBOOLE_0:def 4;
take q;
thus thesis by A1,ZFMISC_1:64;
end;
definition let X be non trivial set;
cluster non trivial Subset of X;
existence
proof
take [#]X;
thus thesis by SUBSET_1:def 4;
end;
end;
theorem Th4:
for T being non trivial set,
X being non trivial Subset of T,
p being set
ex q being Element of T st q in X & q <> p
proof
let T be non trivial set,
X be non trivial Subset of T,
p be set;
set p' = p;
X \ { p' } is non empty by REALSET1:32;
then consider q being set such that
A1: q in X \ { p' } by XBOOLE_0:def 1;
q in X by A1,XBOOLE_0:def 4;
then reconsider q as Element of T;
take q;
thus thesis by A1,ZFMISC_1:64;
end;
theorem Th5:
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
let x1,x2 be set;
assume
A5: x1 in dom g & x2 in dom f \ dom g;
then A6: g.x1 in rng g by FUNCT_1:12;
A7: dom f \ dom g c= dom f by XBOOLE_1:36;
then A8: f.x2 in rng f by A5,FUNCT_1:12;
{ a } c= dom f & { a } c= dom g by A3,XBOOLE_1:17;
then A9: a in dom f & a in dom g by ZFMISC_1:37;
assume g.x1 = f.x2;
then f.x2 in rng f /\ rng g by A6,A8,XBOOLE_0:def 3;
then f.x2 = f.a by A4,TARSKI:def 1;
then x2 = a by A1,A5,A7,A9,FUNCT_1:def 8;
then dom g meets (dom f \ dom g) by A5,A9,XBOOLE_0:3;
hence thesis by XBOOLE_1:79;
end;
hence thesis by A1,A2,TOPMETR2:2;
end;
theorem Th6:
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;
set gf = f" +* g", F = f +* g;
for x being set st x in dom f /\ dom g holds f.x = g.x
proof
let x be set;
assume x in dom f /\ dom g;
then x = a by A3,TARSKI:def 1;
hence thesis by A5;
end;
then A6: f tolerates g by PARTFUN1:def 6;
A7: dom (f") = rng f & dom (g") = rng g by A1,A2,FUNCT_1:55;
for x being set st x in dom (f") /\ dom (g") holds f".x = g".x
proof
let x be set;
assume A8: x in dom (f") /\ dom (g");
{ a } c= dom f by A3,XBOOLE_1:17;
then A9: a in dom f by ZFMISC_1:37;
{ a } c= dom g by A3,XBOOLE_1:17;
then A10: a in dom g by ZFMISC_1:37;
x = f.a by A4,A7,A8,TARSKI:def 1;
then A11: a = f".x by A1,A9,FUNCT_1:54;
x = g.a by A4,A5,A7,A8,TARSKI:def 1;
hence thesis by A2,A10,A11,FUNCT_1:54;
end;
then A12: f" tolerates g" by PARTFUN1:def 6;
A13: F is one-to-one by A1,A2,A3,A4,Th5;
A14: rng F = (rng f) \/ (rng g) by A6,CIRCCMB2:5;
dom gf = (dom (f")) \/ (dom (g")) by FUNCT_4:def 1
.= (rng f) \/ (dom (g")) by A1,FUNCT_1:55
.= (rng f) \/ (rng g) by A2,FUNCT_1:55;
then A15: dom gf = rng F by A6,CIRCCMB2:5;
A16: dom F = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A17: dom f c= dom F by XBOOLE_1:7;
A18: dom g c= dom F by A16,XBOOLE_1:7;
for y,x being set holds
y in rng F & x = gf.y iff x in dom F & y = F.x
proof
let y,x be set;
hereby assume
A19: y in rng F & x = gf.y;
per cases by A15,A19,FUNCT_4:13;
suppose
A20: y in dom (f");
then A21: y in rng f by A1,FUNCT_1:55;
x = f".y by A12,A19,A20,FUNCT_4:16;
then x in dom f & y = f.x by A1,A21,FUNCT_1:54;
hence x in dom F & y = F.x by A6,A17,FUNCT_4:16;
suppose
A22: y in dom (g");
then A23: y in rng g by A2,FUNCT_1:55;
x = g".y by A19,A22,FUNCT_4:14;
then x in dom g & y = g.x by A2,A23,FUNCT_1:54;
hence x in dom F & y = F.x by A18,FUNCT_4:14;
end;
assume
A24: x in dom F & y = F.x;
per cases by A24,FUNCT_4:13;
suppose
A25: x in dom f;
then A26: y = f.x by A6,A24,FUNCT_4:16;
then A27: x = f".y by A1,A25,FUNCT_1:54;
A28: y in rng f by A25,A26,FUNCT_1:12;
rng F = (rng f) \/ (rng g) by A6,CIRCCMB2:5;
then A29: rng f c= rng F by XBOOLE_1:7;
y in dom (f") by A1,A28,FUNCT_1:55;
hence thesis by A12,A27,A28,A29,FUNCT_4:16;
suppose
A30: x in dom g;
then A31: y = g.x by A24,FUNCT_4:14;
then A32: x = g".y by A2,A30,FUNCT_1:54;
A33: y in rng g by A30,A31,FUNCT_1:12;
A34: rng g c= rng F by A14,XBOOLE_1:7;
y in dom (g") by A2,A33,FUNCT_1:55;
hence thesis by A32,A33,A34,FUNCT_4:14;
end;
hence thesis by A13,A15,FUNCT_1:54;
end;
theorem Th7:
for n being Nat,
A being non empty 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 Nat,
A be non empty 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:56;
{ p } c= { p, q } by ZFMISC_1:12;
then A \ { p, q } c= A \ {p} by XBOOLE_1:34;
hence thesis by A1,XBOOLE_1:3;
end;
theorem
for n being Nat,
a,b being Point of TOP-REAL n holds LSeg (a,b) is convex
proof
let n be Nat;
let a,b be Point of TOP-REAL n;
set A = LSeg(a,b);
let w1,w2 be Point of TOP-REAL n;
assume w1 in A & w2 in A;
hence thesis by TOPREAL1:12;
end;
theorem
for s1, s3, s4, l being real number st
s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 holds s1 <= (1-l) * s3+l*s4
proof
let s1, s3, s4, l be real number;
assume A1:s1 <= s3 & s1 < s4 & 0 <= l & l <= 1;
now per cases;
suppose l=0;
hence thesis by A1;
suppose l=1;
hence thesis by A1;
suppose A2: not(l=0 or l=1);
then A3: l>0 & l<1 by A1,REAL_1:def 5;
A4: l*s1<l*s4 by A1,A2,REAL_1:70;
1-l>0 by A3,SQUARE_1:11;
then A5: (1-l)*s1<=(1-l)*s3 by A1,AXIOMS:25;
(1-l)*s1+l*s1=(1-l+l)*s1 by XCMPLX_1:8
.=1 * s1 by XCMPLX_1:27
.=s1;
hence thesis by A4,A5,REAL_1:67;
end;
hence thesis;
end;
theorem Th10:
for x being set, a, b being real number st a <= b &
x in [. a, b .] holds x in ]. a, b .[ or x = a or x = b
proof
let x be set, a,b be real number;
assume a <= b & x in [. a, b .];
then x in ]. a, b .[ \/ {a,b} by RCOMP_1:11;
then x in ]. a, b .[ or x in {a,b} by XBOOLE_0:def 2;
hence x in ]. a, b .[ or x = a or x = b by TARSKI:def 2;
end;
theorem Th11:
for a, b, c, d being real number st
].a,b.[ meets [.c,d.] holds b > c
proof
let a, b, c, d be real number;
assume A1: ].a,b.[ meets [.c,d.];
assume A2: b <= c;
consider x being set such that
A3: x in ].a,b.[ & x in [.c,d.] by A1,XBOOLE_0:3;
x in {r where r is Real: a <r & r< b} by A3,RCOMP_1:def 2;
then consider x' being Real such that
A4: x' = x & a < x' & x' < b;
x in {r where r is Real: c <= r & r <= d} by A3,RCOMP_1:def 1;
then consider y' being Real such that
A5: y' = x & c <= y' & y' <= d;
thus thesis by A2,A4,A5,AXIOMS:22;
end;
theorem Th12:
for a, b, c, d being real number st
b <= c holds [. a, b .] misses ]. c, d .[
proof
let a, b, c, d be real number;
assume A1: b <= c;
assume [.a,b.] meets ].c,d.[;
then consider x being set such that
A2: x in [.a,b.] & x in ].c,d.[ by XBOOLE_0:3;
x in {r where r is Real: a<=r & r<=b} by A2,RCOMP_1:def 1;
then consider x' being Real such that
A3: x' = x & a <= x' & x' <= b;
x in {r where r is Real: c < r & r<d} by A2,RCOMP_1:def 2;
then consider y' being Real such that
A4: y' = x & c < y' & y' < d;
thus thesis by A1,A3,A4,AXIOMS:22;
end;
theorem Th13:
for a, b, c, d being real number st
b <= c holds ]. a, b .[ misses [. c, d .]
proof
let a, b, c, d be real number;
assume A1: b <= c;
assume ]. a, b .[ meets [. c, d .];
then consider x being set such that
A2: x in ]. a, b .[ & x in [. c, d .] by XBOOLE_0:3;
x in {r where r is Real: a<r & r<b} by A2,RCOMP_1:def 2;
then consider x' being Real such that
A3: x' = x & a < x' & x' < b;
x in {r where r is Real: c <= r & r <= d} by A2,RCOMP_1:def 1;
then consider y' being Real such that
A4: y' = x & c <= y' & y' <= d;
thus thesis by A1,A3,A4,AXIOMS:22;
end;
theorem
for a, b, c, d being real number st a < b &
[.a,b.] c= [.c,d.] holds c <= a & b <= d
proof
let a, b, c, d be real number;
assume A1: a < b;
assume A2: [.a,b.] c= [.c,d.];
A3: a in [.a,b.] by A1,RCOMP_1:15;
b in [.a,b.] by A1,RCOMP_1:15;
hence thesis by A2,A3,TOPREAL5:1;
end;
theorem Th15:
for a, b, c, d being real number st a < b &
].a,b.[ c= [.c,d.] holds c <= a & b <= d
proof
let a, b, c, d be real number;
assume A1: a < b & ].a,b.[ c= [.c,d.];
then ].a,b.[ <> {} by RCOMP_1:15;
then A2: ].a,b.[ meets [.c,d.] by A1,XBOOLE_1:69;
assume A3: c > a or b > d;
per cases by A3;
suppose a < c;
then consider ac be real number such that
A4: a < ac & ac < c by REAL_1:75;
b > c by A2,Th11;
then ac < b by A4,AXIOMS:22;
then ac in ].a,b.[ by A4,JORDAN6:45;
hence thesis by A1,A4,TOPREAL5:1;
suppose A5: d < b;
set ad = max (a,d);
ad < b by A1,A5,RCOMP_2:2;
then consider ac be real number such that
A6: ad < ac & ac < b by REAL_1:75;
A7: a <= ad & d <= ad by SQUARE_1:46;
then A8: d < ac by A6,AXIOMS:22;
a < ac by A6,A7,AXIOMS:22;
then ac in ].a,b.[ by A6,JORDAN6:45;
hence thesis by A1,A8,TOPREAL5:1;
end;
theorem
for a, b, c, d being real number st a < b &
].a,b.[ c= [.c,d.] holds [.a,b.] c= [.c,d.]
proof
let a, b, c, d be real number;
assume A1: a < b;
then A2: ].a,b.[ <> {} by RCOMP_1:15;
assume A3: ].a,b.[ c= [.c,d.];
then A4: ].a,b.[ meets [.c,d.] by A2,XBOOLE_1:69;
thus [.a,b.] c= [.c,d.]
proof
let x be set;
assume A5: x in [.a,b.];
per cases by A1,A5,Th10;
suppose A6: x = a;
now per cases;
suppose A7: not a in [.c,d.];
now per cases by A7,TOPREAL5:1;
suppose a < c;
then consider ac be real number such that
A8: a < ac & ac < c by REAL_1:75;
b > c by A4,Th11;
then ac < b by A8,AXIOMS:22;
then ac in ].a,b.[ by A8,JORDAN6:45;
hence thesis by A3,A8,TOPREAL5:1;
suppose d < a;
hence thesis by A4,Th12;
end;
hence thesis;
suppose a in [.c,d.];
hence thesis by A6;
end;
hence thesis;
suppose A9: x = b;
now per cases;
suppose A10: not b in [.c,d.];
now per cases by A10,TOPREAL5:1;
suppose b < c;
then consider ac be real number such that
A11: b < ac & ac < c by REAL_1:75;
b > c by A4,Th11;
hence thesis by A11,AXIOMS:22;
suppose d < b;
hence thesis by A1,A3,Th15;
end;
hence thesis;
suppose b in [.c,d.];
hence thesis by A9;
end;
hence thesis;
suppose x in ].a,b.[;
hence thesis by A3;
end;
end;
theorem Th17:
for A being Subset of I[01],
a, b being real number 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 number;
assume A1: a < b;
assume A2: A = ].a,b.[;
then A3: 0 <= a by A1,Th15,BORSUK_1:83;
b <= 1 by A1,A2,Th15,BORSUK_1:83;
hence thesis by A3,BORSUK_1:83,TREAL_1:1;
end;
theorem Th18:
for A being Subset of I[01],
a, b being real number 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 number;
assume A1: a < b;
A2: ].a,b.[ c= ]. a,b .] by RCOMP_2:17;
assume A = ].a,b.];
then A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:83,XBOOLE_1:1;
then A4: 0 <= a by A1,Th15;
b <= 1 by A1,A3,Th15;
hence thesis by A4,BORSUK_1:83,TREAL_1:1;
end;
theorem Th19:
for A being Subset of I[01],
a, b being real number 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 number;
assume A1: a < b;
A2: ].a,b.[ c= [. a,b .[ by RCOMP_2:17;
assume A = [.a,b.[;
then A3: ].a,b.[ c= [. 0,1 .] by A2,BORSUK_1:83,XBOOLE_1:1;
then A4: 0 <= a by A1,Th15;
b <= 1 by A1,A3,Th15;
hence thesis by A4,BORSUK_1:83,TREAL_1:1;
end;
theorem Th20:
for a, b being real number st a <> b holds Cl ].a,b.] = [.a,b.]
proof
let a, b be real number;
assume A1: a <> b;
A2: ].a,b.] c= [.a,b.] by RCOMP_2:17;
[.a,b.] is closed by RCOMP_1:23;
then A3: Cl ].a,b.] c= [.a,b.] by A2,PSCOMP_1:32;
].a,b.[ c= ].a,b.] by RCOMP_2:17;
then Cl ].a,b.[ c= Cl ].a,b.] by PSCOMP_1:37;
then [.a,b.] c= Cl ].a,b.] by A1,TOPREAL6:82;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th21:
for a, b being real number st a <> b holds Cl [.a,b.[ = [.a,b.]
proof
let a, b be real number;
assume A1: a <> b;
A2: [.a,b.[ c= [.a,b.] by RCOMP_2:17;
[.a,b.] is closed by RCOMP_1:23;
then A3: Cl [.a,b.[ c= [.a,b.] by A2,PSCOMP_1:32;
].a,b.[ c= [.a,b.[ by RCOMP_2:17;
then Cl ].a,b.[ c= Cl [.a,b.[ by PSCOMP_1:37;
then [.a,b.] c= Cl [.a,b.[ by A1,TOPREAL6:82;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
for A being Subset of I[01],
a, b being real number st a < b & A = ].a,b.[ holds
Cl A = [.a,b.]
proof
let A be Subset of I[01],
a, b be real number;
assume A1: a < b & A = ].a,b.[;
then A2: Cl ].a,b.[ = [.a,b.] by TOPREAL6:82;
reconsider A1 = ].a,b.[ as Subset of R^1 by TOPMETR:24;
[.a,b.] c= the carrier of I[01] by A1,Th17;
then A3: [.a,b.] c= [#]I[01] by PRE_TOPC:12;
Cl A = (Cl A1) /\ [#]I[01] by A1,PRE_TOPC:47
.= [.a,b.] /\ [#]I[01] by A2,TOPREAL6:80
.= [.a,b.] by A3,XBOOLE_1:28;
hence thesis;
end;
theorem Th23:
for A being Subset of I[01],
a, b being real number st a < b & A = ].a,b.] holds
Cl A = [.a,b.]
proof
let A be Subset of I[01],
a, b be real number;
assume A1: a < b & A = ].a,b.];
then A2: Cl ].a,b.] = [.a,b.] by Th20;
reconsider A1 = ].a,b.] as Subset of R^1 by TOPMETR:24;
[.a,b.] c= the carrier of I[01] by A1,Th18;
then A3: [.a,b.] c= [#]I[01] by PRE_TOPC:12;
Cl A = (Cl A1) /\ [#]I[01] by A1,PRE_TOPC:47
.= [.a,b.] /\ [#]I[01] by A2,TOPREAL6:80
.= [.a,b.] by A3,XBOOLE_1:28;
hence thesis;
end;
theorem Th24:
for A being Subset of I[01],
a, b being real number st a < b & A = [.a,b.[ holds
Cl A = [.a,b.]
proof
let A be Subset of I[01],
a, b be real number;
assume A1: a < b & A = [.a,b.[;
then A2: Cl [.a,b.[ = [.a,b.] by Th21;
reconsider A1 = [.a,b.[ as Subset of R^1 by TOPMETR:24;
[.a,b.] c= the carrier of I[01] by A1,Th19;
then A3: [.a,b.] c= [#]I[01] by PRE_TOPC:12;
Cl A = (Cl A1) /\ [#]I[01] by A1,PRE_TOPC:47
.= [.a,b.] /\ [#]I[01] by A2,TOPREAL6:80
.= [.a,b.] by A3,XBOOLE_1:28;
hence thesis;
end;
theorem
for a,b being real number st a < b holds
[.a,b.] <> ].a,b.]
proof
let a,b be real number;
assume A1: a < b;
not a in ].a,b.] by RCOMP_2:4;
hence thesis by A1,TOPREAL5:1;
end;
theorem Th26:
for a, b being real number holds
[.a,b.[ misses {b} & ].a,b.] misses {a}
proof
let a, b be real number;
not b in [.a,b.[ by RCOMP_2:3;
hence [.a,b.[ misses {b} by ZFMISC_1:56;
not a in ].a,b.] by RCOMP_2:4;
hence thesis by ZFMISC_1:56;
end;
Lm1:
for a, b being real number holds
].a,b.[ misses {b} & ].a,b.[ misses {a}
proof
let a, b be real number;
not b in ].a,b.[ by JORDAN6:45;
hence ].a,b.[ misses {b} by ZFMISC_1:56;
not a in ].a,b.[ by JORDAN6:45;
hence thesis by ZFMISC_1:56;
end;
theorem Th27:
for a, b being real number st a <= b holds
[. a, b .] \ { a } = ]. a, b .]
proof
let a, b be real number;
A1: ].a,b.] misses { a } by Th26;
assume a <= b;
then [.a,a.] \/ ].a,b.] = [.a,b.] by RCOMP_2:20;
then { a } \/ ].a,b.] = [.a,b.] by RCOMP_1:14;
then ].a,b.] \ { a } = [.a,b.] \ { a } by XBOOLE_1:40;
hence thesis by A1,XBOOLE_1:83;
end;
theorem Th28:
for a, b being real number st a <= b holds
[. a, b .] \ { b } = [. a, b .[
proof
let a, b be real number;
A1: [.a,b.[ misses { b } by Th26;
assume a <= b;
then [.b,b.] \/ [.a,b.[ = [.a,b.] by RCOMP_2:21;
then { b } \/ [.a,b.[ = [.a,b.] by RCOMP_1:14;
then [.a,b.[ \ { b } = [.a,b.] \ { b } by XBOOLE_1:40;
hence thesis by A1,XBOOLE_1:83;
end;
theorem Th29:
for a, b, c being real number st a < b & b < c holds
]. a, b .] /\ [. b, c .[ = { b }
proof
let a, b, c be real number;
assume
A1: a < b & b < c;
then b in [. b, c .[ by RCOMP_2:3;
then A2: { b } c= [. b, c .[ by ZFMISC_1:37;
A3: [. b, c .[ c= [. b, c .] by RCOMP_2:17;
]. a, b .[ misses [. b, c .] by Th13;
then A4: ]. a, b .[ misses [. b, c .[ by A3,XBOOLE_1:63;
]. a, b .] = ]. a, b .[ \/ { b } by A1,RCOMP_2:6;
then ]. a, b .] /\ [. b, c .[ = { b } /\ [. b, c .[ by A4,XBOOLE_1:78
.= { b } by A2,XBOOLE_1:28;
hence thesis;
end;
theorem Th30:
for a, b, c being real number holds
[. a, b .[ misses [. b, c .] & [. a, b .] misses ]. b, c .]
proof
let a, b, c be real number;
thus [.a,b.[ misses [.b,c.]
proof
assume [.a,b.[ meets [.b,c.];
then consider x being set such that
A1: x in [.a,b.[ & x in [.b,c.] by XBOOLE_0:3;
reconsider x' = x as Real by A1;
x' < b & x' >= b by A1,RCOMP_2:3,TOPREAL5:1;
hence thesis;
end;
thus [.a,b.] misses ].b,c.]
proof
assume [.a,b.] meets ].b,c.];
then consider x being set such that
A2: x in [.a,b.] & x in ].b,c.] by XBOOLE_0:3;
reconsider x' = x as Real by A2;
x' <= b & x' > b by A2,RCOMP_2:4,TOPREAL5:1;
hence thesis;
end;
end;
theorem Th31:
for a, b, c being real number st a <= b & b <= c holds
[.a,c.] \ {b} = [.a,b.[ \/ ].b,c.]
proof
let a, b, c be real number;
assume a <= b & b <= c;
then [.a,c.] = [.a,b.[ \/ [.b,b.] \/ ].b,c.] by RCOMP_2:13;
then A1: [.a,c.] = [.a,b.[ \/ {b} \/ ].b,c.] by RCOMP_1:14;
[.a,b.[ misses {b} & ].b,c.] misses {b} by Th26;
then A2: [.a,b.[ \/ ].b,c.] misses {b} by XBOOLE_1:70;
[.a,c.] \ {b} = [.a,b.[ \/ ].b,c.] \/ {b} \ {b} by A1,XBOOLE_1:4;
hence thesis by A2,XBOOLE_1:88;
end;
theorem Th32:
for A being Subset of I[01],
a, b being real number st a <= b & A = [.a,b.] holds
0 <= a & b <= 1
proof
let A be Subset of I[01],
a, b be real number;
assume a <= b & A = [.a,b.];
then a in A & b in A by RCOMP_1:15;
hence thesis by JORDAN5A:2;
end;
theorem Th33:
for A, B being Subset of I[01],
a, b, c being real number 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 number;
assume A1: a < b & b < c & A = [.a,b.[ & B = ].b,c.];
then Cl A = [.a,b.] by Th24;
hence Cl A misses B by A1,Th30;
Cl B = [.b,c.] by A1,Th23;
hence A misses Cl B by A1,Th30;
end;
theorem Th34:
for a, b being real number st a <= b holds
[. a, b .] = [. a, b .[ \/ { b }
proof
let a, b be real number;
assume
A1: a <= b;
[. a, b .[ \/ { b } = [. a, b .[ \/ [. b, b .] by RCOMP_1:14
.= [. a, b .] by A1,RCOMP_2:21;
hence thesis;
end;
theorem Th35:
for a, b being real number st a <= b holds
[. a, b .] = { a } \/ ]. a, b .]
proof
let a, b be real number;
assume
A1: a <= b;
{ a } \/ ]. a, b .] = [. a, a .] \/ ]. a, b .] by RCOMP_1:14
.= [. a, b .] by A1,RCOMP_2:20;
hence thesis;
end;
theorem Th36:
for a, b, c, d being real number st a <= b & b < c & c <= d holds
[. a, d .] = [. a, b .] \/ ]. b, c .[ \/ [. c, d .]
proof
let a, b, c, d be real number;
assume
A1: a <= b & b < c & c <= d;
then a <= c & b <= d by AXIOMS:22;
then [. a, d .] = [. a, b .[ \/ [. b, c .] \/ ]. c, d .] by A1,RCOMP_2:13
.= [. a, b .[ \/ ({ b } \/ ]. b, c .]) \/ ]. c, d .] by A1,Th35
.= [. a, b .[ \/ { b } \/ ]. b, c .] \/ ]. c, d .] by XBOOLE_1:4
.= [. a, b .] \/ ]. b, c .] \/ ]. c, d .] by A1,Th34
.= [. a, b .] \/ (]. b, c .[ \/ { c }) \/ ]. c, d .] by A1,RCOMP_2:6
.= [. a, b .] \/ ]. b, c .[ \/ { c } \/ ]. c, d .] by XBOOLE_1:4
.= [. a, b .] \/ ]. b, c .[ \/ ({ c } \/ ]. c, d .]) by XBOOLE_1:4
.= [. a, b .] \/ ]. b, c .[ \/ [. c, d .] by A1,Th35;
hence thesis;
end;
theorem Th37:
for a, b, c, d being real number st a <= b & b < c & c <= d holds
[. a, d .] \ ([. a, b .] \/ [. c, d .]) = ]. b, c .[
proof
let a, b, c, d be real number;
set A = [. a, b .], B = ]. b, c .[, C = [. c, d .], D = [. a, d .];
assume
A1: a <= b & b < c & c <= d;
A2: B misses A by Th12;
B misses C by Th13;
then A3: B misses A \/ C by A2,XBOOLE_1:70;
D \ (A \/ C) = (B \/ A \/ C) \ (A \/ C) by A1,Th36
.= (B \/ (A \/ C)) \ (A \/ C) by XBOOLE_1:4
.= B by A3,XBOOLE_1:88;
hence thesis;
end;
theorem Th38:
for a, b, c being real number st a < b & b < c holds
]. a, b .] \/ ]. b, c .[ = ]. a, c .[
proof
let a, b, c be real number;
assume
A1: a < b & b < c;
then A2: a < c by AXIOMS:22;
A3: ]. a, c .[ misses { c } by Lm1;
not c in ]. a, b .] by A1,RCOMP_2:4;
then A4: ]. a, b .] misses { c } by ZFMISC_1:56;
]. b, c .[ misses { c } by Lm1;
then A5: ]. a, b .] \/ ]. b, c .[ misses { c } by A4,XBOOLE_1:70;
]. a, b .] \/ ]. b, c .] = ]. a, c .] by A1,RCOMP_2:12;
then ]. a, b .] \/ (]. b, c .[ \/ { c }) = ]. a, c .]
by A1,RCOMP_2:6;
then ]. a, b .] \/ (]. b, c .[ \/ { c }) = ]. a, c .[ \/ { c }
by A2,RCOMP_2:6;
then ]. a, b .] \/ ]. b, c .[ \/ { c } = ]. a, c .[ \/ { c }
by XBOOLE_1:4;
then ]. a, b .] \/ ]. b, c .[ = ]. a, c .[ \/ { c } \ { c }
by A5,XBOOLE_1:88;
hence thesis by A3,XBOOLE_1:88;
end;
theorem Th39:
for a, b, c being real number st a < b & b < c holds
[. b, c .[ c= ]. a, c .[
proof
let a, b, c be real number;
assume
A1: a < b & b < c;
let x be set;
assume
A2: x in [. b, c .[;
then reconsider r = x as real number by XREAL_0:def 1;
A3: b <= r & r < c by A2,RCOMP_2:3;
then a < r by A1,AXIOMS:22;
hence thesis by A3,JORDAN6:45;
end;
theorem Th40:
for a, b, c being real number st a < b & b < c holds
]. a, b .] \/ [. b, c .[ = ]. a, c .[
proof
let a, b, c be real number;
assume
A1: a < b & b < c;
then ]. a, b .] \/ ]. b, c .[ = ]. a, c .[ by Th38;
then A2: ]. a, b .] c= ]. a, c .[ by XBOOLE_1:7;
[. b, c .[ c= ]. a, c .[ by A1,Th39;
hence ]. a, b .] \/ [. b, c .[ c= ]. a, c .[ by A2,XBOOLE_1:8;
thus ]. a, c .[ c= ]. a, b .] \/ [. b, c .[
proof
let x be set; assume A3: x in ]. a, c .[;
then reconsider r = x as real number by XREAL_0:def 1;
A4: a < r & r < c by A3,JORDAN6:45;
now per cases;
suppose r <= b;
then r in ]. a, b .] by A4,RCOMP_2:4;
hence thesis by XBOOLE_0:def 2;
suppose r > b;
then r in [. b, c .[ by A4,RCOMP_2:3;
hence thesis by XBOOLE_0:def 2;
end;
hence thesis;
end;
end;
theorem Th41:
for a, b, c being real number st a < b & b < c holds
]. a, c .[ \ ]. a, b .] = ]. b, c .[
proof
let a, b, c be real number;
assume
A1: a < b & b < c;
A2: ]. a, b .] c= [. a, b .] by RCOMP_2:17;
]. b, c .[ misses [. a, b .] by Th12;
then A3: ]. b, c .[ misses ]. a, b .] by A2,XBOOLE_1:63;
]. a, b .] \/ ]. b, c .[ \ ]. a, b .] = ]. a, c .[ \ ]. a, b .]
by A1,Th38;
then ]. b, c .[ \ ]. a, b .] = ]. a, c .[ \ ]. a, b .] by XBOOLE_1:40;
hence thesis by A3,XBOOLE_1:83;
end;
theorem Th42:
for a, b, c being real number st a < b & b < c holds
]. a, c .[ \ [. b, c .[ = ]. a, b .[
proof
let a, b, c be real number;
assume
A1: a < b & b < c;
then A2: ]. a, c .[ = ]. a, b .] \/ ]. b, c .[ by Th38
.= ]. a, b .[ \/ { b } \/ ]. b, c .[ by A1,RCOMP_2:6
.= ]. a, b .[ \/ ({ b } \/ ]. b, c .[) by XBOOLE_1:4
.= ]. a, b .[ \/ [. b, c .[ by A1,RCOMP_2:5;
A3: [. b, c .[ c= [. b, c .] by RCOMP_2:17;
]. a, b .[ misses [. b, c .] by Th13;
then ]. a, b .[ misses [. b, c .[ by A3,XBOOLE_1:63;
hence thesis by A2,XBOOLE_1:88;
end;
theorem Th43:
for p1, p2 being Point of I[01] holds
[. p1, p2 .] is Subset of I[01] by BORSUK_1:83,RCOMP_1:16;
theorem Th44:
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 .[ c= [. a,b .] by RCOMP_1:15;
[. a,b .] is Subset of I[01] by Th43;
then ]. a,b .[ c= the carrier of I[01] by A1,XBOOLE_1:1;
hence thesis;
end;
begin :: Decompositions of Intervals
theorem
for p being real number holds
{p} is closed-interval Subset of REAL
proof
let p be real number;
A1: p is Real by XREAL_0:def 1;
{p} = [.p,p.] by RCOMP_1:14;
hence thesis by A1,INTEGRA1:def 1;
end;
theorem Th46:
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 A1: a <= b & b <= c & a in A & c in A;
per cases by A1,REAL_1:def 5;
suppose a = b or b = c;
hence thesis by A1;
suppose A2: a < b & b < c & a in A & c in A;
assume not b in A;
then A3: A c= [. 0,1 .] \ {b} by BORSUK_1:83,ZFMISC_1:40;
A4: 0 <= a & c <= 1 by JORDAN5A:2;
then A5: 0 < b & b < 1 by A2,AXIOMS:22;
then A6: A c= [. 0,b .[ \/ ]. b,1 .] by A3,Th31;
A7: [.0,b.[ c= [.0,b.] & ].b,1 .] c= [.b,1 .] by RCOMP_2:17;
b in [. 0,1 .] & 0 in [.0,1 .] & 1 in [.0,1 .] by A5,TOPREAL5:1;
then [.0,b.] c= [. 0,1 .] & [. b,1 .] c= [.0,1 .] by RCOMP_1:16;
then [.0,b.[ c= the carrier of I[01] & ].b,1 .] c= the carrier of I[01]
by A7,BORSUK_1:83,XBOOLE_1:1;
then reconsider B = [.0,b.[, C = ].b,1 .] as non empty Subset of I[01]
by A2,A4,RCOMP_2:3,4;
A8: B,C are_separated by A5,Th33;
now per cases by A6,A8,CONNSP_1:17;
suppose A c= B;
hence contradiction by A2,RCOMP_2:3;
suppose A c= C;
hence contradiction by A2,RCOMP_2:4;
end;
hence thesis;
end;
theorem Th47:
for A being non empty connected Subset of I[01],
a, b being real number 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 number;
assume A1: a in A & b in A;
then A2: 0 <= a & b <= 1 by JORDAN5A:2;
let x be set; 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 & a <= z & z <= b;
0 <= z & z <= 1 by A2,A3,AXIOMS:22;
then reconsider z as Point of I[01] by JORDAN5A:2;
z in A by A1,A3,Th46;
hence thesis by A3;
end;
theorem Th48:
for a, b being real number,
A being Subset of I[01] st a <= b & A = [.a,b.] holds
A is closed
proof
let a, b be real number,
A be Subset of I[01];
assume A1: a <= b & A = [.a,b.];
then 0 <= a & b <= 1 by Th32;
then A2: Closed-Interval-TSpace(a,b) is closed SubSpace of
Closed-Interval-TSpace(0,1) by A1,TREAL_1:6;
then the carrier of Closed-Interval-TSpace(a,b) is
Subset of Closed-Interval-TSpace(0,1)
by BORSUK_1:35;
then reconsider BA = the carrier of Closed-Interval-TSpace(a,b) as
Subset of Closed-Interval-TSpace(0,1);
BA is closed by A2,BORSUK_1:def 14;
hence thesis by A1,TOPMETR:25,27;
end;
theorem Th49:
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];
assume A1: p1 <= p2;
A2: 0 <= p1 & p2 <= 1 by JORDAN5A:2;
set S = [. p1, p2 .];
S c= [.0,1.] by BORSUK_1:83,RCOMP_1:16;
then reconsider S as Subset of I[01] by BORSUK_1:83;
A3: S is closed by A1,Th48;
A4: Closed-Interval-TSpace(p1,p2) is connected by A1,TREAL_1:23;
I[01] | S = Closed-Interval-TSpace(p1,p2) by A1,A2,JGRAPH_5:7;
hence thesis by A1,A3,A4,COMPTS_1:17,CONNSP_1:def 3,RCOMP_1:15;
end;
theorem Th50:
for X being Subset of I[01],
X' being Subset of REAL st X' = X holds
X' is bounded_above bounded_below
proof
let X be Subset of I[01],
X' be Subset of REAL;
assume A1: X' = X;
then for r being real number st r in X' holds r <= 1 by JORDAN5A:2;
hence X' is bounded_above by SEQ_4:def 1;
for r being real number st r in X' holds 0 <= r by A1,JORDAN5A:2;
hence thesis by SEQ_4:def 2;
end;
theorem Th51:
for X being Subset of I[01],
X' being Subset of REAL,
x being real number st x in X' & X' = X holds
inf X' <= x & x <= sup X'
proof
let X be Subset of I[01],
X' be Subset of REAL,
x be real number;
assume A1: x in X' & X' = X;
then X' is bounded_above bounded_below by Th50;
hence thesis by A1,SEQ_4:def 4,def 5;
end;
Lm2:
I[01] is closed SubSpace of R^1 by TOPMETR:27,TREAL_1:5;
theorem Th52:
for A being Subset of REAL, B being Subset of I[01] st A = B holds
A is closed iff B is closed
proof
let A be Subset of REAL, B be Subset of I[01];
assume A1: A = B;
A2: the carrier of I[01] c= the carrier of R^1 by BORSUK_1:35;
then A c= the carrier of R^1 by A1,XBOOLE_1:1;
then reconsider C = A as Subset of R^1;
reconsider Z = the carrier of I[01] as Subset of R^1
by A2;
Z is closed by Lm2,BORSUK_1:def 14;
then A3: B is closed iff C is closed by A1,TSEP_1:8;
hereby assume A is closed;
then A4: C is closed by TOPREAL6:79;
C c= the carrier of I[01] by A1;
then C c= [#] I[01] by PRE_TOPC:12;
then C /\ [#] I[01] = B by A1,XBOOLE_1:28;
hence B is closed by A4,PRE_TOPC:43;
end;
assume B is closed;
hence thesis by A3,TOPREAL6:79;
end;
theorem Th53:
for C being closed-interval Subset of REAL holds inf C <= sup C
proof
let C be closed-interval Subset of REAL;
consider c being Element of C;
inf C <= c & c <= sup C by INTEGRA2:1;
hence thesis by AXIOMS:22;
end;
theorem Th54:
for C being non empty compact connected Subset of I[01],
C' being Subset of REAL st C = C' & [. inf C', sup C' .] c= C' holds
[. inf C', sup C' .] = C'
proof
let C be non empty compact connected Subset of I[01],
C' be Subset of REAL;
assume A1: C = C' & [. inf C', sup C' .] c= C';
assume [. inf C', sup C' .] <> C';
then not C' c= [. inf C', sup C' .] by A1,XBOOLE_0:def 10;
then consider c being set such that
A2: c in C' & not c in [. inf C', sup C' .] by TARSKI:def 3;
reconsider c as real number by A2,XREAL_0:def 1;
inf C' <= c & c <= sup C' by A1,A2,Th51;
hence thesis by A2,TOPREAL5:1;
end;
theorem Th55:
for C being non empty compact connected Subset of I[01] holds
C is closed-interval Subset of REAL
proof
let C be non empty compact connected Subset of I[01];
reconsider C' = C as Subset of REAL by BORSUK_1:83,XBOOLE_1:1;
C is closed by COMPTS_1:16;
then A1: C' is closed by Th52;
A2: C' is bounded_below bounded_above by Th50;
then A3: inf C' in C' by A1,RCOMP_1:31;
sup C' in C' by A1,A2,RCOMP_1:30;
then [. inf C', sup C' .] c= C' by A3,Th47;
then A4: [. inf C', sup C' .] = C' by Th54;
C' is bounded by A2,SEQ_4:def 3;
then inf C' <= sup C' by SEQ_4:24;
hence thesis by A4,INTEGRA1:def 1;
end;
theorem Th56:
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 C' = C as closed-interval Subset of REAL by Th55;
A1: C' = [. inf C', sup C' .] by INTEGRA1:5;
inf C' <= sup C' by Th53;
then inf C' in C & sup C' in C by A1,RCOMP_1:15;
then reconsider p1 = inf C', p2 = sup C' as Point of I[01];
take p1, p2;
thus p1 <= p2 by Th53;
thus thesis by INTEGRA1:5;
end;
begin :: Decompositions of Simple Closed Curves
definition
func I(01) -> strict non empty SubSpace of I[01] means :Def1:
the carrier of it = ]. 0,1 .[;
existence
proof
reconsider E = ]. 0,1 .[ as non empty Subset of I[01]
by BORSUK_1:83,RCOMP_1:15;
take I[01] | E;
thus thesis by JORDAN1:1;
end;
uniqueness by TSEP_1:5;
end;
theorem Th57:
for A being Subset of I[01] st A = the carrier of I(01) holds
I(01) = I[01] | A
proof
let A be Subset of I[01];
assume
A1: A = the carrier of I(01);
the carrier of (I[01]|A) = A by JORDAN1:1;
hence thesis by A1,TSEP_1:5;
end;
theorem Th58:
the carrier of I(01) = (the carrier of I[01]) \ {0,1}
proof
A1: the carrier of I(01) = ]. 0,1 .[ by Def1;
A2: ].0,1.[ misses {0,1} by JORDAN6:44;
[.0,1.] = ].0,1.[ \/ {0,1} by RCOMP_1:11;
hence thesis by A1,A2,BORSUK_1:83,XBOOLE_1:88;
end;
theorem Th59:
I(01) is open SubSpace of I[01] by Th58,JORDAN6:41,TSEP_1:def 1;
theorem Th60:
for r being real number holds
r in the carrier of I(01) iff 0 < r & r < 1
proof
let r be real number;
hereby assume r in the carrier of I(01);
then r in ]. 0, 1 .[ by Def1;
hence 0 < r & r < 1 by JORDAN6:45;
end;
assume 0 < r & r < 1;
then r in ]. 0, 1 .[ by JORDAN6:45;
hence thesis by Def1;
end;
theorem Th61:
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
A1: a < b & b <> 1;
0 <= a & b <= 1 by JORDAN5A:2;
then A2: b < 1 by A1,REAL_1:def 5;
]. a, b .] c= the carrier of I(01)
proof
let x be set;
assume x in ]. a, b .];
then x in { r where r is Real : a < r & r <= b } by RCOMP_2:def 2;
then consider r being Real such that
A3: x = r & a < r & r <= b;
0 < r & r < 1 by A2,A3,AXIOMS:22,JORDAN5A:2;
hence thesis by A3,Th60;
end;
hence thesis by A1,RCOMP_2:4;
end;
theorem Th62:
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
A1: a < b & a <> 0;
A2: 0 <= a & b <= 1 by JORDAN5A:2;
[. a, b .[ c= the carrier of I(01)
proof
let x be set;
assume x in [. a, b .[;
then x in { r where r is Real : a <= r & r < b } by RCOMP_2:def 1;
then consider r being Real such that
A3: x = r & a <= r & r < b;
0 < r & r < 1 by A1,A2,A3,AXIOMS:22;
hence thesis by A3,Th60;
end;
hence thesis by A1,RCOMP_2: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;
consider f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|D
such that
A1: f is_homeomorphism by TOPREAL2:def 1;
thus thesis by A1,T_0TOPSP:def 1;
end;
theorem
for D being non empty Subset of TOP-REAL 2,
p1, p2 being Point of TOP-REAL 2 st D is_an_arc_of p1, p2 holds
I(01), (TOP-REAL 2) | (D \ {p1,p2}) are_homeomorphic
proof
let D be non empty Subset of TOP-REAL 2,
p1, p2 be Point of TOP-REAL 2;
assume A1: D is_an_arc_of p1, p2;
then consider f being map of I[01], (TOP-REAL 2)|D such that
A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2;
A3: f is continuous one-to-one by A2,TOPS_2:def 5;
set fD = f | the carrier of I(01);
A4: the carrier of I(01) c= the carrier of I[01] by BORSUK_1:35;
A5: dom f = the carrier of I[01] by FUNCT_2:def 1;
then A6: dom fD = the carrier of I(01) by A4,RELAT_1:91;
reconsider K0 = the carrier of I(01) as Subset of I[01]
by A4;
A7: rng f = [#] ((TOP-REAL 2)|D) by A2,TOPS_2:def 5
.= the carrier of ((TOP-REAL 2)|D) by PRE_TOPC:12
.= D by JORDAN1:1;
A8: 0 in dom f & 1 in dom f by A5,JORDAN5A:2;
A9: f .: the carrier of I(01) =
f .: (the carrier of I[01]) \ f .: {0,1} by A3,Th58,FUNCT_1:123
.= D \ f .: {0,1} by A5,A7,RELAT_1:146
.= D \ {p1,p2} by A2,A8,FUNCT_1:118;
rng fD = f .: the carrier of I(01) by RELAT_1:148;
then A10: rng fD = the carrier of ((TOP-REAL 2)|(D \ {p1,p2}))
by A9,JORDAN1:1;
A11: I(01) = I[01] | K0 by Th57;
fD is Function of the carrier of I(01),
the carrier of (TOP-REAL 2)|D by A4,FUNCT_2:38;
then reconsider fD1 = fD as map of I[01]|K0, (TOP-REAL 2)|D by A11;
A12: fD1 is continuous by A3,TOPMETR:10;
fD is Function of the carrier of I(01),
the carrier of ((TOP-REAL 2)|(D \ {p1,p2})) by A6,A10,FUNCT_2:3;
then reconsider fD as map of I(01), (TOP-REAL 2)|(D \ {p1,p2});
A13: dom fD = [#]I(01) by A6,PRE_TOPC:12;
A14: D \ {p1,p2} c= D by XBOOLE_1:36;
reconsider D1 = D \ {p1,p2} as non empty Subset of the carrier
of TOP-REAL 2 by A1,JORDAN6:56;
reconsider D0 = D \ {p1,p2} as Subset of (TOP-REAL 2)|D
by A14,JORDAN1:1;
A15: (TOP-REAL 2)|D1 = ((TOP-REAL 2)|D)|D0 by GOBOARD9:4;
A16: rng fD = [#]((TOP-REAL 2)|(D \ {p1,p2})) by A10,PRE_TOPC:12;
f is one-to-one by A2,TOPS_2:def 5;
then A17: fD is one-to-one by FUNCT_1:84;
A18: fD is continuous by A11,A12,A15,TOPMETR:9;
set g = (f") | D1;
A19: f" is continuous by A2,TOPS_2:def 5;
A20: D1 = the carrier of (TOP-REAL 2)|D1 by JORDAN1:1;
D1 c= the carrier of (TOP-REAL 2)|D by A14,JORDAN1:1;
then g is Function of the carrier of (TOP-REAL 2)|D1,
the carrier of I[01] by A20,FUNCT_2:38;
then reconsider ff = g as map of (TOP-REAL 2)|D1, I[01];
A21: ff is continuous by A15,A19,TOPMETR:10;
A22: rng fD = [#]((TOP-REAL 2)|(D \ {p1,p2})) by A10,PRE_TOPC:12;
rng f = [#]((TOP-REAL 2)|D) by A2,TOPS_2:def 5;
then fD" = (fD qua Function)" & f" = (f qua Function)"
by A3,A17,A22,TOPS_2:def 4;
then ff = fD" by A3,A9,RFUNCT_2:40;
then fD" is continuous by A11,A21,TOPMETR:9;
then fD is_homeomorphism by A13,A16,A17,A18,TOPS_2:def 5;
hence thesis by T_0TOPSP:def 1;
end;
theorem Th65:
for D being Subset of TOP-REAL 2,
p1, p2 being Point of TOP-REAL 2 st
D is_an_arc_of p1, p2 holds
I[01], (TOP-REAL 2) | D are_homeomorphic
proof
let D be Subset of TOP-REAL 2,
p1, p2 be Point of TOP-REAL 2;
assume D is_an_arc_of p1, p2;
then ex f being map of I[01], (TOP-REAL 2)|D st
f is_homeomorphism & f.0 = p1 & f.1 = p2 by TOPREAL1:def 2;
hence thesis by T_0TOPSP:def 1;
end;
theorem
for p1, p2 being Point of TOP-REAL 2 st p1 <> p2 holds
I[01], (TOP-REAL 2) | LSeg (p1, p2) are_homeomorphic
proof
let p1, p2 be Point of TOP-REAL 2;
assume p1 <> p2;
then LSeg (p1, p2) is_an_arc_of p1, p2 by TOPREAL1:15;
hence thesis by Th65;
end;
theorem Th67:
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 & E = [. p1,p2 .];
reconsider T = I(01)|E as SubSpace of I[01] by TSEP_1:7;
0 <= p1 & p2 <= 1 by JORDAN5A:2;
then reconsider S = Closed-Interval-TSpace(p1,p2) as SubSpace of I[01]
by A1,TOPMETR:27,TREAL_1:6;
A2: the carrier of S = E by A1,TOPMETR:25;
the carrier of T = E by JORDAN1:1;
then A3: S = T by A2,TSEP_1:5;
set f = L[01]((#)(p1,p2), (p1,p2)(#));
f is_homeomorphism by A1,TREAL_1:20;
hence thesis by A3,TOPMETR:27,T_0TOPSP:def 1;
end;
theorem Th68:
for A being non empty Subset of TOP-REAL 2,
p, q being Point of TOP-REAL 2,
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 map of I[01]|E, (TOP-REAL 2)|A st
E = [. a, b .] & f is_homeomorphism & f.a = p & f.b = q
proof
let A be non empty Subset of TOP-REAL 2,
p, q be Point of TOP-REAL 2,
a, b be Point of I[01];
assume that
A1: A is_an_arc_of p, q and
A2: a < b;
reconsider E = [. a, b .] as non empty Subset of I[01] by A2,Th49;
take E;
consider f being map of I[01], (TOP-REAL 2)|A such that
A3: f is_homeomorphism & f.0 = p & f.1 = q by A1,TOPREAL1:def 2;
0 <= a & b <= 1 by JORDAN5A:2;
then A5: I[01]|E = Closed-Interval-TSpace(a,b) by A2,JGRAPH_5:7;
then reconsider e = P[01](a,b,(#)(0,1),(0,1)(#)) as map of I[01]|E, I[01]
by TOPMETR:27;
set g = f * e;
A6: e is_homeomorphism by A2,A5,TOPMETR:27,TREAL_1:20;
reconsider g as map of I[01]|E, (TOP-REAL 2)|A;
take g;
thus E = [. a, b .];
thus g is_homeomorphism by A3,A6,TOPS_2:71;
A7: 0 = (#)(0,1) & a = (#)(a,b) by A2,TREAL_1:def 1;
A8: 1 = (0,1)(#) & b = (a,b)(#) by A2,TREAL_1:def 2;
a in E by A2,RCOMP_1:15;
then a in the carrier of I[01]|E by JORDAN1:1;
hence g.a = f.(e.a) by FUNCT_2:21
.= p by A2,A3,A7,TREAL_1:16;
b in E by A2,RCOMP_1:15;
then b in the carrier of I[01]|E by JORDAN1:1;
hence g.b = f.(e.b) by FUNCT_2:21
.= q by A2,A3,A8,TREAL_1:16;
end;
theorem Th69:
for A being TopSpace, B being non empty TopSpace,
f being map of A, B,
C being TopSpace, X being Subset of A st
f is continuous &
C is SubSpace of B holds
for h being map 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 map 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;
let h be map of A|X, C;
assume
A3: h = f|X;
the carrier of A|X = X by JORDAN1:1;
then f|X is Function of the carrier of A|X, the carrier of B
by FUNCT_2:38;
then reconsider g = f|X as map of A|X, B;
g is continuous by A1,TOPMETR:10;
hence thesis by A2,A3,TOPMETR:8;
end;
theorem Th70:
for X being Subset of I[01],
a, b being Point of I[01] st
a <= b & X = ]. a, b .[ holds X is open
proof
let X be Subset of I[01],
a, b be Point of I[01];
assume
A1: a <= b & X = ]. a, b .[;
per cases;
suppose a <> b;
then A2: a < b by A1,REAL_1:def 5;
A3: 0 in the carrier of I[01] & 1 in the carrier of I[01] by JORDAN5A:2;
A4: 0 <= a by JORDAN5A:2;
reconsider A = [. 0, a .] as Subset of I[01] by A3,Th43;
A5: b <= 1 by JORDAN5A:2;
reconsider B = [. b, 1 .] as Subset of I[01] by A3,Th43;
A6: A is closed by A4,Th48;
B is closed by A5,Th48;
then A7: A \/ B is closed by A6,TOPS_1:36;
A8: X = [. 0, 1 .] \ (A \/ B) by A1,A2,A4,A5,Th37;
[#] I[01] = [. 0, 1 .] by BORSUK_1:83,PRE_TOPC:12;
then X = (A \/ B)` by A8,PRE_TOPC:17;
hence thesis by A7,TOPS_1:29;
suppose a = b;
then X = {} by A1,RCOMP_1:12;
then X in the topology of I[01] by PRE_TOPC:5;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th71:
for X being Subset of I(01),
a, b being Point of I[01] st
a <= b & X = ]. a, b .[ holds X is open
proof
let X be Subset of I(01),
a, b be Point of I[01];
assume A1: a <= b & X = ]. a, b .[;
then reconsider X' = X as Subset of I[01] by Th44;
X' is open by A1,Th70;
hence thesis by Th59,TSEP_1:17;
end;
theorem Th72:
for X being non empty Subset of I(01),
a being Point of I[01] st
0 < a & X = ]. 0, a .] holds X is closed
proof
let X be non empty Subset of I(01),
a be Point of I[01];
assume A1: 0 < a & X = ]. 0, a .];
A2: 1 in the carrier of I[01] by JORDAN5A:2;
A3: a <= 1 by JORDAN5A:2;
a <> 1
proof
assume
A4: a = 1;
a in X by A1,RCOMP_2:4;
hence contradiction by A4,Th60;
end;
then A5: a < 1 by A3,REAL_1:def 5;
[#] I(01) = the carrier of I(01) by PRE_TOPC:12 .= ]. 0, 1 .[ by Def1;
then [#] I(01) \ X = ]. a, 1 .[ by A1,A5,Th41;
then [#] I(01) \ X is open by A2,A3,Th71;
hence thesis by PRE_TOPC:def 6;
end;
theorem Th73:
for X being non empty Subset of I(01),
a being Point of I[01] st
X = [. a, 1 .[ holds X is closed
proof
let X be non empty Subset of I(01),
a be Point of I[01];
assume A1: X = [. a, 1 .[;
A2: 1 in the carrier of I[01] & 0 in the carrier of I[01] by JORDAN5A:2;
A3: a <> 1 by A1,RCOMP_2:7;
a <= 1 by JORDAN5A:2;
then A4: a < 1 by A3,REAL_1:def 5;
A5: [#] I(01) = the carrier of I(01) by PRE_TOPC:12
.= ]. 0, 1 .[ by Def1;
A6: a <> 0
proof
assume a = 0;
then 0 in X by A1,RCOMP_2:3;
then 0 in the carrier of I(01);
then 0 in ]. 0, 1 .[ by Def1;
hence thesis by JORDAN6:45;
end;
A7: 0 <= a by JORDAN5A:2;
then [#] I(01) \ X = ]. 0, a .[ by A1,A4,A5,A6,Th42;
then [#] I(01) \ X is open by A2,A7,Th71;
hence thesis by PRE_TOPC:def 6;
end;
theorem Th74:
for A being non empty Subset of TOP-REAL 2,
p, q being Point of TOP-REAL 2,
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 map of I(01)|E, (TOP-REAL 2)|(A \ {p}) st
E = ]. a, b .] & f is_homeomorphism & f.b = q
proof
let A be non empty Subset of TOP-REAL 2,
p, q be Point of TOP-REAL 2,
a, b be Point of I[01];
assume
A1: A is_an_arc_of p, q & a < b & b <> 1;
then consider F being non empty Subset of I[01],
s being map of I[01]|F, (TOP-REAL 2)|A such that
A2: F = [. a, b .] & s is_homeomorphism & s.a = p & s.b = q by Th68;
reconsider E = ]. a, b .] as non empty Subset of I(01) by A1,Th61;
A3: the carrier of I(01)|E = E by JORDAN1:1;
set X = E;
A4: X = F \ {a} by A1,A2,Th27;
A5: E c= F by A2,RCOMP_2:17;
the carrier of I[01]|F = F by JORDAN1:1;
then reconsider X' = E as Subset of I[01]|F by A5;
set sX = s|E;
A6: s is continuous one-to-one by A2,TOPS_2:def 5;
A7: rng s = [#] ((TOP-REAL 2)|A) by A2,TOPS_2:def 5;
then A8: rng s = A by PRE_TOPC:def 10;
A9: dom s = [#] (I[01]|F) by A2,TOPS_2:def 5
.= F by PRE_TOPC:def 10;
then A10: X c= dom s by A2,RCOMP_2:17;
A11: a in dom s by A1,A2,A9,RCOMP_1:15;
A12: s.:X = s.:F \ s.:{a} by A4,A6,FUNCT_1:123
.= s.:F \ {s.a} by A11,FUNCT_1:117
.= rng s \ {p} by A2,A9,RELAT_1:146
.= [#] ((TOP-REAL 2)|(A \ {p})) by A8,PRE_TOPC:def 10;
then A13: [#] ((TOP-REAL 2)|(A \ {p})) = rng sX by RELAT_1:148;
then A14: rng (s|E) = the carrier of (TOP-REAL 2)|(A \ {p}) by PRE_TOPC:12;
A15: dom sX = X by A10,RELAT_1:91
.= [#] (I(01)|X) by PRE_TOPC:def 10;
then dom sX = the carrier of (I(01)|X) by PRE_TOPC:12;
then sX is Function of the carrier of (I(01)|X),
the carrier of (TOP-REAL 2)|(A \ {p}) by A14,FUNCT_2:3;
then reconsider sX as map of I(01)|E, (TOP-REAL 2)|(A \ {p});
the carrier of I(01)|X = X by JORDAN1:1;
then A16: the carrier of I(01)|X = the carrier of (I[01]|F|X') by JORDAN1:1;
A17: I(01)|X is SubSpace of I[01] by TSEP_1:7;
I[01]|F|X' is SubSpace of I[01] by TSEP_1:7;
then A18: I(01)|X = I[01]|F|X' by A16,A17,TSEP_1:5;
A19: the carrier of (TOP-REAL 2)|(A \ {p}) = A \ {p} by JORDAN1:1;
the carrier of (TOP-REAL 2)|A = A by JORDAN1:1;
then A20: the carrier of (TOP-REAL 2)|(A \ {p}) c=
the carrier of (TOP-REAL 2)|A by A19,XBOOLE_1:36;
then (TOP-REAL 2)|(A \ {p}) is SubSpace of (TOP-REAL 2)|A by TSEP_1:4;
then A21: sX is continuous by A6,A18,Th69;
A22: sX is one-to-one by A6,FUNCT_1:84;
A23: s" is continuous by A2,TOPS_2:def 5;
the carrier of I(01)|X c= the carrier of I[01]|F by A3,A5,JORDAN1:1;
then A24: I(01)|X is SubSpace of I[01]|F by A17,TSEP_1:4;
reconsider Ap = A \ {p} as Subset of (TOP-REAL 2)|A
by A19,A20;
Ap c= A by XBOOLE_1:36;
then A25: ((TOP-REAL 2)|A)|Ap = (TOP-REAL 2)|(A \ {p}) by JORDAN6:47;
sX" = (sX qua Function)" by A13,A22,TOPS_2:def 4
.= (s qua Function)" | (s.:X) by A6,RFUNCT_2:40
.= s" | [#] ((TOP-REAL 2)|(A \ {p})) by A6,A7,A12,TOPS_2:def 4
.= s" | Ap by PRE_TOPC:def 10;
then sX" is continuous by A23,A24,A25,Th69;
then A26: sX is_homeomorphism by A13,A15,A21,A22,TOPS_2:def 5;
b in X by A1,RCOMP_2:4;
then sX.b = q by A2,FUNCT_1:72;
hence thesis by A26;
end;
theorem Th75:
for A being non empty Subset of TOP-REAL 2,
p, q being Point of TOP-REAL 2,
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 map of I(01)|E, (TOP-REAL 2)|(A \ {q}) st
E = [. a, b .[ & f is_homeomorphism & f.a = p
proof
let A be non empty Subset of TOP-REAL 2,
p, q be Point of TOP-REAL 2,
a, b be Point of I[01];
assume
A1: A is_an_arc_of p, q & a < b & a <> 0;
then consider F being non empty Subset of I[01],
s being map of I[01]|F, (TOP-REAL 2)|A such that
A2: F = [. a, b .] & s is_homeomorphism & s.a = p & s.b = q by Th68;
reconsider E = [. a, b .[ as non empty Subset of I(01) by A1,Th62;
A3: the carrier of I(01)|E = E by JORDAN1:1;
set X = E;
A4: X = F \ {b} by A1,A2,Th28;
A5: E c= F by A2,RCOMP_2:17;
the carrier of I[01]|F = F by JORDAN1:1;
then reconsider X' = E as Subset of I[01]|F by A5;
set sX = s|E;
A6: s is continuous one-to-one by A2,TOPS_2:def 5;
A7: rng s = [#] ((TOP-REAL 2)|A) by A2,TOPS_2:def 5;
then A8: rng s = A by PRE_TOPC:def 10;
A9: dom s = [#] (I[01]|F) by A2,TOPS_2:def 5
.= F by PRE_TOPC:def 10;
then A10: X c= dom s by A2,RCOMP_2:17;
A11: b in dom s by A1,A2,A9,RCOMP_1:15;
A12: s.:X = s.:F \ s.:{b} by A4,A6,FUNCT_1:123
.= s.:F \ {s.b} by A11,FUNCT_1:117
.= rng s \ {q} by A2,A9,RELAT_1:146
.= [#] ((TOP-REAL 2)|(A \ {q})) by A8,PRE_TOPC:def 10;
then A13: [#] ((TOP-REAL 2)|(A \ {q})) = rng sX by RELAT_1:148;
then A14: rng (s|E) = the carrier of (TOP-REAL 2)|(A \ {q}) by PRE_TOPC:12;
A15: dom sX = X by A10,RELAT_1:91
.= [#] (I(01)|X) by PRE_TOPC:def 10;
then dom sX = the carrier of (I(01)|X) by PRE_TOPC:12;
then sX is Function of the carrier of (I(01)|X),
the carrier of (TOP-REAL 2)|(A \ {q}) by A14,FUNCT_2:3;
then reconsider sX as map of I(01)|E, (TOP-REAL 2)|(A \ {q});
the carrier of I(01)|X = X by JORDAN1:1;
then A16: the carrier of I(01)|X = the carrier of (I[01]|F|X') by JORDAN1:1;
A17: I(01)|X is SubSpace of I[01] by TSEP_1:7;
I[01]|F|X' is SubSpace of I[01] by TSEP_1:7;
then A18: I(01)|X = I[01]|F|X' by A16,A17,TSEP_1:5;
A19: the carrier of (TOP-REAL 2)|(A \ {q}) = A \ {q} by JORDAN1:1;
the carrier of (TOP-REAL 2)|A = A by JORDAN1:1;
then A20: the carrier of (TOP-REAL 2)|(A \ {q}) c=
the carrier of (TOP-REAL 2)|A by A19,XBOOLE_1:36;
then (TOP-REAL 2)|(A \ {q}) is SubSpace of (TOP-REAL 2)|A by TSEP_1:4;
then A21: sX is continuous by A6,A18,Th69;
A22: sX is one-to-one by A6,FUNCT_1:84;
A23: s" is continuous by A2,TOPS_2:def 5;
the carrier of I(01)|X c= the carrier of I[01]|F by A3,A5,JORDAN1:1;
then A24: I(01)|X is SubSpace of I[01]|F by A17,TSEP_1:4;
reconsider Ap = A \ {q} as Subset of (TOP-REAL 2)|A
by A19,A20;
Ap c= A by XBOOLE_1:36;
then A25: ((TOP-REAL 2)|A)|Ap = (TOP-REAL 2)|(A \ {q}) by JORDAN6:47;
sX" = (sX qua Function)" by A13,A22,TOPS_2:def 4
.= (s qua Function)" | (s.:X) by A6,RFUNCT_2:40
.= s" | [#] ((TOP-REAL 2)|(A \ {q})) by A6,A7,A12,TOPS_2:def 4
.= s" | Ap by PRE_TOPC:def 10;
then sX" is continuous by A23,A24,A25,Th69;
then A26: sX is_homeomorphism by A13,A15,A21,A22,TOPS_2:def 5;
a in X by A1,RCOMP_2:3;
then sX.a = p by A2,FUNCT_1:72;
hence thesis by A26;
end;
theorem Th76:
for A, B being non empty Subset of TOP-REAL 2,
p, q being Point of TOP-REAL 2 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 2) | ((A \ {p}) \/ (B \ {p})) are_homeomorphic
proof
let A, B be non empty Subset of TOP-REAL 2,
p, q be Point of TOP-REAL 2;
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 } & p <> q;
reconsider a = 0, b = 1/2, c = 1 as Point of I[01] by JORDAN5A:2;
A4: 0 in the carrier of I[01] & 1/2 in the carrier of I[01] by JORDAN5A:2;
consider E1 being non empty Subset of I(01),
sx being map of I(01)|E1, (TOP-REAL 2)|(A \ {p}) such that
A5: E1 = ]. a, b .] & sx is_homeomorphism & sx.b = q by A1,Th74;
consider E2 being non empty Subset of I(01),
ty being map of I(01)|E2, (TOP-REAL 2)|(B \ {p}) such that
A6: E2 = [. b, c .[ & ty is_homeomorphism & ty.b = q by A2,Th75;
set T1 = I(01)|E1, T2 = I(01)|E2, T = I(01),
S = (TOP-REAL 2) | ((A \ {p}) \/ (B \ {p})),
U1 = (TOP-REAL 2) | (A \ {p}), U2 = (TOP-REAL 2)|(B \ {p});
B is_an_arc_of p, q by A2,JORDAN5B:14;
then A7: A \ {p} is non empty & B \ {p} is non empty by A1,Th7;
A \ {p} c= (A \ {p}) \/ (B \ {p}) by XBOOLE_1:7;
then (A \ {p}) \/ (B \ {p}) is non empty by A7,XBOOLE_1:3;
then the carrier of S is non empty by JORDAN1:1;
then reconsider S as non empty SubSpace of TOP-REAL 2 by STRUCT_0:def 1;
A8: the carrier of U1 is non empty by A7,JORDAN1:1;
the carrier of U2 is non empty by A7,JORDAN1:1;
then reconsider U1, U2 as non empty SubSpace of TOP-REAL 2
by A8,STRUCT_0:def 1;
A9: [#] U1 = A \ {p} by PRE_TOPC:def 10;
A10: [#] U2 = B \ {p} by PRE_TOPC:def 10;
A11: the carrier of U1 = A \ {p} by JORDAN1:1;
A12: the carrier of S = (A \ {p}) \/ (B \ {p}) by JORDAN1:1;
then A13: the carrier of U1 c= the carrier of S by A11,XBOOLE_1:7;
then A14: U1 is SubSpace of S by TSEP_1:4;
the carrier of U2 = B \ {p} by JORDAN1:1;
then A15: the carrier of U2 c= the carrier of S by A12,XBOOLE_1:7;
then A16: U2 is SubSpace of S by TSEP_1:4;
sx is Function of the carrier of T1, the carrier of S by A13,FUNCT_2:9;
then reconsider sx' = sx as map of T1, S;
sx is continuous by A5,TOPS_2:def 5;
then A17: sx' is continuous by A14,TOPMETR:7;
ty is Function of the carrier of T2, the carrier of S by A15,FUNCT_2:9;
then reconsider ty' = ty as map of T2, S;
ty is continuous by A6,TOPS_2:def 5;
then A18: ty' is continuous by A16,TOPMETR:7;
reconsider F1 = [#] T1, F2 = [#] T2 as non empty Subset of T
by PRE_TOPC:def 10;
A19: F1 = ]. 0, 1/2 .] by A5,PRE_TOPC:def 10;
then A20: F1 is closed by A4,Th72;
A21: F2 = [. 1/2, 1 .[ by A6,PRE_TOPC:def 10;
then A22: F2 is closed by A4,Th73;
A23: ([#] T1) \/ ([#] T2) = ]. 0, 1 .[ by A19,A21,Th40
.= the carrier of I(01) by Def1
.= [#] T by PRE_TOPC:12;
A24: ([#] T1) /\ ([#] T2) = { 1/2 } by A19,A21,Th29;
for d be set st d in ([#] T1) /\ ([#] T2) holds sx.d = ty.d
proof
let d be set;
assume d in ([#] T1) /\ ([#] T2);
then d = b by A24,TARSKI:def 1;
hence thesis by A5,A6;
end;
then consider F being map of T,S such that
A25: F = sx'+*ty & F is continuous by A17,A18,A20,A22,A23,JGRAPH_2:9;
A26: dom F = the carrier of I(01) by FUNCT_2:def 1
.= [#] I(01) by PRE_TOPC:12;
A27: sx' is one-to-one by A5,TOPS_2:def 5;
A28: ty' is one-to-one by A6,TOPS_2:def 5;
A29: dom sx' = [#] T1 & dom ty' = [#] T2 by TOPS_2:51;
then A30: dom sx' /\ dom ty' = { b } by A19,A21,Th29;
A31: rng sx = [#] ((TOP-REAL 2)|(A \ {p})) by A5,TOPS_2:def 5;
then A32: rng sx = A \ {p} by PRE_TOPC:def 10;
A33:rng ty = [#] ((TOP-REAL 2)|(B \ {p})) by A6,TOPS_2:def 5;
then A34:rng ty = B \ {p} by PRE_TOPC:def 10;
then A35: rng sx' /\ rng ty' = ((A \ {p}) /\ B) \ {p} by A32,XBOOLE_1:49
.= ((A /\ B) \ {p}) \ {p} by XBOOLE_1:49
.= (A /\ B) \ ({p} \/ {p}) by XBOOLE_1:41
.= { sx'.b } by A3,A5,ZFMISC_1:23;
then A36: F is one-to-one by A25,A27,A28,A30,Th5;
A37: sx" = (sx qua Function)" by A27,A31,TOPS_2:def 4;
A38: ty" = (ty qua Function)" by A28,A33,TOPS_2:def 4;
sx' tolerates ty'
proof
let t be set;
assume t in dom sx' /\ dom ty';
then t = b by A30,TARSKI:def 1;
hence thesis by A5,A6;
end;
then A39: rng F = rng sx' \/ rng ty' by A25,CIRCCMB2:5
.= [#] S by A32,A34,PRE_TOPC:def 10;
then F" = (F qua Function)" by A36,TOPS_2:def 4;
then A40: F" = sx" +* ty" by A5,A6,A25,A27,A28,A30,A35,A37,A38,Th6;
the carrier of T1 c= the carrier of T by BORSUK_1:35;
then sx" is Function of the carrier of U1, the carrier of T
by FUNCT_2:9;
then reconsider f = sx" as map of U1, T;
the carrier of T2 c= the carrier of T by BORSUK_1:35;
then ty" is Function of the carrier of U2, the carrier of T
by FUNCT_2:9;
then reconsider g = ty" as map of U2, T;
[#] U1 c= (A \ {p}) \/ (B \ {p}) by A9,XBOOLE_1:7;
then A41: [#] U1 c= the carrier of S by JORDAN1:1;
[#] U2 c= (A \ {p}) \/ (B \ {p}) by A10,XBOOLE_1:7;
then [#] U2 c= the carrier of S by JORDAN1:1;
then reconsider V1 = [#] U1, V2 = [#] U2 as Subset of S by A41;
A42: ([#] U1) \/ ([#] U2) = [#] S by A9,A10,PRE_TOPC:def 10;
A43: V1 is closed
proof
reconsider A' = A as Subset of TOP-REAL 2;
A' is compact by A1,JORDAN5A:1;
then A44: A' is closed by COMPTS_1:16;
A45: A \ {p} c= A by XBOOLE_1:36;
A46: not p in {q} by A3,TARSKI:def 1;
q in A by A1,TOPREAL1:4;
then {q} c= A by ZFMISC_1:37;
then A47: {q} c= A \ {p} by A46,ZFMISC_1:40;
A48: A /\ (B \ {p}) = A /\ B \ {p} by XBOOLE_1:49
.= {q} by A3,ZFMISC_1:23;
A' /\ [#] S = A' /\ ((A \ {p}) \/ (B \ {p})) by PRE_TOPC:def 10
.= (A /\ (A \ {p})) \/ (A /\ (B \ {p})) by XBOOLE_1:23
.= (A \ {p}) \/ (A /\ (B \ {p})) by A45,XBOOLE_1:28
.= A \ {p} by A47,A48,XBOOLE_1:12
.= V1 by PRE_TOPC:def 10;
hence thesis by A44,PRE_TOPC:43;
end;
A49: V2 is closed
proof
reconsider B' = B as Subset of TOP-REAL 2;
B' is compact by A2,JORDAN5A:1;
then A50: B' is closed by COMPTS_1:16;
A51: B \ {p} c= B by XBOOLE_1:36;
A52: not p in {q} by A3,TARSKI:def 1;
q in B by A2,TOPREAL1:4;
then {q} c= B by ZFMISC_1:37;
then A53: {q} c= B \ {p} by A52,ZFMISC_1:40;
A54: B /\ (A \ {p}) = B /\ A \ {p} by XBOOLE_1:49
.= {q} by A3,ZFMISC_1:23;
B' /\ [#] S = B' /\ ((A \ {p}) \/ (B \ {p})) by PRE_TOPC:def 10
.= (B /\ (A \ {p})) \/ (B /\ (B \ {p})) by XBOOLE_1:23
.= (B /\ (A \ {p})) \/ (B \ {p}) by A51,XBOOLE_1:28
.= B \ {p} by A53,A54,XBOOLE_1:12
.= V2 by PRE_TOPC:def 10;
hence thesis by A50,PRE_TOPC:43;
end;
sx" is continuous by A5,TOPS_2:def 5;
then A55: f is continuous by TOPMETR:7;
ty" is continuous by A6,TOPS_2:def 5;
then A56: g is continuous by TOPMETR:7;
for r being set st r in ([#] U1) /\ ([#] U2) holds f.r = g.r
proof
let r be set;
assume r in ([#] U1) /\ ([#] U2);
then A57: r = q by A5,A31,A33,A35,TARSKI:def 1;
b in E1 by A5,RCOMP_2:4;
then A58: b in dom sx by A29,PRE_TOPC:def 10;
b in E2 by A6,RCOMP_2:3;
then A59: b in dom ty by A29,PRE_TOPC:def 10;
f.q = b by A5,A27,A37,A58,FUNCT_1:56;
hence thesis by A6,A28,A38,A57,A59,FUNCT_1:56;
end;
then consider h being map of S,T such that
A60: h = f+*g & h is continuous
by A14,A16,A42,A43,A49,A55,A56,JGRAPH_2:9;
F is_homeomorphism by A25,A26,A36,A39,A40,A60,TOPS_2:def 5;
hence thesis by T_0TOPSP:def 1;
end;
theorem Th77:
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;
assume A1: p in D;
consider q being Point of TOP-REAL 2 such that
A2: q in D & p <> q by Th4;
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;
not q in {p} by A2,TARSKI:def 1;
then reconsider R2p = D \ {p} as non empty Subset of TOP-REAL 2
by A2,XBOOLE_0:def 4;
A7: D \ {p} = (P1 \ {p}) \/ (P2 \ {p}) by A5,XBOOLE_1:42;
P2 is_an_arc_of q, p by A4,JORDAN5B:14;
then (TOP-REAL 2) | R2p, I(01) are_homeomorphic by A2,A3,A6,A7,Th76;
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
A1: p in D & q in D;
consider r being Point of TOP-REAL 2 such that
A2: r in D & p <> r by Th4;
reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2
by A2,ZFMISC_1:64;
per cases;
suppose A3: p = q;
(TOP-REAL 2) | Dp, (TOP-REAL 2) | Dp are_homeomorphic;
hence thesis by A3;
suppose A4: p <> q;
then reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2
by A1,ZFMISC_1:64;
reconsider Dq = D \ {q} as non empty Subset of TOP-REAL 2
by A1,A4,ZFMISC_1:64;
A5: (TOP-REAL 2) | Dp, I(01) are_homeomorphic by A1,Th77;
(TOP-REAL 2) | Dq, I(01) are_homeomorphic by A1,Th77;
hence thesis by A5,BORSUK_3:3;
end;
theorem Th79:
for C being non empty Subset of TOP-REAL 2,
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 2)|C are_homeomorphic holds
ex s1, s2 being Point of TOP-REAL 2 st C is_an_arc_of s1,s2
proof
let C be non empty Subset of TOP-REAL 2,
E be Subset of I(01);
given p1, p2 being Point of I[01] such that
A1: p1 < p2 & E = [. p1,p2 .];
A2: the carrier of I(01)|E = E by JORDAN1:1;
E is non empty by A1,Th49;
then A3: I(01)|E is non empty by A2,STRUCT_0:def 1;
assume
A4: I(01)|E, (TOP-REAL 2)|C are_homeomorphic;
I[01], I(01)|E are_homeomorphic by A1,Th67;
then I[01], (TOP-REAL 2)|C are_homeomorphic by A3,A4,BORSUK_3:3;
then consider g being map of I[01], (TOP-REAL 2)|C such that
A5: g is_homeomorphism by T_0TOPSP:def 1;
set s1 = g.0, s2 = g.1;
A6: the carrier of (TOP-REAL 2)|C c= the carrier of TOP-REAL 2
by BORSUK_1:35;
0 in the carrier of I[01] by JORDAN5A:2;
then A7: g.0 in the carrier of (TOP-REAL 2)|C by FUNCT_2:7;
1 in the carrier of I[01] by JORDAN5A:2;
then g.1 in the carrier of (TOP-REAL 2)|C by FUNCT_2:7;
then reconsider s1, s2 as Point of TOP-REAL 2 by A6,A7;
C is_an_arc_of s1, s2 by A5,TOPREAL1:def 2;
hence thesis;
end;
theorem Th80:
for Dp being non empty Subset of TOP-REAL 2,
f being map of (TOP-REAL 2) | Dp, I(01),
C being non empty Subset of TOP-REAL 2 st
f is_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 map of (TOP-REAL 2) | Dp, I(01),
C be non empty Subset of TOP-REAL 2;
assume
A1: f is_homeomorphism & C c= Dp;
given p1, p2 being Point of I[01] such that
A2: p1 < p2 & f.:C = [. p1,p2 .];
reconsider E = [. p1,p2 .] as Subset of I(01) by A2;
set g = f"| E;
f" is_homeomorphism by A1,TOPS_2:70;
then A3: f" is one-to-one by TOPS_2:def 5;
A4: f is continuous one-to-one by A1,TOPS_2:def 5;
A5: f"(f.:C) = C
proof
thus f"(f.:C) c= C by A4,FUNCT_1:152;
dom f = the carrier of (TOP-REAL 2) | Dp by FUNCT_2:def 1;
then C c= dom f by A1,JORDAN1:1;
hence C c= f"(f.:C) by FUNCT_1:146;
end;
A6: rng f = [#] I(01) by A1,TOPS_2:def 5;
then A7: f".:E = C by A2,A4,A5,TOPS_2:68;
A8: rng g = f".:E by RELAT_1:148
.= the carrier of ((TOP-REAL 2)|C) by A7,JORDAN1:1
.= [#] ((TOP-REAL 2)|C) by PRE_TOPC:12;
the carrier of (I(01)|E) = E by JORDAN1:1;
then g is Function of the carrier of I(01)|E,
the carrier of (TOP-REAL 2)|Dp by FUNCT_2:38;
then g is Function of the carrier of I(01)|E,
the carrier of (TOP-REAL 2)|C by A8,FUNCT_2:8;
then reconsider g as map of I(01)|E, (TOP-REAL 2)|C;
dom (f") = the carrier of I(01) by FUNCT_2:def 1;
then dom g = E by RELAT_1:91 .= the carrier of (I(01)|E) by JORDAN1:1;
then A9: dom g = [#] (I(01)|E) by PRE_TOPC:12;
A10: g is one-to-one by A3,FUNCT_1:84;
the carrier of (TOP-REAL 2)|C = C & the carrier of (TOP-REAL 2)|Dp = Dp
by JORDAN1:1;
then A11: (TOP-REAL 2)|C is SubSpace of (TOP-REAL 2) | Dp by A1,TOPMETR:4;
f" is continuous by A1,TOPS_2:def 5;
then A12: g is continuous by A11,Th69;
A13: g" = (g qua Function)" by A8,A10,TOPS_2:def 4
.= ((f" qua Function)")|((f").:E) by A3,RFUNCT_2:40
.= ((f qua Function)"")|((f").:E) by A4,A6,TOPS_2:def 4
.= f|C by A4,A7,FUNCT_1:65;
then reconsider t = f|C as map of (TOP-REAL 2) | C, I(01)|E;
C c= the carrier of ((TOP-REAL 2) | Dp) by A1,JORDAN1:1;
then reconsider C' = C as Subset of (TOP-REAL 2) | Dp;
((TOP-REAL 2) | Dp)|C' = (TOP-REAL 2) | C by A1,JORDAN6:47;
then t is continuous by A4,Th69;
then g is_homeomorphism by A8,A9,A10,A12,A13,TOPS_2:def 5;
then I(01)|E, (TOP-REAL 2)|C are_homeomorphic by T_0TOPSP:def 1;
hence thesis by A2,Th79;
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 Th2;
suppose C is non trivial;
then consider d1,d2 being Point of TOP-REAL 2 such that
A3: d1 in C & d2 in C & d1 <> d2 by SPPOL_1:4;
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 & C c= D \ {p} by Th1;
A5: d1 in D \ {p} & d2 in D \ {p} by A3,A4;
reconsider Dp = D \ {p} as non empty Subset of TOP-REAL 2 by A3,A4;
(TOP-REAL 2) | Dp, I(01) are_homeomorphic by A4,Th77;
then consider f being map of (TOP-REAL 2) | Dp, I(01) such that
A6: f is_homeomorphism by T_0TOPSP:def 1;
A7: C c= the carrier of (TOP-REAL 2) | Dp by A4,JORDAN1:1;
then reconsider C' = C as Subset of (TOP-REAL 2) | Dp;
set fC = f.:C';
C c= [#] ((TOP-REAL 2) | Dp) by A7,PRE_TOPC:12;
then A8: C' is compact by COMPTS_1:11;
A9: C' is connected by CONNSP_1:24;
A10: f is continuous by A6,TOPS_2:def 5;
rng f = [#] I(01) by A6,TOPS_2:def 5;
then reconsider fC as compact connected Subset of I(01)
by A8,A9,A10,COMPTS_1:24,TOPREAL5:5;
reconsider fC' = fC as Subset of I[01] by PRE_TOPC:39;
fC' c= the carrier of I(01);
then A11: fC' c= [#] I(01) by PRE_TOPC:12;
A12: for P being Subset of I(01) st P=fC' holds P is compact;
A13: d1 in the carrier of (TOP-REAL 2) | Dp by A5,JORDAN1:1;
A14: f.d1 in f.:C' by A3,FUNCT_2:43;
A15: d2 in the carrier of (TOP-REAL 2) | Dp by A5,JORDAN1:1;
A16: f.d2 in f.:C' by A3,FUNCT_2:43;
then reconsider fC' as non empty compact connected Subset of I[01]
by A11,A12,COMPTS_1:11,CONNSP_1:24;
A17: d1 in dom f by A13,FUNCT_2:def 1;
A18: d2 in dom f by A15,FUNCT_2:def 1;
consider p1, p2 being Point of I[01] such that
A19: p1 <= p2 & fC' = [. p1,p2 .] by Th56;
A20: f is one-to-one by A6,TOPS_2:def 5;
p1 <> p2
proof
assume p1 = p2;
then A21: fC' = {p1} by A19,RCOMP_1:14;
then A22: f.d1 = p1 by A14,TARSKI:def 1;
f.d2 = p1 by A16,A21,TARSKI:def 1;
hence thesis by A3,A17,A18,A20,A22,FUNCT_1:def 8;
end;
then p1 < p2 by A19,REAL_1:def 5;
then consider s1, s2 being Point of TOP-REAL 2 such that
A23: C is_an_arc_of s1,s2 by A4,A6,A19,Th80;
thus thesis by A23;
end;