Copyright (c) 1997 Association of Mizar Users
environ
vocabulary PRE_TOPC, CARD_1, FUNCT_1, RELAT_1, SUBSET_1, BOOLE, COMPTS_1,
ORDINAL2, FUNCT_4, FUNCOP_1, TOPS_2, BORSUK_1, GRAPH_1, RCOMP_1, RELAT_2,
ARYTM_3, ARYTM_1, TREAL_1, SEQ_1, TOPMETR, SEQM_3, SETFAM_1, TARSKI,
TSP_1, METRIC_1, URYSOHN1, PCOMPS_1, EUCLID, MCART_1, CONNSP_2, TOPS_1,
BORSUK_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, REAL_1,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, PRE_TOPC, EUCLID, TOPS_2,
MCART_1, RCOMP_1, PCOMPS_1, CARD_1, TOPS_1, COMPTS_1, CONNSP_1, TREAL_1,
FUNCT_4, SEQM_3, BORSUK_1, T_0TOPSP, TOPMETR, BINOP_1, FUNCT_3, GRCAT_1,
URYSOHN1, TSP_1, WEIERSTR;
constructors EUCLID, TOPS_2, CONNSP_1, REAL_1, T_0TOPSP, TREAL_1, SEQM_3,
TOPS_1, WEIERSTR, RCOMP_1, COMPTS_1, YELLOW_8, URYSOHN1, GRCAT_1,
MEMBERED;
clusters SUBSET_1, STRUCT_0, TOPMETR, FUNCT_1, PRE_TOPC, BORSUK_1, TSP_1,
YELLOW_6, YELLOW_8, WAYBEL10, METRIC_1, RELSET_1, MEMBERED, FUNCT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, PRE_TOPC, COMPTS_1, URYSOHN1, T_0TOPSP, XBOOLE_0;
theorems BORSUK_1, FUNCOP_1, TOPS_2, TREAL_1, FUNCT_2, FUNCT_1, PRE_TOPC,
RCOMP_1, TARSKI, RELAT_1, JORDAN1, REAL_1, TOPS_1, REAL_2, URYSOHN1,
TOPMETR, FUNCT_4, TOPMETR2, HEINE, PCOMPS_1, SEQM_3, AXIOMS, MCART_1,
ZFMISC_1, BINOP_1, CONNSP_2, FUNCT_3, COMPTS_1, T_0TOPSP, GRCAT_1,
CARD_1, SPPOL_1, WEIERSTR, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0,
XCMPLX_1;
schemes FUNCT_2, FUNCT_1;
begin :: Preliminaries
reserve T,T1,T2,S for non empty TopSpace;
scheme FrCard { A() -> non empty set, X() -> set,
F(set) -> set, P[set] }:
Card { F(w) where w is Element of A(): w in X() & P[w] } <=` Card X()
proof
deffunc G(set) = F($1);
consider f be Function such that
A1: dom f = X() & for x be set st x in X() holds f.x = G(x) from Lambda;
{ F(w) where w is Element of A(): w in X() & P[w]} c= rng f
proof let x be set;
assume x in { F(w) where w is Element of A(): w in X() & P[w]};
then consider w being Element of A() such that
A2: x = F(w) & w in X() & P[w];
f.w = x by A1,A2;
hence thesis by A1,A2,FUNCT_1:def 5;
end;
hence thesis by A1,CARD_1:28;
end;
theorem
for f being map of T1,S, g being map of T2,S st
T1 is SubSpace of T & T2 is SubSpace of T &
([#] T1) \/ ([#] T2) = [#] T &
T1 is compact & T2 is compact & T is_T2 &
f is continuous & g is continuous &
( for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p )
ex h being map of T,S st h = f+*g & h is continuous
proof
let f be map of T1,S, g be map of T2,S;
assume that
A1: T1 is SubSpace of T & T2 is SubSpace of T and
A2: ([#] T1) \/ ([#] T2) = [#] T and
A3: T1 is compact and
A4: T2 is compact and
A5: T is_T2 and
A6: f is continuous and
A7: g is continuous and
A8: for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p;
set h = f+*g;
A9: dom f = the carrier of T1 by FUNCT_2:def 1 .= [#] T1 by PRE_TOPC:12;
A10: dom g = the carrier of T2 by FUNCT_2:def 1 .= [#] T2 by PRE_TOPC:12;
then A11: dom h = [#] T by A2,A9,FUNCT_4:def 1
.= the carrier of T by PRE_TOPC:12;
rng f c= the carrier of S & rng g c= the carrier of S by RELSET_1:12;
then rng f \/ rng g c= the carrier of S & rng h c= rng f \/ rng g
by FUNCT_4:18,XBOOLE_1:8; then rng h c= the carrier of S by XBOOLE_1:1;
then h is Function of the carrier of T, the carrier of S by A11,FUNCT_2:4;
then reconsider h as map of T,S ;
take h;
thus h = f+*g;
for P being Subset of S st P is closed holds h"P is closed
proof
let P be Subset of S;
assume A12: P is closed;
A13: h"P c= dom h & dom h = dom f \/ dom g by FUNCT_4:def 1,RELAT_1:167;
then A14: h"P = h"P /\ ([#] T1 \/ [#] T2) by A9,A10,XBOOLE_1:28
.= (h"P /\ [#](T1)) \/ (h"P /\ [#](T2)) by XBOOLE_1:23;
A15: for x being set st x in [#] T1 holds h.x = f.x
proof
let x be set such that A16: x in [#] T1;
now per cases;
suppose A17: x in [#] T2;
then x in [#] T1 /\ [#] T2 by A16,XBOOLE_0:def 3;
then f.x = g.x by A8;
hence thesis by A10,A17,FUNCT_4:14;
suppose not x in [#] T2;
hence h.x = f.x by A10,FUNCT_4:12;
end;
hence thesis;
end;
now let x be set;
thus x in h"P /\ [#] T1 implies x in f"P
proof
assume x in h"P /\ [#] T1;
then x in h"P & x in dom f & x in [#] T1 by A9,XBOOLE_0:def 3;
then h.x in P & x in dom f & f.x = h.x by A15,FUNCT_1:def 13;
hence x in f"P by FUNCT_1:def 13;
end;
assume x in f"P;
then x in dom f & f.x in P by FUNCT_1:def 13;
then x in dom h & x in [#] T1 & h.x in P by A9,A13,A15,XBOOLE_0:def 2;
then x in h"P & x in [#] T1 by FUNCT_1:def 13;
hence x in h"P /\ [#] T1 by XBOOLE_0:def 3;
end;
then A18: h"P /\ [#] T1 = f"P by TARSKI:2;
now let x be set;
thus x in h"P /\ [#] T2 implies x in g"P
proof
assume x in h"P /\ [#] T2;
then x in h"P & x in dom g & x in [#] T2 by A10,XBOOLE_0:def 3;
then h.x in P & x in dom g & g.x = h.x by FUNCT_1:def 13,FUNCT_4:14;
hence x in g"P by FUNCT_1:def 13;
end;
assume x in g"P;
then x in dom g & g.x in P by FUNCT_1:def 13;
then x in dom h & x in [#]
T2 & h.x in P by A10,A13,FUNCT_4:14,XBOOLE_0:def 2;
then x in h"P & x in [#] T2 by FUNCT_1:def 13;
hence x in h"P /\ [#] T2 by XBOOLE_0:def 3;
end;
then A19: h"P = f"P \/ g"P by A14,A18,TARSKI:2;
f"P c= the carrier of T1;
then f"P c= [#] T1 & [#] T1 c= [#] T by A2,PRE_TOPC:12,XBOOLE_1:7;
then f"P c= [#] T by XBOOLE_1:1;
then f"P is Subset of T by PRE_TOPC:12;
then reconsider P1 = f"P as Subset of T;
g"P c= the carrier of T2;
then g"P c= [#] T2 & [#] T2 c= [#] T by A2,PRE_TOPC:12,XBOOLE_1:7;
then g"P c= [#] T by XBOOLE_1:1;
then g"P is Subset of T by PRE_TOPC:12;
then reconsider P2 = g"P as Subset of T;
reconsider P12 = P1 \/ P2 as Subset of T;
reconsider P3 = f"P as Subset of T1;
reconsider P4 = g"P as Subset of T2;
P3 is closed & P4 is closed by A6,A7,A12,PRE_TOPC:def 12;
then P3 is compact & P4 is compact by A3,A4,COMPTS_1:17;
then P1 is compact & P2 is compact by A1,BORSUK_1:42;
then P12 is compact by COMPTS_1:19;
hence h"P is closed by A5,A19,COMPTS_1:16;
end;
hence h is continuous by PRE_TOPC:def 12;
end;
definition
let S, T be non empty TopSpace;
cluster continuous map of S, T;
existence
proof
consider a be Point of T;
S --> a is continuous by BORSUK_1:36;
hence thesis;
end;
end;
definition let T be non empty TopStruct;
cluster id T -> open continuous;
coherence
proof
thus id T is open
proof
let A be Subset of T;
assume A1: A is open;
(id the carrier of T).:A = A by BORSUK_1:3;
hence thesis by A1,GRCAT_1:def 11;
end;
let V be Subset of T such that
A2: V is closed;
(id T)"V = (id the carrier of T)"V by GRCAT_1:def 11
.= V by BORSUK_1:4;
hence (id T)"V is closed by A2;
end;
end;
definition
let T be non empty TopStruct;
cluster continuous one-to-one map of T, T;
existence
proof
take id T;
thus thesis;
end;
end;
canceled;
theorem
for S, T being non empty TopSpace,
f being map of S, T st f is_homeomorphism holds
f" is open
proof
let S, T be non empty TopSpace,
f be map of S, T;
assume f is_homeomorphism;
then A1:dom f = [#]S & rng f = [#]
T & f is one-to-one continuous by TOPS_2:def 5;
let P be Subset of T;
assume A2: P is open;
f"P = (f").:P by A1,TOPS_2:68;
hence thesis by A1,A2,TOPS_2:55;
end;
begin :: Paths and arcwise connected spaces
definition let T be TopStruct; let a, b be Point of T;
given f be map of I[01], T such that
A1: f is continuous & f.0 = a & f.1 = b;
mode Path of a, b -> map of I[01], T means :Def1:
it is continuous & it.0 = a & it.1 = b;
existence by A1;
end;
theorem Th4:
for T be non empty TopSpace, a be Point of T
ex f be map of I[01], T st f is continuous & f.0 = a & f.1 = a
proof
let T be non empty TopSpace, a be Point of T;
set IT = I[01] --> a;
A1: IT = (the carrier of I[01]) --> a by BORSUK_1:def 3;
reconsider IT as map of I[01], T;
A2: IT.0 = a & IT.1 = a by A1,BORSUK_1:def 17,def 18,FUNCOP_1:13;
IT is continuous by BORSUK_1:36;
then reconsider IT as Path of a, a by A2,Def1;
IT is continuous by BORSUK_1:36;
hence thesis by A2;
end;
definition let T be non empty TopSpace; let a be Point of T;
cluster continuous Path of a, a;
existence
proof
set IT = I[01] --> a;
A1: IT = (the carrier of I[01]) --> a by BORSUK_1:def 3;
reconsider IT as map of I[01], T;
A2: IT.0 = a & IT.1 = a by A1,BORSUK_1:def 17,def 18,FUNCOP_1:13;
IT is continuous by BORSUK_1:36;
then reconsider IT as Path of a, a by A2,Def1;
IT is continuous by BORSUK_1:36;
hence thesis;
end;
end;
definition let T be TopStruct;
attr T is arcwise_connected means :Def2:
for a, b being Point of T ex f being map of I[01], T st
f is continuous & f.0 = a & f.1 = b;
correctness;
end;
definition
cluster arcwise_connected non empty TopSpace;
existence
proof
set T = I[01] | { 0[01] };
A1: the carrier of T = { 0[01] } by JORDAN1:1;
0[01] in the carrier of I[01] & 0[01] in { 0[01] }
by TARSKI:def 1;
then reconsider nl = 0[01] as Point of T by JORDAN1:1;
for a, b being Point of T ex f being map of I[01], T st
f is continuous & f.0 = a & f.1 = b
proof
let a, b be Point of T;
A2: a = nl & b = nl by A1,TARSKI:def 1;
reconsider f = I[01] --> nl as map of I[01], T;
A3: f is continuous by BORSUK_1:36;
f = (the carrier of I[01]) --> nl by BORSUK_1:def 3;
then f.0 = a & f.1 = b by A2,BORSUK_1:def 17,def 18,FUNCOP_1:13;
hence thesis by A3;
end;
then T is arcwise_connected by Def2;
hence thesis;
end;
end;
definition let T be arcwise_connected TopStruct;
let a, b be Point of T;
redefine mode Path of a, b means :Def3:
it is continuous & it.0 = a & it.1 = b;
compatibility
proof
ex f be map of I[01], T st
f is continuous & f.0 = a & f.1 = b by Def2;
hence thesis by Def1;
end;
end;
definition let T be arcwise_connected TopStruct;
let a, b be Point of T;
cluster -> continuous Path of a, b;
coherence by Def3;
end;
reserve GY for non empty TopSpace,
r,s for Real;
Lm1: 0 in [.0,1.] & 1 in [.0,1.]
proof
0 in {r:0<=r & r<=1} & 1 in {s:0<=s & s<=1};
hence thesis by RCOMP_1:def 1;
end;
theorem Th5:
for GX being non empty TopSpace st
GX is arcwise_connected holds GX is connected
proof let GX be non empty TopSpace;
assume A1: for x,y being Point of GX
ex h being map of I[01],GX st h is continuous
& x=h.0 & y=h.1;
for x, y being Point of GX ex GY st (GY is connected &
ex f being map of GY,GX st f is continuous
& x in rng f & y in rng f )
proof let x, y be Point of GX;
now consider h being map of I[01],GX such that
A2: h is continuous and A3: x=h.0 & y=h.1 by A1;
[#] I[01] = the carrier of I[01] by PRE_TOPC:12;
then 0 in dom h & 1 in dom h by Lm1,BORSUK_1:83,TOPS_2:51;
then x in rng h & y in rng h by A3,FUNCT_1:def 5;
hence thesis by A2,TREAL_1:22;
end;
hence thesis;
end;
hence thesis by JORDAN1:2;
end;
definition
cluster arcwise_connected -> connected (non empty TopSpace);
coherence by Th5;
end;
begin :: Basic operations on paths
definition let T be non empty TopSpace;
let a, b, c be Point of T;
let P be Path of a, b,
Q be Path of b, c;
given f, g be map of I[01], T such that
A1: f is continuous & f.0 = a & f.1 = b &
g is continuous & g.0 = b & g.1 = c;
func P + Q -> Path of a, c means :Def4:
for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies it.t = P.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies it.t = Q.(2*t'-1) );
existence
proof
set e1 = P[01](0, 1/2, (#)(0,1), (0,1)(#));
set e2 = P[01](1/2, 1, (#)(0,1), (0,1)(#));
set E1 = P * e1;
set E2 = Q * e2;
set f = E1 +* E2;
A2:dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1
.= [.0,1/2.] by TOPMETR:25;
A3:dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1
.= [.1/2,1.] by TOPMETR:25;
A4: dom P = the carrier of I[01] & dom Q = the carrier of I[01]
by FUNCT_2:def 1;
then A5:rng e1 c= dom P by RELSET_1:12,TOPMETR:27;
rng e2 c= the carrier of Closed-Interval-TSpace(0,1) by RELSET_1:12;
then A6: dom E2 = dom e2 by A4,RELAT_1:46,TOPMETR:27;
A7: dom f = dom E1 \/ dom E2 by FUNCT_4:def 1
.= [.0,1/2.] \/ [.1/2,1.] by A2,A3,A5,A6,RELAT_1:46
.= the carrier of I[01] by BORSUK_1:83,TREAL_1:2;
A8: for t' being Real st 0 <= t' & t' <= 1/2 holds E1.t' = P.(2*t')
proof
let t' be Real such that
A9: 0 <= t' & t' <= 1/2;
dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1;
then dom e1 = [.0, 1/2.] by TOPMETR:25
.= {r : 0 <= r & r <= 1/2 } by RCOMP_1:def 1;
then A10: t' in dom e1 by A9;
then reconsider s = t' as Point of Closed-Interval-TSpace (0, 1/2)
by FUNCT_2:def 1;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
by BORSUK_1:def 17,def 18,TREAL_1:8;
e1.s = ((r2 - r1)/(1/2 - 0))*t' + ((1/2)*r1 - 0 * r2)/(1/2) by TREAL_1:14
.= 2*t' by BORSUK_1:def 17,def 18,TREAL_1:8;
hence thesis by A10,FUNCT_1:23;
end;
not 0 in { r : 1/2 <= r & r <= 1 }
proof
assume 0 in { r : 1/2 <= r & r <= 1 };
then consider rr being Real such that
A11: rr = 0 & 1/2 <= rr & rr <= 1;
thus thesis by A11;
end;
then not 0 in dom E2 by A3,A6,RCOMP_1:def 1;
then A12:f.0 = E1.0 by FUNCT_4:12
.= P.(2*0) by A8
.= a by A1,Def1;
A13:rng P c= the carrier of T & rng Q c= the carrier of T by RELSET_1:12;
rng E1 c= rng P & rng E2 c= rng Q by RELAT_1:45;
then A14:rng E1 c= the carrier of T & rng E2 c= the carrier of T by A13,
XBOOLE_1:1;
A15: rng f c= rng E1 \/ rng E2 by FUNCT_4:18;
rng E1 \/ rng E2 c= (the carrier of T) \/ the carrier of T
by A14,XBOOLE_1:13;
then rng f c= the carrier of T by A15,XBOOLE_1:1;
then f is Function of the carrier of I[01], the carrier of T
by A7,FUNCT_2:def 1,RELSET_1:11;
then reconsider f as map of I[01], T ;
reconsider T1 = Closed-Interval-TSpace (0, 1/2),
T2 = Closed-Interval-TSpace (1/2, 1) as SubSpace of I[01]
by TOPMETR:27,TREAL_1:6;
A16: e1 is continuous map of
Closed-Interval-TSpace(0,1/2),Closed-Interval-TSpace(0,1)
by TREAL_1:15;
A17:e2 is continuous by TREAL_1:15;
E1 is Function of the carrier of Closed-Interval-TSpace (0, 1/2),
the carrier of T by FUNCT_2:19,TOPMETR:27;
then reconsider ff = E1 as map of T1, T ;
A18:E2 is Function of the carrier of Closed-Interval-TSpace (1/2, 1),
the carrier of T by FUNCT_2:19,TOPMETR:27;
then reconsider gg = E2 as map of T2, T ;
1/2 in { r : 0 <= r & r <= 1 };
then reconsider pol = 1/2 as Point of I[01] by BORSUK_1:83,RCOMP_1:def 1;
P is continuous & Q is continuous by A1,Def1;
then A19:ff is continuous & gg is continuous by A16,A17,TOPMETR:27,TOPS_2:58
;
A20:[#] T1 = the carrier of T1 by PRE_TOPC:12
.= [.0,1/2.] by TOPMETR:25;
A21:[#] T2 = the carrier of T2 by PRE_TOPC:12
.= [.1/2,1.] by TOPMETR:25;
then A22: ([#] T1) \/ ([#] T2) = the carrier of I[01] by A20,BORSUK_1:83,
TREAL_1:2
.= [#] I[01] by PRE_TOPC:12;
A23: for t' being Real st 1/2 <= t' & t' <= 1 holds E2.t' = Q.(2*t'-1)
proof
let t' be Real such that
A24: 1/2 <= t' & t' <= 1;
dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1;
then dom e2 = [.1/2,1.] by TOPMETR:25
.= {r : 1/2 <= r & r <= 1 } by RCOMP_1:def 1;
then A25: t' in dom e2 by A24;
then reconsider s = t' as Point of Closed-Interval-TSpace (1/2,1)
by FUNCT_2:def 1;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real
by BORSUK_1:def 17,def 18,TREAL_1:8;
e2.s = ((r2 - r1)/(1 - 1/2))*t' + (1*r1 - (1/2)*r2)/(1 - 1/2)
by TREAL_1:14
.= 2*t' + (- 1) by BORSUK_1:def 17,def 18,TREAL_1:8
.= 2*t' - 1 by XCMPLX_0:def 8;
hence thesis by A25,FUNCT_1:23;
end;
A26:ff.(1/2) = P.(2*(1/2)) by A8
.= b by A1,Def1
.= Q.(2*(1/2)-1) by A1,Def1
.= gg.pol by A23;
A27:([#] T1) /\ ([#] T2) = {pol} by A20,A21,TOPMETR2:1;
R^1 is_T2 by PCOMPS_1:38,TOPMETR:def 7;
then T1 is compact & T2 is compact & I[01] is_T2 & ff.pol = gg.pol
by A26,HEINE:11,TOPMETR:3;
then consider h being map of I[01], T such that
A28: h = ff+*gg & h is continuous by A19,A22,A27,TOPMETR2:4;
1 in { r : 1/2 <= r & r <= 1 };
then 1 in dom E2 by A3,A6,RCOMP_1:def 1;
then f.1 = E2.1 by FUNCT_4:14
.= Q.(2*1-1) by A23
.= c by A1,Def1;
then reconsider f as Path of a, c by A12,A28,Def1;
for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies f.t = P.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies f.t = Q.(2*t'-1) )
proof
let t be Point of I[01], t' be Real;
assume A29: t = t';
thus 0 <= t' & t' <= 1/2 implies f.t = P.(2*t')
proof
assume A30: 0 <= t' & t' <= 1/2;
then t' in { r : 0 <= r & r <= 1/2 };
then A31: t' in [.0,1/2.] by RCOMP_1:def 1;
per cases;
suppose A32: t' <> 1/2;
not t' in dom E2
proof
assume t' in dom E2;
then t' in [.0,1/2.] /\ [.1/2,1.] by A3,A6,A31,XBOOLE_0:def 3;
then t' in {1/2} by TOPMETR2:1;
hence thesis by A32,TARSKI:def 1;
end;
then f.t = E1.t by A29,FUNCT_4:12
.= P.(2*t') by A8,A29,A30;
hence thesis;
suppose A33: t' = 1/2;
1/2 in { r : 1/2 <= r & r <= 1 };
then 1/2 in [.1/2, 1.] by RCOMP_1:def 1;
then 1/2 in the carrier of Closed-Interval-TSpace(1/2,1)
by TOPMETR:25;
then t in dom E2 by A18,A29,A33,FUNCT_2:def 1;
then f.t = E1.t by A26,A29,A33,FUNCT_4:14
.= P.(2*t') by A8,A29,A30;
hence thesis;
end;
thus 1/2 <= t' & t' <= 1 implies f.t = Q.(2*t'-1)
proof
assume A34: 1/2 <= t' & t' <= 1;
then t' in { r : 1/2 <= r & r <= 1 };
then t' in [.1/2,1.] by RCOMP_1:def 1;
then f.t = E2.t by A3,A6,A29,FUNCT_4:14
.= Q.(2*t'-1) by A23,A29,A34;
hence thesis;
end;
end;
hence thesis;
end;
uniqueness
proof
let A, B be Path of a, c such that
A35: for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies A.t = P.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies A.t = Q.(2*t'-1) )
and
A36: for t being Point of I[01], t' being Real st t = t' holds
( 0 <= t' & t' <= 1/2 implies B.t = P.(2*t') ) &
( 1/2 <= t' & t' <= 1 implies B.t = Q.(2*t'-1) );
A37: dom B = the carrier of I[01] by FUNCT_2:def 1;
A = B
proof
A38: dom A = dom B by A37,FUNCT_2:def 1;
for x be set st x in dom A holds A.x = B.x
proof
let x be set; assume A39: x in dom A;
then A40: x in the carrier of I[01] by FUNCT_2:def 1;
reconsider y = x as Point of I[01] by A39,FUNCT_2:def 1;
x in { r : 0 <= r & r <= 1 } by A40,BORSUK_1:83,RCOMP_1:def 1;
then consider r' being Real such that
A41: r' = x & 0 <= r' & r' <= 1;
per cases;
suppose A42: r' <= 1/2;
then A.y = P.(2*r') by A35,A41
.= B.y by A36,A41,A42;
hence thesis;
suppose A43: 1/2 < r';
then A.y = Q.(2*r'-1) by A35,A41
.= B.y by A36,A41,A43;
hence thesis;
end;
hence thesis by A38,FUNCT_1:9;
end;
hence thesis;
end;
end;
definition let T be non empty TopSpace;
let a be Point of T;
cluster constant Path of a, a;
existence
proof
set IT = I[01] --> a;
A1: IT = (the carrier of I[01]) --> a by BORSUK_1:def 3;
reconsider IT as map of I[01], T;
A2: IT.0 = a & IT.1 = a by A1,BORSUK_1:def 17,def 18,FUNCOP_1:13;
IT is continuous by BORSUK_1:36;
then reconsider IT as Path of a, a by A2,Def1;
for n1,n2 being set st n1 in dom IT & n2 in dom IT holds IT.n1=IT.n2
proof
let n1,n2 be set;
assume n1 in dom IT & n2 in dom IT;
then A3: n1 in the carrier of I[01] & n2 in the carrier of I[01] by FUNCT_2:def
1;
then IT.n1 = a by A1,FUNCOP_1:13
.= IT.n2 by A1,A3,FUNCOP_1:13;
hence thesis;
end;
then IT is constant by SEQM_3:def 5;
hence thesis;
end;
end;
theorem
for T being non empty TopSpace,
a being Point of T,
P being constant Path of a, a holds P = I[01] --> a
proof
let T be non empty TopSpace,
a be Point of T,
P be constant Path of a, a;
set IT = I[01] --> a;
A1: IT = (the carrier of I[01]) --> a by BORSUK_1:def 3;
A2: dom IT = the carrier of I[01] by FUNCT_2:def 1;
A3: dom P = the carrier of I[01] by FUNCT_2:def 1;
A4:ex f be map of I[01], T st f is continuous & f.0 = a & f.1 = a by Th4;
for x be set st x in the carrier of I[01] holds P.x = IT.x
proof
let x be set; assume A5: x in the carrier of I[01];
A6: P.0 = a by A4,Def1;
0 in { r : 0 <= r & r <= 1 };
then 0 in the carrier of I[01] by BORSUK_1:83,RCOMP_1:def 1;
then P.x = a by A3,A5,A6,SEQM_3:def 5
.= IT.x by A1,A5,FUNCOP_1:13;
hence thesis;
end;
hence thesis by A2,A3,FUNCT_1:9;
end;
theorem Th7:
for T being non empty TopSpace,
a being Point of T,
P being constant Path of a, a holds P + P = P
proof
let T be non empty TopSpace,
a be Point of T,
P be constant Path of a, a;
A1: dom (P + P) = the carrier of I[01] by FUNCT_2:def 1;
A2: the carrier of I[01] = dom P by FUNCT_2:def 1;
A3:ex f be map of I[01], T st f is continuous & f.0 = a & f.1 = a by Th4;
for x be set st x in the carrier of I[01] holds P.x = (P+P).x
proof
let x be set; assume A4: x in the carrier of I[01];
then reconsider p = x as Point of I[01];
x in { r : 0 <= r & r <= 1 } by A4,BORSUK_1:83,RCOMP_1:def 1;
then consider r being Real such that
A5: r = x & 0 <= r & r <= 1;
per cases;
suppose A6: r < 1/2;
A7: 2 * r >= 0 by A5,REAL_2:121;
r * 2 < 1/2 * 2 by A6,REAL_1:70;
then 2 * r in { e where e is Real : 0 <= e & e <= 1 } by A7;
then 2 * r in the carrier of I[01] by BORSUK_1:83,RCOMP_1:def 1;
then P.(2*r) = P.p by A2,SEQM_3:def 5;
hence thesis by A3,A5,A6,Def4;
suppose A8: r >= 1/2;
then r * 2 >= 1/2 * 2 by AXIOMS:25;
then 2 * r >= 1 + 0;
then A9: 2 * r - 1 >= 0 by REAL_1:84;
r * 2 <= 1 * 2 by A5,AXIOMS:25;
then 2 * r - 1 <= 2 - 1 by REAL_1:92;
then 2 * r - 1 in { e where e is Real : 0 <= e & e <= 1 } by A9;
then 2 * r - 1 in the carrier of I[01] by BORSUK_1:83,RCOMP_1:def 1;
then P.(2*r-1) = P.p by A2,SEQM_3:def 5;
hence thesis by A3,A5,A8,Def4;
end;
hence thesis by A1,A2,FUNCT_1:9;
end;
definition let T be non empty TopSpace,
a be Point of T,
P be constant Path of a, a;
cluster P + P -> constant;
coherence by Th7;
end;
definition let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a, b;
given f be map of I[01], T such that
A1:f is continuous & f.0 = a & f.1 = b;
func - P -> Path of b, a means :Def5:
for t being Point of I[01], t' being Real st t = t' holds
it.t = P.(1-t');
existence
proof
set e = L[01]((0,1)(#),(#)(0,1));
A2: e.0 = e.(#)(0,1) by TREAL_1:def 1
.= (0,1)(#) by TREAL_1:12
.= 1 by TREAL_1:def 2;
A3: e.1 = e.(0,1)(#) by TREAL_1:def 2
.= (#)(0,1) by TREAL_1:12
.= 0 by TREAL_1:def 1;
set f = P * e;
f is Function of the carrier of Closed-Interval-TSpace (0,1),
the carrier of T by FUNCT_2:19,TOPMETR:27;
then reconsider f as map of I[01], T by TOPMETR:27;
A4: for t being Point of I[01], t' being Real st t = t' holds
f.t = P.(1-t')
proof
let t be Point of I[01], t' be Real; assume A5: t = t';
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:27;
A6: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
t in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:27;
then t in dom e by FUNCT_2:def 1;
then f.t = P.(e.ee) by FUNCT_1:23
.= P.((0-1)*t' + 1) by A5,A6,TREAL_1:10
.= P.((-1)*t' + 1)
.= P.(1 + -1*t') by XCMPLX_1:175
.= P.(1 - 1*t') by XCMPLX_0:def 8;
hence thesis;
end;
0 in { r : 0 <= r & r <= 1 };
then 0 in [.0,1.] by RCOMP_1:def 1;
then 0 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:25;
then 0 in dom e by FUNCT_2:def 1;
then A7: f.0 = P.1 by A2,FUNCT_1:23
.= b by A1,Def1;
1 in { r : 0 <= r & r <= 1 };
then 1 in [.0,1.] by RCOMP_1:def 1;
then 1 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:25;
then 1 in dom e by FUNCT_2:def 1;
then A8: f.1 = P.0 by A3,FUNCT_1:23
.= a by A1,Def1;
A9: P is continuous by A1,Def1;
e is continuous map of
Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(0,1)
by TREAL_1:11;
then f is continuous by A9,TOPMETR:27,TOPS_2:58;
then reconsider f as Path of b, a by A7,A8,Def1;
take f;
thus thesis by A4;
end;
uniqueness
proof
let R, Q be Path of b, a such that
A10: for t being Point of I[01], t' being Real st t = t' holds
R.t = P.(1-t') and
A11: for t being Point of I[01], t' being Real st t = t' holds
Q.t = P.(1-t');
A12: dom R = the carrier of I[01] by FUNCT_2:def 1;
A13: the carrier of I[01] = dom Q by FUNCT_2:def 1;
for x be set st x in the carrier of I[01] holds R.x = Q.x
proof
let x be set; assume A14: x in the carrier of I[01];
then reconsider x' = x as Point of I[01];
reconsider x2 = x as Real by A14,BORSUK_1:83;
R.x' = P.(1-x2) by A10
.= Q.x' by A11;
hence thesis;
end;
hence thesis by A12,A13,FUNCT_1:9;
end;
end;
Lm2:
for r be Real st 0 <= r & r <= 1 holds 0 <= 1-r & 1-r <= 1
proof
let r be Real; assume 0 <= r & r <= 1;
then 1-1 <= 1-r & 1-r <= 1-0 by REAL_1:92;
hence thesis;
end;
Lm3:
for r being Real holds
0 <= r & r <= 1 iff r in the carrier of I[01]
proof
let r be Real;
A1: [.0,1.] = { r1 where r1 is Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;
hence 0 <= r & r <= 1 implies r in the carrier of I[01] by BORSUK_1:83;
assume r in the carrier of I[01];
then consider r2 being Real such that A2: r2 = r & 0 <= r2 & r2 <= 1
by A1,BORSUK_1:83;
thus thesis by A2;
end;
Lm4:
for r being Real st r in the carrier of I[01] holds
1-r in the carrier of I[01]
proof
let r be Real;
assume r in the carrier of I[01];
then 0 <= r & r <= 1 by Lm3;
then 0 <= 1-r & 1-r <= 1 by Lm2;
hence thesis by Lm3;
end;
theorem Th8:
for T being non empty TopSpace,
a being Point of T,
P being constant Path of a, a holds - P = P
proof
let T be non empty TopSpace,
a be Point of T,
P be constant Path of a, a;
A1: ex f be map of I[01], T st f is continuous & f.0 = a & f.1 = a by Th4;
A2: dom (-P) = the carrier of I[01] by FUNCT_2:def 1;
A3: dom P = the carrier of I[01] by FUNCT_2:def 1;
for x be set st x in the carrier of I[01] holds P.x = (-P).x
proof
let x be set; assume A4: x in the carrier of I[01];
then reconsider x2 = x as Real by BORSUK_1:83;
reconsider x3 = 1 - x2 as Point of I[01] by A4,Lm4;
(-P).x = P.x3 by A1,A4,Def5
.= P.x by A3,A4,SEQM_3:def 5;
hence thesis;
end;
hence thesis by A2,A3,FUNCT_1:9;
end;
definition let T be non empty TopSpace,
a be Point of T,
P be constant Path of a, a;
cluster - P -> constant;
coherence by Th8;
end;
begin :: The product of two topological spaces
theorem Th9:
for X, Y being non empty TopSpace
for A being Subset-Family of Y
for f being map of X, Y holds
f"(union A) = union (f"A)
proof
let X, Y be non empty TopSpace;
let A be Subset-Family of Y;
let f be map of X, Y;
thus thesis
proof
thus f"(union A) c= union (f"A)
proof
let x be set;
reconsider uA = union A as Subset of Y;
assume
A1: x in f"(union A);
then f.x in uA by FUNCT_2:46;
then consider YY being set such that
A2: f.x in YY & YY in A by TARSKI:def 4;
reconsider fY = f"YY as Subset of X;
A3: fY in f"A by A2,WEIERSTR:def 1;
x in f"YY by A1,A2,FUNCT_2:46;
hence thesis by A3,TARSKI:def 4;
end;
thus union (f"A) c= f"(union A)
proof
let x be set;
assume x in union (f"A);
then consider YY be set such that
A4: x in YY & YY in f"A by TARSKI:def 4;
reconsider B1 = YY as Subset of X by A4;
consider B being Subset of Y such that
A5: B in A & B1 = f"B by A4,WEIERSTR:def 1;
f.x in B by A4,A5,FUNCT_1:def 13;
then A6: f.x in union A by A5,TARSKI:def 4;
x in the carrier of X by A4;
then x in dom f by FUNCT_2:def 1;
hence thesis by A6,FUNCT_1:def 13;
end;
end;
end;
definition let S1, S2, T1, T2 be non empty TopSpace;
let f be map of S1, S2, g be map of T1, T2;
redefine func [:f, g:] -> map of [:S1, T1:], [:S2, T2:];
coherence
proof
set h = [:f, g:];
A1: dom h = [:the carrier of S1, the carrier of T1:] by FUNCT_2:def 1
.= the carrier of [:S1, T1:] by BORSUK_1:def 5;
rng h c= [:the carrier of S2, the carrier of T2:]
by RELSET_1:12;
then rng h c= the carrier of [:S2, T2:] by BORSUK_1:def 5;
then h is Function of the carrier of [:S1, T1:], the carrier of [:S2, T2:]
by A1,FUNCT_2:def 1,RELSET_1:11;
hence thesis ;
end;
end;
theorem Th10:
for S1, S2, T1, T2 be non empty TopSpace,
f be continuous map of S1, T1,
g be continuous map of S2, T2,
P1, P2 being Subset of [:T1, T2:] holds
(P2 in Base-Appr P1 implies [:f,g:]"P2 is open)
proof
let S1, S2, T1, T2 be non empty TopSpace,
f be continuous map of S1, T1,
g be continuous map of S2, T2,
P1, P2 be Subset of [:T1, T2:];
assume P2 in Base-Appr P1;
then P2 in { [:X1,Y1:] where X1 is Subset of T1,
Y1 is Subset of T2:
[:X1,Y1:] c= P1 & X1 is open & Y1 is open} by BORSUK_1:def 6;
then consider X11 be Subset of T1,
Y11 be Subset of T2 such that
A1: P2 = [:X11,Y11:] & [:X11,Y11:] c= P1 & X11 is open & Y11 is open;
A2:[:f,g:]"P2 = [:f"X11, g"Y11:] by A1,FUNCT_3:94;
f"X11 is open & g"Y11 is open by A1,TOPS_2:55;
hence thesis by A2,BORSUK_1:46;
end;
theorem Th11:
for S1, S2, T1, T2 be non empty TopSpace,
f be continuous map of S1, T1,
g be continuous map of S2, T2,
P2 being Subset of [:T1, T2:] holds
(P2 is open implies [:f,g:]"P2 is open)
proof
let S1, S2, T1, T2 be non empty TopSpace,
f be continuous map of S1, T1,
g be continuous map of S2, T2,
P2 be Subset of [:T1, T2:];
assume P2 is open;
then P2 = union Base-Appr P2 by BORSUK_1:54;
then A1: [:f,g:]"(P2 qua Subset of [:T1, T2:]) =
union ([:f,g:]"Base-Appr P2) by Th9;
reconsider Kill = [:f,g:]"Base-Appr P2 as Subset-Family of [:S1, S2:];
for P being Subset of [:S1, S2:] holds P in Kill implies P is open
proof
let P be Subset of [:S1, S2:];
assume P in Kill;
then consider B being Subset of [:T1, T2:] such that
A2: B in Base-Appr P2 & P = [:f,g:]"B by WEIERSTR:def 1;
reconsider B as Subset of [:T1, T2:];
[:f,g:]"B is open by A2,Th10;
hence P is open by A2;
end;
then Kill is open by TOPS_2:def 1; hence thesis by A1,TOPS_2:26;
end;
theorem Th12:
for S1, S2, T1, T2 be non empty TopSpace,
f be continuous map of S1, T1,
g be continuous map of S2, T2 holds
[:f,g:] is continuous
proof
let S1, S2, T1, T2 be non empty TopSpace,
f be continuous map of S1, T1,
g be continuous map of S2, T2;
for P1 be Subset of [:T1, T2:] st P1 is open holds
[:f,g:]"P1 is open by Th11;
hence thesis by TOPS_2:55;
end;
definition
cluster empty -> T_0 TopStruct;
coherence by T_0TOPSP:def 7;
end;
definition let T1, T2 be discerning (non empty TopSpace);
cluster [:T1, T2:] -> discerning;
coherence
proof
set T = [:T1,T2:];
now let p,q be Point of T; assume A1: p <> q;
p in the carrier of T & q in the carrier of T;
then A2: p in [:the carrier of T1, the carrier of T2:] &
q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 5;
then consider x,y be set such that
A3: x in the carrier of T1 & y in
the carrier of T2 & p = [x,y] by ZFMISC_1:def 2;
consider z,v be set such that
A4: z in the carrier of T1 & v in the carrier of T2 & q = [z,v]
by A2,ZFMISC_1:def 2;
reconsider x, z as Point of T1 by A3,A4;
reconsider y, v as Point of T2 by A3,A4;
per cases;
suppose x <> z;
then consider V1 being Subset of T1 such that
A5: V1 is open &
((x in V1 & not z in V1) or (z in V1 & not x in V1)) by T_0TOPSP:def 7;
A6: [#]T2 is open by TOPS_1:53;
A7: y in [#]T2 & v in [#]T2 by A3,A4,PRE_TOPC:12;
set X = [:V1, [#]T2:];
A8: X is open by A5,A6,BORSUK_1:46;
now per cases by A5;
suppose x in V1 & not z in V1;
hence (p in X & not q in X) or (q in X & not p in
X) by A3,A4,A7,ZFMISC_1:106;
suppose z in V1 & not x in V1;
hence (p in X & not q in X) or (q in X & not p in
X) by A3,A4,A7,ZFMISC_1:106;
end;
hence ex X being Subset of T st X is open &
((p in X & not q in X) or (q in X & not p in X)) by A8;
suppose x = z;
then consider V1 being Subset of T2 such that
A9: V1 is open &
((y in V1 & not v in V1) or (v in V1 & not y in V1))
by A1,A3,A4,T_0TOPSP:def 7;
A10: [#]T1 is open by TOPS_1:53;
A11: x in [#]T1 & z in [#]T1 by A3,A4,PRE_TOPC:12;
set X = [:[#]T1, V1:];
A12: X is open by A9,A10,BORSUK_1:46;
now per cases by A9;
suppose y in V1 & not v in V1;
hence (p in X & not q in X) or (q in X & not p in X)
by A3,A4,A11,ZFMISC_1:106;
suppose v in V1 & not y in V1;
hence (p in X & not q in X) or (q in X & not p in X)
by A3,A4,A11,ZFMISC_1:106;
end;
hence ex X being Subset of T st X is open &
((p in X & not q in X) or (q in X & not p in X)) by A12;
end;
hence thesis by T_0TOPSP:def 7;
end;
end;
canceled;
theorem Th14:
for T1, T2 be non empty TopSpace holds
T1 is_T1 & T2 is_T1 implies [:T1, T2:] is_T1
proof
let T1, T2 be non empty TopSpace;
assume A1: T1 is_T1 & T2 is_T1;
set T = [:T1, T2:];
T is_T1
proof
let p,q be Point of T;
assume A2: p <> q;
p in the carrier of T & q in the carrier of T;
then A3: p in [:the carrier of T1, the carrier of T2:] &
q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 5;
then consider x,y be set such that
A4: x in the carrier of T1 & y in
the carrier of T2 & p = [x,y] by ZFMISC_1:def 2;
consider z,v be set such that
A5: z in the carrier of T1 & v in the carrier of T2 & q = [z,v]
by A3,ZFMISC_1:def 2;
reconsider x, z as Point of T1 by A4,A5;
reconsider y, v as Point of T2 by A4,A5;
per cases;
suppose x <> z;
then consider Y, V be Subset of T1 such that
A6: Y is open & V is open &
x in Y & not z in Y & z in V & not x in V by A1,URYSOHN1:def 9;
A7: [#]T2 is open by TOPS_1:53;
A8: y in [#]T2 & v in [#]T2 by A4,A5,PRE_TOPC:12;
set X = [:Y, [#]T2:], Z = [:V, [#]T2:];
A9: X is open & Z is open by A6,A7,BORSUK_1:46;
A10: p in X & q in Z by A4,A5,A6,A8,ZFMISC_1:106;
not q in X & not p in Z by A4,A5,A6,ZFMISC_1:106;
hence thesis by A9,A10;
suppose A11: x = z;
then consider Y, V be Subset of T2 such that
A12: Y is open & V is open &
y in Y & not v in Y & v in V & not y in V by A1,A2,A4,A5,URYSOHN1:def 9;
reconsider Y, V as Subset of T2;
A13: [#]T1 is open by TOPS_1:53;
A14: x in [#]T1 & z in [#]T1 by A4,A11,PRE_TOPC:12;
set X = [:[#]T1, Y:], Z = [:[#]T1, V:];
A15: X is open & Z is open by A12,A13,BORSUK_1:46;
A16: p in X & q in Z by A4,A5,A12,A14,ZFMISC_1:106;
not p in Z & not q in X by A4,A5,A12,ZFMISC_1:106;
hence thesis by A15,A16;
end;
hence thesis;
end;
definition let T1, T2 be being_T1 (non empty TopSpace);
cluster [:T1, T2:] -> being_T1;
coherence by Th14;
end;
Lm5:
for T1, T2 be non empty TopSpace holds
T1 is_T2 & T2 is_T2 implies [:T1, T2:] is_T2
proof
let T1, T2 be non empty TopSpace;
assume A1: T1 is_T2 & T2 is_T2;
set T = [:T1, T2:];
T is_T2
proof
let p,q be Point of T;
assume A2: p <> q;
p in the carrier of T & q in the carrier of T;
then A3: p in [:the carrier of T1, the carrier of T2:] &
q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 5;
then consider x,y be set such that
A4: x in the carrier of T1 & y in
the carrier of T2 & p = [x,y] by ZFMISC_1:def 2;
consider z,v be set such that
A5: z in the carrier of T1 & v in the carrier of T2 & q = [z,v]
by A3,ZFMISC_1:def 2;
reconsider x, z as Point of T1 by A4,A5;
reconsider y, v as Point of T2 by A4,A5;
per cases;
suppose x <> z;
then consider Y, V be Subset of T1 such that
A6: Y is open & V is open &
x in Y & z in V & Y misses V by A1,COMPTS_1:def 4;
reconsider Y, V as Subset of T1;
A7: [#]T2 is open by TOPS_1:53;
A8: y in [#]T2 & v in [#]T2 by A4,A5,PRE_TOPC:12;
reconsider X = [:Y, [#]T2:], Z = [:V, [#]T2:] as Subset of T;
A9: X is open & Z is open by A6,A7,BORSUK_1:46;
p in X & q in Z & X misses Z by A4,A5,A6,A8,ZFMISC_1:106,127;
hence thesis by A9;
suppose A10: x = z;
then consider Y, V be Subset of T2 such that
A11: Y is open & V is open &
y in Y & v in V & Y misses V by A1,A2,A4,A5,COMPTS_1:def 4;
reconsider Y, V as Subset of T2;
A12: [#]T1 is open by TOPS_1:53;
A13: x in [#]T1 & z in [#]T1 by A4,A10,PRE_TOPC:12;
reconsider X = [:[#]T1, Y:], Z = [:[#]T1, V:] as Subset of T;
A14: X is open & Z is open by A11,A12,BORSUK_1:46;
p in X & q in Z & X misses Z by A4,A5,A11,A13,ZFMISC_1:106,127;
hence thesis by A14;
end;
hence thesis;
end;
definition let T1, T2 be being_T2 (non empty TopSpace);
cluster [:T1, T2:] -> being_T2;
coherence by Lm5;
end;
definition
cluster I[01] -> compact being_T2;
coherence
proof
I[01] = TopSpaceMetr (Closed-Interval-MSpace(0,1)) by TOPMETR:27,def 8;
hence thesis by HEINE:11,PCOMPS_1:38,TOPMETR:27;
end;
end;
definition let n be Nat;
cluster TOP-REAL n -> being_T2;
coherence by SPPOL_1:26;
end;
definition let T be non empty arcwise_connected TopSpace;
let a, b be Point of T;
let P, Q be Path of a, b;
pred P, Q are_homotopic means
ex f being map of [:I[01],I[01]:], T st
f is continuous &
for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = Q.s &
for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b;
reflexivity
proof
let P be Path of a, b;
defpred Z[set, set] means $2 = P.($1`1);
A1: for x be set st x in [:the carrier of I[01], the carrier of I[01]:]
ex y be set st y in the carrier of T & Z[x,y]
proof
let x be set;
assume x in [:the carrier of I[01], the carrier of I[01]:];
then x`1 in the carrier of I[01] by MCART_1:10;
then P.(x`1) in the carrier of T by FUNCT_2:7;
hence thesis;
end;
consider f being Function of
[:the carrier of I[01], the carrier of I[01]:], the carrier of T
such that
A2: for x being set st x in [:the carrier of I[01], the carrier of I[01]:]
holds Z[x, f.x] from FuncEx1(A1);
the carrier of [:I[01],I[01]:]
= [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5;
then reconsider f as Function of the carrier of [:I[01],I[01]:],
the carrier of T;
reconsider f as map of [:I[01],I[01]:], T ;
ex f being map of [:I[01],I[01]:], T st
f is continuous &
for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = P.s &
for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b
proof
take f;
A3: for W being Point of [:I[01], I[01]:],
G being a_neighborhood of f.W
ex H being a_neighborhood of W st f.:H c= G
proof
let W be Point of [:I[01], I[01]:],
G be a_neighborhood of f.W;
W in the carrier of [:I[01], I[01]:];
then A4: W in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 5
;
then reconsider W1 = W`1 as Point of I[01] by MCART_1:10;
reconsider G' = G as a_neighborhood of P.W1 by A2,A4;
consider H be a_neighborhood of W1 such that
A5: P.:H c= G' by BORSUK_1:def 2;
A6: W1 in Int H by CONNSP_2:def 1;
set HH = [:H, the carrier of I[01]:];
HH c= [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:118;
then HH c= the carrier of [:I[01], I[01]:] by BORSUK_1:def 5;
then reconsider HH as Subset of [:I[01], I[01]:];
the carrier of I[01] c= the carrier of I[01];
then reconsider AI = the carrier of I[01] as Subset of
I[01];
A7: AI = [#]I[01] by PRE_TOPC:12;
A8: Int HH = [:Int H, Int AI:] by BORSUK_1:47;
A9: ex x,y be set st [x,y] = W by A4,ZFMISC_1:102;
Int AI = the carrier of I[01] by A7,TOPS_1:43;
then W`2 in Int AI by A4,MCART_1:10;
then W in Int HH by A6,A8,A9,MCART_1:11;
then reconsider HH as a_neighborhood of W by CONNSP_2:def 1;
take HH;
f.:HH c= G
proof
let a be set; assume a in f.:HH;
then consider b be set such that
A10: b in dom f & b in HH & a = f.b by FUNCT_1:def 12;
A11: dom f = [:the carrier of I[01], the carrier of I[01]:] by FUNCT_2:def 1;
reconsider b as Point of [:I[01], I[01]:] by A10;
dom P = the carrier of I[01] by FUNCT_2:def 1;
then A12: b`1 in H & b`1 in dom P by A10,A11,MCART_1:10;
f.b = P.(b`1) by A2,A10,A11;
then f.b in P.:H by A12,FUNCT_1:def 12;
hence thesis by A5,A10;
end;
hence thesis;
end;
A13: for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = P.s
proof
let s be Point of I[01];
reconsider s0 = [s,0], s1 = [s,1] as set;
s in the carrier of I[01] & 0 in the carrier of I[01] &
1 in the carrier of I[01] by Lm3;
then s0 in [:the carrier of I[01], the carrier of I[01]:] &
s1 in [:the carrier of I[01], the carrier of I[01]:]
by ZFMISC_1:106;
then A14: Z[s0, f.s0] & Z[s1, f.s1] by A2;
A15: f.(s,0) = f.s0 by BINOP_1:def 1
.= P.s by A14,MCART_1:7;
f.(s,1) = f.s1 by BINOP_1:def 1
.= P.s by A14,MCART_1:7;
hence thesis by A15;
end;
for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b
proof
let t be Point of I[01];
reconsider t0 = [0,t], t1 = [1,t] as set;
A16: P.0 = a & P.1 = b by Def3;
t in the carrier of I[01] & 0 in the carrier of I[01] &
1 in the carrier of I[01] by Lm3;
then t0 in [:the carrier of I[01], the carrier of I[01]:] &
t1 in [:the carrier of I[01], the carrier of I[01]:]
by ZFMISC_1:106;
then f.t0 = P.(t0`1) & f.t1 = P.(t1`1) by A2;
then f.(0,t) = P.(t0`1) & f.(1,t) = P.(t1`1) by BINOP_1:def 1;
hence thesis by A16,MCART_1:7;
end;
hence thesis by A3,A13,BORSUK_1:def 2;
end;
hence thesis;
end;
symmetry
proof
let P, Q be Path of a, b;
given f being map of [:I[01],I[01]:], T such that
A17: f is continuous &
for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = Q.s &
for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b;
id the carrier of I[01] = id I[01] by GRCAT_1:def 11;
then reconsider fA = id the carrier of I[01] as continuous map
of I[01], I[01];
reconsider fB = L[01]((0,1)(#),(#)(0,1)) as continuous map of I[01], I[01]
by TOPMETR:27,TREAL_1:11;
set F = [:fA, fB:];
A18: F is continuous by Th12;
A19:dom L[01]((0,1)(#),(#)(0,1)) = the carrier of I[01] by FUNCT_2:def 1,
TOPMETR:27;
set LL = L[01]((0,1)(#),(#)(0,1));
reconsider ff=f * F as map of [:I[01],I[01]:], T;
A20: ff is continuous by A17,A18,TOPS_2:58;
A21: for s being Point of I[01] holds ff.(s,0) = Q.s & ff.(s,1) = P.s
proof
let s be Point of I[01];
A22: for t being Point of I[01], t' being Real st t = t' holds
LL.t = 1-t'
proof
let t be Point of I[01], t' be Real; assume A23: t = t';
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:27;
A24: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
LL.t = LL.ee
.= ((0-1)*t' + 1) by A23,A24,TREAL_1:10
.= ((-1)*t' + 1)
.= (1 + -1*t') by XCMPLX_1:175
.= (1 - 1*t') by XCMPLX_0:def 8;
hence thesis;
end;
dom id the carrier of I[01] = the carrier of I[01] by FUNCT_2:def 1;
then A25: s in dom id the carrier of I[01] & 0 in dom LL &
1 in dom L[01]((0,1)(#),(#)(0,1)) by A19,Lm3;
then A26: F.([s,0]) = [(id the carrier of I[01]).s,LL.0]
by FUNCT_3:def 9
.= [s, LL.0[01]] by BORSUK_1:def 17,FUNCT_1:35
.= [s, 1 - 0] by A22,BORSUK_1:def 17
.= [s, 1];
A27: F.([s,1]) = [(id the carrier of I[01]).s,(L[01]((0,1)(#),(#)(0,1))).1]
by A25,FUNCT_3:def 9
.= [s,LL.1[01]] by BORSUK_1:def 18,FUNCT_1:35
.= [s,1 - 1] by A22,BORSUK_1:def 18
.= [s,0];
A28: dom F = [:dom id the carrier of I[01],
dom L[01]((0,1)(#),(#)(0,1)):] by FUNCT_3:def 9;
then A29: [s,1] in dom F by A25,ZFMISC_1:106;
A30: [s,0] in dom F by A25,A28,ZFMISC_1:106;
A31: ff.(s,0) = ff.([s,0]) by BINOP_1:def 1
.= f.(F.([s,0])) by A30,FUNCT_1:23
.= f.(s,1) by A26,BINOP_1:def 1
.= Q.s by A17;
ff.(s,1) = ff.([s,1]) by BINOP_1:def 1
.= f.(F.([s,1])) by A29,FUNCT_1:23
.= f.(s,0) by A27,BINOP_1:def 1
.= P.s by A17;
hence thesis by A31;
end;
for t being Point of I[01] holds ff.(0,t) = a & ff.(1,t) = b
proof
let t be Point of I[01];
A32: t in the carrier of I[01];
A33: dom L[01]((0,1)(#),(#)(0,1)) = the carrier of I[01] by FUNCT_2:def 1,
TOPMETR:27;
reconsider tt = t as Real by A32,BORSUK_1:83;
for t being Point of I[01], t' being Real st t = t' holds
LL.t = 1-t'
proof
let t be Point of I[01], t' be Real; assume A34: t = t';
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:27;
A35: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
LL.t = LL.ee
.= ((0-1)*t' + 1) by A34,A35,TREAL_1:10
.= ((-1)*t' + 1)
.= (1 + -1*t') by XCMPLX_1:175
.= (1 - 1*t') by XCMPLX_0:def 8;
hence thesis;
end;
then A36: (L[01]((0,1)(#),(#)(0,1))).t = 1 - tt;
A37: dom id the carrier of I[01] = the carrier of I[01] by FUNCT_2:def 1;
then A38: 0 in dom id the carrier of I[01] & 1 in dom id the carrier of I[01] &
t in dom L[01]((0,1)(#),(#)(0,1)) by A33,Lm3;
then A39: F.([0,t]) = [(id the carrier of I[01]).0,(L[01]((0,1)(#),(#)(0,1))).t
]
by FUNCT_3:def 9
.= [0,1 - tt] by A36,A37,A38,FUNCT_1:35;
A40: F.([1,t]) = [(id the carrier of I[01]).1,(L[01]((0,1)(#),(#)(0,1))).t]
by A38,FUNCT_3:def 9
.= [1,1 - tt] by A36,A37,A38,FUNCT_1:35;
reconsider t' = 1 - tt as Point of I[01] by Lm4;
A41: dom F = [:dom id the carrier of I[01],
dom L[01]((0,1)(#),(#)(0,1)):] by FUNCT_3:def 9;
then A42: [1,t] in dom F by A38,ZFMISC_1:106;
A43: [0,t] in dom F by A38,A41,ZFMISC_1:106;
A44: ff.(0,t) = ff.([0,t]) by BINOP_1:def 1
.= f.(F.([0,t])) by A43,FUNCT_1:23
.= f.(0,t') by A39,BINOP_1:def 1
.= a by A17;
ff.(1,t) = ff.([1,t]) by BINOP_1:def 1
.= f.(F.([1,t])) by A42,FUNCT_1:23
.= f.(1,t') by A40,BINOP_1:def 1
.= b by A17;
hence thesis by A44;
end;
hence thesis by A20,A21;
end;
end;