:: The Fundamental Group of the Circle
:: by Artur Korni{\l}owicz
::
:: Received February 22, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, EUCLID, CARD_1, STRUCT_0, BORSUK_1, TOPMETR, TARSKI,
ZFMISC_1, PRE_TOPC, SUBSET_1, RELAT_1, ARYTM_1, XXREAL_0, ARYTM_3,
GR_CY_1, FINSET_1, ORDINAL1, METRIC_1, XXREAL_1, XBOOLE_0, REAL_1,
RLVECT_3, PBOOLE, FUNCT_1, CARD_3, RELAT_2, PCOMPS_1, FRECHET, CONNSP_1,
CONNSP_3, RCOMP_1, CONNSP_2, TOPS_1, TOPS_2, ORDINAL2, T_0TOPSP,
CANTOR_1, SETFAM_1, GRAPH_1, BORSUK_6, TOPREALB, SUPINF_2, SIN_COS,
COMPLEX1, SQUARE_1, MCART_1, INT_1, ALGSTR_1, TAXONOM2, TEX_2, RCOMP_3,
FINSEQ_1, FUNCT_4, COMPTS_1, FUNCOP_1, BORSUK_2, TOPALG_1, EQREL_1,
WAYBEL20, TOPALG_2, GROUP_6, ALGSTR_0, JGRAPH_2, FUNCT_2, WELLORD1,
TOPREAL2, TOPALG_5, MSSUBFAM, MEASURE5, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, RELAT_1,
EQREL_1, FUNCT_1, PBOOLE, CARD_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
FINSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, INT_1, NAT_1,
SEQM_3, FINSEQ_1, FUNCT_4, RCOMP_1, DOMAIN_1, STRUCT_0, ALGSTR_0,
PRE_TOPC, TOPS_1, GR_CY_1, GROUP_6, METRIC_1, CANTOR_1, YELLOW_8,
BORSUK_1, TOPS_2, COMPTS_1, CONNSP_1, CONNSP_2, CONNSP_3, TEX_2, TSEP_1,
TOPMETR, EUCLID, PCOMPS_1, FRECHET, BORSUK_2, SIN_COS, BORSUK_3, FCONT_1,
TAXONOM2, BORSUK_6, TOPALG_1, TOPREAL9, TOPALG_2, TOPREALB, RCOMP_3,
XXREAL_0;
constructors SQUARE_1, BINARITH, SIN_COS, TOPS_1, CONNSP_1, FUNCOP_1,
COMPTS_1, GRCAT_1, TSEP_1, TEX_2, CANTOR_1, MONOID_0, CONNSP_3, YELLOW_8,
TAXONOM2, BORSUK_3, FCONT_1, TOPALG_1, TOPREAL9, TOPREALB, RCOMP_3,
BORSUK_6, SEQ_4, FRECHET, GROUP_6, FUNCT_4, REAL_1, BINOP_2;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1,
COMPTS_1, METRIC_1, BORSUK_1, TSEP_1, GR_CY_1, MONOID_0, EUCLID, TOPMETR,
BORSUK_2, YELLOW13, TOPALG_1, TOPALG_2, TOPALG_3, TOPREALB, RCOMP_3,
VALUED_0, XXREAL_2, FRECHET, CONNSP_1, GROUP_6, SQUARE_1, SIN_COS,
ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, BORSUK_2, TARSKI, XBOOLE_0,
CONNSP_1, T_0TOPSP, CONNSP_2, RCOMP_3, SETFAM_1;
equalities COMPTS_1, BINOP_1, GR_CY_1, STRUCT_0, BORSUK_1, ALGSTR_0, TOPALG_1;
expansions FUNCT_1, FUNCT_2, GROUP_6, TOPS_2, TSEP_1, BORSUK_2, COMPTS_1,
TARSKI, XBOOLE_0, CONNSP_1, CONNSP_2;
theorems GROUP_6, PRE_TOPC, XREAL_0, FUNCT_2, BORSUK_1, INT_1, SIN_COS,
EUCLID, JGRAPH_1, SQUARE_1, TOPREAL9, TOPALG_1, TOPS_2, BORSUK_3,
FUNCT_1, TOPMETR, JGRAPH_2, BORSUK_4, RELAT_1, FUNCOP_1, FCONT_1,
BORSUK_6, BORSUK_2, TOPALG_2, BINOP_1, TARSKI, ZFMISC_1, FUNCT_4, TSEP_1,
XBOOLE_1, COMPLEX2, SETFAM_1, XBOOLE_0, TAXONOM2, FINSEQ_3, NAT_1,
SEQM_3, FINSEQ_5, TEX_2, DOMAIN_1, TOPS_1, GOBOARD9, CONNSP_1, TOPALG_3,
TOPREALA, TOPREALB, FINSET_1, TOPS_3, CONNSP_3, CONNSP_2, TOPGRP_1,
XREAL_1, CANTOR_1, FRECHET, TOPGEN_2, CARD_3, RCOMP_3, XXREAL_0, CARD_1,
XXREAL_1, RLVECT_1, JORDAN16, XTUPLE_0;
schemes FUNCT_2, NAT_1, PBOOLE, BINOP_1;
begin :: Preliminaries
set o = |[0,0]|;
set I = the carrier of I[01];
set R = the carrier of R^1;
Lm1: 0 in INT by INT_1:def 1;
Lm2: 0 in I by BORSUK_1:43;
then
Lm3: {0} c= I by ZFMISC_1:31;
Lm4: 0 in {0} by TARSKI:def 1;
Lm5: the carrier of [:I[01],I[01]:] = [:I,I:] by BORSUK_1:def 2;
reconsider j0 = 0, j1 = 1 as Point of I[01] by BORSUK_1:def 14,def 15;
Lm6: [#]I[01] = I;
Lm7: I[01] | [#]I[01] = I[01] by TSEP_1:3;
Lm8: 1-0 <= 1;
Lm9: 3/2-1/2 <= 1;
registration
cluster INT.Group -> infinite;
coherence;
end;
reserve a, r, s for Real;
theorem Th1:
r <= s implies for p being Point of Closed-Interval-MSpace(r,s)
holds Ball(p,a) = [.r,s.] or Ball(p,a) = [.r,p+a.[ or Ball(p,a) = ].p-a,s.] or
Ball(p,a) = ].p-a,p+a.[
proof
set M = Closed-Interval-MSpace(r,s);
assume r <= s;
then
A1: the carrier of M = [.r,s.] by TOPMETR:10;
let p be Point of M;
set B = Ball(p,a);
reconsider p1 = p as Point of RealSpace by TOPMETR:8;
set B1 = Ball(p1,a);
A2: B = B1 /\ the carrier of M by TOPMETR:9;
A3: B1 = ].p1-a, p1+a.[ by FRECHET:7;
per cases;
suppose that
A4: p1+a <= s and
A5: p1-a < r;
B = [.r,p1+a.[
proof
thus B c= [.r,p1+a.[
proof
let b be object;
assume
A6: b in B;
then reconsider b as Element of B;
b in B1 by A2,A6,XBOOLE_0:def 4;
then
A7: b < p1+a by A3,XXREAL_1:4;
r <= b by A1,A6,XXREAL_1:1;
hence thesis by A7,XXREAL_1:3;
end;
let b be object;
assume
A8: b in [.r,p1+a.[;
then reconsider b as Real;
A9: r <= b by A8,XXREAL_1:3;
A10: b < p1+a by A8,XXREAL_1:3;
then b <= s by A4,XXREAL_0:2;
then
A11: b in [.r,s.] by A9,XXREAL_1:1;
p1-a < b by A5,A9,XXREAL_0:2;
then b in B1 by A3,A10,XXREAL_1:4;
hence thesis by A1,A2,A11,XBOOLE_0:def 4;
end;
hence thesis;
end;
suppose that
A12: p1+a <= s and
A13: p1-a >= r;
B = ].p1-a,p1+a.[
proof
thus B c= ].p1-a,p1+a.[ by A2,A3,XBOOLE_1:17;
let b be object;
assume
A14: b in ].p1-a,p1+a.[;
then reconsider b as Real;
b < p1+a by A14,XXREAL_1:4;
then
A15: b <= s by A12,XXREAL_0:2;
p1-a <= b by A14,XXREAL_1:4;
then r <= b by A13,XXREAL_0:2;
then b in [.r,s.] by A15,XXREAL_1:1;
hence thesis by A1,A2,A3,A14,XBOOLE_0:def 4;
end;
hence thesis;
end;
suppose that
A16: p1+a > s and
A17: p1-a < r;
B = [.r,s.]
proof
thus B c= [.r,s.] by A1;
let b be object;
assume
A18: b in [.r,s.];
then reconsider b as Real;
b <= s by A18,XXREAL_1:1;
then
A19: b < p1+a by A16,XXREAL_0:2;
r <= b by A18,XXREAL_1:1;
then p1-a < b by A17,XXREAL_0:2;
then b in B1 by A3,A19,XXREAL_1:4;
hence thesis by A1,A2,A18,XBOOLE_0:def 4;
end;
hence thesis;
end;
suppose that
A20: p1+a > s and
A21: p1-a >= r;
B = ].p1-a,s.]
proof
thus B c= ].p1-a,s.]
proof
let b be object;
assume
A22: b in B;
then reconsider b as Element of B;
b in B1 by A2,A22,XBOOLE_0:def 4;
then
A23: p1-a < b by A3,XXREAL_1:4;
b <= s by A1,A22,XXREAL_1:1;
hence thesis by A23,XXREAL_1:2;
end;
let b be object;
assume
A24: b in ].p1-a,s.];
then reconsider b as Real;
A25: b <= s by A24,XXREAL_1:2;
A26: p1-a < b by A24,XXREAL_1:2;
then r <= b by A21,XXREAL_0:2;
then
A27: b in [.r,s.] by A25,XXREAL_1:1;
b < p1+a by A20,A25,XXREAL_0:2;
then b in B1 by A3,A26,XXREAL_1:4;
hence thesis by A1,A2,A27,XBOOLE_0:def 4;
end;
hence thesis;
end;
end;
theorem Th2:
r <= s implies ex B being Basis of Closed-Interval-TSpace(r,s) st
(ex f being ManySortedSet of Closed-Interval-TSpace(r,s) st for y being Point
of Closed-Interval-MSpace(r,s)
holds f.y = {Ball(y,1/n) where n is Nat: n <> 0}
& B = Union f) & for X being Subset of Closed-Interval-TSpace(r,s)
st X in B holds X is connected
proof
set L = Closed-Interval-TSpace(r,s), M = Closed-Interval-MSpace(r,s);
assume
A1: r <= s;
defpred P[object,object] means
ex x being Point of L, y being Point of M, B being
Basis of x st $1 = x & x = y & $2 = B &
B = {Ball(y,1/n) where n is Nat: n <> 0};
A2: L = TopSpaceMetr(M) by TOPMETR:def 7;
A3: for i being object st i in the carrier of L ex j being object st P[i,j]
proof
let i be object;
assume i in the carrier of L;
then reconsider i as Point of L;
reconsider m = i as Point of M by A2,TOPMETR:12;
reconsider j = i as Element of TopSpaceMetr(M) by A2;
set B = Balls(j);
A4: ex y being Point of M st y = j &
B = { Ball(y,1/n) where n is Nat: n <> 0 } by FRECHET:def 1;
reconsider B1 = B as Basis of i by A2;
take B, i, m, B1;
thus thesis by A4;
end;
consider f being ManySortedSet of the carrier of L such that
A5: for i being object st i in the carrier of L holds P[i,f.i] from PBOOLE:
sch 3(A3);
for x being Element of L holds f.x is Basis of x
proof
let x be Element of L;
P[x,f.x] by A5;
hence thesis;
end;
then reconsider B = Union f as Basis of L by TOPGEN_2:2;
take B;
hereby
take f;
let x be Point of M;
the carrier of M = [.r,s.] by A1,TOPMETR:10
.= the carrier of L by A1,TOPMETR:18;
then P[x,f.x] by A5;
hence f.x = {Ball(x,1/n) where n is Nat: n <> 0} & B = Union f;
end;
let X be Subset of L;
assume X in B;
then X in union rng f by CARD_3:def 4;
then consider Z being set such that
A6: X in Z and
A7: Z in rng f by TARSKI:def 4;
consider x being object such that
A8: x in dom f and
A9: f.x = Z by A7,FUNCT_1:def 3;
consider
x1 being Point of L, y being Point of M, B1 being Basis of x1 such
that
x = x1 and
x1 = y and
A10: f.x = B1 & B1 = {Ball(y,1/n) where n is Nat: n <> 0} by A5,A8;
consider n being Nat such that
A11: X = Ball(y,1/n) and
n <> 0 by A6,A9,A10;
reconsider X1 = X as Subset of R^1 by PRE_TOPC:11;
Ball(y,1/n) = [.r,s.] or Ball(y,1/n) = [.r,y+1/n.[ or Ball(y,1/n) = ].y
-1/n,s.] or Ball(y,1/n) = ].y-1/n,y+1/n.[ by A1,Th1;
then X1 is connected by A11;
hence thesis by CONNSP_1:23;
end;
theorem Th3:
for T being TopStruct, A being Subset of T, t be Point of T st t
in A holds Component_of(t,A) c= A
proof
let T be TopStruct, A be Subset of T, t be Point of T;
assume
A1: t in A;
then Down(t,A) = t by CONNSP_3:def 3;
then
A2: Component_of(t,A) = Component_of Down(t,A) by A1,CONNSP_3:def 7;
the carrier of (T|A) = A by PRE_TOPC:8;
hence thesis by A2;
end;
registration
let T be TopSpace, A be open Subset of T;
cluster T|A -> open;
coherence
by PRE_TOPC:8;
end;
theorem Th4:
for T being TopSpace, S being SubSpace of T, A being Subset of T,
B being Subset of S st A = B holds T|A = S|B
proof
let T be TopSpace, S be SubSpace of T, A be Subset of T, B be Subset of S;
assume A = B;
then S|B is SubSpace of T & [#](S|B) = A by PRE_TOPC:def 5,TSEP_1:7;
hence thesis by PRE_TOPC:def 5;
end;
theorem Th5:
for S, T being TopSpace, A, B being Subset of T, C, D being
Subset of S st the TopStruct of S = the TopStruct of T & A = C & B = D & A,B
are_separated holds C,D are_separated
by TOPS_3:80;
theorem
for S, T being TopSpace st the TopStruct of S = the TopStruct of T & S
is connected holds T is connected
proof
let S, T be TopSpace such that
A1: the TopStruct of S = the TopStruct of T and
A2: S is connected;
let A, B be Subset of T such that
A3: [#]T = A \/ B and
A4: A,B are_separated;
reconsider A1 = A, B1 = B as Subset of S by A1;
[#]S = the carrier of S & A1,B1 are_separated by A1,A4,Th5;
then A1 = {}S or B1 = {}S by A1,A2,A3;
hence thesis;
end;
theorem Th7:
for S, T being TopSpace, A being Subset of S, B being Subset of T
st the TopStruct of S = the TopStruct of T & A = B & A is connected holds B is
connected
proof
let S, T be TopSpace, A be Subset of S, B be Subset of T such that
A1: the TopStruct of S = the TopStruct of T and
A2: A = B & A is connected;
now
let P, Q be Subset of T such that
A3: B = P \/ Q and
A4: P,Q are_separated;
reconsider P1 = P, Q1 = Q as Subset of S by A1;
P1,Q1 are_separated by A1,A4,Th5;
then P1 = {}S or Q1 = {}S by A2,A3,CONNSP_1:15;
hence P = {}T or Q = {}T;
end;
hence thesis by CONNSP_1:15;
end;
theorem Th8:
for S, T being non empty TopSpace, s being Point of S, t being
Point of T, A being a_neighborhood of s st the TopStruct of S = the TopStruct
of T & s = t holds A is a_neighborhood of t
proof
let S, T be non empty TopSpace, s be Point of S, t be Point of T, A be
a_neighborhood of s such that
A1: the TopStruct of S = the TopStruct of T and
A2: s = t;
reconsider B = A as Subset of T by A1;
A3: s in Int A by CONNSP_2:def 1;
Int A = Int B by A1,TOPS_3:77;
hence thesis by A2,A3,CONNSP_2:def 1;
end;
theorem
for S, T being non empty TopSpace, A being Subset of S, B being Subset
of T, N being a_neighborhood of A st the TopStruct of S = the TopStruct of T &
A = B holds N is a_neighborhood of B
proof
let S, T be non empty TopSpace, A be Subset of S, B be Subset of T, N be
a_neighborhood of A such that
A1: the TopStruct of S = the TopStruct of T and
A2: A = B;
reconsider M = N as Subset of T by A1;
A3: A c= Int N by CONNSP_2:def 2;
Int M = Int N by A1,TOPS_3:77;
hence thesis by A2,A3,CONNSP_2:def 2;
end;
theorem Th10:
for S, T being non empty TopSpace, A, B being Subset of T, f
being Function of S,T st f is being_homeomorphism & A is_a_component_of B holds
f"A is_a_component_of f"B
proof
let S, T be non empty TopSpace, A, B being Subset of T, f be Function of S,T
such that
A1: f is being_homeomorphism;
A2: rng f = [#]T by A1
.= the carrier of T;
set Y = f"A;
given X being Subset of T|B such that
A3: X = A and
A4: X is a_component;
A5: the carrier of (T|B) = B by PRE_TOPC:8;
then f"X c= f"B by RELAT_1:143;
then reconsider Y as Subset of S|(f"B) by A3,PRE_TOPC:8;
take Y;
thus Y = f"A;
X is connected by A4;
then A is connected by A3,CONNSP_1:23;
then f"A is connected by A1,TOPS_2:62;
hence Y is connected by CONNSP_1:23;
let Z being Subset of S|(f"B) such that
A6: Z is connected and
A7: Y c= Z;
A8: f.:Y c= f.:Z by A7,RELAT_1:123;
A9: f is one-to-one by A1;
A10: f is continuous by A1;
the carrier of S|(f"B) = f"B by PRE_TOPC:8;
then f.:Z c= f.:(f"B) by RELAT_1:123;
then reconsider R = f.:Z as Subset of T|B by A5,A2,FUNCT_1:77;
reconsider Z1 = Z as Subset of S by PRE_TOPC:11;
dom f = the carrier of S by FUNCT_2:def 1;
then
A11: Z1 c= dom f;
Z1 is connected by A6,CONNSP_1:23;
then f.:Z1 is connected by A10,TOPS_2:61;
then
A12: R is connected by CONNSP_1:23;
X = f.:Y by A3,A2,FUNCT_1:77;
then X = R by A4,A12,A8;
hence thesis by A3,A9,A11,FUNCT_1:94;
end;
begin :: Locally connectedness
theorem Th11:
for T being non empty TopSpace, S being non empty SubSpace of T,
A being non empty Subset of T, B being non empty Subset of S st A = B & A is
locally_connected holds B is locally_connected
by Th4;
theorem Th12:
for S, T being non empty TopSpace st the TopStruct of S = the
TopStruct of T & S is locally_connected holds T is locally_connected
proof
let S, T be non empty TopSpace such that
A1: the TopStruct of S = the TopStruct of T and
A2: S is locally_connected;
let t be Point of T;
reconsider s = t as Point of S by A1;
let U be Subset of T;
reconsider U1 = U as Subset of S by A1;
assume U is a_neighborhood of t;
then
A3: U1 is a_neighborhood of s by A1,Th8;
S is_locally_connected_in s by A2;
then consider V1 being Subset of S such that
A4: V1 is a_neighborhood of s and
A5: V1 is connected and
A6: V1 c= U1 by A3;
reconsider V = V1 as Subset of T by A1;
take V;
thus V is a_neighborhood of t by A1,A4,Th8;
thus V is connected by A1,A5,Th7;
thus thesis by A6;
end;
theorem Th13:
for T being non empty TopSpace holds T is locally_connected iff
[#]T is locally_connected
proof
let T be non empty TopSpace;
T is SubSpace of T by TSEP_1:2;
then
A1: the TopStruct of T = the TopStruct of (T| [#]T) by PRE_TOPC:8,TSEP_1:5;
hence T is locally_connected implies [#]T is locally_connected by Th12;
assume [#]T is locally_connected;
then T| [#]T is locally_connected;
hence thesis by A1,Th12;
end;
Lm10: for T being non empty TopSpace, S being non empty open SubSpace of T st
T is locally_connected holds the TopStruct of S is locally_connected
proof
let T be non empty TopSpace;
let S be non empty open SubSpace of T;
reconsider A = [#]S as non empty Subset of T by TSEP_1:1;
A1: A is open by TSEP_1:def 1;
assume T is locally_connected;
then [#]S is locally_connected by A1,Th11,CONNSP_2:17;
then S is locally_connected by Th13;
then the TopStruct of S is locally_connected by Th12;
then [#]the TopStruct of S is locally_connected by Th13;
then (the TopStruct of S)| [#]the TopStruct of S is locally_connected;
hence thesis by TSEP_1:3;
end;
theorem Th14:
for T being non empty TopSpace, S being non empty open SubSpace
of T st T is locally_connected holds S is locally_connected
proof
let T be non empty TopSpace;
let S be non empty open SubSpace of T;
assume T is locally_connected;
then the TopStruct of S is locally_connected by Lm10;
hence thesis by Th12;
end;
theorem
for S, T being non empty TopSpace st S,T are_homeomorphic & S is
locally_connected holds T is locally_connected
proof
let S, T be non empty TopSpace;
given f being Function of S,T such that
A1: f is being_homeomorphism;
assume
A2: S is locally_connected;
now
let A be non empty Subset of T, B being Subset of T;
assume A is open & B is_a_component_of A;
then
A3: f"A is open & f"B is_a_component_of f"A by A1,Th10,TOPGRP_1:26;
rng f = [#]T by A1;
then f"A is non empty by RELAT_1:139;
then f"B is open by A2,A3,CONNSP_2:18;
hence B is open by A1,TOPGRP_1:26;
end;
hence thesis by CONNSP_2:18;
end;
theorem Th16:
for T being non empty TopSpace st ex B being Basis of T st for X
being Subset of T st X in B holds X is connected holds T is locally_connected
proof
let T be non empty TopSpace;
given B being Basis of T such that
A1: for X being Subset of T st X in B holds X is connected;
let x be Point of T;
let U be Subset of T such that
A2: x in Int U;
Int U in the topology of T & the topology of T c= UniCl B by CANTOR_1:def 2
,PRE_TOPC:def 2;
then consider Y being Subset-Family of T such that
A3: Y c= B and
A4: Int U = union Y by CANTOR_1:def 1;
consider V being set such that
A5: x in V and
A6: V in Y by A2,A4,TARSKI:def 4;
reconsider V as Subset of T by A6;
take V;
B c= the topology of T & V in B by A3,A6,TOPS_2:64;
then V is open by PRE_TOPC:def 2;
hence x in Int V by A5,TOPS_1:23;
thus V is connected by A1,A3,A6;
A7: Int U c= U by TOPS_1:16;
V c= union Y by A6,ZFMISC_1:74;
hence thesis by A4,A7;
end;
theorem Th17:
r <= s implies Closed-Interval-TSpace(r,s) is locally_connected
proof
assume r <= s;
then ex B being Basis of Closed-Interval-TSpace(r,s) st (ex f being
ManySortedSet of Closed-Interval-TSpace(r,s) st for y being Point of
Closed-Interval-MSpace(r,s) holds f.y = {Ball(y,1/n) where n is Nat:
n <> 0} & B = Union f) & for X being Subset of Closed-Interval-TSpace(r,s) st X
in B holds X is connected by Th2;
hence thesis by Th16;
end;
registration
cluster I[01] -> locally_connected;
coherence by Th17,TOPMETR:20;
end;
registration
let A be non empty open Subset of I[01];
cluster I[01] | A -> locally_connected;
coherence by Th14;
end;
begin :: Some useful functions
definition
let r be Real;
func ExtendInt(r) -> Function of I[01], R^1 means
:Def1:
for x being Point of I[01] holds it.x = r*x;
existence
proof
defpred P[Real,set] means $2 = r*$1;
A1: for x being Element of I[01] ex y being Element of R st P[x,y]
proof
let x be Element of I[01];
take r*x;
thus thesis by TOPMETR:17,XREAL_0:def 1;
end;
ex f being Function of I, R st for x being Element of I[01] holds P[x,
f.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let f, g be Function of I[01], R^1 such that
A2: for x being Point of I[01] holds f.x = r*x and
A3: for x being Point of I[01] holds g.x = r*x;
for x being Point of I[01] holds f.x = g.x
proof
let x be Point of I[01];
thus f.x = r*x by A2
.= g.x by A3;
end;
hence f = g;
end;
end;
registration
let r be Real;
cluster ExtendInt(r) -> continuous;
coherence
proof
reconsider f1 = id I[01] as Function of I[01],R^1 by BORSUK_1:40,FUNCT_2:7
,TOPMETR:17;
f1 is continuous by PRE_TOPC:26;
then consider g being Function of I[01],R^1 such that
A1: for p being Point of I[01], r1 being Real st f1.p=r1 holds
g.p=r*r1 and
A2: g is continuous by JGRAPH_2:23;
for x being Point of I[01] holds g.x = (ExtendInt(r)).x
proof
let x be Point of I[01];
thus g.x = r*f1.x by A1
.= r*x
.= (ExtendInt(r)).x by Def1;
end;
hence thesis by A2,FUNCT_2:63;
end;
end;
definition
let r be Real;
redefine func ExtendInt(r) -> Path of R^1(0),R^1(r); :: redefines ExtendInt (TOPALG_5, definition)
coherence
proof
thus ExtendInt(r) is continuous;
thus (ExtendInt(r)).0 = r * 0 by Def1,BORSUK_1:def 14
.= R^1(0) by TOPREALB:def 2;
thus (ExtendInt(r)).1 = r * 1 by Def1,BORSUK_1:def 15
.= R^1(r) by TOPREALB:def 2;
end;
end;
definition
let S, T, Y be non empty TopSpace, H be Function of [:S,T:],Y, t be Point of
T;
func Prj1(t,H) -> Function of S,Y means
:Def2:
for s being Point of S holds it.s = H.(s,t);
existence
proof
deffunc F(Point of S) = H. [$1,t];
consider f being Function of the carrier of S, the carrier of Y such that
A1: for x being Element of S holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let x be Point of S;
thus thesis by A1;
end;
uniqueness
proof
let f, g be Function of S,Y such that
A2: for s being Point of S holds f.s = H.(s,t) and
A3: for s being Point of S holds g.s = H.(s,t);
now
let s be Point of S;
thus f.s = H.(s,t) by A2
.= g.s by A3;
end;
hence thesis;
end;
end;
definition
let S, T, Y be non empty TopSpace, H be Function of [:S,T:],Y, s be Point of
S;
func Prj2(s,H) -> Function of T,Y means
:Def3:
for t being Point of T holds it.t = H.(s,t);
existence
proof
deffunc F(Point of T) = H. [s,$1];
consider f being Function of the carrier of T, the carrier of Y such that
A1: for x being Element of T holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let x be Point of T;
thus thesis by A1;
end;
uniqueness
proof
let f, g be Function of T,Y such that
A2: for t being Point of T holds f.t = H.(s,t) and
A3: for t being Point of T holds g.t = H.(s,t);
now
let t be Point of T;
thus f.t = H.(s,t) by A2
.= g.t by A3;
end;
hence thesis;
end;
end;
registration
let S, T, Y be non empty TopSpace, H be continuous Function of [:S,T:],Y, t
be Point of T;
cluster Prj1(t,H) -> continuous;
coherence
proof
for p being Point of S, V being Subset of Y st Prj1(t,H).p in V & V is
open holds ex W being Subset of S st p in W & W is open & Prj1(t,H).:W c= V
proof
let p be Point of S, V be Subset of Y such that
A1: Prj1(t,H).p in V & V is open;
Prj1(t,H).p = H.(p,t) by Def2;
then consider W being Subset of [:S,T:] such that
A2: [p,t] in W and
A3: W is open and
A4: H.:W c= V by A1,JGRAPH_2:10;
consider A being Subset-Family of [:S,T:] such that
A5: W = union A and
A6: for e being set st e in A ex X1 being Subset of S, Y1 being
Subset of T st e = [:X1,Y1:] & X1 is open & Y1 is open by A3,BORSUK_1:5;
consider e being set such that
A7: [p,t] in e and
A8: e in A by A2,A5,TARSKI:def 4;
consider X1 being Subset of S, Y1 being Subset of T such that
A9: e = [:X1,Y1:] and
A10: X1 is open and
Y1 is open by A6,A8;
take X1;
thus p in X1 by A7,A9,ZFMISC_1:87;
thus X1 is open by A10;
let x be object;
assume x in Prj1(t,H).:X1;
then consider c being Point of S such that
A11: c in X1 and
A12: x = Prj1(t,H).c by FUNCT_2:65;
t in Y1 by A7,A9,ZFMISC_1:87;
then [c,t] in [:X1,Y1:] by A11,ZFMISC_1:87;
then [c,t] in W by A5,A8,A9,TARSKI:def 4;
then
A13: H. [c,t] in H.:W by FUNCT_2:35;
Prj1(t,H).c = H.(c,t) by Def2
.= H. [c,t];
hence thesis by A4,A12,A13;
end;
hence thesis by JGRAPH_2:10;
end;
end;
registration
let S, T, Y be non empty TopSpace, H be continuous Function of [:S,T:],Y, s
be Point of S;
cluster Prj2(s,H) -> continuous;
coherence
proof
for p being Point of T, V being Subset of Y st Prj2(s,H).p in V & V is
open holds ex W being Subset of T st p in W & W is open & Prj2(s,H).:W c= V
proof
let p be Point of T, V be Subset of Y such that
A1: Prj2(s,H).p in V & V is open;
Prj2(s,H).p = H.(s,p) by Def3;
then consider W being Subset of [:S,T:] such that
A2: [s,p] in W and
A3: W is open and
A4: H.:W c= V by A1,JGRAPH_2:10;
consider A being Subset-Family of [:S,T:] such that
A5: W = union A and
A6: for e being set st e in A ex X1 being Subset of S, Y1 being
Subset of T st e = [:X1,Y1:] & X1 is open & Y1 is open by A3,BORSUK_1:5;
consider e being set such that
A7: [s,p] in e and
A8: e in A by A2,A5,TARSKI:def 4;
consider X1 being Subset of S, Y1 being Subset of T such that
A9: e = [:X1,Y1:] and
X1 is open and
A10: Y1 is open by A6,A8;
take Y1;
thus p in Y1 by A7,A9,ZFMISC_1:87;
thus Y1 is open by A10;
let x be object;
assume x in Prj2(s,H).:Y1;
then consider c being Point of T such that
A11: c in Y1 and
A12: x = Prj2(s,H).c by FUNCT_2:65;
s in X1 by A7,A9,ZFMISC_1:87;
then [s,c] in [:X1,Y1:] by A11,ZFMISC_1:87;
then [s,c] in W by A5,A8,A9,TARSKI:def 4;
then
A13: H. [s,c] in H.:W by FUNCT_2:35;
Prj2(s,H).c = H.(s,c) by Def3
.= H. [s,c];
hence thesis by A4,A12,A13;
end;
hence thesis by JGRAPH_2:10;
end;
end;
theorem
for T being non empty TopSpace, a, b being Point of T, P, Q being Path
of a,b, H being Homotopy of P,Q, t being Point of I[01] st H is continuous
holds Prj1(t,H) is continuous;
theorem
for T being non empty TopSpace, a, b being Point of T, P, Q being Path
of a,b, H being Homotopy of P,Q, s being Point of I[01] st H is continuous
holds Prj2(s,H) is continuous;
set TUC = Tunit_circle(2);
set cS1 = the carrier of TUC;
Lm11: now
TUC = Tcircle(0.TOP-REAL 2,1) by TOPREALB:def 7;
hence cS1 = Sphere(|[0,0]|,1) by EUCLID:54,TOPREALB:9;
end;
Lm12: dom CircleMap = REAL by FUNCT_2:def 1,TOPMETR:17;
definition
let r be Real;
func cLoop(r) -> Function of I[01], Tunit_circle(2) means
:Def4:
for x being Point of I[01] holds it.x = |[ cos(2*PI*r*x), sin(2*PI*r*x) ]|;
existence
proof
defpred P[Real,set] means $2 = |[ cos(2*PI*r*$1), sin(2*PI*r*$1) ]|;
A1: for x being Element of I[01] ex y being Element of cS1 st P[x,y]
proof
let x be Element of I[01];
set y = |[ cos(2*PI*r*x), sin(2*PI*r*x) ]|;
|. y - o .| = |. y .| by EUCLID:54,RLVECT_1:13
.= sqrt((y`1)^2+(y`2)^2) by JGRAPH_1:30
.= sqrt((cos(2*PI*r*x))^2+(y`2)^2) by EUCLID:52
.= sqrt((cos(2*PI*r*x))^2+(sin(2*PI*r*x))^2) by EUCLID:52
.= 1 by SIN_COS:29,SQUARE_1:18;
then reconsider y as Element of cS1 by Lm11,TOPREAL9:9;
take y;
thus thesis;
end;
ex f being Function of I, cS1 st for x being Element of I[01] holds P[
x,f.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let f, g be Function of I[01], TUC such that
A2: for x being Point of I[01] holds f.x = |[cos(2*PI*r*x),sin(2*PI*r* x)]| and
A3: for x being Point of I[01] holds g.x = |[cos(2*PI*r*x),sin(2*PI*r* x)]|;
for x being Point of I[01] holds f.x = g.x
proof
let x be Point of I[01];
thus f.x = |[cos(2*PI*r*x),sin(2*PI*r*x)]| by A2
.= g.x by A3;
end;
hence f = g;
end;
end;
theorem Th20:
cLoop(r) = CircleMap * ExtendInt(r)
proof
for x being Point of I[01] holds (cLoop(r)).x = (CircleMap * ExtendInt(r
)). x
proof
let x be Point of I[01];
A1: (ExtendInt(r)).x = r*x by Def1;
thus (cLoop(r)).x = |[ cos(2*PI*r*x), sin(2*PI*r*x) ]| by Def4
.= |[ cos(2*PI*(ExtendInt(r)).x), sin(2*PI*(ExtendInt(r)).x) ]| by A1
.= CircleMap.((ExtendInt(r)).x) by TOPREALB:def 11
.= (CircleMap * ExtendInt(r)).x by FUNCT_2:15;
end;
hence thesis;
end;
definition
let n be Integer;
redefine func cLoop(n) -> Loop of c[10]; :: redefines cLoop (TOPALG_5, definition)
coherence
proof
set f = cLoop(n);
f = CircleMap * ExtendInt(n) by Th20;
hence f is continuous;
thus f.0 = |[ cos(2*PI*n*j0), sin(2*PI*n*j0) ]| by Def4
.= c[10] by SIN_COS:31,TOPREALB:def 8;
thus f.1 = |[ cos(2*PI*n*j1), sin(2*PI*n*j1) ]| by Def4
.= |[ cos(0), sin(2*PI*n+0) ]| by COMPLEX2:9
.= c[10] by COMPLEX2:8,SIN_COS:31,TOPREALB:def 8;
end;
end;
begin :: Main theorems
Lm13: ex F being Subset-Family of Tunit_circle(2) st F is Cover of
Tunit_circle(2) & F is open & for U being Subset of Tunit_circle(2) st U in F
ex D being mutually-disjoint open Subset-Family of R^1 st union D = (CircleMap)
"U & for d being Subset of R^1 st d in D for f being Function of R^1 | d, (
Tunit_circle(2)) | U st f = CircleMap|d holds f is being_homeomorphism
proof
consider F being Subset-Family of Tunit_circle(2) such that
A1: F = { (CircleMap).:].0,1.[, (CircleMap).:].1/2,3/2.[ } and
A2: F is Cover of Tunit_circle(2) & F is open and
A3: for U being Subset of Tunit_circle(2) holds ( U = (CircleMap).:].0,1
.[ implies union IntIntervals(0,1) = (CircleMap)"U & for d being Subset of R^1
st d in IntIntervals(0,1) for f being Function of R^1 | d, (Tunit_circle(2)) |
U st f = CircleMap|d holds f is being_homeomorphism ) & ( U = (CircleMap).:].1/
2,3/2.[ implies union IntIntervals(1/2,3/2) = (CircleMap)"U & for d being
Subset of R^1 st d in IntIntervals(1/2,3/2) for f being Function of R^1 | d, (
Tunit_circle(2)) | U st f = CircleMap|d holds f is being_homeomorphism ) by
TOPREALB:45;
take F;
thus F is Cover of Tunit_circle(2) & F is open by A2;
let U be Subset of Tunit_circle(2);
assume
A4: U in F;
per cases by A1,A4,TARSKI:def 2;
suppose
A5: U = (CircleMap).:].0,1.[;
reconsider D = IntIntervals(0,1) as mutually-disjoint open Subset-Family
of R^1 by Lm8,TOPREALB:4;
take D;
thus thesis by A3,A5;
end;
suppose
A6: U = (CircleMap).:].1/2,3/2.[;
reconsider D = IntIntervals(1/2,3/2) as mutually-disjoint open
Subset-Family of R^1 by Lm9,TOPREALB:4;
take D;
thus thesis by A3,A6;
end;
end;
Lm14: [#]Sspace(0[01]) = {0} by TEX_2:def 2;
Lm15: for F being Subset-Family of Closed-Interval-TSpace(r,s), C being
IntervalCover of F, G being IntervalCoverPts of C holds F is Cover of
Closed-Interval-TSpace(r,s) & F is open connected & r <= s implies G is non
empty
proof
let F be Subset-Family of Closed-Interval-TSpace(r,s), C be IntervalCover of
F, G be IntervalCoverPts of C;
assume
F is Cover of Closed-Interval-TSpace(r,s) & F is open connected & r <= s;
then len G = len C + 1 by RCOMP_3:def 3;
hence thesis by CARD_1:27;
end;
theorem Th21:
for UL being Subset-Family of Tunit_circle(2) st UL is Cover of
Tunit_circle(2) & UL is open for Y being non empty TopSpace, F being continuous
Function of [:Y,I[01]:], Tunit_circle(2), y being Point of Y ex T being non
empty FinSequence of REAL st T.1 = 0 & T.len T = 1 & T is increasing & ex N
being open Subset of Y st y in N & for i being Nat st i in dom T & i
+1 in dom T ex Ui being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:
N,[.T.i,T.(i+1).]:] c= Ui
proof
set L = Closed-Interval-TSpace(0,1);
let UL be Subset-Family of TUC such that
A1: UL is Cover of TUC and
A2: UL is open;
let Y be non empty TopSpace, F be continuous Function of [:Y,I[01]:], TUC, y
be Point of Y;
A3: [#]TUC = union UL by A1,SETFAM_1:45;
A4: for i being Point of I[01] ex U being non empty open Subset of TUC st F.
[y,i] in U & U in UL
proof
let i be Point of I[01];
consider U being set such that
A5: F. [y,i] in U & U in UL by A3,TARSKI:def 4;
reconsider U as non empty open Subset of TUC by A2,A5;
take U;
thus thesis by A5;
end;
then ex U being non empty open Subset of TUC st F. [y,0[01]] in U & U in UL;
then reconsider UL1 = UL as non empty set;
set C = the carrier of Y;
defpred I0[set,set] means ex V being open Subset of TUC st V in UL1 & F. [y,
$1] in V & $2 = V;
A6: for i being Element of I ex z being Element of UL1 st I0[i,z]
proof
let i be Element of I;
ex U being non empty open Subset of TUC st F. [y,i] in U & U in UL by A4;
hence thesis;
end;
consider I0 being Function of I, UL1 such that
A7: for i being Element of I holds I0[i,I0.i] from FUNCT_2:sch 3(A6);
defpred I1[object,object] means
ex M being open Subset of Y, O being open
connected Subset of I[01] st y in M & $1 in O & F.:[:M,O:] c= I0.$1 & $2 = [:M,
O:];
A8: for i being Element of I ex z being Subset of [:C,I:] st I1[i,z]
proof
let i be Element of I;
consider V being open Subset of TUC such that
V in UL1 and
A9: F. [y,i] in V and
A10: I0.i = V by A7;
consider W being Subset of [:Y,I[01]:] such that
A11: [y,i] in W and
A12: W is open and
A13: F.:W c= V by A9,JGRAPH_2:10;
consider Q being Subset-Family of [:Y,I[01]:] such that
A14: W = union Q and
A15: for e being set st e in Q ex A being Subset of Y, B being Subset
of I[01] st e = [:A,B:] & A is open & B is open by A12,BORSUK_1:5;
consider Z being set such that
A16: [y,i] in Z and
A17: Z in Q by A11,A14,TARSKI:def 4;
consider A being Subset of Y, B being Subset of I[01] such that
A18: Z = [:A,B:] and
A19: A is open and
A20: B is open by A15,A17;
reconsider A as open Subset of Y by A19;
A21: i in B by A16,A18,ZFMISC_1:87;
reconsider B as non empty open Subset of I[01] by A16,A18,A20;
reconsider i1 = i as Point of I[01]|B by A21,PRE_TOPC:8;
Component_of i1 is a_component by CONNSP_1:40;
then
A22: Component_of i1 is open by CONNSP_2:15;
Component_of(i,B) = Component_of i1 by A21,CONNSP_3:def 7;
then reconsider
D = Component_of(i,B) as open connected Subset of I[01] by A21,A22,
CONNSP_3:33,TSEP_1:17;
reconsider z = [:A,D:] as Subset of [:C,I:] by BORSUK_1:def 2;
take z, A, D;
thus y in A by A16,A18,ZFMISC_1:87;
thus i in D by A21,CONNSP_3:26;
D c= B by A21,Th3;
then
A23: z c= [:A,B:] by ZFMISC_1:95;
[:A,B:] c= W by A14,A17,A18,ZFMISC_1:74;
then z c= W by A23;
then F.:z c= F.:W by RELAT_1:123;
hence F.:[:A,D:] c= I0.i by A10,A13;
thus thesis;
end;
consider I1 being Function of I, bool [:C,I:] such that
A24: for i being Element of I holds I1[i,I1.i] from FUNCT_2:sch 3(A8);
reconsider C1 = rng I1 as Subset-Family of [:Y,I[01]:] by BORSUK_1:def 2;
A25: C1 is open
proof
let P be Subset of [:Y,I[01]:];
assume P in C1;
then consider i being object such that
A26: i in dom I1 and
A27: I1.i = P by FUNCT_1:def 3;
I1[i,I1.i] by A24,A26;
hence thesis by A27,BORSUK_1:6;
end;
A28: dom I1 = I by FUNCT_2:def 1;
[:{y},[#]I[01]:] c= union C1
proof
let a be object;
assume a in [:{y},[#]I[01]:];
then consider a1, a2 being object such that
A29: a1 in {y} and
A30: a2 in [#]I[01] and
A31: a = [a1,a2] by ZFMISC_1:def 2;
A32: a1 = y by A29,TARSKI:def 1;
reconsider a2 as Point of I[01] by A30;
consider M being open Subset of Y, O being open connected Subset of I[01]
such that
A33: y in M & a2 in O and
F.:[:M,O:] c= I0.a2 and
A34: I1.a2 = [:M,O:] by A24;
[y,a2] in [:M,O:] & [:M,O:] in C1 by A28,A33,A34,FUNCT_1:def 3,ZFMISC_1:87;
hence thesis by A31,A32,TARSKI:def 4;
end;
then
A35: C1 is Cover of [:{y},[#]I[01]:] by SETFAM_1:def 11;
[:{y},[#]I[01]:] is compact by BORSUK_3:23;
then consider G being Subset-Family of [:Y,I[01]:] such that
A36: G c= C1 and
A37: G is Cover of [:{y},[#]I[01]:] and
A38: G is finite by A35,A25;
set NN = {M where M is open Subset of Y: y in M & ex O being open Subset of
I[01] st [:M,O:] in G};
NN c= bool C
proof
let a be object;
assume a in NN;
then ex M being open Subset of Y st a = M & y in M & ex O being open
Subset of I[01] st [:M,O:] in G;
hence thesis;
end;
then reconsider NN as Subset-Family of Y;
consider p being Function such that
A39: rng p = G and
A40: dom p in omega by A38,FINSET_1:def 1;
defpred F[object,object] means
ex M being open Subset of Y, O being non empty open
Subset of I[01] st y in M & p.$1 = [:M,O:] & $2 = M;
A41: for x being object st x in dom p ex y being object st y in NN & F[x,y]
proof
let x be object;
assume x in dom p;
then
A42: p.x in rng p by FUNCT_1:def 3;
then consider i being object such that
A43: i in dom I1 and
A44: I1.i = p.x by A36,A39,FUNCT_1:def 3;
consider M being open Subset of Y, O being open connected Subset of I[01]
such that
A45: y in M & i in O and
F.:[:M,O:] c= I0.i and
A46: I1.i = [:M,O:] by A24,A43;
take M;
thus thesis by A39,A42,A44,A45,A46;
end;
consider p1 being Function of dom p, NN such that
A47: for x being object st x in dom p holds F[x,p1.x] from FUNCT_2:sch 1(
A41);
set ICOV = {O where O is open connected Subset of I[01]: ex M being open
Subset of Y st [:M,O:] in G};
A48: [:{y},[#]I[01]:] c= union G by A37,SETFAM_1:def 11;
A49: y in {y} by TARSKI:def 1;
then [y,0[01]] in [:{y},[#]I[01]:] by ZFMISC_1:def 2;
then consider Z being set such that
[y,0[01]] in Z and
A50: Z in G by A48,TARSKI:def 4;
consider i being object such that
A51: i in dom I1 and
A52: I1.i = Z by A36,A50,FUNCT_1:def 3;
consider M being open Subset of Y, O being open connected Subset of I[01]
such that
A53: y in M and
i in O and
F.:[:M,O:] c= I0.i and
A54: I1.i = [:M,O:] by A24,A51;
A55: M in NN by A50,A52,A53,A54;
then
A56: dom p1 = dom p by FUNCT_2:def 1;
rng p1 = NN
proof
thus rng p1 c= NN;
let a be object;
assume a in NN;
then consider M being open Subset of Y such that
A57: a = M and
y in M and
A58: ex O being open Subset of I[01] st [:M,O:] in G;
consider O being open Subset of I[01] such that
A59: [:M,O:] in G by A58;
consider b being object such that
A60: b in dom p and
A61: p.b = [:M,O:] by A39,A59,FUNCT_1:def 3;
consider M1 being open Subset of Y, O1 being non empty open Subset of
I[01] such that
A62: y in M1 & p.b = [:M1,O1:] and
A63: p1.b = M1 by A47,A60;
M1 = M by A61,A62,ZFMISC_1:110;
hence thesis by A56,A57,A60,A63,FUNCT_1:def 3;
end;
then
A64: NN is finite by A40,A56,FINSET_1:def 1;
NN is open
proof
let a be Subset of Y;
assume a in NN;
then ex M being open Subset of Y st a = M & y in M & ex O being open
Subset of I[01] st [:M,O:] in G;
hence thesis;
end;
then reconsider N = meet NN as open Subset of Y by A64,TOPS_2:20;
ICOV c= bool I
proof
let a be object;
assume a in ICOV;
then ex O being open connected Subset of I[01] st a = O & ex M being open
Subset of Y st [:M,O:] in G;
hence thesis;
end;
then reconsider ICOV as Subset-Family of L by TOPMETR:20;
[#]L c= union ICOV
proof
let a be object;
assume a in [#]L;
then reconsider a as Point of I[01] by TOPMETR:20;
[y,a] in [:{y},[#]I[01]:] by A49,ZFMISC_1:def 2;
then consider Z being set such that
A65: [y,a] in Z and
A66: Z in G by A48,TARSKI:def 4;
consider i being object such that
A67: i in dom I1 and
A68: I1.i = Z by A36,A66,FUNCT_1:def 3;
consider M being open Subset of Y, O being open connected Subset of I[01]
such that
y in M and
i in O and
F.:[:M,O:] c= I0.i and
A69: I1.i = [:M,O:] by A24,A67;
a in O & O in ICOV by A65,A66,A68,A69,ZFMISC_1:87;
hence thesis by TARSKI:def 4;
end;
then
A70: ICOV is Cover of L by SETFAM_1:def 11;
set NCOV = the IntervalCover of ICOV;
set T = the IntervalCoverPts of NCOV;
A71: ICOV is connected
proof
let X be Subset of L;
assume X in ICOV;
then ex O being open connected Subset of I[01] st X = O & ex M being open
Subset of Y st [:M,O:] in G;
hence thesis by TOPMETR:20;
end;
A72: ICOV is open
proof
let a be Subset of L;
assume a in ICOV;
then ex O being open connected Subset of I[01] st a = O & ex M being open
Subset of Y st [:M,O:] in G;
hence thesis by TOPMETR:20;
end;
then reconsider T as non empty FinSequence of REAL by A70,A71,Lm15;
take T;
thus T.1 = 0 & T.len T = 1 by A70,A72,A71,RCOMP_3:def 3;
thus T is increasing by A70,A72,A71,RCOMP_3:65;
take N;
now
let Z be set;
assume Z in NN;
then ex M being open Subset of Y st Z = M & y in M & ex O being open
Subset of I[01] st [:M,O:] in G;
hence y in Z;
end;
hence y in N by A55,SETFAM_1:def 1;
let i be Nat;
assume that
A73: i in dom T and
A74: i+1 in dom T;
A75: 1 <= i by A73,FINSEQ_3:25;
A76: i+1 <= len T by A74,FINSEQ_3:25;
len T = len NCOV + 1 by A70,A72,A71,RCOMP_3:def 3;
then i <= len NCOV by A76,XREAL_1:6;
then i in dom NCOV by A75,FINSEQ_3:25;
then
A77: NCOV.i in rng NCOV by FUNCT_1:def 3;
rng NCOV c= ICOV by A70,A72,A71,RCOMP_3:def 2;
then NCOV.i in ICOV by A77;
then consider O being open connected Subset of I[01] such that
A78: NCOV.i = O and
A79: ex M being open Subset of Y st [:M,O:] in G;
consider M being open Subset of Y such that
A80: [:M,O:] in G by A79;
i < len T by A76,NAT_1:13;
then
A81: [.T.i,T.(i+1).] c= O by A70,A72,A71,A75,A78,RCOMP_3:66;
consider j being object such that
A82: j in dom I1 and
A83: I1.j = [:M,O:] by A36,A80,FUNCT_1:def 3;
consider V being open Subset of TUC such that
A84: V in UL1 and
A85: F. [y,j] in V and
A86: I0.j = V by A7,A82;
reconsider V as non empty open Subset of TUC by A85;
take V;
thus V in UL by A84;
consider M1 being open Subset of Y, O1 being open connected Subset of I[01]
such that
A87: y in M1 and
A88: j in O1 and
A89: F.:[:M1,O1:] c= I0.j and
A90: I1.j = [:M1,O1:] by A24,A82;
M = M1 by A83,A87,A88,A90,ZFMISC_1:110;
then M in NN by A80,A87;
then N c= M by SETFAM_1:3;
then [:N,[.T.i,T.(i+1).]:] c= [:M1,O1:] by A83,A90,A81,ZFMISC_1:96;
then F.:[:N,[.T.i,T.(i+1).]:] c= F.:[:M1,O1:] by RELAT_1:123;
hence thesis by A89,A86;
end;
theorem Th22:
for Y being non empty TopSpace, F being Function of [:Y,I[01]:],
Tunit_circle(2), Ft being Function of [:Y,Sspace(0[01]):], R^1 st F is
continuous & Ft is continuous & F | [:the carrier of Y,{0}:] = CircleMap*Ft ex
G being Function of [:Y,I[01]:], R^1 st G is continuous & F = CircleMap*G & G |
[:the carrier of Y,{0}:] = Ft & for H being Function of [:Y,I[01]:], R^1 st H
is continuous & F = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft holds G = H
proof
consider UL being Subset-Family of TUC such that
A1: UL is Cover of TUC & UL is open and
A2: for U being Subset of TUC st U in UL ex D being mutually-disjoint
open Subset-Family of R^1 st union D = (CircleMap)"U & for d being Subset of
R^1 st d in D for f being Function of R^1 | d, TUC | U st f = CircleMap|d holds
f is being_homeomorphism by Lm13;
let Y be non empty TopSpace, F be Function of [:Y,I[01]:], TUC, Ft be
Function of [:Y,Sspace(0[01]):], R^1 such that
A3: F is continuous and
A4: Ft is continuous and
A5: F | [:the carrier of Y,{0}:] = CircleMap*Ft;
defpred A[set,set] means ex y being Point of Y, t being Point of I[01], N
being non empty open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 st $1
= [y,t] & $2 = Fn.$1 & y in N & Fn is continuous & F | [:N,I:] = CircleMap*Fn &
Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] & for H being Function of [:Y|N,
I[01]:], R^1 st H is continuous & F | [:N,I:] = CircleMap*H & H | [:the carrier
of Y,{0}:] = Ft | [:N,I:] holds Fn = H;
A6: dom F = the carrier of [:Y,I[01]:] by FUNCT_2:def 1
.= [:the carrier of Y,I:] by BORSUK_1:def 2;
A7: the carrier of [:Y,Sspace(0[01]):] = [:the carrier of Y, the carrier of
Sspace(0[01]):] by BORSUK_1:def 2;
then
A8: dom Ft = [:the carrier of Y,{0}:] by Lm14,FUNCT_2:def 1;
A9: for x being Point of [:Y,I[01]:] ex z being Point of R^1 st A[x,z]
proof
let x be Point of [:Y,I[01]:];
consider y being Point of Y, t being Point of I[01] such that
A10: x = [y,t] by BORSUK_1:10;
consider TT being non empty FinSequence of REAL such that
A11: TT.1 = 0 and
A12: TT.len TT = 1 and
A13: TT is increasing and
A14: ex N being open Subset of Y st y in N & for i being Nat
st i in dom TT & i+1 in dom TT ex Ui being non empty Subset of
Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1).]:] c= Ui by A3,A1,Th21;
consider N being open Subset of Y such that
A15: y in N and
A16: for i being Nat st i in dom TT & i+1 in dom TT ex Ui
being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1)
.]:] c= Ui by A14;
reconsider N as non empty open Subset of Y by A15;
defpred N[Nat] means $1 in dom TT implies ex N2 being non empty
open Subset of Y, S being non empty Subset of I[01], Fn being Function of [:Y|
N2,I[01]|S:], R^1 st S = [.0,TT.$1.] & y in N2 & N2 c= N & Fn is continuous & F
| [:N2,S:] = CircleMap*Fn & Fn | [:the carrier of Y,{0}:] = Ft | [:N2,I:];
A17: len TT in dom TT by FINSEQ_5:6;
A18: 1 in dom TT by FINSEQ_5:6;
A19: now
let i be Element of NAT such that
A20: i in dom TT;
1 <= i by A20,FINSEQ_3:25;
then 1 = i or 1 < i by XXREAL_0:1;
hence
A21: 0 <= TT.i by A11,A13,A18,A20,SEQM_3:def 1;
assume
A22: i+1 in dom TT;
A23: i+0 < i+1 by XREAL_1:8;
hence
A24: TT.i < TT.(i+1) by A13,A20,A22,SEQM_3:def 1;
i+1 <= len TT by A22,FINSEQ_3:25;
then i+1 = len TT or i+1 < len TT by XXREAL_0:1;
hence TT.(i+1) <= 1 by A12,A13,A17,A22,SEQM_3:def 1;
hence TT.i < 1 by A24,XXREAL_0:2;
thus 0 < TT.(i+1) by A13,A20,A21,A22,A23,SEQM_3:def 1;
end;
A25: now
let i be Nat such that
A26: 0 <= TT.i and
A27: TT.(i+1) <= 1;
thus [.TT.i,TT.(i+1).] c= I
proof
let a be object;
assume
A28: a in [.TT.i,TT.(i+1).];
then reconsider a as Real;
a <= TT.(i+1) by A28,XXREAL_1:1;
then
A29: a <= 1 by A27,XXREAL_0:2;
0 <= a by A26,A28,XXREAL_1:1;
hence thesis by A29,BORSUK_1:43;
end;
end;
A30: for i being Nat st N[i] holds N[i+1]
proof
let i be Nat;
assume that
A31: N[i] and
A32: i+1 in dom TT;
per cases by A32,TOPREALA:2;
suppose
A33: i = 0;
take N2 = N;
set Fn = Ft | [:N2,{0}:];
set S = [.0,TT.(i+1).];
A34: S = {0} by A11,A33,XXREAL_1:17;
reconsider S as non empty Subset of I[01] by A11,A33,Lm3,XXREAL_1:17;
A35: dom Fn = [:N2,S:] by A8,A34,RELAT_1:62,ZFMISC_1:96;
reconsider K0 = [:N2,S:] as non empty Subset of [:Y,Sspace(0[01]):] by
A7,A34,Lm14,ZFMISC_1:96;
A36: the carrier of [:Y|N2,I[01]|S:] = [:the carrier of (Y|N2), the
carrier of ( I[01]|S):] & rng Fn c= R by BORSUK_1:def 2,RELAT_1:def 19;
the carrier of (Y|N2) = N2 & the carrier of (I[01]|S) = S
by PRE_TOPC:8;
then reconsider Fn as Function of [:Y|N2,I[01]|S:], R^1 by A35,A36,
FUNCT_2:2;
A37: dom (F | [:N2,S:]) = [:N2,S:] by A6,RELAT_1:62,ZFMISC_1:96;
reconsider S1 = S as non empty Subset of Sspace(0[01]) by A11,A33,Lm14,
XXREAL_1:17;
take S, Fn;
thus S = [.0,TT.(i+1).];
thus y in N2 by A15;
thus N2 c= N;
I[01]|S = Sspace(0[01]) by A34,TOPALG_3:5
.= (Sspace(0[01]))|S1 by A34,Lm14,TSEP_1:3;
then [:Y|N2,I[01]|S:] = [:Y,Sspace(0[01]):]|K0 by BORSUK_3:22;
hence Fn is continuous by A4,A34,TOPMETR:7;
rng Fn c= dom CircleMap by Lm12,TOPMETR:17;
then
A38: dom (CircleMap*Fn) = dom Fn by RELAT_1:27;
A39: [:N2,S:] c= dom Ft by A8,A34,ZFMISC_1:96;
for x being object st x in dom (F | [:N2,S:]) holds (F | [:N2,S:]).x
= (CircleMap*Fn).x
proof
let x be object such that
A40: x in dom (F | [:N2,S:]);
thus (F | [:N2,S:]).x = F.x by A37,A40,FUNCT_1:49
.= (CircleMap*Ft).x by A5,A7,A35,A37,A40,Lm14,FUNCT_1:49
.= CircleMap.(Ft.x) by A39,A37,A40,FUNCT_1:13
.= CircleMap.(Fn.x) by A34,A37,A40,FUNCT_1:49
.= (CircleMap*Fn).x by A35,A37,A40,FUNCT_1:13;
end;
hence F | [:N2,S:] = CircleMap*Fn by A35,A37,A38;
A41: dom (Fn | [:the carrier of Y,{0}:]) = [:N2,S:] /\ [:the carrier
of Y,{0}:] by A35,RELAT_1:61;
A42: for x being object st x in dom (Fn | [:the carrier of Y,{0}:]) holds
(Fn | [:the carrier of Y,{0}:]).x = (Ft | [:N2,I:]).x
proof
A43: [:N2,{0}:] c= [:N2,I:] by Lm3,ZFMISC_1:95;
let x be object such that
A44: x in dom (Fn | [:the carrier of Y,{0}:]);
A45: x in [:N2,{0}:] by A34,A41,A44,XBOOLE_0:def 4;
x in [:the carrier of Y,{0}:] by A41,A44,XBOOLE_0:def 4;
hence (Fn | [:the carrier of Y,{0}:]).x = Fn.x by FUNCT_1:49
.= Ft.x by A45,FUNCT_1:49
.= (Ft | [:N2,I:]).x by A45,A43,FUNCT_1:49;
end;
dom (Ft | [:N2,I:]) = [:the carrier of Y,{0}:] /\ [:N2,I:] by A8,
RELAT_1:61
.= [:N2,S:] by A34,ZFMISC_1:101;
hence thesis by A34,A41,A42,ZFMISC_1:101;
end;
suppose
A46: i in dom TT;
set SS = [.TT.i,TT.(i+1).];
consider Ui being non empty Subset of TUC such that
A47: Ui in UL and
A48: F.:[:N,SS:] c= Ui by A16,A32,A46;
consider D being mutually-disjoint open Subset-Family of R^1 such that
A49: union D = (CircleMap)"Ui and
A50: for d being Subset of R^1 st d in D for f being Function of
R^1 | d, TUC | Ui st f = CircleMap|d holds f is being_homeomorphism by A2,A47;
A51: the carrier of (TUC | Ui) = Ui by PRE_TOPC:8;
A52: TT.i < TT.(i+1) by A19,A32,A46;
then TT.i in SS by XXREAL_1:1;
then
A53: [y,TT.i] in [:N,SS:] by A15,ZFMISC_1:87;
consider N2 being open Subset of Y, S being non empty Subset of I[01],
Fn being Function of [:Y|N2,I[01]|S:], R^1 such that
A54: S = [.0,TT.i.] and
A55: y in N2 and
A56: N2 c= N and
A57: Fn is continuous and
A58: F | [:N2,S:] = CircleMap*Fn and
A59: Fn | [:the carrier of Y,{0}:] = Ft | [:N2,I:] by A31,A46;
reconsider N2 as non empty open Subset of Y by A55;
A60: the carrier of [:Y|N2,I[01]|S:] = [:the carrier of (Y|N2), the
carrier of (I[01]|S):] by BORSUK_1:def 2;
N2 c= N2;
then reconsider N7 = N2 as non empty Subset of Y|N2 by PRE_TOPC:8;
A61: dom Fn = the carrier of [:Y|N2,I[01]|S:] by FUNCT_2:def 1;
A62: 0 <= TT.i by A19,A46;
then
A63: TT.i in S by A54,XXREAL_1:1;
then reconsider Ti = {TT.i} as non empty Subset of I[01] by ZFMISC_1:31
;
A64: the carrier of I[01]|S = S by PRE_TOPC:8;
then reconsider Ti2 = Ti as non empty Subset of I[01]|S by A63,
ZFMISC_1:31;
set FnT = Fn | [:N2,Ti:];
A65: the carrier of [:Y|N2,I[01]|Ti:] = [:the carrier of Y|N2, the
carrier of I[01]|Ti:] & rng FnT c= REAL by BORSUK_1:def 2;
A66: [:N2,SS:] c= [:N,SS:] by A56,ZFMISC_1:96;
A67: the carrier of (Y|N2) = N2 by PRE_TOPC:8;
{TT.i} c= S by A63,ZFMISC_1:31;
then
A68: dom FnT = [:N2,{TT.i}:] by A64,A60,A67,A61,RELAT_1:62,ZFMISC_1:96;
A69: [:Y|N2|N7,I[01]|S|Ti2:] = [:Y|N2,I[01]|S:] | [:N7,Ti2:] by BORSUK_3:22;
A70: the carrier of I[01]|Ti = Ti by PRE_TOPC:8;
rng FnT c= the carrier of R^1 by RELAT_1:def 19;
then reconsider FnT as Function of [:Y|N2,I[01]|Ti:],R^1
by A67,A68,A65,A70,FUNCT_2:2;
Y|N2|N7 = Y|N2 & I[01]|S|Ti2 = I[01]|Ti by GOBOARD9:2;
then
A71: FnT is continuous by A57,A69,TOPMETR:7;
A72: Fn. [y,TT.i] in REAL by XREAL_0:def 1;
[y,TT.i] in dom F by A6,A63,ZFMISC_1:87;
then
A73: F. [y,TT.i] in F.:[:N,SS:] by A53,FUNCT_2:35;
A74: [y,TT.i] in [:N2,S:] by A55,A63,ZFMISC_1:87;
then F. [y,TT.i] = (CircleMap*Fn). [y,TT.i] by A58,FUNCT_1:49
.= CircleMap.(Fn. [y,TT.i]) by A64,A60,A67,A74,FUNCT_2:15;
then Fn. [y,TT.i] in (CircleMap)"Ui
by A48,A73,FUNCT_2:38,TOPMETR:17,A72;
then consider Uit being set such that
A75: Fn. [y,TT.i] in Uit and
A76: Uit in D by A49,TARSKI:def 4;
reconsider Uit as non empty Subset of R^1 by A75,A76;
[#]R^1 <> {} & Uit is open by A76,TOPS_2:def 1;
then FnT"Uit is open by A71,TOPS_2:43;
then consider SF being Subset-Family of [:Y|N2,I[01]|Ti:] such that
A77: FnT"Uit = union SF and
A78: for e being set st e in SF ex X1 being Subset of Y|N2, Y1
being Subset of I[01]|Ti st e = [:X1,Y1:] & X1 is open & Y1 is open by
BORSUK_1:5;
A79: TT.i in {TT.i} by TARSKI:def 1;
then
A80: [y,TT.i] in [:N2,{TT.i}:] by A55,ZFMISC_1:def 2;
then FnT. [y,TT.i] in Uit by A75,FUNCT_1:49;
then [y,TT.i] in FnT"Uit by A80,A68,FUNCT_1:def 7;
then consider N5 being set such that
A81: [y,TT.i] in N5 and
A82: N5 in SF by A77,TARSKI:def 4;
set f = CircleMap|Uit;
A83: dom f = Uit by Lm12,RELAT_1:62,TOPMETR:17;
A84: rng f c= Ui
proof
let b be object;
assume b in rng f;
then consider a being object such that
A85: a in dom f and
A86: f.a = b by FUNCT_1:def 3;
a in union D by A76,A83,A85,TARSKI:def 4;
then CircleMap.a in Ui by A49,FUNCT_2:38;
hence thesis by A83,A85,A86,FUNCT_1:49;
end;
consider X1 being Subset of Y|N2, Y1 being Subset of I[01]|Ti such
that
A87: N5 = [:X1,Y1:] and
A88: X1 is open and
Y1 is open by A78,A82;
the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8;
then reconsider f as Function of R^1 | Uit, TUC | Ui
by A51,A83,A84,FUNCT_2:2;
consider NY being Subset of Y such that
A89: NY is open and
A90: NY /\ [#](Y|N2) = X1 by A88,TOPS_2:24;
consider y1, y2 being object such that
A91: y1 in X1 and
A92: y2 in Y1 and
A93: [y,TT.i] = [y1,y2] by A81,A87,ZFMISC_1:def 2;
set N1 = NY /\ N2;
y = y1 by A93,XTUPLE_0:1;
then
A94: y in NY by A90,A91,XBOOLE_0:def 4;
then reconsider N1 as non empty open Subset of Y by A55,A89,
XBOOLE_0:def 4;
A95: N1 c= N2 by XBOOLE_1:17;
then [:N1,SS:] c= [:N2,SS:] by ZFMISC_1:96;
then [:N1,SS:] c= [:N,SS:] by A66;
then
A96: F.:[:N1,SS:] c= F.:[:N,SS:] by RELAT_1:123;
TT.(i+1) <= 1 by A19,A32,A46;
then reconsider SS as non empty Subset of I[01] by A25,A62,A52,
XXREAL_1:1;
A97: dom (F| [:N1,SS:]) = [:N1,SS:] by A6,RELAT_1:62,ZFMISC_1:96;
set Fni1 = f"*(F| [:N1,SS:]);
f" is being_homeomorphism by A50,A76,TOPS_2:56;
then
A98: dom (f") = [#](TUC | Ui);
A99: rng (F| [:N1,SS:]) c= dom (f")
proof
let b be object;
assume b in rng (F| [:N1,SS:]);
then consider a being object such that
A100: a in dom (F| [:N1,SS:]) and
A101: (F| [:N1,SS:]).a = b by FUNCT_1:def 3;
b = F.a by A97,A100,A101,FUNCT_1:49;
then b in F.:[:N1,SS:] by A97,A100,FUNCT_2:35;
then b in F.:[:N,SS:] by A96;
then b in Ui by A48;
hence thesis by A98,PRE_TOPC:8;
end;
then
A102: dom Fni1 = dom (F| [:N1,SS:]) by RELAT_1:27;
set Fn2 = Fn | [:N1,S:];
A103: the carrier of (Y|N1) = N1 by PRE_TOPC:8;
then
A104: [:N1,S:] = the carrier of [:Y|N1,I[01]|S:] by A64,BORSUK_1:def 2;
then
A105: dom Fn2 = the carrier of [:Y|N1,I[01]|S:] by A64,A60,A67,A61,A95,
RELAT_1:62,ZFMISC_1:96;
reconsider ff = f as Function;
A106: f is being_homeomorphism by A50,A76;
then
A107: f is one-to-one;
A108: rng Fn2 c= R by RELAT_1:def 19;
AAA: rng Fni1 c= the carrier of (R^1 | Uit) by RELAT_1:def 19;
the carrier of (R^1 | Uit) is Subset of R^1 by TSEP_1:1;
then
A109: rng Fni1 c= R by AAA,XBOOLE_1:1;
A110: the carrier of (I[01]|SS) = SS by PRE_TOPC:8;
then
A111: [:N1,SS:] = the carrier of [:Y|N1,I[01]|SS:] by A103,BORSUK_1:def 2;
then reconsider
Fni1 as Function of [:Y|N1,I[01]|SS:], R^1 by A97,A102,A109,FUNCT_2:2;
reconsider Fn2 as Function of [:Y|N1,I[01]|S:],R^1
by A105,A108,FUNCT_2:2;
set Fn1 = Fn2 +* Fni1;
A112: rng Fn1 c= rng Fn2 \/ rng Fni1 by FUNCT_4:17;
dom (Fn | [:N1,S:]) = [:N1,S:]
by A64,A60,A67,A61,A95,RELAT_1:62,ZFMISC_1:96;
then
A113: dom Fn1 = [:N1,S:] \/ [:N1,SS:] by A97,A102,FUNCT_4:def 1;
A114: rng f = [#](TUC | Ui) by A106;
then f is onto;
then
A115: f" = ff" by A107,TOPS_2:def 4;
A116: Y1 = Ti
proof
thus Y1 c= Ti by A70;
let a be object;
assume a in Ti;
then a = TT.i by TARSKI:def 1;
hence thesis by A92,A93,XTUPLE_0:1;
end;
A117: Fn.:[:N1,{TT.i}:] c= Uit
proof
let b be object;
assume b in Fn.:[:N1,{TT.i}:];
then consider a being Point of [:Y|N2,I[01]|S:] such that
A118: a in [:N1,{TT.i}:] and
A119: Fn.a = b by FUNCT_2:65;
a in N5 by A87,A90,A116,A118,PRE_TOPC:def 5;
then
A120: a in union SF by A82,TARSKI:def 4;
then a in dom FnT by A77,FUNCT_1:def 7;
then Fn.a = FnT.a by FUNCT_1:47;
hence thesis by A77,A119,A120,FUNCT_1:def 7;
end;
A121: for p being set st p in ([#][:Y|N1,I[01]|S:]) /\ [#][:Y|N1,I[01]
|SS:] holds Fn2.p = Fni1.p
proof
A122: the carrier of (Y|N2) = N2 by PRE_TOPC:8;
let p be set such that
A123: p in ([#][:Y|N1,I[01]|S:]) /\ [#][:Y|N1,I[01]|SS:];
A124: p in ([#][:Y|N1,I[01]|SS:]) /\ [#][:Y|N1,I[01]|S:] by A123;
then
A125: Fn.p = Fn2.p by A104,FUNCT_1:49;
[:N1,S:] /\ [:N1,SS:] = [:N1,S /\ SS:] by ZFMISC_1:99;
then
A126: p in [:N1,{TT.i}:] by A54,A62,A52,A111,A104,A123,XXREAL_1:418;
then consider
p1 being Element of N1, p2 being Element of {TT.i} such
that
A127: p = [p1,p2] by DOMAIN_1:1;
A128: p1 in N1;
S /\ SS = {TT.i} by A54,A62,A52,XXREAL_1:418;
then p2 in S by XBOOLE_0:def 4;
then
A129: p in [:N2,S:] by A95,A127,A128,ZFMISC_1:def 2;
then
A130: Fn.p in Fn.:[:N1,{TT.i}:] by A64,A60,A67,A126,FUNCT_2:35;
(F| [:N1,SS:]).p = F.p by A111,A123,FUNCT_1:49
.= (F | [:N2,S:]).p by A129,FUNCT_1:49
.= CircleMap.(Fn.p) by A58,A64,A60,A61,A122,A129,FUNCT_1:13
.= (CircleMap|Uit).(Fn.p) by A117,A130,FUNCT_1:49
.= ff.(Fn2.p) by A104,A124,FUNCT_1:49;
hence Fn2.p = ff".((F| [:N1,SS:]).p) by A117,A83,A107,A125,A130,
FUNCT_1:32
.= Fni1.p by A115,A97,A111,A123,FUNCT_1:13;
end;
A131: [:N1,S:] c= [:N2,S:] by A95,ZFMISC_1:96;
then reconsider
K0 = [:N1,S:] as Subset of [:Y|N2,I[01]|S:] by A64,A60,PRE_TOPC:8;
A132: [:N1,SS:] c= dom F by A6,ZFMISC_1:96;
reconsider gF = F| [:N1,SS:] as Function of [:Y|N1,I[01]|SS:], TUC by
A97,A99,A111,FUNCT_2:2;
reconsider fF = F| [:N1,SS:] as Function of [:Y|N1,I[01]|SS:], TUC |
Ui by A98,A97,A99,A111,FUNCT_2:2;
[:Y|N1,I[01]|SS:] = [:Y,I[01]:] | [:N1,SS:] by BORSUK_3:22;
then gF is continuous by A3,TOPMETR:7;
then
A133: fF is continuous by TOPMETR:6;
f" is continuous by A106;
then f"*fF is continuous by A133;
then
A134: Fni1 is continuous by PRE_TOPC:26;
reconsider aN1 = N1 as non empty Subset of Y|N2 by A95,PRE_TOPC:8;
S c= S;
then reconsider aS = S as non empty Subset of I[01]|S by PRE_TOPC:8;
[:Y|N2,I[01]|S:] | K0 = [:Y|N2|aN1,I[01]|S|aS:] by BORSUK_3:22
.= [:Y|N1,I[01]|S|aS:] by GOBOARD9:2
.= [:Y|N1,I[01]|S:] by GOBOARD9:2;
then
A135: Fn2 is continuous by A57,TOPMETR:7;
take N1;
take S1 = S \/ SS;
A136: [:N1,S:] \/ [:N1,SS:] = [:N1,S1:] by ZFMISC_1:97;
A137: the carrier of (I[01]|S1) = S1 by PRE_TOPC:8;
then [:N1,S1:] = the carrier of [:Y|N1,I[01]|S1:]
by A103,BORSUK_1:def 2;
then reconsider Fn1 as Function of [:Y|N1,I[01]|S1:], R^1
by A136,A113,A112,FUNCT_2:2,XBOOLE_1:1;
take Fn1;
thus
A138: S1 = [.0,TT.(i+1).] by A54,A62,A52,XXREAL_1:165;
0 <= TT.(i+1) by A19,A32;
then 0 in S1 by A138,XXREAL_1:1;
then
A139: {0} c= S1 by ZFMISC_1:31;
A140: dom (Fn1 | [:the carrier of Y,{0}:]) = dom Fn1 /\ [:the carrier
of Y,{0}:] by RELAT_1:61;
then
A141: dom (Fn1 | [:the carrier of Y,{0}:]) = [:N1 /\ the carrier of Y,
S1 /\ {0}:] by A136,A113,ZFMISC_1:100
.= [:N1,S1 /\ {0}:] by XBOOLE_1:28
.= [:N1,{0}:] by A139,XBOOLE_1:28;
A142: for a being object st a in dom (Fn1 | [:the carrier of Y,{0}:])
holds (Fn1 | [:the carrier of Y,{0}:]).a = (Ft | [:N1,I:]).a
proof
let a be object;
A143: [:N1,I:] c= [:N2,I:] by A95,ZFMISC_1:96;
assume
A144: a in dom (Fn1 | [:the carrier of Y,{0}:]);
then
A145: a in [:the carrier of Y,{0}:] by A140,XBOOLE_0:def 4;
then consider a1, a2 being object such that
a1 in the carrier of Y and
A146: a2 in {0} and
A147: a = [a1,a2] by ZFMISC_1:def 2;
A148: a2 = 0 by A146,TARSKI:def 1;
0 in S by A54,A62,XXREAL_1:1;
then {0} c= S by ZFMISC_1:31;
then
A149: [:N1,{0}:] c= [:N1,S:] by ZFMISC_1:96;
then
A150: a in [:N1,S:] by A141,A144;
A151: [:N1,S:] c= [:N1,I:] by ZFMISC_1:96;
then
A152: a in [:N1,I:] by A150;
per cases;
suppose
A153: not a in dom Fni1;
thus (Fn1 | [:the carrier of Y,{0}:]).a = Fn1.a by A145,FUNCT_1:49
.= (Fn | [:N1,S:]).a by A153,FUNCT_4:11
.= Fn.a by A141,A144,A149,FUNCT_1:49
.= (Ft | [:N2,I:]).a by A59,A145,FUNCT_1:49
.= Ft.a by A152,A143,FUNCT_1:49
.= (Ft | [:N1,I:]).a by A150,A151,FUNCT_1:49;
end;
suppose
A154: a in dom Fni1;
set e = (Ft | [:N1,I:]).a;
a in [:N1,SS:] by A6,A102,A154,RELAT_1:62,ZFMISC_1:96;
then consider b1, b2 being object such that
A155: b1 in N1 and
A156: b2 in SS and
A157: a = [b1,b2] by ZFMISC_1:def 2;
a2 = b2 by A147,A157,XTUPLE_0:1;
then
A158: a2 = TT.i by A62,A148,A156,XXREAL_1:1;
a1 = b1 by A147,A157,XTUPLE_0:1;
then
A159: [a1,TT.i] in [:N1,S:] & [a1,TT.i] in [:N1,{TT.i}:] by A63,A79,A155,
ZFMISC_1:87;
e = Ft.a by A150,A151,FUNCT_1:49
.= (Ft | [:N2,I:]).a by A152,A143,FUNCT_1:49
.= Fn.a by A59,A145,FUNCT_1:49;
then
A160: e in Fn.:[:N1,{TT.i}:] by A64,A60,A67,A61,A131,A147,A158,A159,
FUNCT_1:def 6;
then
A161: ff.e = CircleMap.e by A117,FUNCT_1:49
.= CircleMap.(Ft.a) by A150,A151,FUNCT_1:49
.= (CircleMap*Ft).a by A8,A145,FUNCT_1:13
.= F.a by A5,A145,FUNCT_1:49;
thus (Fn1 | [:the carrier of Y,{0}:]).a = Fn1.a by A145,FUNCT_1:49
.= Fni1.a by A154,FUNCT_4:13
.= ff".((F| [:N1,SS:]).a) by A115,A102,A154,FUNCT_1:13
.= ff".(F.a) by A97,A102,A154,FUNCT_1:49
.= (Ft | [:N1,I:]).a by A117,A83,A107,A160,A161,FUNCT_1:32;
end;
end;
A162: rng Fn1 c= dom CircleMap by Lm12,TOPMETR:17;
then
A163: dom (CircleMap*Fn1) = dom Fn1 by RELAT_1:27;
A164: for a being object st a in dom (CircleMap*Fn1) holds (CircleMap*Fn1
).a = F . a
proof
let a be object such that
A165: a in dom (CircleMap*Fn1);
per cases;
suppose
A166: a in dom Fni1;
A167: [:N1,SS:] c= [:the carrier of Y,I:] by ZFMISC_1:96;
A168: a in [:N1,SS:] by A6,A102,A166,RELAT_1:62,ZFMISC_1:96;
then F.a in F.:[:N1,SS:] by A6,A167,FUNCT_1:def 6;
then
A169: F.a in F.:[:N,SS:] by A96;
then a in F"(dom (ff")) by A6,A48,A51,A98,A115,A168,A167,
FUNCT_1:def 7;
then
A170: a in dom (ff"*F) by RELAT_1:147;
thus (CircleMap*Fn1).a = CircleMap.(Fn1.a) by A165,FUNCT_2:15
.= CircleMap.(Fni1.a) by A166,FUNCT_4:13
.= CircleMap.(f".((F| [:N1,SS:]).a)) by A102,A166,FUNCT_1:13
.= CircleMap.(f".(F.a)) by A97,A102,A166,FUNCT_1:49
.= CircleMap.((ff"*F).a) by A132,A115,A97,A102,A166,FUNCT_1:13
.= (CircleMap*(ff"*F)).a by A170,FUNCT_1:13
.= (CircleMap*ff"*F).a by RELAT_1:36
.= (CircleMap*ff").(F.a) by A132,A97,A102,A166,FUNCT_1:13
.= F.a by A48,A51,A114,A107,A169,TOPALG_3:2;
end;
suppose
A171: not a in dom Fni1;
then
A172: a in [:N1,S:] by A97,A102,A113,A163,A165,XBOOLE_0:def 3;
thus (CircleMap*Fn1).a = CircleMap.(Fn1.a) by A165,FUNCT_2:15
.= CircleMap.(Fn | [:N1,S:].a) by A171,FUNCT_4:11
.= CircleMap.(Fn.a) by A172,FUNCT_1:49
.= (CircleMap*Fn).a by A64,A60,A67,A131,A172,FUNCT_2:15
.= F.a by A58,A131,A172,FUNCT_1:49;
end;
end;
A173: S c= S1 by XBOOLE_1:7;
then
A174: [#](I[01]|S1) = the carrier of (I[01]|S1) & I[01]|S is SubSpace
of I[01]|S1 by A64,A137,TSEP_1:4;
A175: SS c= S1 by XBOOLE_1:7;
then reconsider
F1 = [#](I[01]|S), F2 = [#](I[01]|SS) as Subset of I[01]|S1
by A137,A173,PRE_TOPC:8;
reconsider hS = F1, hSS = F2 as Subset of I[01] by PRE_TOPC:8;
hS is closed by A54,BORSUK_4:23,PRE_TOPC:8;
then
A176: F1 is closed by TSEP_1:8;
thus y in N1 by A55,A94,XBOOLE_0:def 4;
thus N1 c= N by A56,A95;
hSS is closed by BORSUK_4:23,PRE_TOPC:8;
then
A177: F2 is closed by TSEP_1:8;
I[01]|SS is SubSpace of I[01]|S1 by A110,A137,A175,TSEP_1:4;
then ex h being Function of [:Y|N1,I[01]|S1:],R^1 st h = Fn2+*Fni1 &
h is continuous by A64,A110,A137,A174,A176,A177,A135,A134,A121,TOPALG_3:19;
hence Fn1 is continuous;
dom Fn1 = dom F /\ [:N1,S1:] by A6,A136,A113,XBOOLE_1:28,ZFMISC_1:96;
hence F | [:N1,S1:] = CircleMap*Fn1 by A162,A164,FUNCT_1:46,RELAT_1:27;
dom (Ft | [:N1,I:]) = dom Ft /\ [:N1,I:] by RELAT_1:61
.= [:(the carrier of Y) /\ N1,{0} /\ I:] by A8,ZFMISC_1:100
.= [:N1,{0} /\ I:] by XBOOLE_1:28
.= [:N1,{0}:] by Lm3,XBOOLE_1:28;
hence thesis by A141,A142;
end;
end;
A178: N[ 0 ] by FINSEQ_3:24;
for i being Nat holds N[i] from NAT_1:sch 2(A178,A30);
then consider
N2 being non empty open Subset of Y, S being non empty Subset of
I[01], Fn1 being Function of [:Y|N2,I[01]|S:], R^1 such that
A179: S = [.0,TT.len TT.] and
A180: y in N2 and
A181: N2 c= N and
A182: Fn1 is continuous and
A183: F | [:N2,S:] = CircleMap*Fn1 and
A184: Fn1 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] by A17;
Fn1.x in REAL by XREAL_0:def 1;
then reconsider z = Fn1.x as Point of R^1 by TOPMETR:17;
A185: I[01]|S = I[01] by A12,A179,Lm6,BORSUK_1:40,TSEP_1:3;
then reconsider Fn1 as Function of [:Y|N2,I[01]:], R^1;
take z, y, t, N2;
take Fn1;
thus x = [y,t] & z = Fn1.x & y in N2 & Fn1 is continuous & F | [:N2,I:] =
CircleMap*Fn1 & Fn1 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] by A10,A12,A179
,A180,A182,A183,A184,A185,BORSUK_1:40;
let H be Function of [:Y|N2,I[01]:], R^1 such that
A186: H is continuous and
A187: F | [:N2,I:] = CircleMap*H and
A188: H | [:the carrier of Y,{0}:] = Ft | [:N2,I:];
defpred M[Nat] means $1 in dom TT implies ex Z being non empty
Subset of I[01] st Z = [.0,TT.$1.] & Fn1 | [:N2,Z:] = H | [:N2,Z:];
A189: dom Fn1 = the carrier of [:Y|N2,I[01]:] by FUNCT_2:def 1;
A190: the carrier of [:Y|N2,I[01]:] = [:the carrier of Y|N2,I:] & the
carrier of Y |N2 = N2 by BORSUK_1:def 2,PRE_TOPC:8;
A191: dom H = the carrier of [:Y|N2,I[01]:] by FUNCT_2:def 1;
A192: for i being Nat st M[i] holds M[i+1]
proof
let i be Nat such that
A193: M[i] and
A194: i+1 in dom TT;
per cases by A194,TOPREALA:2;
suppose
A195: i = 0;
set Z = [.0,TT.(i+1).];
A196: Z = {0} by A11,A195,XXREAL_1:17;
reconsider Z as non empty Subset of I[01] by A11,A195,Lm3,XXREAL_1:17;
A197: [:N2,Z:] c= [:N2,I:] by ZFMISC_1:95;
then
A198: dom (Fn1 | [:N2,Z:]) = [:N2,Z:] by A190,A189,RELAT_1:62;
A199: for x being object st x in dom (Fn1 | [:N2,Z:]) holds (Fn1 | [:N2,Z
:]).x = (H | [:N2,Z:]).x
proof
let x be object;
A200: [:N2,Z:] c= [:the carrier of Y,Z:] by ZFMISC_1:95;
assume
A201: x in dom (Fn1 | [:N2,Z:]);
hence (Fn1 | [:N2,Z:]).x = Fn1.x by A198,FUNCT_1:49
.= (Fn1 | [:the carrier of Y,{0}:]).x by A196,A198,A201,A200,
FUNCT_1:49
.= H.x by A184,A188,A196,A198,A201,A200,FUNCT_1:49
.= (H | [:N2,Z:]).x by A198,A201,FUNCT_1:49;
end;
take Z;
thus Z = [.0,TT.(i+1).];
dom (H | [:N2,Z:]) = [:N2,Z:] by A191,A190,A197,RELAT_1:62;
hence thesis by A189,A199,RELAT_1:62;
end;
suppose
A202: i in dom TT;
set ZZ = [.TT.i,TT.(i+1).];
A203: 0 <= TT.i by A19,A202;
A204: TT.(i+1) <= 1 by A19,A194,A202;
then reconsider ZZ as Subset of I[01] by A25,A203;
consider Z being non empty Subset of I[01] such that
A205: Z = [.0,TT.i.] and
A206: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A193,A202;
take Z1 = Z \/ ZZ;
A207: TT.i < TT.(i+1) by A19,A194,A202;
hence Z1 = [.0,TT.(i+1).] by A205,A203,XXREAL_1:165;
A208: [:N2,Z1:] c= [:N2,I:] by ZFMISC_1:95;
then
A209: dom (Fn1 | [:N2,Z1:]) = [:N2,Z1:] by A190,A189,RELAT_1:62;
A210: for x being object st x in dom (Fn1 | [:N2,Z1:]) holds (Fn1 | [:N2,
Z1:]).x = (H | [:N2,Z1:]).x
proof
0 <= TT.(i+1) by A19,A194;
then
A211: TT.(i+1) is Point of I[01] by A204,BORSUK_1:43;
0 <= TT.i & TT.i <= 1 by A19,A194,A202;
then TT.i is Point of I[01] by BORSUK_1:43;
then
A212: ZZ is connected by A207,A211,BORSUK_4:24;
consider Ui being non empty Subset of TUC such that
A213: Ui in UL and
A214: F.:[:N,ZZ:] c= Ui by A16,A194,A202;
consider D being mutually-disjoint open Subset-Family of R^1 such
that
A215: union D = (CircleMap)"Ui and
A216: for d being Subset of R^1 st d in D for f being Function
of R^1 | d, TUC | Ui st f = CircleMap|d holds f is being_homeomorphism by A2
,A213;
let x be object such that
A217: x in dom (Fn1 | [:N2,Z1:]);
consider x1, x2 being object such that
A218: x1 in N2 and
A219: x2 in Z1 and
A220: x = [x1,x2] by A209,A217,ZFMISC_1:def 2;
A221: TT.i in ZZ by A207,XXREAL_1:1;
then [x1,TT.i] in [:N,ZZ:] by A181,A218,ZFMISC_1:87;
then
A222: F. [x1,TT.i] in F.:[:N,ZZ:] by FUNCT_2:35;
reconsider xy = {x1} as non empty Subset of Y by A218,ZFMISC_1:31;
A223: xy c= N2 by A218,ZFMISC_1:31;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:Y|N2,I[01]:] by A190,
ZFMISC_1:96;
A224: dom (H | [:xy,ZZ:]) = [:xy,ZZ:] by A191,A190,A223,RELAT_1:62
,ZFMISC_1:96;
A225: D is Cover of Fn1.:xZZ
proof
let b be object;
A226: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96;
assume b in Fn1.:xZZ;
then consider a being Point of [:Y|N2,I[01]:] such that
A227: a in xZZ and
A228: Fn1.a = b by FUNCT_2:65;
xy c= N by A181,A218,ZFMISC_1:31;
then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95;
then a in [:N,ZZ:] by A227;
then
A229: F.a in F.:[:N,ZZ:] by A6,A226,FUNCT_1:def 6;
CircleMap.(Fn1.a) = (CircleMap*Fn1).a by FUNCT_2:15
.= F.a by A12,A179,A183,A190,BORSUK_1:40,FUNCT_1:49;
hence b in union D by A214,A215,A228,A229,Lm12,FUNCT_1:def 7
,TOPMETR:17;
end;
A230: D is Cover of H.:xZZ
proof
let b be object;
A231: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96;
assume b in H.:xZZ;
then consider a being Point of [:Y|N2,I[01]:] such that
A232: a in xZZ and
A233: H.a = b by FUNCT_2:65;
A234: CircleMap.(H.a) = (CircleMap*H).a by FUNCT_2:15
.= F.a by A187,A190,FUNCT_1:49;
xy c= N by A181,A218,ZFMISC_1:31;
then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95;
then a in [:N,ZZ:] by A232;
then F.a in F.:[:N,ZZ:] by A6,A231,FUNCT_1:def 6;
hence b in union D by A214,A215,A233,A234,Lm12,FUNCT_1:def 7
,TOPMETR:17;
end;
A235: H. [x1,TT.i] in REAL by XREAL_0:def 1;
TT.i in Z by A205,A203,XXREAL_1:1;
then
A236: [x1,TT.i] in [:N2,Z:] by A218,ZFMISC_1:87;
then
A237: Fn1. [x1,TT.i] = (Fn1 | [:N2,Z:]). [x1,TT.i] by FUNCT_1:49
.= H. [x1,TT.i] by A206,A236,FUNCT_1:49;
A238: [:N2,Z:] c= [:N2,I:] by ZFMISC_1:95;
then F. [x1,TT.i] = (CircleMap*H). [x1,TT.i] by A187,A236,FUNCT_1:49
.= CircleMap.(H. [x1,TT.i]) by A191,A190,A236,A238,FUNCT_1:13;
then H. [x1,TT.i] in (CircleMap)"Ui by A214,A222,FUNCT_2:38,A235
,TOPMETR:17;
then consider Uith being set such that
A239: H. [x1,TT.i] in Uith and
A240: Uith in D by A215,TARSKI:def 4;
A241: Fn1. [x1,TT.i] in REAL by XREAL_0:def 1;
F. [x1,TT.i] = (CircleMap*Fn1). [x1,TT.i] by A12,A179,A183,A236,A238,
BORSUK_1:40,FUNCT_1:49
.= CircleMap.(Fn1. [x1,TT.i]) by A190,A189,A236,A238,FUNCT_1:13;
then Fn1. [x1,TT.i] in (CircleMap)"Ui by A214,A222,FUNCT_2:38,A241
,TOPMETR:17;
then consider Uit being set such that
A242: Fn1. [x1,TT.i] in Uit and
A243: Uit in D by A215,TARSKI:def 4;
I[01] is SubSpace of I[01] by TSEP_1:2;
then
A244: [:Y|N2,I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21;
xy is connected by A218;
then [:xy,ZZ:] is connected by A212,TOPALG_3:16;
then
A245: xZZ is connected by A244,CONNSP_1:23;
reconsider Uith as non empty Subset of R^1 by A239,A240;
A246: x1 in xy by TARSKI:def 1;
then
A247: [x1,TT.i] in xZZ by A221,ZFMISC_1:87;
then H. [x1,TT.i] in H.:xZZ by FUNCT_2:35;
then Uith meets H.:xZZ by A239,XBOOLE_0:3;
then
A248: H.:xZZ c= Uith by A186,A245,A240,A230,TOPALG_3:12,TOPS_2:61;
reconsider Uit as non empty Subset of R^1 by A242,A243;
set f = CircleMap|Uit;
A249: dom f = Uit by Lm12,RELAT_1:62,TOPMETR:17;
A250: rng f c= Ui
proof
let b be object;
assume b in rng f;
then consider a being object such that
A251: a in dom f and
A252: f.a = b by FUNCT_1:def 3;
a in union D by A243,A249,A251,TARSKI:def 4;
then CircleMap.a in Ui by A215,FUNCT_2:38;
hence thesis by A249,A251,A252,FUNCT_1:49;
end;
the carrier of (TUC | Ui) = Ui & the carrier of (R^1 | Uit) =
Uit by PRE_TOPC:8;
then reconsider f as Function of R^1 | Uit, TUC | Ui by A249,A250,
FUNCT_2:2;
A253: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A190,A189,A223,RELAT_1:62
,ZFMISC_1:96;
H. [x1,TT.i] in H.:xZZ by A191,A247,FUNCT_1:def 6;
then Uit meets Uith by A242,A248,A237,XBOOLE_0:3;
then
A254: Uit = Uith by A243,A240,TAXONOM2:def 5;
A255: rng (H | [:xy,ZZ:]) c= dom f
proof
let b be object;
assume b in rng (H | [:xy,ZZ:]);
then consider a being object such that
A256: a in dom (H | [:xy,ZZ:]) and
A257: (H | [:xy,ZZ:]).a = b by FUNCT_1:def 3;
H.a = b by A224,A256,A257,FUNCT_1:49;
then b in H.:xZZ by A191,A224,A256,FUNCT_1:def 6;
hence thesis by A248,A254,A249;
end;
Fn1. [x1,TT.i] in Fn1.:xZZ by A247,FUNCT_2:35;
then Uit meets Fn1.:xZZ by A242,XBOOLE_0:3;
then
A258: Fn1.:xZZ c= Uit by A182,A185,A243,A245,A225,TOPALG_3:12,TOPS_2:61;
A259: rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be object;
assume b in rng (Fn1 | [:xy,ZZ:]);
then consider a being object such that
A260: a in dom (Fn1 | [:xy,ZZ:]) and
A261: (Fn1 | [:xy,ZZ:]).a = b by FUNCT_1:def 3;
Fn1.a = b by A253,A260,A261,FUNCT_1:49;
then b in Fn1.:xZZ by A189,A253,A260,FUNCT_1:def 6;
hence thesis by A258,A249;
end;
then
A262: dom (f*(Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27;
A263: for x being object st x in dom (f*(Fn1 | [:xy,ZZ:])) holds (f*(
Fn1 | [:xy,ZZ:])).x = (f*(H | [:xy,ZZ:])).x
proof
let x be object such that
A264: x in dom (f*(Fn1 | [:xy,ZZ:]));
A265: Fn1.x in Fn1.:[:xy,ZZ:] by A189,A253,A262,A264,FUNCT_1:def 6;
A266: H.x in H.:[:xy,ZZ:] by A191,A253,A262,A264,FUNCT_1:def 6;
thus (f*(Fn1 | [:xy,ZZ:])).x = ((f*Fn1) | [:xy,ZZ:]).x by
RELAT_1:83
.= (f*Fn1).x by A253,A262,A264,FUNCT_1:49
.= f.(Fn1.x) by A189,A264,FUNCT_1:13
.= CircleMap.(Fn1.x) by A258,A265,FUNCT_1:49
.= (CircleMap*Fn1).x by A189,A264,FUNCT_1:13
.= CircleMap.(H.x) by A12,A179,A183,A187,A191,A264,BORSUK_1:40
,FUNCT_1:13
.= f.(H.x) by A248,A254,A266,FUNCT_1:49
.= (f*H).x by A191,A264,FUNCT_1:13
.= ((f*H) | [:xy,ZZ:]).x by A253,A262,A264,FUNCT_1:49
.= (f*(H | [:xy,ZZ:])).x by RELAT_1:83;
end;
f is being_homeomorphism by A216,A243;
then
A267: f is one-to-one;
dom (f*(H | [:xy,ZZ:])) = dom (H | [:xy,ZZ:]) by A255,RELAT_1:27;
then
A268: f*(Fn1 | [:xy,ZZ:]) = f*(H | [:xy,ZZ:]) by A253,A224,A259,A263,
RELAT_1:27;
per cases;
suppose
x2 in ZZ;
then
A269: x in [:xy,ZZ:] by A220,A246,ZFMISC_1:87;
thus (Fn1 | [:N2,Z1:]).x = Fn1.x by A209,A217,FUNCT_1:49
.= (Fn1 | [:xy,ZZ:]).x by A269,FUNCT_1:49
.= (H | [:xy,ZZ:]).x by A267,A253,A224,A259,A255,A268,FUNCT_1:27
.= H.x by A269,FUNCT_1:49
.= (H | [:N2,Z1:]).x by A209,A217,FUNCT_1:49;
end;
suppose
not x2 in ZZ;
then x2 in Z by A219,XBOOLE_0:def 3;
then
A270: x in [:N2,Z:] by A218,A220,ZFMISC_1:87;
thus (Fn1 | [:N2,Z1:]).x = Fn1.x by A209,A217,FUNCT_1:49
.= (Fn1 | [:N2,Z:]).x by A270,FUNCT_1:49
.= H.x by A206,A270,FUNCT_1:49
.= (H | [:N2,Z1:]).x by A209,A217,FUNCT_1:49;
end;
end;
dom (H | [:N2,Z1:]) = [:N2,Z1:] by A191,A190,A208,RELAT_1:62;
hence thesis by A189,A210,RELAT_1:62;
end;
end;
A271: M[ 0 ] by FINSEQ_3:24;
for i being Nat holds M[i] from NAT_1:sch 2(A271,A192);
then consider Z being non empty Subset of I[01] such that
A272: Z = [.0,TT.len TT.] and
A273: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A17;
thus Fn1 = Fn1 | [:N2,Z:] by A12,A190,A189,A272,BORSUK_1:40,RELAT_1:69
.= H by A12,A191,A190,A272,A273,BORSUK_1:40,RELAT_1:69;
end;
consider G being Function of [:Y,I[01]:],R^1 such that
A274: for x being Point of [:Y,I[01]:] holds A[x,G.x] from FUNCT_2:sch 3
(A9 );
take G;
A275: now
let N be Subset of Y, F be Function of [:Y|N,I[01]:],R^1;
thus dom F = the carrier of [:Y|N,I[01]:] by FUNCT_2:def 1
.= [:the carrier of Y|N,I:] by BORSUK_1:def 2
.= [:N,I:] by PRE_TOPC:8;
end;
A276: for p being Point of [:Y,I[01]:], y being Point of Y, t being Point of
I[01], N1, N2 being non empty open Subset of Y, Fn1 being Function of [:Y|N1,
I[01]:],R^1, Fn2 being Function of [:Y|N2,I[01]:],R^1 st p = [y,t] & y in N1 &
y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2,I:] = CircleMap*Fn2
& Fn2 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] & F | [:N1,I:] = CircleMap*Fn1
& Fn1 | [:the carrier of Y,{0}:] = Ft | [:N1,I:] holds Fn1 | [:{y},I:] = Fn2 |
[:{y},I:]
proof
let p be Point of [:Y,I[01]:], y be Point of Y, t be Point of I[01], N1,
N2 be non empty open Subset of Y, Fn1 be Function of [:Y|N1,I[01]:],R^1, Fn2 be
Function of [:Y|N2,I[01]:],R^1 such that
p = [y,t] and
A277: y in N1 and
A278: y in N2 and
A279: Fn2 is continuous and
A280: Fn1 is continuous and
A281: F | [:N2,I:] = CircleMap*Fn2 and
A282: Fn2 | [:the carrier of Y,{0}:] = Ft | [:N2,I:] and
A283: F | [:N1,I:] = CircleMap*Fn1 and
A284: Fn1 | [:the carrier of Y,{0}:] = Ft | [:N1,I:];
A285: {y} c= N1 by A277,ZFMISC_1:31;
consider TT being non empty FinSequence of REAL such that
A286: TT.1 = 0 and
A287: TT.len TT = 1 and
A288: TT is increasing and
A289: ex N being open Subset of Y st y in N & for i being Nat
st i in dom TT & i+1 in dom TT ex Ui being non empty Subset of
Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1).]:] c= Ui by A3,A1,Th21;
consider N being open Subset of Y such that
A290: y in N and
A291: for i being Nat st i in dom TT & i+1 in dom TT ex Ui
being non empty Subset of Tunit_circle(2) st Ui in UL & F.:[:N,[.TT.i,TT.(i+1)
.]:] c= Ui by A289;
reconsider N as non empty open Subset of Y by A290;
defpred M[Nat] means $1 in dom TT implies ex Z being non empty
Subset of I[01] st Z = [.0,TT.$1.] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:];
A292: len TT in dom TT by FINSEQ_5:6;
A293: dom Fn2 = the carrier of [:Y|N2,I[01]:] by FUNCT_2:def 1;
A294: dom Fn2 = [:N2,I:] by A275;
A295: {y} c= N2 by A278,ZFMISC_1:31;
A296: the carrier of [:Y|N1,I[01]:] = [:the carrier of Y|N1,I:] & the
carrier of Y |N1 = N1 by BORSUK_1:def 2,PRE_TOPC:8;
A297: the carrier of [:Y|N2,I[01]:] = [:the carrier of Y|N2,I:] & the
carrier of Y |N2 = N2 by BORSUK_1:def 2,PRE_TOPC:8;
A298: dom Fn1 = [:N1,I:] by A275;
A299: dom Fn1 = the carrier of [:Y|N1,I[01]:] by FUNCT_2:def 1;
A300: 1 in dom TT by FINSEQ_5:6;
A301: for i being Nat st M[i] holds M[i+1]
proof
let i be Nat such that
A302: M[i] and
A303: i+1 in dom TT;
per cases by A303,TOPREALA:2;
suppose
A304: i = 0;
set Z = [.0,TT.(i+1).];
A305: Z = {0} by A286,A304,XXREAL_1:17;
reconsider Z as non empty Subset of I[01] by A286,A304,Lm3,XXREAL_1:17;
A306: [:{y},Z:] c= [:N2,I:] by A295,ZFMISC_1:96;
A307: dom (Fn1 | [:{y},Z:]) = [:{y},Z:] by A285,A298,RELAT_1:62,ZFMISC_1:96;
A308: [:{y},Z:] c= [:N1,I:] by A285,ZFMISC_1:96;
A309: for x being object st x in dom (Fn1 | [:{y},Z:]) holds (Fn1 | [:{y}
,Z:]).x = (Fn2 | [:{y},Z:]).x
proof
let x be object;
A310: [:{y},Z:] c= [:the carrier of Y,Z:] by ZFMISC_1:95;
assume
A311: x in dom (Fn1 | [:{y},Z:]);
hence (Fn1 | [:{y},Z:]).x = Fn1.x by A307,FUNCT_1:49
.= (Fn1 | [:the carrier of Y,{0}:]).x by A305,A307,A311,A310,
FUNCT_1:49
.= Ft.x by A284,A308,A307,A311,FUNCT_1:49
.= (Ft | [:N2,I:]).x by A307,A306,A311,FUNCT_1:49
.= Fn2.x by A282,A305,A307,A311,A310,FUNCT_1:49
.= (Fn2 | [:{y},Z:]).x by A307,A311,FUNCT_1:49;
end;
take Z;
thus Z = [.0,TT.(i+1).];
dom (Fn2 | [:{y},Z:]) = [:{y},Z:] by A295,A294,RELAT_1:62,ZFMISC_1:96;
hence thesis by A307,A309;
end;
suppose
A312: i in dom TT;
A313: now
let i be Element of NAT such that
A314: i in dom TT;
1 <= i by A314,FINSEQ_3:25;
then 1 = i or 1 < i by XXREAL_0:1;
hence
A315: 0 <= TT.i by A286,A288,A300,A314,SEQM_3:def 1;
assume
A316: i+1 in dom TT;
A317: i+0 < i+1 by XREAL_1:8;
hence
A318: TT.i < TT.(i+1) by A288,A314,A316,SEQM_3:def 1;
i+1 <= len TT by A316,FINSEQ_3:25;
then i+1 = len TT or i+1 < len TT by XXREAL_0:1;
hence TT.(i+1) <= 1 by A287,A288,A292,A316,SEQM_3:def 1;
hence TT.i < 1 by A318,XXREAL_0:2;
thus 0 < TT.(i+1) by A288,A314,A315,A316,A317,SEQM_3:def 1;
end;
then
A319: 0 <= TT.i by A312;
A320: TT.(i+1) <= 1 by A303,A312,A313;
set ZZ = [.TT.i,TT.(i+1).];
consider Z being non empty Subset of I[01] such that
A321: Z = [.0,TT.i.] and
A322: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A302,A312;
now
let i be Nat such that
A323: 0 <= TT.i and
A324: TT.(i+1) <= 1;
thus [.TT.i,TT.(i+1).] c= I
proof
let a be object;
assume
A325: a in [.TT.i,TT.(i+1).];
then reconsider a as Real;
a <= TT.(i+1) by A325,XXREAL_1:1;
then
A326: a <= 1 by A324,XXREAL_0:2;
0 <= a by A323,A325,XXREAL_1:1;
hence thesis by A326,BORSUK_1:43;
end;
end;
then reconsider ZZ as Subset of I[01] by A319,A320;
take Z1 = Z \/ ZZ;
A327: TT.i < TT.(i+1) by A303,A312,A313;
hence Z1 = [.0,TT.(i+1).] by A321,A319,XXREAL_1:165;
A328: dom (Fn1 | [:{y},Z1:]) = [:{y},Z1:] by A285,A298,RELAT_1:62,ZFMISC_1:96
;
A329: for x being object st x in dom (Fn1 | [:{y},Z1:]) holds (Fn1 | [:{y
},Z1:]).x = (Fn2 | [:{y},Z1:]).x
proof
0 <= TT.(i+1) by A303,A313;
then
A330: TT.(i+1) is Point of I[01] by A320,BORSUK_1:43;
0 <= TT.i & TT.i <= 1 by A303,A312,A313;
then TT.i is Point of I[01] by BORSUK_1:43;
then
A331: ZZ is connected by A327,A330,BORSUK_4:24;
A332: TT.i in ZZ by A327,XXREAL_1:1;
consider Ui being non empty Subset of TUC such that
A333: Ui in UL and
A334: F.:[:N,ZZ:] c= Ui by A291,A303,A312;
consider D being mutually-disjoint open Subset-Family of R^1 such
that
A335: union D = (CircleMap)"Ui and
A336: for d being Subset of R^1 st d in D for f being Function
of R^1 | d, TUC | Ui st f = CircleMap|d holds f is being_homeomorphism by A2
,A333;
let x be object such that
A337: x in dom (Fn1 | [:{y},Z1:]);
consider x1, x2 being object such that
A338: x1 in {y} and
A339: x2 in Z1 and
A340: x = [x1,x2] by A328,A337,ZFMISC_1:def 2;
reconsider xy = {x1} as non empty Subset of Y by A338,ZFMISC_1:31;
A341: xy c= N2 by A295,A338,ZFMISC_1:31;
then
A342: [:xy,ZZ:] c= [:N2,I:] by ZFMISC_1:96;
A343: x1 = y by A338,TARSKI:def 1;
then [x1,TT.i] in [:N,ZZ:] by A290,A332,ZFMISC_1:87;
then
A344: F. [x1,TT.i] in F.:[:N,ZZ:] by FUNCT_2:35;
A345: xy c= N1 by A285,A338,ZFMISC_1:31;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:Y|N1,I[01]:] by A296,
ZFMISC_1:96;
xy is connected by A338;
then
A346: [:xy,ZZ:] is connected by A331,TOPALG_3:16;
A347: xy c= N by A290,A343,ZFMISC_1:31;
A348: D is Cover of Fn1.:xZZ
proof
let b be object;
A349: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96;
assume b in Fn1.:xZZ;
then consider a being Point of [:Y|N1,I[01]:] such that
A350: a in xZZ and
A351: Fn1.a = b by FUNCT_2:65;
A352: CircleMap.(Fn1.a) = (CircleMap*Fn1).a by FUNCT_2:15
.= F.a by A283,A296,FUNCT_1:49;
[:xy,ZZ:] c= [:N,ZZ:] by A347,ZFMISC_1:95;
then a in [:N,ZZ:] by A350;
then F.a in F.:[:N,ZZ:] by A6,A349,FUNCT_1:def 6;
hence b in union D by A334,A335,A351,A352,Lm12,FUNCT_1:def 7
,TOPMETR:17;
end;
A353: I[01] is SubSpace of I[01] by TSEP_1:2;
then [:Y|N1,I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21;
then
A354: xZZ is connected by A346,CONNSP_1:23;
reconsider XZZ = [:xy,ZZ:] as Subset of [:Y|N2,I[01]:] by A297,A341,
ZFMISC_1:96;
[:Y|N2,I[01]:] is SubSpace of [:Y,I[01]:] by A353,BORSUK_3:21;
then
A355: XZZ is connected by A346,CONNSP_1:23;
A356: D is Cover of Fn2.:xZZ
proof
let b be object;
A357: [:N,ZZ:] c= [:the carrier of Y,I:] by ZFMISC_1:96;
assume b in Fn2.:xZZ;
then consider a being Point of [:Y|N2,I[01]:] such that
A358: a in xZZ and
A359: Fn2.a = b by FUNCT_2:65;
A360: CircleMap.(Fn2.a) = (CircleMap*Fn2).a by FUNCT_2:15
.= F.a by A281,A297,FUNCT_1:49;
[:xy,ZZ:] c= [:N,ZZ:] by A347,ZFMISC_1:95;
then a in [:N,ZZ:] by A358;
then F.a in F.:[:N,ZZ:] by A6,A357,FUNCT_1:def 6;
hence b in union D by A334,A335,A359,A360,Lm12,FUNCT_1:def 7
,TOPMETR:17;
end;
A361: TT.i in Z by A321,A319,XXREAL_1:1;
then
A362: [x1,TT.i] in [:{y},Z:] by A338,ZFMISC_1:87;
A363: Fn1. [x1,TT.i] in REAL by XREAL_0:def 1;
A364: [:{y},Z:] c= [:N1,I:] by A285,ZFMISC_1:96;
then F. [x1,TT.i] = (CircleMap*Fn1). [x1,TT.i] by A283,A362,
FUNCT_1:49
.= CircleMap.(Fn1. [x1,TT.i]) by A298,A362,A364,FUNCT_1:13;
then Fn1. [x1,TT.i] in (CircleMap)"Ui by A334,A344,FUNCT_2:38,A363
,TOPMETR:17;
then consider Uit being set such that
A365: Fn1. [x1,TT.i] in Uit and
A366: Uit in D by A335,TARSKI:def 4;
reconsider Uit as non empty Subset of R^1 by A365,A366;
set f = CircleMap|Uit;
A367: dom f = Uit by Lm12,RELAT_1:62,TOPMETR:17;
A368: rng f c= Ui
proof
let b be object;
assume b in rng f;
then consider a being object such that
A369: a in dom f and
A370: f.a = b by FUNCT_1:def 3;
a in union D by A366,A367,A369,TARSKI:def 4;
then CircleMap.a in Ui by A335,FUNCT_2:38;
hence thesis by A367,A369,A370,FUNCT_1:49;
end;
the carrier of (TUC | Ui) = Ui & the carrier of (R^1 | Uit) =
Uit by PRE_TOPC:8;
then reconsider f as Function of R^1 | Uit, TUC | Ui by A367,A368,
FUNCT_2:2;
A371: [:N2,Z:] c= [:N2,I:] by ZFMISC_1:95;
A372: Fn2. [x1,TT.i] in REAL by XREAL_0:def 1;
A373: [x1,TT.i] in [:N2,Z:] by A295,A338,A361,ZFMISC_1:87;
then F. [x1,TT.i] = (CircleMap*Fn2). [x1,TT.i] by A281,A371,
FUNCT_1:49
.= CircleMap.(Fn2. [x1,TT.i]) by A293,A297,A373,A371,FUNCT_1:13;
then Fn2. [x1,TT.i] in (CircleMap)"Ui by A334,A344,FUNCT_2:38,A372
,TOPMETR:17;
then consider Uith being set such that
A374: Fn2. [x1,TT.i] in Uith and
A375: Uith in D by A335,TARSKI:def 4;
reconsider Uith as non empty Subset of R^1 by A374,A375;
A376: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A296,A299,A345,RELAT_1:62
,ZFMISC_1:96;
A377: x1 in xy by TARSKI:def 1;
then
A378: [x1,TT.i] in xZZ by A332,ZFMISC_1:87;
then Fn1. [x1,TT.i] in Fn1.:xZZ by FUNCT_2:35;
then Uit meets Fn1.:xZZ by A365,XBOOLE_0:3;
then
A379: Fn1.:xZZ c= Uit by A280,A366,A354,A348,TOPALG_3:12,TOPS_2:61;
A380: rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be object;
assume b in rng (Fn1 | [:xy,ZZ:]);
then consider a being object such that
A381: a in dom (Fn1 | [:xy,ZZ:]) and
A382: (Fn1 | [:xy,ZZ:]).a = b by FUNCT_1:def 3;
Fn1.a = b by A376,A381,A382,FUNCT_1:49;
then b in Fn1.:xZZ by A299,A376,A381,FUNCT_1:def 6;
hence thesis by A379,A367;
end;
then
A383: dom (f*(Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27;
[x1,TT.i] in [:xy,ZZ:] by A338,A343,A332,ZFMISC_1:87;
then [x1,TT.i] in dom Fn2 by A294,A342;
then
A384: Fn2. [x1,TT.i] in Fn2.:xZZ by A378,FUNCT_2:35;
then Uith meets Fn2.:xZZ by A374,XBOOLE_0:3;
then
A385: Fn2.:xZZ c= Uith by A279,A375,A355,A356,TOPALG_3:12,TOPS_2:61;
Fn1. [x1,TT.i] = (Fn1 | [:{y},Z:]). [x1,TT.i] by A362,FUNCT_1:49
.= Fn2. [x1,TT.i] by A322,A362,FUNCT_1:49;
then Uit meets Uith by A365,A384,A385,XBOOLE_0:3;
then
A386: Uit = Uith by A366,A375,TAXONOM2:def 5;
A387: for x being object st x in dom (f*(Fn1 | [:xy,ZZ:])) holds (f*(
Fn1 | [:xy,ZZ:])).x = (f*(Fn2 | [:xy,ZZ:])).x
proof
A388: dom (Fn1 | [:xy,ZZ:]) c= dom Fn1 by RELAT_1:60;
let x be object such that
A389: x in dom (f*(Fn1 | [:xy,ZZ:]));
A390: Fn1.x in Fn1.:[:xy,ZZ:] by A299,A376,A383,A389,FUNCT_1:def 6;
A391: Fn2.x in Fn2.:[:xy,ZZ:] by A294,A342,A376,A383,A389,FUNCT_1:def 6;
dom (Fn1 | [:xy,ZZ:]) = dom Fn1 /\ [:xy,ZZ:] by RELAT_1:61;
then
A392: x in [:xy,ZZ:] by A383,A389,XBOOLE_0:def 4;
thus (f*(Fn1 | [:xy,ZZ:])).x = ((f*Fn1) | [:xy,ZZ:]).x by
RELAT_1:83
.= (f*Fn1).x by A376,A383,A389,FUNCT_1:49
.= f.(Fn1.x) by A299,A389,FUNCT_1:13
.= CircleMap.(Fn1.x) by A379,A390,FUNCT_1:49
.= (CircleMap*Fn1).x by A299,A389,FUNCT_1:13
.= F.x by A283,A298,A383,A389,A388,FUNCT_1:49
.= (CircleMap*Fn2).x by A281,A342,A392,FUNCT_1:49
.= CircleMap.(Fn2.x) by A294,A342,A392,FUNCT_1:13
.= f.(Fn2.x) by A385,A386,A391,FUNCT_1:49
.= (f*Fn2).x by A294,A342,A392,FUNCT_1:13
.= ((f*Fn2) | [:xy,ZZ:]).x by A376,A383,A389,FUNCT_1:49
.= (f*(Fn2 | [:xy,ZZ:])).x by RELAT_1:83;
end;
A393: dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:] by A293,A297,A341,RELAT_1:62
,ZFMISC_1:96;
A394: rng (Fn2 | [:xy,ZZ:]) c= dom f
proof
let b be object;
assume b in rng (Fn2 | [:xy,ZZ:]);
then consider a being object such that
A395: a in dom (Fn2 | [:xy,ZZ:]) and
A396: (Fn2 | [:xy,ZZ:]).a = b by FUNCT_1:def 3;
Fn2.a = b by A393,A395,A396,FUNCT_1:49;
then b in Fn2.:xZZ by A293,A393,A395,FUNCT_1:def 6;
hence thesis by A385,A386,A367;
end;
then dom (f*(Fn2 | [:xy,ZZ:])) = dom (Fn2 | [:xy,ZZ:]) by RELAT_1:27;
then
A397: f*(Fn1 | [:xy,ZZ:]) = f*(Fn2 | [:xy,ZZ:]) by A376,A393,A380,A387,
RELAT_1:27;
f is being_homeomorphism by A336,A366;
then
A398: f is one-to-one;
per cases;
suppose
x2 in ZZ;
then
A399: x in [:xy,ZZ:] by A340,A377,ZFMISC_1:87;
thus (Fn1 | [:{y},Z1:]).x = Fn1.x by A328,A337,FUNCT_1:49
.= (Fn1 | [:xy,ZZ:]).x by A399,FUNCT_1:49
.= (Fn2 | [:xy,ZZ:]).x by A398,A376,A393,A380,A394,A397,
FUNCT_1:27
.= Fn2.x by A399,FUNCT_1:49
.= (Fn2 | [:{y},Z1:]).x by A328,A337,FUNCT_1:49;
end;
suppose
not x2 in ZZ;
then x2 in Z by A339,XBOOLE_0:def 3;
then
A400: x in [:{y},Z:] by A338,A340,ZFMISC_1:87;
thus (Fn1 | [:{y},Z1:]).x = Fn1.x by A328,A337,FUNCT_1:49
.= (Fn1 | [:{y},Z:]).x by A400,FUNCT_1:49
.= Fn2.x by A322,A400,FUNCT_1:49
.= (Fn2 | [:{y},Z1:]).x by A328,A337,FUNCT_1:49;
end;
end;
dom (Fn2 | [:{y},Z1:]) = [:{y},Z1:] by A295,A293,A297,RELAT_1:62
,ZFMISC_1:96;
hence thesis by A328,A329;
end;
end;
A401: M[ 0 ] by FINSEQ_3:24;
for i being Nat holds M[i] from NAT_1:sch 2(A401,A301);
then ex Z being non empty Subset of I[01] st Z = [.0,TT.len TT.] & Fn1 |
[:{y},Z:] = Fn2 | [:{y},Z:] by A292;
hence thesis by A287,BORSUK_1:40;
end;
for p being Point of [:Y,I[01]:], V being Subset of R^1 st G.p in V &
V is open holds ex W being Subset of [:Y,I[01]:] st p in W & W is open & G.:W
c= V
proof
let p be Point of [:Y,I[01]:], V be Subset of R^1 such that
A402: G.p in V & V is open;
consider y being Point of Y, t being Point of I[01], N being non empty
open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that
A403: p = [y,t] and
A404: G.p = Fn.p and
A405: y in N and
A406: Fn is continuous and
A407: F | [:N,I:] = CircleMap*Fn & Fn | [:the carrier of Y,{0}:] = Ft
| [:N,I:] and
for H being Function of [:Y|N,I[01]:], R^1 st H is continuous & F | [:
N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H
by A274;
A408: the carrier of [:Y|N,I[01]:] = [:the carrier of (Y|N),I:] by
BORSUK_1:def 2
.= [:N,I:] by PRE_TOPC:8;
then p in the carrier of [:Y|N,I[01]:] by A403,A405,ZFMISC_1:87;
then consider W being Subset of [:Y|N,I[01]:] such that
A409: p in W and
A410: W is open and
A411: Fn.:W c= V by A402,A404,A406,JGRAPH_2:10;
A412: dom Fn = [:N,I:] by A408,FUNCT_2:def 1;
A413: [#](Y|N) = N by PRE_TOPC:def 5;
then
A414: [#][:Y|N,I[01]:] = [:N,[#]I[01]:] by BORSUK_3:1;
[:Y|N,I[01]:] = [:Y,I[01]:] | [:N,[#]I[01]:] by Lm7,BORSUK_3:22;
then consider C being Subset of [:Y,I[01]:] such that
A415: C is open and
A416: C /\ [#][:Y|N,I[01]:] = W by A410,TOPS_2:24;
take WW = C /\ [:N,[#]I[01]:];
thus p in WW by A409,A416,A413,BORSUK_3:1;
[:N,[#]I[01]:] is open by BORSUK_1:6;
hence WW is open by A415;
let y be object;
assume y in G.:WW;
then consider x being Point of [:Y,I[01]:] such that
A417: x in WW and
A418: y = G.x by FUNCT_2:65;
consider y0 being Point of Y, t0 being Point of I[01], N0 being non empty
open Subset of Y, Fn0 being Function of [:Y|N0,I[01]:], R^1 such that
A419: x = [y0,t0] and
A420: G.x = Fn0.x and
A421: y0 in N0 & Fn0 is continuous & F | [:N0,I:] = CircleMap*Fn0 &
Fn0 | [:the carrier of Y,{0}:] = Ft | [:N0,I :] and
for H being Function of [:Y|N0,I[01]:], R^1 st H is continuous & F |
[:N0,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N0,I:] holds Fn0
= H by A274;
x in [:N,[#]I[01]:] by A417,XBOOLE_0:def 4;
then
A422: y0 in N by A419,ZFMISC_1:87;
A423: x in [:{y0},I:] by A419,ZFMISC_1:105;
then Fn.x = (Fn | [:{y0},I:]).x by FUNCT_1:49
.= (Fn0 | [:{y0},I:]).x by A276,A406,A407,A419,A421,A422
.= Fn0.x by A423,FUNCT_1:49;
then y in Fn.:W by A412,A416,A414,A417,A418,A420,FUNCT_1:def 6;
hence thesis by A411;
end;
hence G is continuous by JGRAPH_2:10;
for x being Point of [:Y,I[01]:] holds F.x = (CircleMap*G).x
proof
let x be Point of [:Y,I[01]:];
consider y being Point of Y, t being Point of I[01], N being non empty
open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that
A424: x = [y,t] and
A425: G.x = Fn.x and
A426: y in N and
Fn is continuous and
A427: F | [:N,I:] = CircleMap*Fn and
Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] and
for H being Function of [:Y|N,I[01]:], R^1 st H is continuous & F | [:
N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H
by A274;
A428: the carrier of [:Y|N,I[01]:] = [:the carrier of (Y|N),I:] by
BORSUK_1:def 2
.= [:N,I:] by PRE_TOPC:8;
then
A429: x in the carrier of [:Y|N,I[01]:] by A424,A426,ZFMISC_1:87;
thus (CircleMap*G).x = CircleMap.(G.x) by FUNCT_2:15
.= (CircleMap*Fn).x by A425,A429,FUNCT_2:15
.= F.x by A427,A428,A429,FUNCT_1:49;
end;
hence F = CircleMap*G;
A430: [:the carrier of Y,{0}:] c= [:the carrier of Y,I:] by Lm3,ZFMISC_1:95;
A431: the carrier of [:Y,I[01]:] = [:the carrier of Y,I:] by BORSUK_1:def 2;
then
A432: dom G = [:the carrier of Y,I:] by FUNCT_2:def 1;
A433: for x being object st x in dom Ft holds Ft.x = G.x
proof
let x be object;
assume
A434: x in dom Ft;
then x in dom G by A8,A432,A430;
then consider
y being Point of Y, t being Point of I[01], N being non empty
open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that
A435: x = [y,t] and
A436: G.x = Fn.x and
A437: y in N and
Fn is continuous and
F | [:N,I:] = CircleMap*Fn and
A438: Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] and
for H being Function of [:Y|N,I[01]:], R^1 st H is continuous & F | [:
N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds Fn = H
by A274;
x in [:N,I:] by A435,A437,ZFMISC_1:87;
hence Ft.x = (Ft | [:N,I:]).x by FUNCT_1:49
.= G.x by A7,A434,A436,A438,Lm14,FUNCT_1:49;
end;
dom Ft = dom G /\ [:the carrier of Y,{0}:] by A8,A432,A430,XBOOLE_1:28;
hence G | [:the carrier of Y,{0}:] = Ft by A433,FUNCT_1:46;
let H be Function of [:Y,I[01]:], R^1 such that
A439: H is continuous & F = CircleMap*H and
A440: H | [:the carrier of Y,{0}:] = Ft;
for x being Point of [:Y,I[01]:] holds G.x = H.x
proof
let x be Point of [:Y,I[01]:];
consider y being Point of Y, t being Point of I[01], N being non empty
open Subset of Y, Fn being Function of [:Y|N,I[01]:], R^1 such that
A441: x = [y,t] and
A442: G.x = Fn.x and
A443: y in N and
Fn is continuous and
F | [:N,I:] = CircleMap*Fn and
Fn | [:the carrier of Y,{0}:] = Ft | [:N,I:] and
A444: for H being Function of [:Y|N,I[01]:], R^1 st H is continuous &
F | [:N,I:] = CircleMap*H & H | [:the carrier of Y,{0}:] = Ft | [:N,I:] holds
Fn = H by A274;
A445: the carrier of [:Y|N,I[01]:] = [:the carrier of (Y|N),I:] by
BORSUK_1:def 2
.= [:N,I:] by PRE_TOPC:8;
then
A446: x in the carrier of [:Y|N,I[01]:] by A441,A443,ZFMISC_1:87;
dom H = the carrier of [:Y,I[01]:] by FUNCT_2:def 1;
then [:N,I:] c= dom H by A431,ZFMISC_1:95;
then
A447: dom (H | [:N,I:]) = [:N,I:] by RELAT_1:62;
rng (H | [:N,I:]) c= R by RELAT_1:def 19;
then reconsider
H1 = H | [:N,I:] as Function of [:Y|N,I[01]:], R^1 by A445,A447,FUNCT_2:2;
A448: H | [:N,I:] | [:the carrier of Y,{0}:] = H | ([:the carrier of Y,{0}
:] /\ [:N,I:]) by RELAT_1:71
.= Ft | [:N,I:] by A440,RELAT_1:71;
H1 is continuous & F | [:N,I:] = CircleMap*(H| [:N,I:]) by A439,RELAT_1:83
,TOPALG_3:17;
hence G.x = (H| [:N,I:]).x by A442,A444,A448
.= H.x by A445,A446,FUNCT_1:49;
end;
hence thesis;
end;
theorem Th23:
for x0, y0 being Point of Tunit_circle(2), xt being Point of R^1
, f being Path of x0,y0 st xt in (CircleMap)"{x0} ex ft being Function of I[01]
, R^1 st ft.0 = xt & f = CircleMap*ft & ft is continuous & for f1 being
Function of I[01], R^1 st f1 is continuous & f = CircleMap*f1 & f1.0 = xt holds
ft = f1
proof
set Y = 1TopSp{1};
let x0, y0 be Point of TUC;
let xt be Point of R^1;
let f be Path of x0,y0;
deffunc F(set,Element of I) = f.$2;
consider F being Function of [:the carrier of Y,I:], cS1 such that
A1: for y being Element of Y, i being Element of I holds F.(y,i) = F(y,i
) from BINOP_1:sch 4;
reconsider j = 1 as Point of Y by TARSKI:def 1;
A2: [j,j0] in [:the carrier of Y,{0}:] by Lm4,ZFMISC_1:87;
A3: the carrier of [:Y,I[01]:] = [:the carrier of Y, I:] by BORSUK_1:def 2;
then reconsider F as Function of [:Y,I[01]:], TUC;
set Ft = [:Y,Sspace(0[01]):] --> xt;
A4: the carrier of [:Y,Sspace(0[01]):] = [:the carrier of Y, the carrier of
Sspace(0[01]):] by BORSUK_1:def 2;
then
A5: for y being Element of Y, i being Element of {0} holds Ft. [y,i] = xt
by Lm14,FUNCOP_1:7;
A6: [#]Y = the carrier of Y;
for p being Point of [:Y,I[01]:], V being Subset of TUC st F.p in V & V
is open holds ex W being Subset of [:Y,I[01]:] st p in W & W is open & F.:W c=
V
proof
let p be Point of [:Y,I[01]:], V be Subset of TUC such that
A7: F.p in V & V is open;
consider p1 being Point of Y, p2 being Point of I[01] such that
A8: p = [p1,p2] by BORSUK_1:10;
F.(p1,p2) = f.p2 by A1;
then consider S being Subset of I[01] such that
A9: p2 in S and
A10: S is open and
A11: f.:S c= V by A7,A8,JGRAPH_2:10;
set W = [:{1},S:];
W c= [:the carrier of Y,I:] by ZFMISC_1:95;
then reconsider W as Subset of [:Y,I[01]:] by BORSUK_1:def 2;
take W;
thus p in W by A8,A9,ZFMISC_1:87;
thus W is open by A6,A10,BORSUK_1:6;
let y be object;
assume y in F.:W;
then consider x being object such that
A12: x in the carrier of [:Y,I[01]:] and
A13: x in W and
A14: y = F.x by FUNCT_2:64;
consider x1 being Point of Y, x2 being Point of I[01] such that
A15: x = [x1,x2] by A12,BORSUK_1:10;
x2 in S by A13,A15,ZFMISC_1:87;
then
A16: f.x2 in f.:S by FUNCT_2:35;
y = F.(x1,x2) by A14,A15
.= f.x2 by A1;
hence thesis by A11,A16;
end;
then
A17: F is continuous by JGRAPH_2:10;
assume xt in (CircleMap)"{x0};
then
A18: CircleMap.xt in {x0} by FUNCT_2:38;
A19: for x being object st x in dom (CircleMap*Ft) holds (F | [:the carrier of
Y,{0}:]).x = (CircleMap*Ft).x
proof
let x be object such that
A20: x in dom (CircleMap*Ft);
consider x1, x2 being object such that
A21: x1 in the carrier of Y and
A22: x2 in {0} and
A23: x = [x1,x2] by A4,A20,Lm14,ZFMISC_1:def 2;
A24: x2 = 0 by A22,TARSKI:def 1;
thus (F | [:the carrier of Y,{0}:]).x = F.(x1,x2) by A4,A20,A23,Lm14,
FUNCT_1:49
.= f.x2 by A1,A21,A24,Lm2
.= x0 by A24,BORSUK_2:def 4
.= CircleMap.xt by A18,TARSKI:def 1
.= CircleMap.(Ft.x) by A5,A21,A22,A23
.= (CircleMap*Ft).x by A20,FUNCT_1:12;
end;
A25: dom (CircleMap*Ft) = [:the carrier of Y,{0}:] by A4,Lm14,FUNCT_2:def 1;
A26: dom F = the carrier of [:Y,I[01]:] by FUNCT_2:def 1;
then
A27: [:the carrier of Y,{0}:] c= dom F by A3,Lm3,ZFMISC_1:95;
then dom (F | [:the carrier of Y,{0}:]) = [:the carrier of Y,{0}:] by
RELAT_1:62;
then consider G being Function of [:Y,I[01]:], R^1 such that
A28: G is continuous and
A29: F = CircleMap*G and
A30: G | [:the carrier of Y,{0}:] = Ft and
A31: for H being Function of [:Y,I[01]:], R^1 st H is continuous & F =
CircleMap*H & H | [:the carrier of Y,{0}:] = Ft holds G = H by A17,A25,A19
,Th22,FUNCT_1:2;
take ft = Prj2(j,G);
thus ft.0 = G.(j,j0) by Def3
.= Ft. [j,j0] by A30,A2,FUNCT_1:49
.= xt by A5,Lm4;
for i being Point of I[01] holds f.i = (CircleMap*ft).i
proof
let i be Point of I[01];
A32: the carrier of [:Y,I[01]:] = [:the carrier of Y, the carrier of I[01]
:] by BORSUK_1:def 2;
thus (CircleMap*ft).i = CircleMap.(ft.i) by FUNCT_2:15
.= CircleMap.(G.(j,i)) by Def3
.= (CircleMap*G).(j,i) by A32,BINOP_1:18
.= f.i by A1,A29;
end;
hence f = CircleMap*ft;
thus ft is continuous by A28;
let f1 be Function of I[01], R^1;
deffunc H(set,Element of I) = f1.$2;
consider H being Function of [:the carrier of Y,I:], R such that
A33: for y being Element of Y, i being Element of I holds H.(y,i) = H(y,
i) from BINOP_1:sch 4;
reconsider H as Function of [:Y,I[01]:], R^1 by A3;
assume that
A34: f1 is continuous and
A35: f = CircleMap*f1 and
A36: f1.0 = xt;
for p being Point of [:Y,I[01]:], V being Subset of R^1 st H.p in V & V
is open holds ex W being Subset of [:Y,I[01]:] st p in W & W is open & H.:W c=
V
proof
let p be Point of [:Y,I[01]:], V be Subset of R^1 such that
A37: H.p in V & V is open;
consider p1 being Point of Y, p2 being Point of I[01] such that
A38: p = [p1,p2] by BORSUK_1:10;
H.p = H.(p1,p2) by A38
.= f1.p2 by A33;
then consider W being Subset of I[01] such that
A39: p2 in W and
A40: W is open and
A41: f1.:W c= V by A34,A37,JGRAPH_2:10;
take W1 = [:[#]Y,W:];
thus p in W1 by A38,A39,ZFMISC_1:87;
thus W1 is open by A40,BORSUK_1:6;
let y be object;
assume y in H.:W1;
then consider c being Element of [:Y,I[01]:] such that
A42: c in W1 and
A43: y = H.c by FUNCT_2:65;
consider c1, c2 being object such that
A44: c1 in [#]Y and
A45: c2 in W and
A46: c = [c1,c2] by A42,ZFMISC_1:def 2;
A47: f1.c2 in f1.:W by A45,FUNCT_2:35;
H.c = H.(c1,c2) by A46
.= f1.c2 by A33,A44,A45;
hence thesis by A41,A43,A47;
end;
then
A48: H is continuous by JGRAPH_2:10;
for x being Point of [:Y,I[01]:] holds F.x = (CircleMap*H).x
proof
let x be Point of [:Y,I[01]:];
consider x1 being Point of Y, x2 being Point of I[01] such that
A49: x = [x1,x2] by BORSUK_1:10;
thus (CircleMap*H).x = CircleMap.(H.(x1,x2)) by A49,FUNCT_2:15
.= CircleMap.(f1.x2) by A33
.= (CircleMap*f1).x2 by FUNCT_2:15
.= F.(x1,x2) by A1,A35
.= F.x by A49;
end;
then
A50: F = CircleMap*H;
for i being Point of I[01] holds ft.i = f1.i
proof
let i be Point of I[01];
A51: dom H = the carrier of [:Y,I[01]:] by FUNCT_2:def 1;
then
A52: dom (H | [:the carrier of Y,{0}:]) = [:the carrier of Y,{0}:] by A26,A27,
RELAT_1:62;
A53: for x being object st x in dom (H | [:the carrier of Y,{0}:]) holds (H |
[:the carrier of Y,{0}:]).x = Ft.x
proof
let x be object;
assume
A54: x in dom (H | [:the carrier of Y,{0}:]);
then consider x1, x2 being object such that
A55: x1 in the carrier of Y and
A56: x2 in {0} and
A57: x = [x1,x2] by A52,ZFMISC_1:def 2;
A58: x2 = j0 by A56,TARSKI:def 1;
thus (H | [:the carrier of Y,{0}:]).x = H.(x1,x2) by A54,A57,FUNCT_1:47
.= f1.x2 by A33,A55,A58
.= Ft.x by A5,A36,A55,A56,A57,A58;
end;
dom Ft = [:the carrier of Y,{0}:] by A4,Lm14,FUNCT_2:def 1;
then
A59: H | [:the carrier of Y,{0}:] = Ft by A26,A27,A51,A53,RELAT_1:62;
thus ft.i = G.(j,i) by Def3
.= H.(j,i) by A31,A50,A48,A59
.= f1.i by A33;
end;
hence thesis;
end;
theorem Th24:
for x0, y0 being Point of Tunit_circle(2), P, Q being Path of x0
,y0, F being Homotopy of P,Q, xt being Point of R^1 st P,Q are_homotopic & xt
in (CircleMap)"{x0} ex yt being Point of R^1, Pt, Qt being Path of xt,yt, Ft
being Homotopy of Pt,Qt st Pt,Qt are_homotopic & F = CircleMap*Ft & yt in (
CircleMap)"{y0} & for F1 being Homotopy of Pt,Qt st F = CircleMap*F1 holds Ft =
F1
proof
let x0, y0 be Point of TUC;
let P, Q be Path of x0,y0;
let F be Homotopy of P,Q;
let xt be Point of R^1;
set cP1 = the constant Loop of x0;
set g1 = I[01] --> xt;
set cP2 = the constant Loop of y0;
assume
A1: P,Q are_homotopic;
then
A2: F is continuous by BORSUK_6:def 11;
assume
A3: xt in (CircleMap)"{x0};
then consider ft being Function of I[01], R^1 such that
A4: ft.0 = xt and
A5: P = CircleMap*ft and
A6: ft is continuous and
for f1 being Function of I[01], R^1 st f1 is continuous & P = CircleMap*
f1 & f1.0 = xt holds ft = f1 by Th23;
defpred P[set,set,set] means $3 = ft.$1;
A7: for x being Element of I for y being Element of {0} ex z being Element
of REAL st P[x,y,z]
proof let x be Element of I;
ft.x in REAL by XREAL_0:def 1;
hence thesis;
end;
consider Ft being Function of [:I,{0}:], REAL such that
A8: for y being Element of I, i being Element of {0} holds P[y,i, Ft.(y
,i)] from BINOP_1:sch 3(A7);
CircleMap.xt in {x0} by A3,FUNCT_2:38;
then
A9: CircleMap.xt = x0 by TARSKI:def 1;
A10: for x being Point of I[01] holds cP1.x = (CircleMap*g1).x
proof
let x be Point of I[01];
thus cP1.x = x0 by TOPALG_3:21
.= CircleMap.(g1.x) by A9,TOPALG_3:4
.= (CircleMap*g1).x by FUNCT_2:15;
end;
consider ft1 being Function of I[01], R^1 such that
ft1.0 = xt and
cP1 = CircleMap*ft1 and
ft1 is continuous and
A11: for f1 being Function of I[01], R^1 st f1 is continuous & cP1 =
CircleMap*f1 & f1.0 = xt holds ft1 = f1 by A3,Th23;
g1.j0 = xt by TOPALG_3:4;
then
A12: ft1 = g1 by A11,A10,FUNCT_2:63;
A13: rng Ft c= REAL;
A14: dom Ft = [:I,{0}:] by FUNCT_2:def 1;
A15: the carrier of [:I[01],Sspace(0[01]):] = [:I, the carrier of Sspace(
0[01]):] by BORSUK_1:def 2;
then reconsider Ft as Function of [:I[01],Sspace(0[01]):], R^1 by Lm14,
TOPMETR:17;
A16: for x being object st x in dom (CircleMap*Ft) holds (F | [:I,{0}:]).x = (
CircleMap*Ft).x
proof
let x be object such that
A17: x in dom (CircleMap*Ft);
consider x1, x2 being object such that
A18: x1 in I and
A19: x2 in {0} and
A20: x = [x1,x2] by A15,A17,Lm14,ZFMISC_1:def 2;
x2 = 0 by A19,TARSKI:def 1;
hence (F | [:I,{0}:]).x = F.(x1,0) by A15,A17,A20,Lm14,FUNCT_1:49
.= (CircleMap*ft).x1 by A1,A5,A18,BORSUK_6:def 11
.= CircleMap.(ft.x1) by A18,FUNCT_2:15
.= CircleMap.(Ft.(x1,x2)) by A8,A18,A19
.= (CircleMap*Ft).x by A17,A20,FUNCT_1:12;
end;
for p being Point of [:I[01],Sspace(0[01]):], V being Subset of R^1 st
Ft.p in V & V is open holds ex W being Subset of [:I[01],Sspace(0[01]):] st p
in W & W is open & Ft.:W c= V
proof
let p be Point of [:I[01],Sspace(0[01]):], V be Subset of R^1 such that
A21: Ft.p in V & V is open;
consider p1 being Point of I[01], p2 being Point of Sspace(0[01]) such
that
A22: p = [p1,p2] by A15,DOMAIN_1:1;
P[p1,p2,Ft.(p1,p2)] by A8,Lm14;
then consider W1 being Subset of I[01] such that
A23: p1 in W1 and
A24: W1 is open and
A25: ft.:W1 c= V by A6,A21,A22,JGRAPH_2:10;
reconsider W1 as non empty Subset of I[01] by A23;
take W = [:W1,[#]Sspace(0[01]):];
thus p in W by A22,A23,ZFMISC_1:def 2;
thus W is open by A24,BORSUK_1:6;
let y be object;
assume y in Ft.:W;
then consider x being Element of [:I[01],Sspace(0[01]):] such that
A26: x in W and
A27: y = Ft.x by FUNCT_2:65;
consider x1 being Element of W1, x2 being Point of Sspace(0[01]) such that
A28: x = [x1,x2] by A26,DOMAIN_1:1;
( P[x1,x2,Ft.(x1,x2)])& ft.x1 in ft.:W1 by A8,Lm14,FUNCT_2:35;
hence thesis by A25,A27,A28;
end;
then
A29: Ft is continuous by JGRAPH_2:10;
take yt = ft.j1;
A30: [j1,j0] in [:I,{0}:] by Lm4,ZFMISC_1:87;
reconsider ft as Path of xt,yt by A4,A6,BORSUK_2:def 4;
A31: [j0,j0] in [:I,{0}:] by Lm4,ZFMISC_1:87;
A32: dom F = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1;
then
A33: [:I,{0}:] c= dom F by Lm3,Lm5,ZFMISC_1:95;
then dom (F | [:I,{0}:]) = [:I,{0}:] by RELAT_1:62;
then F | [:I,{0}:] = CircleMap*Ft by A14,A13,A16,Lm12,FUNCT_1:2,RELAT_1:27;
then consider G being Function of [:I[01],I[01]:], R^1 such that
A34: G is continuous and
A35: F = CircleMap*G and
A36: G | [:I,{0}:] = Ft and
A37: for H being Function of [:I[01],I[01]:], R^1 st H is continuous & F
= CircleMap*H & H | [:the carrier of I[01],{0}:] = Ft holds G = H by A2,A29
,Th22;
set sM0 = Prj2(j0,G);
A38: for x being Point of I[01] holds cP1.x = (CircleMap*sM0).x
proof
let x be Point of I[01];
thus (CircleMap*sM0).x = CircleMap.(sM0.x) by FUNCT_2:15
.= CircleMap.(G.(j0,x)) by Def3
.= (CircleMap*G).(j0,x) by Lm5,BINOP_1:18
.= x0 by A1,A35,BORSUK_6:def 11
.= cP1.x by TOPALG_3:21;
end;
set g2 = I[01] --> yt;
A39: CircleMap.yt = P.j1 by A5,FUNCT_2:15
.= y0 by BORSUK_2:def 4;
A40: for x being Point of I[01] holds cP2.x = (CircleMap*g2).x
proof
let x be Point of I[01];
thus cP2.x = y0 by TOPALG_3:21
.= CircleMap.(g2.x) by A39,TOPALG_3:4
.= (CircleMap*g2).x by FUNCT_2:15;
end;
A41: CircleMap.yt in {y0} by A39,TARSKI:def 1;
then yt in (CircleMap)"{y0} by FUNCT_2:38;
then consider ft2 being Function of I[01], R^1 such that
ft2.0 = yt and
cP2 = CircleMap*ft2 and
ft2 is continuous and
A42: for f1 being Function of I[01], R^1 st f1 is continuous & cP2 =
CircleMap*f1 & f1.0 = yt holds ft2 = f1 by Th23;
g2.j0 = yt by TOPALG_3:4;
then
A43: ft2 = g2 by A42,A40,FUNCT_2:63;
set sM1 = Prj2(j1,G);
A44: for x being Point of I[01] holds cP2.x = (CircleMap*sM1).x
proof
let x be Point of I[01];
thus (CircleMap*sM1).x = CircleMap.(sM1.x) by FUNCT_2:15
.= CircleMap.(G.(j1,x)) by Def3
.= (CircleMap*G).(j1,x) by Lm5,BINOP_1:18
.= y0 by A1,A35,BORSUK_6:def 11
.= cP2.x by TOPALG_3:21;
end;
sM1.0 = G.(j1,j0) by Def3
.= Ft.(j1,j0) by A36,A30,FUNCT_1:49
.= yt by A8,Lm4;
then
A45: ft2 = sM1 by A34,A42,A44,FUNCT_2:63;
sM0.0 = G.(j0,j0) by Def3
.= Ft.(j0,j0) by A36,A31,FUNCT_1:49
.= xt by A4,A8,Lm4;
then
A46: ft1 = sM0 by A34,A11,A38,FUNCT_2:63;
set Qt = Prj1(j1,G);
A47: Qt.0 = G.(j0,j1) by Def2
.= sM0.j1 by Def3
.= xt by A46,A12,TOPALG_3:4;
Qt.1 = G.(j1,j1) by Def2
.= sM1.j1 by Def3
.= yt by A45,A43,TOPALG_3:4;
then reconsider Qt as Path of xt,yt by A34,A47,BORSUK_2:def 4;
A48: now
let s be Point of I[01];
[s,0] in [:I,{0}:] by Lm4,ZFMISC_1:87;
hence G.(s,0) = Ft.(s,j0) by A36,FUNCT_1:49
.= ft.s by A8,Lm4;
thus G.(s,1) = Qt.s by Def2;
let t be Point of I[01];
thus G.(0,t) = sM0.t by Def3
.= xt by A46,A12,TOPALG_3:4;
thus G.(1,t) = sM1.t by Def3
.= yt by A45,A43,TOPALG_3:4;
end;
then ft,Qt are_homotopic by A34;
then reconsider G as Homotopy of ft,Qt by A34,A48,BORSUK_6:def 11;
take ft, Qt;
take G;
thus
A49: ft,Qt are_homotopic by A34,A48;
thus F = CircleMap*G by A35;
thus yt in (CircleMap)"{y0} by A41,FUNCT_2:38;
let F1 be Homotopy of ft,Qt such that
A50: F = CircleMap*F1;
A51: dom F1 = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1;
then
A52: dom (F1 | [:I,{0}:]) = [:I,{0}:] by A32,A33,RELAT_1:62;
for x being object st x in dom (F1 | [:I,{0}:])
holds (F1 | [:I,{0}:]).x = Ft.x
proof
let x be object;
assume
A53: x in dom (F1 | [:I,{0}:]);
then consider x1, x2 being object such that
A54: x1 in I and
A55: x2 in {0} and
A56: x = [x1,x2] by A52,ZFMISC_1:def 2;
A57: x2 = 0 by A55,TARSKI:def 1;
thus (F1 | [:I,{0}:]).x = F1.(x1,x2) by A53,A56,FUNCT_1:47
.= ft.x1 by A49,A54,A57,BORSUK_6:def 11
.= Ft.(x1,x2) by A8,A54,A55
.= Ft.x by A56;
end;
then F1 | [:I,{0}:] = Ft by A32,A33,A14,A51,RELAT_1:62;
hence thesis by A37,A50;
end;
definition
func Ciso -> Function of INT.Group, pi_1(Tunit_circle(2),c[10]) means
:Def5:
for n being Integer holds it.n = Class(EqRel(Tunit_circle(2),c[10]),cLoop(n));
existence
proof
defpred P[Integer,set] means $2 = Class(EqRel(TUC,c[10]),cLoop($1));
A1: for x being Element of INT ex y being Element of pi_1(TUC,c[10]) st P[ x,y]
proof
let x be Element of INT;
reconsider y = Class(EqRel(TUC,c[10]),cLoop(x)) as Element of pi_1(TUC,
c[10]) by TOPALG_1:47;
take y;
thus thesis;
end;
consider f being Function of INT,the carrier of pi_1(TUC,c[10]) such that
A2: for x being Element of INT holds P[x,f.x] from FUNCT_2:sch 3(A1);
reconsider f as Function of INT.Group, pi_1(TUC,c[10]);
take f;
let n be Integer;
n in INT by INT_1:def 2;
hence thesis by A2;
end;
uniqueness
proof
let f, g be Function of INT.Group, pi_1(TUC,c[10]) such that
A3: for n being Integer holds f.n = Class(EqRel(TUC,c[10]),cLoop(n)) and
A4: for n being Integer holds g.n = Class(EqRel(TUC,c[10]),cLoop(n));
for x being Element of INT.Group holds f.x = g.x
proof
let x be Element of INT.Group;
thus f.x = Class(EqRel(TUC,c[10]),cLoop(x)) by A3
.= g.x by A4;
end;
hence thesis;
end;
end;
theorem Th25:
for i being Integer, f being Path of R^1(0),R^1(i) holds Ciso.i
= Class(EqRel(Tunit_circle(2),c[10]),CircleMap*f)
proof
let i be Integer;
let f be Path of R^1(0),R^1(i);
set P = CircleMap*f;
A1: P.0 = CircleMap.(f.j0) by FUNCT_2:15
.= CircleMap.R^1(0) by BORSUK_2:def 4
.= CircleMap.0 by TOPREALB:def 2
.= |[ cos(2*PI*0), sin(2*PI*0) ]| by TOPREALB:def 11
.= c[10] by SIN_COS:31,TOPREALB:def 8;
P.1 = CircleMap.(f.j1) by FUNCT_2:15
.= CircleMap.R^1(i) by BORSUK_2:def 4
.= CircleMap.i by TOPREALB:def 2
.= |[ cos(2*PI*i+0), sin(2*PI*i+0) ]| by TOPREALB:def 11
.= |[ cos(0), sin(2*PI*i+0) ]| by COMPLEX2:9
.= c[10] by COMPLEX2:8,SIN_COS:31,TOPREALB:def 8;
then reconsider P as Loop of c[10] by A1,BORSUK_2:def 4;
A2: cLoop(i) = CircleMap * ExtendInt(i) by Th20;
A3: cLoop(i),P are_homotopic
proof
reconsider J = R^1 as non empty interval SubSpace of R^1;
reconsider r0 = R^1(0), ri = R^1(i) as Point of J;
reconsider O = ExtendInt(i), ff = f as Path of r0,ri;
reconsider G = R1Homotopy(O,ff) as Function of [:I[01],I[01]:],R^1;
take F = CircleMap*G;
thus F is continuous;
let s be Point of I[01];
thus F.(s,0) = CircleMap.(G.(s,j0)) by Lm5,BINOP_1:18
.= CircleMap.((1-j0) * (ExtendInt(i)).s + j0 * f.s) by TOPALG_2:def 4
.= (cLoop(i)).s by A2,FUNCT_2:15;
thus F.(s,1) = CircleMap.(G.(s,j1)) by Lm5,BINOP_1:18
.= CircleMap.((1-j1) * (ExtendInt(i)).s + j1 * f.s) by TOPALG_2:def 4
.= P.s by FUNCT_2:15;
thus F.(0,s) = CircleMap.(G.(j0,s)) by Lm5,BINOP_1:18
.= CircleMap.((1-s) * (ExtendInt(i)).j0 + s * f.j0) by TOPALG_2:def 4
.= CircleMap.((1-s) * R^1(0) + s * f.j0) by BORSUK_2:def 4
.= CircleMap.((1-s) * R^1(0) + s * R^1(0)) by BORSUK_2:def 4
.= CircleMap.((1-s) * 0 + s * 0) by TOPREALB:def 2
.= c[10] by TOPREALB:32;
thus F.(1,s) = CircleMap.(G.(j1,s)) by Lm5,BINOP_1:18
.= CircleMap.((1-s) * (ExtendInt(i)).j1 + s * f.j1) by TOPALG_2:def 4
.= CircleMap.((1-s) * R^1(i) + s * f.j1) by BORSUK_2:def 4
.= CircleMap.((1-s) * R^1(i) + s * R^1(i)) by BORSUK_2:def 4
.= CircleMap.i by TOPREALB:def 2
.= c[10] by TOPREALB:32;
end;
thus Ciso.i = Class(EqRel(TUC,c[10]),cLoop(i)) by Def5
.= Class(EqRel(TUC,c[10]),CircleMap*f) by A3,TOPALG_1:46;
end;
registration
cluster Ciso -> multiplicative;
coherence
proof
set f = Ciso;
let x, y be Element of INT.Group;
consider fX, fY being Loop of c[10] such that
A1: f.x = Class(EqRel(TUC,c[10]),fX) and
A2: f.y = Class(EqRel(TUC,c[10]),fY) and
A3: (the multF of pi_1(TUC,c[10])).(f.x,f.y) = Class(EqRel(TUC,c[10]
),fX+fY) by TOPALG_1:def 5;
f.y = Class(EqRel(TUC,c[10]),cLoop(y)) by Def5;
then
A4: fY,cLoop(y) are_homotopic by A2,TOPALG_1:46;
reconsider tx = AffineMap(1,x) as Function of R^1,R^1 by TOPMETR:17;
set p = tx*ExtendInt(y);
A5: p.0 = tx.((ExtendInt(y)).j0) by FUNCT_2:15
.= tx.(y*j0) by Def1
.= 1*0+x by FCONT_1:def 4
.= R^1(x) by TOPREALB:def 2;
A6: p.1 = tx.((ExtendInt(y)).j1) by FUNCT_2:15
.= tx.(y*j1) by Def1
.= 1*y+x by FCONT_1:def 4
.= R^1(x+y) by TOPREALB:def 2;
tx is being_homeomorphism by JORDAN16:20;
then tx is continuous;
then reconsider p as Path of R^1(x),R^1(x+y) by A5,A6,BORSUK_2:def 4;
A7: for a being Point of I[01] holds (CircleMap * (ExtendInt(x)+p)).a =
(cLoop(x)+cLoop(y)).a
proof
let a be Point of I[01];
per cases;
suppose
A8: a <= 1/2;
then
A9: 2*a is Point of I[01] by BORSUK_6:3;
thus (CircleMap * (ExtendInt(x)+p)).a = CircleMap.((ExtendInt(x)+p).
a) by FUNCT_2:15
.= CircleMap.((ExtendInt(x)).(2*a)) by A8,BORSUK_6:def 2
.= CircleMap.(x*(2*a)) by A9,Def1
.= |[ cos(2*PI*(x*(2*a))), sin(2*PI*(x*(2*a))) ]| by TOPREALB:def 11
.= |[ cos(2*PI*x*(2*a)), sin(2*PI*x*(2*a)) ]|
.= (cLoop(x)).(2*a) by A9,Def4
.= (cLoop(x)+cLoop(y)).a by A8,BORSUK_6:def 2;
end;
suppose
A10: 1/2 <= a;
then
A11: 2*a-1 is Point of I[01] by BORSUK_6:4;
thus (CircleMap * (ExtendInt(x)+p)).a = CircleMap.((ExtendInt(x)+p).
a) by FUNCT_2:15
.= CircleMap.(p.(2*a-1)) by A10,BORSUK_6:def 2
.= CircleMap.(tx.((ExtendInt(y)).(2*a-1))) by A11,FUNCT_2:15
.= CircleMap.(tx.(y*(2*a-1))) by A11,Def1
.= CircleMap.(1*(y*(2*a-1))+x) by FCONT_1:def 4
.= |[ cos(2*PI*((y*(2*a-1))+x)), sin(2*PI*((y*(2*a-1))+x)) ]| by
TOPREALB:def 11
.= |[ cos(2*PI*(y*(2*a-1))), sin(2*PI*(y*(2*a-1))+2*PI*x) ]| by
COMPLEX2:9
.= |[ cos(2*PI*y*(2*a-1)), sin(2*PI*y*(2*a-1)) ]| by COMPLEX2:8
.= (cLoop(y)).(2*a-1) by A11,Def4
.= (cLoop(x)+cLoop(y)).a by A10,BORSUK_6:def 2;
end;
end;
f.x = Class(EqRel(TUC,c[10]),cLoop(x)) by Def5;
then fX,cLoop(x) are_homotopic by A1,TOPALG_1:46;
then
A12: fX+fY,cLoop(x)+cLoop(y) are_homotopic by A4,BORSUK_6:76;
thus f.(x*y) = Class(EqRel(TUC,c[10]),CircleMap*(ExtendInt(x)+p)) by Th25
.= Class(EqRel(TUC,c[10]),cLoop(x)+cLoop(y)) by A7,FUNCT_2:63
.= f.x * f.y by A3,A12,TOPALG_1:46;
end;
end;
registration
cluster Ciso -> one-to-one onto;
coherence
proof
thus Ciso is one-to-one
proof
set xt = R^1(0);
let m, n be object;
assume that
A1: m in dom Ciso & n in dom Ciso and
A2: Ciso.m = Ciso.n;
reconsider m, n as Integer by A1;
Ciso.m = Class(EqRel(TUC,c[10]),cLoop(m)) & Ciso.n = Class(EqRel(TUC
,c[10]), cLoop(n)) by Def5;
then
A3: cLoop(m),cLoop(n) are_homotopic by A2,TOPALG_1:46;
then consider F being Function of [:I[01],I[01]:], TUC such that
A4: F is continuous and
A5: for s being Point of I[01] holds F.(s,0) = (cLoop(m)).s & F.(s,1
) = (cLoop(n)).s & for t being Point of I[01] holds F.(0,t) = c[10] & F.(1,t) =
c[10];
A6: xt in (CircleMap)"{c[10]} by Lm1,TOPREALB:33,def 2;
then consider ftm being Function of I[01], R^1 such that
ftm.0 = xt and
cLoop(m) = CircleMap*ftm and
ftm is continuous and
A7: for f1 being Function of I[01], R^1 st f1 is continuous & cLoop
(m) = CircleMap*f1 & f1.0 = xt holds ftm = f1 by Th23;
F is Homotopy of cLoop(m),cLoop(n) by A3,A4,A5,BORSUK_6:def 11;
then consider
yt being Point of R^1, Pt, Qt being Path of xt,yt, Ft being
Homotopy of Pt,Qt such that
A8: Pt,Qt are_homotopic and
A9: F = CircleMap*Ft and
yt in (CircleMap)"{c[10]} and
for F1 being Homotopy of Pt,Qt st F = CircleMap*F1 holds Ft = F1 by A3,A6
,Th24;
A10: cLoop(n) = CircleMap*ExtendInt(n) by Th20;
set ft0 = Prj1(j0,Ft);
A11: now
let x be Point of I[01];
thus (CircleMap*ft0).x = CircleMap.(ft0.x) by FUNCT_2:15
.= CircleMap.(Ft.(x,j0)) by Def2
.= F.(x,j0) by A9,Lm5,BINOP_1:18
.= (cLoop(m)).x by A5;
end;
ft0.0 = Ft.(j0,j0) by Def2
.= xt by A8,BORSUK_6:def 11;
then
A12: ft0 = ftm by A7,A11,FUNCT_2:63;
set ft1 = Prj1(j1,Ft);
A13: now
let x be Point of I[01];
thus (CircleMap*ft1).x = CircleMap.(ft1.x) by FUNCT_2:15
.= CircleMap.(Ft.(x,j1)) by Def2
.= F.(x,j1) by A9,Lm5,BINOP_1:18
.= (cLoop(n)).x by A5;
end;
consider ftn being Function of I[01], R^1 such that
ftn.0 = xt and
cLoop(n) = CircleMap*ftn and
ftn is continuous and
A14: for f1 being Function of I[01], R^1 st f1 is continuous & cLoop
(n) = CircleMap*f1 & f1.0 = xt holds ftn = f1 by A6,Th23;
A15: cLoop(m) = CircleMap*ExtendInt(m) by Th20;
ft1.0 = Ft.(j0,j1) by Def2
.= xt by A8,BORSUK_6:def 11;
then
A16: ft1 = ftn by A14,A13,FUNCT_2:63;
(ExtendInt(n)).0 = n*j0 by Def1
.= xt by TOPREALB:def 2;
then ExtendInt(n) = ftn by A14,A10;
then
A17: ft1.j1 = n*1 by A16,Def1;
(ExtendInt(m)).0 = m*j0 by Def1
.= xt by TOPREALB:def 2;
then ExtendInt(m) = ftm by A7,A15;
then
A18: ft0.j1 = m*1 by A12,Def1;
ft0.j1 = Ft.(j1,j0) by Def2
.= yt by A8,BORSUK_6:def 11
.= Ft.(j1,j1) by A8,BORSUK_6:def 11
.= ft1.j1 by Def2;
hence thesis by A18,A17;
end;
thus rng Ciso c= the carrier of pi_1(TUC,c[10]);
let q be object;
assume q in the carrier of pi_1(TUC,c[10]);
then consider f being Loop of c[10] such that
A19: q = Class(EqRel(TUC,c[10]),f) by TOPALG_1:47;
R^1(0) in (CircleMap)"{c[10]} by Lm1,TOPREALB:33,def 2;
then consider ft being Function of I[01], R^1 such that
A20: ft.0 = R^1(0) and
A21: f = CircleMap*ft and
A22: ft is continuous and
for f1 being Function of I[01], R^1 st f1 is continuous & f =
CircleMap*f1 & f1.0 = R^1(0) holds ft = f1 by Th23;
A23: ft.1 in REAL by XREAL_0:def 1;
CircleMap.(ft.j1) = (CircleMap*ft).j1 by FUNCT_2:15
.= c[10] by A21,BORSUK_2:def 4;
then CircleMap.(ft.1) in {c[10]} by TARSKI:def 1;
then
A24: ft.1 in INT by Lm12,FUNCT_1:def 7,TOPREALB:33,A23;
ft.1 = R^1(ft.1) by TOPREALB:def 2;
then ft is Path of R^1(0),R^1(ft.1) by A20,A22,BORSUK_2:def 4;
then dom Ciso = INT & Ciso.(ft.1) = Class(EqRel(TUC,c[10]),CircleMap*ft)
by A24,Th25,FUNCT_2:def 1;
hence thesis by A19,A21,A24,FUNCT_1:def 3;
end;
end;
theorem
Ciso is bijective;
Lm16: for r being positive Real, o being Point of TOP-REAL 2, x being
Point of Tcircle(o,r) holds INT.Group,pi_1(Tcircle(o,r),x) are_isomorphic
proof
let r be positive Real, o be Point of TOP-REAL 2, x be Point of
Tcircle(o,r);
TUC = Tcircle(0.TOP-REAL 2,1) by TOPREALB:def 7;
then pi_1(TUC,c[10]),pi_1(Tcircle(o,r),x) are_isomorphic by TOPALG_3:33
,TOPREALB:20;
then consider
h being Homomorphism of pi_1(TUC,c[10]), pi_1(Tcircle(o,r),x) such
that
A1: h is bijective;
take h*Ciso;
thus thesis by A1,GROUP_6:64;
end;
theorem Th27:
for S being being_simple_closed_curve SubSpace of TOP-REAL 2, x
being Point of S holds INT.Group, pi_1(S,x) are_isomorphic
proof
set r = the positive Real,o = the Point of TOP-REAL 2,y = the Point of
Tcircle(o,r);
let S be being_simple_closed_curve SubSpace of TOP-REAL 2, x be Point of S;
INT.Group,pi_1(Tcircle(o,r),y) are_isomorphic & pi_1(Tcircle(o,r),y),
pi_1(S,x) are_isomorphic by Lm16,TOPALG_3:33,TOPREALB:11;
hence thesis by GROUP_6:67;
end;
registration
let S be being_simple_closed_curve SubSpace of TOP-REAL 2, x be Point of S;
cluster pi_1(S,x) -> infinite;
coherence
proof
INT.Group, pi_1(S,x) are_isomorphic by Th27;
hence thesis by GROUP_6:74;
end;
end;