:: TOPALG_5 semantic presentation
begin
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 the carrier of I[01]
by BORSUK_1:43;
then Lm3: {0} c= the carrier of I[01]
by ZFMISC_1:31;
Lm4: 0 in {0}
by TARSKI:def_1;
Lm5: the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def_2;
reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15;
Lm6: [#] I[01] = the carrier of I[01]
;
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
not INT.Group is finite ;
end;
theorem Th1: :: TOPALG_5:1
for r, s, a being real number st r <= s holds
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
let r, s, a be real number ; ::_thesis: ( 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).[ ) )
set M = Closed-Interval-MSpace (r,s);
assume r <= s ; ::_thesis: 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).[ )
then A1: the carrier of (Closed-Interval-MSpace (r,s)) = [.r,s.] by TOPMETR:10;
let p be Point of (Closed-Interval-MSpace (r,s)); ::_thesis: ( 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).[ )
set B = Ball (p,a);
reconsider p1 = p as Point of RealSpace by TOPMETR:8;
set B1 = Ball (p1,a);
A2: Ball (p,a) = (Ball (p1,a)) /\ the carrier of (Closed-Interval-MSpace (r,s)) by TOPMETR:9;
( a is Real & p1 is Real ) by XREAL_0:def_1;
then A3: Ball (p1,a) = ].(p1 - a),(p1 + a).[ by FRECHET:7;
percases ( ( p1 + a <= s & p1 - a < r ) or ( p1 + a <= s & p1 - a >= r ) or ( p1 + a > s & p1 - a < r ) or ( p1 + a > s & p1 - a >= r ) ) ;
supposethat A4: p1 + a <= s and
A5: p1 - a < r ; ::_thesis: ( 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).[ )
Ball (p,a) = [.r,(p1 + a).[
proof
thus Ball (p,a) c= [.r,(p1 + a).[ :: according to XBOOLE_0:def_10 ::_thesis: [.r,(p1 + a).[ c= Ball (p,a)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,a) or b in [.r,(p1 + a).[ )
assume A6: b in Ball (p,a) ; ::_thesis: b in [.r,(p1 + a).[
then reconsider b = b as Element of Ball (p,a) ;
b in Ball (p1,a) 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 b in [.r,(p1 + a).[ by A7, XXREAL_1:3; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in [.r,(p1 + a).[ or b in Ball (p,a) )
assume A8: b in [.r,(p1 + a).[ ; ::_thesis: b in Ball (p,a)
then reconsider b = 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 Ball (p1,a) by A3, A10, XXREAL_1:4;
hence b in Ball (p,a) by A1, A2, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( 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).[ ) ; ::_thesis: verum
end;
supposethat A12: p1 + a <= s and
A13: p1 - a >= r ; ::_thesis: ( 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).[ )
Ball (p,a) = ].(p1 - a),(p1 + a).[
proof
thus Ball (p,a) c= ].(p1 - a),(p1 + a).[ by A2, A3, XBOOLE_1:17; :: according to XBOOLE_0:def_10 ::_thesis: ].(p1 - a),(p1 + a).[ c= Ball (p,a)
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in ].(p1 - a),(p1 + a).[ or b in Ball (p,a) )
assume A14: b in ].(p1 - a),(p1 + a).[ ; ::_thesis: b in Ball (p,a)
then reconsider b = 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 b in Ball (p,a) by A1, A2, A3, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( 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).[ ) ; ::_thesis: verum
end;
supposethat A16: p1 + a > s and
A17: p1 - a < r ; ::_thesis: ( 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).[ )
Ball (p,a) = [.r,s.]
proof
thus Ball (p,a) c= [.r,s.] by A1; :: according to XBOOLE_0:def_10 ::_thesis: [.r,s.] c= Ball (p,a)
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in [.r,s.] or b in Ball (p,a) )
assume A18: b in [.r,s.] ; ::_thesis: b in Ball (p,a)
then reconsider b = 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 Ball (p1,a) by A3, A19, XXREAL_1:4;
hence b in Ball (p,a) by A1, A2, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( 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).[ ) ; ::_thesis: verum
end;
supposethat A20: p1 + a > s and
A21: p1 - a >= r ; ::_thesis: ( 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).[ )
Ball (p,a) = ].(p1 - a),s.]
proof
thus Ball (p,a) c= ].(p1 - a),s.] :: according to XBOOLE_0:def_10 ::_thesis: ].(p1 - a),s.] c= Ball (p,a)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,a) or b in ].(p1 - a),s.] )
assume A22: b in Ball (p,a) ; ::_thesis: b in ].(p1 - a),s.]
then reconsider b = b as Element of Ball (p,a) ;
b in Ball (p1,a) 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 b in ].(p1 - a),s.] by A23, XXREAL_1:2; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in ].(p1 - a),s.] or b in Ball (p,a) )
assume A24: b in ].(p1 - a),s.] ; ::_thesis: b in Ball (p,a)
then reconsider b = 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 Ball (p1,a) by A3, A26, XXREAL_1:4;
hence b in Ball (p,a) by A1, A2, A27, XBOOLE_0:def_4; ::_thesis: verum
end;
hence ( 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).[ ) ; ::_thesis: verum
end;
end;
end;
theorem Th2: :: TOPALG_5:2
for r, s being real number st r <= s holds
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 Element of 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
let r, s be real number ; ::_thesis: ( 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 Element of NAT : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) ) )
set L = Closed-Interval-TSpace (r,s);
set M = Closed-Interval-MSpace (r,s);
assume A1: r <= s ; ::_thesis: 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 Element of NAT : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) )
defpred S1[ set , set ] means ex x being Point of (Closed-Interval-TSpace (r,s)) ex y being Point of (Closed-Interval-MSpace (r,s)) ex B being Basis of st
( $1 = x & x = y & $2 = B & B = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } );
A2: Closed-Interval-TSpace (r,s) = TopSpaceMetr (Closed-Interval-MSpace (r,s)) by TOPMETR:def_7;
A3: for i being set st i in the carrier of (Closed-Interval-TSpace (r,s)) holds
ex j being set st S1[i,j]
proof
let i be set ; ::_thesis: ( i in the carrier of (Closed-Interval-TSpace (r,s)) implies ex j being set st S1[i,j] )
assume i in the carrier of (Closed-Interval-TSpace (r,s)) ; ::_thesis: ex j being set st S1[i,j]
then reconsider i = i as Point of (Closed-Interval-TSpace (r,s)) ;
reconsider m = i as Point of (Closed-Interval-MSpace (r,s)) by A2, TOPMETR:12;
reconsider j = i as Element of (TopSpaceMetr (Closed-Interval-MSpace (r,s))) by A2;
set B = Balls j;
A4: ex y being Point of (Closed-Interval-MSpace (r,s)) st
( y = j & Balls j = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) by FRECHET:def_1;
reconsider B1 = Balls j as Basis of by A2;
take Balls j ; ::_thesis: S1[i, Balls j]
take i ; ::_thesis: ex y being Point of (Closed-Interval-MSpace (r,s)) ex B being Basis of st
( i = i & i = y & Balls j = B & B = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } )
take m ; ::_thesis: ex B being Basis of st
( i = i & i = m & Balls j = B & B = { (Ball (m,(1 / n))) where n is Element of NAT : n <> 0 } )
take B1 ; ::_thesis: ( i = i & i = m & Balls j = B1 & B1 = { (Ball (m,(1 / n))) where n is Element of NAT : n <> 0 } )
thus ( i = i & i = m & Balls j = B1 & B1 = { (Ball (m,(1 / n))) where n is Element of NAT : n <> 0 } ) by A4; ::_thesis: verum
end;
consider f being ManySortedSet of the carrier of (Closed-Interval-TSpace (r,s)) such that
A5: for i being set st i in the carrier of (Closed-Interval-TSpace (r,s)) holds
S1[i,f . i] from PBOOLE:sch_3(A3);
for x being Element of (Closed-Interval-TSpace (r,s)) holds f . x is Basis of
proof
let x be Element of (Closed-Interval-TSpace (r,s)); ::_thesis: f . x is Basis of
S1[x,f . x] by A5;
hence f . x is Basis of ; ::_thesis: verum
end;
then reconsider B = Union f as Basis of (Closed-Interval-TSpace (r,s)) by TOPGEN_2:2;
take B ; ::_thesis: ( 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 Element of NAT : n <> 0 } & B = Union f ) & ( for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected ) )
hereby ::_thesis: for X being Subset of (Closed-Interval-TSpace (r,s)) st X in B holds
X is connected
take f = f; ::_thesis: for x being Point of (Closed-Interval-MSpace (r,s)) holds
( f . x = { (Ball (x,(1 / n))) where n is Element of NAT : n <> 0 } & B = Union f )
let x be Point of (Closed-Interval-MSpace (r,s)); ::_thesis: ( f . x = { (Ball (x,(1 / n))) where n is Element of NAT : n <> 0 } & B = Union f )
the carrier of (Closed-Interval-MSpace (r,s)) = [.r,s.] by A1, TOPMETR:10
.= the carrier of (Closed-Interval-TSpace (r,s)) by A1, TOPMETR:18 ;
then S1[x,f . x] by A5;
hence ( f . x = { (Ball (x,(1 / n))) where n is Element of NAT : n <> 0 } & B = Union f ) ; ::_thesis: verum
end;
let X be Subset of (Closed-Interval-TSpace (r,s)); ::_thesis: ( X in B implies X is connected )
assume X in B ; ::_thesis: X is connected
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 set such that
A8: x in dom f and
A9: f . x = Z by A7, FUNCT_1:def_3;
consider x1 being Point of (Closed-Interval-TSpace (r,s)), y being Point of (Closed-Interval-MSpace (r,s)), B1 being Basis of such that
x = x1 and
x1 = y and
A10: ( f . x = B1 & B1 = { (Ball (y,(1 / n))) where n is Element of NAT : n <> 0 } ) by A5, A8;
consider n being Element of 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 X is connected by CONNSP_1:23; ::_thesis: verum
end;
theorem Th3: :: TOPALG_5:3
for T being TopStruct
for A being Subset of T
for t being Point of T st t in A holds
Component_of (t,A) c= A
proof
let T be TopStruct ; ::_thesis: for A being Subset of T
for t being Point of T st t in A holds
Component_of (t,A) c= A
let A be Subset of T; ::_thesis: for t being Point of T st t in A holds
Component_of (t,A) c= A
let t be Point of T; ::_thesis: ( t in A implies Component_of (t,A) c= A )
assume A1: t in A ; ::_thesis: Component_of (t,A) c= 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 Component_of (t,A) c= A by A2; ::_thesis: verum
end;
registration
let T be TopSpace;
let A be open Subset of T;
clusterT | A -> open ;
coherence
T | A is open
proof
let X be Subset of T; :: according to TSEP_1:def_1 ::_thesis: ( not X = the carrier of (T | A) or X is open )
thus ( not X = the carrier of (T | A) or X is open ) by PRE_TOPC:8; ::_thesis: verum
end;
end;
theorem Th4: :: TOPALG_5:4
for T being TopSpace
for S being SubSpace of T
for A being Subset of T
for B being Subset of S st A = B holds
T | A = S | B
proof
let T be TopSpace; ::_thesis: for S being SubSpace of T
for A being Subset of T
for B being Subset of S st A = B holds
T | A = S | B
let S be SubSpace of T; ::_thesis: for A being Subset of T
for B being Subset of S st A = B holds
T | A = S | B
let A be Subset of T; ::_thesis: for B being Subset of S st A = B holds
T | A = S | B
let B be Subset of S; ::_thesis: ( A = B implies T | A = S | B )
assume A = B ; ::_thesis: T | A = S | B
then ( S | B is SubSpace of T & [#] (S | B) = A ) by PRE_TOPC:def_5, TSEP_1:7;
hence T | A = S | B by PRE_TOPC:def_5; ::_thesis: verum
end;
theorem Th5: :: TOPALG_5:5
for S, T being TopSpace
for A, B being Subset of T
for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds
C,D are_separated
proof
let S, T be TopSpace; ::_thesis: for A, B being Subset of T
for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds
C,D are_separated
let A, B be Subset of T; ::_thesis: for C, D being Subset of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated holds
C,D are_separated
let C, D be Subset of S; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = C & B = D & A,B are_separated implies C,D are_separated )
assume A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ( not A = C or not B = D or not A,B are_separated or C,D are_separated )
assume A2: ( A = C & B = D ) ; ::_thesis: ( not A,B are_separated or C,D are_separated )
assume A,B are_separated ; ::_thesis: C,D are_separated
then A3: ( Cl A misses B & A misses Cl B ) by CONNSP_1:def_1;
( Cl A = Cl C & Cl B = Cl D ) by A1, A2, TOPS_3:80;
hence C,D are_separated by A2, A3, CONNSP_1:def_1; ::_thesis: verum
end;
theorem :: TOPALG_5:6
for S, T being TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is connected holds
T is connected
proof
let S, T be TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is connected implies T is connected )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: S is connected ; ::_thesis: T is connected
let A, B be Subset of T; :: according to CONNSP_1:def_2 ::_thesis: ( not [#] T = A \/ B or not A,B are_separated or A = {} T or B = {} T )
assume that
A3: [#] T = A \/ B and
A4: A,B are_separated ; ::_thesis: ( A = {} T or B = {} T )
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, CONNSP_1:def_2;
hence ( A = {} T or B = {} T ) ; ::_thesis: verum
end;
theorem Th7: :: TOPALG_5:7
for S, T being TopSpace
for A being Subset of S
for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds
B is connected
proof
let S, T be TopSpace; ::_thesis: for A being Subset of S
for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds
B is connected
let A be Subset of S; ::_thesis: for B being Subset of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected holds
B is connected
let B be Subset of T; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B & A is connected implies B is connected )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: ( A = B & A is connected ) ; ::_thesis: B is connected
now__::_thesis:_for_P,_Q_being_Subset_of_T_st_B_=_P_\/_Q_&_P,Q_are_separated_&_not_P_=_{}_T_holds_
Q_=_{}_T
let P, Q be Subset of T; ::_thesis: ( B = P \/ Q & P,Q are_separated & not P = {} T implies Q = {} T )
assume that
A3: B = P \/ Q and
A4: P,Q are_separated ; ::_thesis: ( P = {} T or Q = {} T )
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 ) ; ::_thesis: verum
end;
hence B is connected by CONNSP_1:15; ::_thesis: verum
end;
theorem Th8: :: TOPALG_5:8
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t
proof
let S, T be non empty TopSpace; ::_thesis: for s being Point of S
for t being Point of T
for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t
let s be Point of S; ::_thesis: for t being Point of T
for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t
let t be Point of T; ::_thesis: for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t
let A be a_neighborhood of s; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t implies A is a_neighborhood of t )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: s = t ; ::_thesis: A is a_neighborhood of 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 A is a_neighborhood of t by A2, A3, CONNSP_2:def_1; ::_thesis: verum
end;
theorem :: TOPALG_5:9
for S, T being non empty TopSpace
for A being Subset of S
for B being Subset of T
for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds
N is a_neighborhood of B
proof
let S, T be non empty TopSpace; ::_thesis: for A being Subset of S
for B being Subset of T
for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds
N is a_neighborhood of B
let A be Subset of S; ::_thesis: for B being Subset of T
for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds
N is a_neighborhood of B
let B be Subset of T; ::_thesis: for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds
N is a_neighborhood of B
let N be a_neighborhood of A; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B implies N is a_neighborhood of B )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: A = B ; ::_thesis: N is a_neighborhood of 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 N is a_neighborhood of B by A2, A3, CONNSP_2:def_2; ::_thesis: verum
end;
theorem Th10: :: TOPALG_5:10
for S, T being non empty TopSpace
for A, B being Subset of T
for 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; ::_thesis: for A, B being Subset of T
for 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
let A, B be Subset of T; ::_thesis: for 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
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism & A is_a_component_of B implies f " A is_a_component_of f " B )
assume A1: f is being_homeomorphism ; ::_thesis: ( not A is_a_component_of B or f " A is_a_component_of f " B )
A2: rng f = [#] T by A1, TOPS_2:def_5
.= 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 ; :: according to CONNSP_1:def_6 ::_thesis: f " A is_a_component_of f " B
A5: the carrier of (T | B) = B by PRE_TOPC:8;
then f " X c= f " B by RELAT_1:143;
then reconsider Y = f " A as Subset of (S | (f " B)) by A3, PRE_TOPC:8;
take Y ; :: according to CONNSP_1:def_6 ::_thesis: ( Y = f " A & Y is a_component )
thus Y = f " A ; ::_thesis: Y is a_component
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; :: according to CONNSP_1:def_5 ::_thesis: for b1 being Element of bool the carrier of (S | (f " B)) holds
( not b1 is connected or not Y c= b1 or Y = b1 )
let Z be Subset of (S | (f " B)); ::_thesis: ( not Z is connected or not Y c= Z or Y = Z )
assume that
A6: Z is connected and
A7: Y c= Z ; ::_thesis: Y = Z
A8: f .: Y c= f .: Z by A7, RELAT_1:123;
A9: f is one-to-one by A1, TOPS_2:def_5;
A10: f is continuous by A1, TOPS_2:def_5;
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, CONNSP_1:def_5;
hence Y = Z by A3, A9, A11, FUNCT_1:94; ::_thesis: verum
end;
begin
theorem Th11: :: TOPALG_5:11
for T being non empty TopSpace
for S being non empty SubSpace of T
for A being non empty Subset of T
for B being non empty Subset of S st A = B & A is locally_connected holds
B is locally_connected
proof
let T be non empty TopSpace; ::_thesis: for S being non empty SubSpace of T
for A being non empty Subset of T
for B being non empty Subset of S st A = B & A is locally_connected holds
B is locally_connected
let S be non empty SubSpace of T; ::_thesis: for A being non empty Subset of T
for B being non empty Subset of S st A = B & A is locally_connected holds
B is locally_connected
let A be non empty Subset of T; ::_thesis: for B being non empty Subset of S st A = B & A is locally_connected holds
B is locally_connected
let B be non empty Subset of S; ::_thesis: ( A = B & A is locally_connected implies B is locally_connected )
assume that
A1: A = B and
A2: A is locally_connected ; ::_thesis: B is locally_connected
T | A = S | B by A1, Th4;
hence S | B is locally_connected by A2, CONNSP_2:def_6; :: according to CONNSP_2:def_6 ::_thesis: verum
end;
theorem Th12: :: TOPALG_5:12
for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally_connected holds
T is locally_connected
proof
let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally_connected implies T is locally_connected )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: S is locally_connected ; ::_thesis: T is locally_connected
let t be Point of T; :: according to CONNSP_2:def_4 ::_thesis: T is_locally_connected_in t
reconsider s = t as Point of S by A1;
let U be Subset of T; :: according to CONNSP_2:def_3 ::_thesis: ( not U is a_neighborhood of t or ex b1 being Element of bool the carrier of T st
( b1 is a_neighborhood of t & b1 is connected & b1 c= U ) )
reconsider U1 = U as Subset of S by A1;
assume U is a_neighborhood of t ; ::_thesis: ex b1 being Element of bool the carrier of T st
( b1 is a_neighborhood of t & b1 is connected & b1 c= U )
then A3: U1 is a_neighborhood of s by A1, Th8;
S is_locally_connected_in s by A2, CONNSP_2:def_4;
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, CONNSP_2:def_3;
reconsider V = V1 as Subset of T by A1;
take V ; ::_thesis: ( V is a_neighborhood of t & V is connected & V c= U )
thus V is a_neighborhood of t by A1, A4, Th8; ::_thesis: ( V is connected & V c= U )
thus V is connected by A1, A5, Th7; ::_thesis: V c= U
thus V c= U by A6; ::_thesis: verum
end;
theorem Th13: :: TOPALG_5:13
for T being non empty TopSpace holds
( T is locally_connected iff [#] T is locally_connected )
proof
let T be non empty TopSpace; ::_thesis: ( T is locally_connected iff [#] T is locally_connected )
T is SubSpace of T by TSEP_1:2;
then A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (T | ([#] T)), the topology of (T | ([#] T)) #) by PRE_TOPC:8, TSEP_1:5;
hereby ::_thesis: ( [#] T is locally_connected implies T is locally_connected )
assume T is locally_connected ; ::_thesis: [#] T is locally_connected
then T | ([#] T) is locally_connected by A1, Th12;
hence [#] T is locally_connected by CONNSP_2:def_6; ::_thesis: verum
end;
assume [#] T is locally_connected ; ::_thesis: T is locally_connected
then T | ([#] T) is locally_connected by CONNSP_2:def_6;
hence T is locally_connected by A1, Th12; ::_thesis: verum
end;
Lm10: for T being non empty TopSpace
for S being non empty open SubSpace of T st T is locally_connected holds
TopStruct(# the carrier of S, the topology of S #) is locally_connected
proof
let T be non empty TopSpace; ::_thesis: for S being non empty open SubSpace of T st T is locally_connected holds
TopStruct(# the carrier of S, the topology of S #) is locally_connected
let S be non empty open SubSpace of T; ::_thesis: ( T is locally_connected implies TopStruct(# the carrier of S, the topology of S #) is locally_connected )
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 ; ::_thesis: TopStruct(# the carrier of S, the topology of S #) is locally_connected
then [#] S is locally_connected by A1, Th11, CONNSP_2:17;
then S is locally_connected by Th13;
then TopStruct(# the carrier of S, the topology of S #) is locally_connected by Th12;
then [#] TopStruct(# the carrier of S, the topology of S #) is locally_connected by Th13;
then TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #)) is locally_connected by CONNSP_2:def_6;
hence TopStruct(# the carrier of S, the topology of S #) is locally_connected by TSEP_1:3; ::_thesis: verum
end;
theorem Th14: :: TOPALG_5:14
for T being non empty TopSpace
for 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; ::_thesis: for S being non empty open SubSpace of T st T is locally_connected holds
S is locally_connected
let S be non empty open SubSpace of T; ::_thesis: ( T is locally_connected implies S is locally_connected )
assume T is locally_connected ; ::_thesis: S is locally_connected
then TopStruct(# the carrier of S, the topology of S #) is locally_connected by Lm10;
hence S is locally_connected by Th12; ::_thesis: verum
end;
theorem :: TOPALG_5:15
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; ::_thesis: ( S,T are_homeomorphic & S is locally_connected implies T is locally_connected )
given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: ( not S is locally_connected or T is locally_connected )
assume A2: S is locally_connected ; ::_thesis: T is locally_connected
now__::_thesis:_for_A_being_non_empty_Subset_of_T
for_B_being_Subset_of_T_st_A_is_open_&_B_is_a_component_of_A_holds_
B_is_open
let A be non empty Subset of T; ::_thesis: for B being Subset of T st A is open & B is_a_component_of A holds
B is open
let B be Subset of T; ::_thesis: ( A is open & B is_a_component_of A implies B is open )
assume ( A is open & B is_a_component_of A ) ; ::_thesis: B is open
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, TOPS_2:def_5;
then not f " A is 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; ::_thesis: verum
end;
hence T is locally_connected by CONNSP_2:18; ::_thesis: verum
end;
theorem Th16: :: TOPALG_5:16
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; ::_thesis: ( ex B being Basis of T st
for X being Subset of T st X in B holds
X is connected implies T is locally_connected )
given B being Basis of T such that A1: for X being Subset of T st X in B holds
X is connected ; ::_thesis: T is locally_connected
let x be Point of T; :: according to CONNSP_2:def_4 ::_thesis: T is_locally_connected_in x
let U be Subset of T; :: according to CONNSP_2:def_3 ::_thesis: ( not U is a_neighborhood of x or ex b1 being Element of bool the carrier of T st
( b1 is a_neighborhood of x & b1 is connected & b1 c= U ) )
assume A2: x in Int U ; :: according to CONNSP_2:def_1 ::_thesis: ex b1 being Element of bool the carrier of T st
( b1 is a_neighborhood of x & b1 is connected & b1 c= 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 = V as Subset of T by A6;
take V ; ::_thesis: ( V is a_neighborhood of x & V is connected & V c= U )
( 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; :: according to CONNSP_2:def_1 ::_thesis: ( V is connected & V c= U )
thus V is connected by A1, A3, A6; ::_thesis: V c= U
A7: Int U c= U by TOPS_1:16;
V c= union Y by A6, ZFMISC_1:74;
hence V c= U by A4, A7, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th17: :: TOPALG_5:17
for r, s being real number st r <= s holds
Closed-Interval-TSpace (r,s) is locally_connected
proof
let r, s be real number ; ::_thesis: ( r <= s implies Closed-Interval-TSpace (r,s) is locally_connected )
assume r <= s ; ::_thesis: Closed-Interval-TSpace (r,s) is locally_connected
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 Element of 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 Closed-Interval-TSpace (r,s) is locally_connected by Th16; ::_thesis: verum
end;
registration
cluster I[01] -> locally_connected ;
coherence
I[01] is locally_connected by Th17, TOPMETR:20;
end;
registration
let A be non empty open Subset of I[01];
clusterI[01] | A -> locally_connected ;
coherence
I[01] | A is locally_connected by Th14;
end;
begin
definition
let r be real number ;
func ExtendInt r -> Function of I[01],R^1 means :Def1: :: TOPALG_5:def 1
for x being Point of I[01] holds it . x = r * x;
existence
ex b1 being Function of I[01],R^1 st
for x being Point of I[01] holds b1 . x = r * x
proof
defpred S1[ real number , set ] means $2 = r * $1;
A1: for x being Element of I[01] ex y being Element of the carrier of R^1 st S1[x,y]
proof
let x be Element of I[01]; ::_thesis: ex y being Element of the carrier of R^1 st S1[x,y]
take r * x ; ::_thesis: ( r * x is Element of the carrier of R^1 & S1[x,r * x] )
thus ( r * x is Element of the carrier of R^1 & S1[x,r * x] ) by TOPMETR:17, XREAL_0:def_1; ::_thesis: verum
end;
ex f being Function of the carrier of I[01], the carrier of R^1 st
for x being Element of I[01] holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence ex b1 being Function of I[01],R^1 st
for x being Point of I[01] holds b1 . x = r * x ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of I[01],R^1 st ( for x being Point of I[01] holds b1 . x = r * x ) & ( for x being Point of I[01] holds b2 . x = r * x ) holds
b1 = b2
proof
let f, g be Function of I[01],R^1; ::_thesis: ( ( for x being Point of I[01] holds f . x = r * x ) & ( for x being Point of I[01] holds g . x = r * x ) implies f = g )
assume 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 ; ::_thesis: f = g
for x being Point of I[01] holds f . x = g . x
proof
let x be Point of I[01]; ::_thesis: f . x = g . x
thus f . x = r * x by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines ExtendInt TOPALG_5:def_1_:_
for r being real number
for b2 being Function of I[01],R^1 holds
( b2 = ExtendInt r iff for x being Point of I[01] holds b2 . x = r * x );
registration
let r be real number ;
cluster ExtendInt r -> continuous ;
coherence
ExtendInt r is continuous
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]
for r1 being real number 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]; ::_thesis: g . x = (ExtendInt r) . x
thus g . x = r * (f1 . x) by A1
.= r * x by FUNCT_1:18
.= (ExtendInt r) . x by Def1 ; ::_thesis: verum
end;
hence ExtendInt r is continuous by A2, FUNCT_2:63; ::_thesis: verum
end;
end;
definition
let r be real number ;
:: original: ExtendInt
redefine func ExtendInt r -> Path of R^1 0, R^1 r;
coherence
ExtendInt r is Path of R^1 0, R^1 r
proof
thus ExtendInt r is continuous ; :: according to BORSUK_2:def_4 ::_thesis: ( (ExtendInt r) . 0 = R^1 0 & (ExtendInt r) . 1 = R^1 r )
thus (ExtendInt r) . 0 = r * 0 by Def1, BORSUK_1:def_14
.= R^1 0 by TOPREALB:def_2 ; ::_thesis: (ExtendInt r) . 1 = R^1 r
thus (ExtendInt r) . 1 = r * 1 by Def1, BORSUK_1:def_15
.= R^1 r by TOPREALB:def_2 ; ::_thesis: verum
end;
end;
definition
let S, T, Y be non empty TopSpace;
let H be Function of [:S,T:],Y;
let t be Point of T;
func Prj1 (t,H) -> Function of S,Y means :Def2: :: TOPALG_5:def 2
for s being Point of S holds it . s = H . (s,t);
existence
ex b1 being Function of S,Y st
for s being Point of S holds b1 . s = H . (s,t)
proof
deffunc H1( Point of S) -> Element of the carrier of Y = 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 = H1(x) from FUNCT_2:sch_4();
take f ; ::_thesis: for s being Point of S holds f . s = H . (s,t)
let x be Point of S; ::_thesis: f . x = H . (x,t)
thus f . x = H . (x,t) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of S,Y st ( for s being Point of S holds b1 . s = H . (s,t) ) & ( for s being Point of S holds b2 . s = H . (s,t) ) holds
b1 = b2
proof
let f, g be Function of S,Y; ::_thesis: ( ( for s being Point of S holds f . s = H . (s,t) ) & ( for s being Point of S holds g . s = H . (s,t) ) implies f = g )
assume 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) ; ::_thesis: f = g
now__::_thesis:_for_s_being_Point_of_S_holds_f_._s_=_g_._s
let s be Point of S; ::_thesis: f . s = g . s
thus f . s = H . (s,t) by A2
.= g . s by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Prj1 TOPALG_5:def_2_:_
for S, T, Y being non empty TopSpace
for H being Function of [:S,T:],Y
for t being Point of T
for b6 being Function of S,Y holds
( b6 = Prj1 (t,H) iff for s being Point of S holds b6 . s = H . (s,t) );
definition
let S, T, Y be non empty TopSpace;
let H be Function of [:S,T:],Y;
let s be Point of S;
func Prj2 (s,H) -> Function of T,Y means :Def3: :: TOPALG_5:def 3
for t being Point of T holds it . t = H . (s,t);
existence
ex b1 being Function of T,Y st
for t being Point of T holds b1 . t = H . (s,t)
proof
deffunc H1( Point of T) -> Element of the carrier of Y = 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 = H1(x) from FUNCT_2:sch_4();
take f ; ::_thesis: for t being Point of T holds f . t = H . (s,t)
let x be Point of T; ::_thesis: f . x = H . (s,x)
thus f . x = H . (s,x) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of T,Y st ( for t being Point of T holds b1 . t = H . (s,t) ) & ( for t being Point of T holds b2 . t = H . (s,t) ) holds
b1 = b2
proof
let f, g be Function of T,Y; ::_thesis: ( ( for t being Point of T holds f . t = H . (s,t) ) & ( for t being Point of T holds g . t = H . (s,t) ) implies f = g )
assume 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) ; ::_thesis: f = g
now__::_thesis:_for_t_being_Point_of_T_holds_f_._t_=_g_._t
let t be Point of T; ::_thesis: f . t = g . t
thus f . t = H . (s,t) by A2
.= g . t by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Prj2 TOPALG_5:def_3_:_
for S, T, Y being non empty TopSpace
for H being Function of [:S,T:],Y
for s being Point of S
for b6 being Function of T,Y holds
( b6 = Prj2 (s,H) iff for t being Point of T holds b6 . t = H . (s,t) );
registration
let S, T, Y be non empty TopSpace;
let H be continuous Function of [:S,T:],Y;
let t be Point of T;
cluster Prj1 (t,H) -> continuous ;
coherence
Prj1 (t,H) is continuous
proof
for p being Point of S
for 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; ::_thesis: for 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 )
let V be Subset of Y; ::_thesis: ( (Prj1 (t,H)) . p in V & V is open implies ex W being Subset of S st
( p in W & W is open & (Prj1 (t,H)) .: W c= V ) )
assume A1: ( (Prj1 (t,H)) . p in V & V is open ) ; ::_thesis: ex W being Subset of S st
( p in W & W is open & (Prj1 (t,H)) .: W c= V )
(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 holds
ex X1 being Subset of S ex 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 ; ::_thesis: ( p in X1 & X1 is open & (Prj1 (t,H)) .: X1 c= V )
thus p in X1 by A7, A9, ZFMISC_1:87; ::_thesis: ( X1 is open & (Prj1 (t,H)) .: X1 c= V )
thus X1 is open by A10; ::_thesis: (Prj1 (t,H)) .: X1 c= V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Prj1 (t,H)) .: X1 or x in V )
assume x in (Prj1 (t,H)) .: X1 ; ::_thesis: x in V
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 x in V by A4, A12, A13; ::_thesis: verum
end;
hence Prj1 (t,H) is continuous by JGRAPH_2:10; ::_thesis: verum
end;
end;
registration
let S, T, Y be non empty TopSpace;
let H be continuous Function of [:S,T:],Y;
let s be Point of S;
cluster Prj2 (s,H) -> continuous ;
coherence
Prj2 (s,H) is continuous
proof
for p being Point of T
for 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; ::_thesis: for 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 )
let V be Subset of Y; ::_thesis: ( (Prj2 (s,H)) . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & (Prj2 (s,H)) .: W c= V ) )
assume A1: ( (Prj2 (s,H)) . p in V & V is open ) ; ::_thesis: ex W being Subset of T st
( p in W & W is open & (Prj2 (s,H)) .: W c= V )
(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 holds
ex X1 being Subset of S ex 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 ; ::_thesis: ( p in Y1 & Y1 is open & (Prj2 (s,H)) .: Y1 c= V )
thus p in Y1 by A7, A9, ZFMISC_1:87; ::_thesis: ( Y1 is open & (Prj2 (s,H)) .: Y1 c= V )
thus Y1 is open by A10; ::_thesis: (Prj2 (s,H)) .: Y1 c= V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Prj2 (s,H)) .: Y1 or x in V )
assume x in (Prj2 (s,H)) .: Y1 ; ::_thesis: x in V
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 x in V by A4, A12, A13; ::_thesis: verum
end;
hence Prj2 (s,H) is continuous by JGRAPH_2:10; ::_thesis: verum
end;
end;
theorem :: TOPALG_5:18
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b
for H being Homotopy of P,Q
for t being Point of I[01] st H is continuous holds
Prj1 (t,H) is continuous ;
theorem :: TOPALG_5:19
for T being non empty TopSpace
for a, b being Point of T
for P, Q being Path of a,b
for H being Homotopy of P,Q
for 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 (Tunit_circle 2);
Lm11: now__::_thesis:_the_carrier_of_(Tunit_circle_2)_=_Sphere_(|[0,0]|,1)
Tunit_circle 2 = Tcircle ((0. (TOP-REAL 2)),1) by TOPREALB:def_7;
hence the carrier of (Tunit_circle 2) = Sphere (|[0,0]|,1) by EUCLID:54, TOPREALB:9; ::_thesis: verum
end;
Lm12: dom CircleMap = REAL
by FUNCT_2:def_1, TOPMETR:17;
definition
let r be real number ;
func cLoop r -> Function of I[01],(Tunit_circle 2) means :Def4: :: TOPALG_5:def 4
for x being Point of I[01] holds it . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|;
existence
ex b1 being Function of I[01],(Tunit_circle 2) st
for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|
proof
defpred S1[ real number , 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 the carrier of (Tunit_circle 2) st S1[x,y]
proof
let x be Element of I[01]; ::_thesis: ex y being Element of the carrier of (Tunit_circle 2) st S1[x,y]
set y = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|;
|.(|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| - |[0,0]|).| = |.|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]|.| by EUCLID:54, RLVECT_1:13
.= sqrt (((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `1) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `2) ^2)) by JGRAPH_1:30
.= sqrt (((cos (((2 * PI) * r) * x)) ^2) + ((|[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| `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 = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| as Element of the carrier of (Tunit_circle 2) by Lm11, TOPREAL9:9;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
ex f being Function of the carrier of I[01], the carrier of (Tunit_circle 2) st
for x being Element of I[01] holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence ex b1 being Function of I[01],(Tunit_circle 2) st
for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of I[01],(Tunit_circle 2) st ( for x being Point of I[01] holds b1 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) & ( for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) holds
b1 = b2
proof
let f, g be Function of I[01],(Tunit_circle 2); ::_thesis: ( ( for x being Point of I[01] holds f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) & ( for x being Point of I[01] holds g . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| ) implies f = g )
assume 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))]| ; ::_thesis: f = g
for x being Point of I[01] holds f . x = g . x
proof
let x be Point of I[01]; ::_thesis: f . x = g . x
thus f . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines cLoop TOPALG_5:def_4_:_
for r being real number
for b2 being Function of I[01],(Tunit_circle 2) holds
( b2 = cLoop r iff for x being Point of I[01] holds b2 . x = |[(cos (((2 * PI) * r) * x)),(sin (((2 * PI) * r) * x))]| );
theorem Th20: :: TOPALG_5:20
for r being real number holds cLoop r = CircleMap * (ExtendInt r)
proof
let r be real number ; ::_thesis: cLoop r = CircleMap * (ExtendInt r)
for x being Point of I[01] holds (cLoop r) . x = (CircleMap * (ExtendInt r)) . x
proof
let x be Point of I[01]; ::_thesis: (cLoop r) . x = (CircleMap * (ExtendInt r)) . x
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 ; ::_thesis: verum
end;
hence cLoop r = CircleMap * (ExtendInt r) by FUNCT_2:63; ::_thesis: verum
end;
definition
let n be Integer;
:: original: cLoop
redefine func cLoop n -> Loop of c[10] ;
coherence
cLoop n is Loop of c[10]
proof
set f = cLoop n;
cLoop n = CircleMap * (ExtendInt n) by Th20;
hence cLoop n is continuous ; :: according to BORSUK_2:def_4 ::_thesis: ( (cLoop n) . 0 = c[10] & (cLoop n) . 1 = c[10] )
thus (cLoop n) . 0 = |[(cos (((2 * PI) * n) * j0)),(sin (((2 * PI) * n) * j0))]| by Def4
.= c[10] by SIN_COS:31, TOPREALB:def_8 ; ::_thesis: (cLoop n) . 1 = c[10]
thus (cLoop n) . 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 ; ::_thesis: verum
end;
end;
begin
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 holds
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 holds
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) holds
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)) holds
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 ; ::_thesis: ( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) st U in F holds
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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) )
thus ( F is Cover of (Tunit_circle 2) & F is open ) by A2; ::_thesis: for U being Subset of (Tunit_circle 2) st U in F holds
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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
let U be Subset of (Tunit_circle 2); ::_thesis: ( U in F implies 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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) )
assume A4: U in F ; ::_thesis: 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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
percases ( U = CircleMap .: ].0,1.[ or U = CircleMap .: ].(1 / 2),(3 / 2).[ ) by A1, A4, TARSKI:def_2;
supposeA5: U = CircleMap .: ].0,1.[ ; ::_thesis: 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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
reconsider D = IntIntervals (0,1) as mutually-disjoint open Subset-Family of R^1 by Lm8, TOPREALB:4;
take D ; ::_thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by A3, A5; ::_thesis: verum
end;
supposeA6: U = CircleMap .: ].(1 / 2),(3 / 2).[ ; ::_thesis: 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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
reconsider D = IntIntervals ((1 / 2),(3 / 2)) as mutually-disjoint open Subset-Family of R^1 by Lm9, TOPREALB:4;
take D ; ::_thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by A3, A6; ::_thesis: verum
end;
end;
end;
Lm14: [#] (Sspace 0[01]) = {0}
by TEX_2:def_2;
Lm15: for r, s being real number
for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds
not G is empty
proof
let r, s be real number ; ::_thesis: for F being Subset-Family of (Closed-Interval-TSpace (r,s))
for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds
not G is empty
let F be Subset-Family of (Closed-Interval-TSpace (r,s)); ::_thesis: for C being IntervalCover of F
for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds
not G is empty
let C be IntervalCover of F; ::_thesis: for G being IntervalCoverPts of C st F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s holds
not G is empty
let G be IntervalCoverPts of C; ::_thesis: ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s implies not G is empty )
assume ( F is Cover of (Closed-Interval-TSpace (r,s)) & F is open & F is connected & r <= s ) ; ::_thesis: not G is empty
then len G = (len C) + 1 by RCOMP_3:def_3;
hence not G is empty by CARD_1:27; ::_thesis: verum
end;
theorem Th21: :: TOPALG_5:21
for UL being Subset-Family of (Tunit_circle 2) st UL is Cover of (Tunit_circle 2) & UL is open holds
for Y being non empty TopSpace
for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)
for 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 holds
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 (Tunit_circle 2); ::_thesis: ( UL is Cover of (Tunit_circle 2) & UL is open implies for Y being non empty TopSpace
for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)
for 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) )
assume that
A1: UL is Cover of (Tunit_circle 2) and
A2: UL is open ; ::_thesis: for Y being non empty TopSpace
for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)
for 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )
let Y be non empty TopSpace; ::_thesis: for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)
for 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )
let F be continuous Function of [:Y,I[01]:],(Tunit_circle 2); ::_thesis: for 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )
let y be Point of Y; ::_thesis: 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )
A3: [#] (Tunit_circle 2) = union UL by A1, SETFAM_1:45;
A4: for i being Point of I[01] ex U being non empty open Subset of (Tunit_circle 2) st
( F . [y,i] in U & U in UL )
proof
let i be Point of I[01]; ::_thesis: ex U being non empty open Subset of (Tunit_circle 2) st
( F . [y,i] in U & U in UL )
consider U being set such that
A5: ( F . [y,i] in U & U in UL ) by A3, TARSKI:def_4;
reconsider U = U as non empty open Subset of (Tunit_circle 2) by A2, A5, TOPS_2:def_1;
take U ; ::_thesis: ( F . [y,i] in U & U in UL )
thus ( F . [y,i] in U & U in UL ) by A5; ::_thesis: verum
end;
then ex U being non empty open Subset of (Tunit_circle 2) 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 S1[ set , set ] means ex V being open Subset of (Tunit_circle 2) st
( V in UL1 & F . [y,$1] in V & $2 = V );
A6: for i being Element of the carrier of I[01] ex z being Element of UL1 st S1[i,z]
proof
let i be Element of the carrier of I[01]; ::_thesis: ex z being Element of UL1 st S1[i,z]
ex U being non empty open Subset of (Tunit_circle 2) st
( F . [y,i] in U & U in UL ) by A4;
hence ex z being Element of UL1 st S1[i,z] ; ::_thesis: verum
end;
consider I0 being Function of the carrier of I[01],UL1 such that
A7: for i being Element of the carrier of I[01] holds S1[i,I0 . i] from FUNCT_2:sch_3(A6);
defpred S2[ set , set ] means ex M being open Subset of Y ex 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 the carrier of I[01] ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S2[i,z]
proof
let i be Element of the carrier of I[01]; ::_thesis: ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S2[i,z]
consider V being open Subset of (Tunit_circle 2) 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 holds
ex A being Subset of Y ex 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 = A as open Subset of Y by A19;
A21: i in B by A16, A18, ZFMISC_1:87;
reconsider B = B as non empty open Subset of I[01] by A16, A18, A20, ZFMISC_1:87;
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 [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def_2;
take z ; ::_thesis: S2[i,z]
take A ; ::_thesis: ex O being open connected Subset of I[01] st
( y in A & i in O & F .: [:A,O:] c= I0 . i & z = [:A,O:] )
take D ; ::_thesis: ( y in A & i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )
thus y in A by A16, A18, ZFMISC_1:87; ::_thesis: ( i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )
thus i in D by A21, CONNSP_3:26; ::_thesis: ( F .: [:A,D:] c= I0 . i & z = [:A,D:] )
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, XBOOLE_1:1;
then F .: z c= F .: W by RELAT_1:123;
hence F .: [:A,D:] c= I0 . i by A10, A13, XBOOLE_1:1; ::_thesis: z = [:A,D:]
thus z = [:A,D:] ; ::_thesis: verum
end;
consider I1 being Function of the carrier of I[01],(bool [: the carrier of Y, the carrier of I[01]:]) such that
A24: for i being Element of the carrier of I[01] holds S2[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]:]; :: according to TOPS_2:def_1 ::_thesis: ( not P in C1 or P is open )
assume P in C1 ; ::_thesis: P is open
then consider i being set such that
A26: i in dom I1 and
A27: I1 . i = P by FUNCT_1:def_3;
S2[i,I1 . i] by A24, A26;
hence P is open by A27, BORSUK_1:6; ::_thesis: verum
end;
A28: dom I1 = the carrier of I[01] by FUNCT_2:def_1;
[:{y},([#] I[01]):] c= union C1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [:{y},([#] I[01]):] or a in union C1 )
assume a in [:{y},([#] I[01]):] ; ::_thesis: a in union C1
then consider a1, a2 being set 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 = 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 a in union C1 by A31, A32, TARSKI:def_4; ::_thesis: verum
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, COMPTS_1:def_4;
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 ) } ;
{ M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } c= bool the carrier of Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } or a in bool the carrier of Y )
assume a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ; ::_thesis: a in bool the carrier of Y
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 a in bool the carrier of Y ; ::_thesis: verum
end;
then reconsider 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 ) } 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 S3[ set , set ] means ex M being open Subset of Y ex O being non empty open Subset of I[01] st
( y in M & p . $1 = [:M,O:] & $2 = M );
A41: for x being set st x in dom p holds
ex y being set st
( y in NN & S3[x,y] )
proof
let x be set ; ::_thesis: ( x in dom p implies ex y being set st
( y in NN & S3[x,y] ) )
assume x in dom p ; ::_thesis: ex y being set st
( y in NN & S3[x,y] )
then A42: p . x in rng p by FUNCT_1:def_3;
then consider i being set 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 ; ::_thesis: ( M in NN & S3[x,M] )
thus ( M in NN & S3[x,M] ) by A39, A42, A44, A45, A46; ::_thesis: verum
end;
consider p1 being Function of (dom p),NN such that
A47: for x being set st x in dom p holds
S3[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 set 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 ; :: according to XBOOLE_0:def_10 ::_thesis: NN c= rng p1
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in NN or a in rng p1 )
assume a in NN ; ::_thesis: a in rng p1
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 set 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 a in rng p1 by A56, A57, A60, A63, FUNCT_1:def_3; ::_thesis: verum
end;
then A64: NN is finite by A40, A56, FINSET_1:def_1;
NN is open
proof
let a be Subset of Y; :: according to TOPS_2:def_1 ::_thesis: ( not a in NN or a is open )
assume a in NN ; ::_thesis: a is open
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 a is open ; ::_thesis: verum
end;
then reconsider N = meet NN as open Subset of Y by A64, TOPS_2:20;
{ O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } c= bool the carrier of I[01]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } or a in bool the carrier of I[01] )
assume a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ; ::_thesis: a in bool the carrier of I[01]
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 a in bool the carrier of I[01] ; ::_thesis: verum
end;
then reconsider ICOV = { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } as Subset-Family of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
[#] (Closed-Interval-TSpace (0,1)) c= union ICOV
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [#] (Closed-Interval-TSpace (0,1)) or a in union ICOV )
assume a in [#] (Closed-Interval-TSpace (0,1)) ; ::_thesis: a in union ICOV
then reconsider a = 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 set 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 a in union ICOV by TARSKI:def_4; ::_thesis: verum
end;
then A70: ICOV is Cover of (Closed-Interval-TSpace (0,1)) by SETFAM_1:def_11;
set NCOV = the IntervalCover of ICOV;
set T = the IntervalCoverPts of the IntervalCover of ICOV;
A71: ICOV is connected
proof
let X be Subset of (Closed-Interval-TSpace (0,1)); :: according to RCOMP_3:def_1 ::_thesis: ( not X in ICOV or X is connected )
assume X in ICOV ; ::_thesis: X is connected
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 X is connected by TOPMETR:20; ::_thesis: verum
end;
A72: ICOV is open
proof
let a be Subset of (Closed-Interval-TSpace (0,1)); :: according to TOPS_2:def_1 ::_thesis: ( not a in ICOV or a is open )
assume a in ICOV ; ::_thesis: a is open
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 a is open by TOPMETR:20; ::_thesis: verum
end;
then reconsider T = the IntervalCoverPts of the IntervalCover of ICOV as non empty FinSequence of REAL by A70, A71, Lm15;
take T ; ::_thesis: ( 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )
thus ( T . 1 = 0 & T . (len T) = 1 ) by A70, A72, A71, RCOMP_3:def_3; ::_thesis: ( 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )
thus T is increasing by A70, A72, A71, RCOMP_3:65; ::_thesis: 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 holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )
take N ; ::_thesis: ( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )
now__::_thesis:_for_Z_being_set_st_Z_in_NN_holds_
y_in_Z
let Z be set ; ::_thesis: ( Z in NN implies y in Z )
assume Z in NN ; ::_thesis: y in Z
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 ; ::_thesis: verum
end;
hence y in N by A55, SETFAM_1:def_1; ::_thesis: for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )
let i be Nat; ::_thesis: ( i in dom T & i + 1 in dom T implies ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) )
assume that
A73: i in dom T and
A74: i + 1 in dom T ; ::_thesis: ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )
A75: 1 <= i by A73, FINSEQ_3:25;
A76: i + 1 <= len T by A74, FINSEQ_3:25;
len T = (len the IntervalCover of ICOV) + 1 by A70, A72, A71, RCOMP_3:def_3;
then i <= len the IntervalCover of ICOV by A76, XREAL_1:6;
then i in dom the IntervalCover of ICOV by A75, FINSEQ_3:25;
then A77: the IntervalCover of ICOV . i in rng the IntervalCover of ICOV by FUNCT_1:def_3;
rng the IntervalCover of ICOV c= ICOV by A70, A72, A71, RCOMP_3:def_2;
then the IntervalCover of ICOV . i in ICOV by A77;
then consider O being open connected Subset of I[01] such that
A78: the IntervalCover of ICOV . 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 set 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 (Tunit_circle 2) such that
A84: V in UL1 and
A85: F . [y,j] in V and
A86: I0 . j = V by A7, A82;
reconsider V = V as non empty open Subset of (Tunit_circle 2) by A85;
take V ; ::_thesis: ( V in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V )
thus V in UL by A84; ::_thesis: F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V
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 F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V by A89, A86, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th22: :: TOPALG_5:22
for Y being non empty TopSpace
for F being Function of [:Y,I[01]:],(Tunit_circle 2)
for 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 holds
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 (Tunit_circle 2) such that
A1: ( UL is Cover of (Tunit_circle 2) & UL is open ) and
A2: for U being Subset of (Tunit_circle 2) st U in UL holds
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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by Lm13;
let Y be non empty TopSpace; ::_thesis: for F being Function of [:Y,I[01]:],(Tunit_circle 2)
for 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 holds
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 ) )
let F be Function of [:Y,I[01]:],(Tunit_circle 2); ::_thesis: for 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 holds
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 ) )
let Ft be Function of [:Y,(Sspace 0[01]):],R^1; ::_thesis: ( F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft implies 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 ) ) )
assume that
A3: F is continuous and
A4: Ft is continuous and
A5: F | [: the carrier of Y,{0}:] = CircleMap * Ft ; ::_thesis: 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 ) )
defpred S1[ set , set ] means ex y being Point of Y ex t being Point of I[01] ex N being non empty open Subset of Y ex 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, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H ) );
A6: dom F = the carrier of [:Y,I[01]:] by FUNCT_2:def_1
.= [: the carrier of Y, the carrier of I[01]:] 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 S1[x,z]
proof
let x be Point of [:Y,I[01]:]; ::_thesis: ex z being Point of R^1 st S1[x,z]
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 holds
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 holds
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 = N as non empty open Subset of Y by A15;
defpred S2[ Element of NAT ] means ( $1 in dom TT implies ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex 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, the carrier of I[01]:] ) );
A17: len TT in dom TT by FINSEQ_5:6;
A18: 1 in dom TT by FINSEQ_5:6;
A19: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_TT_holds_
(_0_<=_TT_._i_&_(_i_+_1_in_dom_TT_implies_(_TT_._i_<_TT_._(i_+_1)_&_TT_._(i_+_1)_<=_1_&_TT_._i_<_1_&_0_<_TT_._(i_+_1)_)_)_)
let i be Element of NAT ; ::_thesis: ( i in dom TT implies ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) )
assume A20: i in dom TT ; ::_thesis: ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) )
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; ::_thesis: ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) )
assume A22: i + 1 in dom TT ; ::_thesis: ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
A23: i + 0 < i + 1 by XREAL_1:8;
hence A24: TT . i < TT . (i + 1) by A13, A20, A22, SEQM_3:def_1; ::_thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 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; ::_thesis: ( TT . i < 1 & 0 < TT . (i + 1) )
hence TT . i < 1 by A24, XXREAL_0:2; ::_thesis: 0 < TT . (i + 1)
thus 0 < TT . (i + 1) by A13, A20, A21, A22, A23, SEQM_3:def_1; ::_thesis: verum
end;
A25: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<=_TT_._i_&_TT_._(i_+_1)_<=_1_holds_
[.(TT_._i),(TT_._(i_+_1)).]_c=_the_carrier_of_I[01]
let i be Element of NAT ; ::_thesis: ( 0 <= TT . i & TT . (i + 1) <= 1 implies [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] )
assume that
A26: 0 <= TT . i and
A27: TT . (i + 1) <= 1 ; ::_thesis: [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01]
thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [.(TT . i),(TT . (i + 1)).] or a in the carrier of I[01] )
assume A28: a in [.(TT . i),(TT . (i + 1)).] ; ::_thesis: a in the carrier of I[01]
then reconsider a = 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 a in the carrier of I[01] by A29, BORSUK_1:43; ::_thesis: verum
end;
end;
A30: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume that
A31: S2[i] and
A32: i + 1 in dom TT ; ::_thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
percases ( i = 0 or i in dom TT ) by A32, TOPREALA:2;
supposeA33: i = 0 ; ::_thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
take N2 = N; ::_thesis: ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
set Fn = Ft | [:N2,{0}:];
set S = [.0,(TT . (i + 1)).];
A34: [.0,(TT . (i + 1)).] = {0} by A11, A33, XXREAL_1:17;
reconsider S = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A11, A33, Lm3, XXREAL_1:17;
A35: dom (Ft | [:N2,{0}:]) = [: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 (Ft | [:N2,{0}:]) c= the carrier of R^1 ) by BORSUK_1:def_2;
( the carrier of (Y | N2) = N2 & the carrier of (I[01] | S) = S ) by PRE_TOPC:8;
then reconsider Fn = Ft | [:N2,{0}:] 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 ; ::_thesis: ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
take Fn ; ::_thesis: ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
thus S = [.0,(TT . (i + 1)).] ; ::_thesis: ( y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
thus y in N2 by A15; ::_thesis: ( N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
thus N2 c= N ; ::_thesis: ( Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
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; ::_thesis: ( F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
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 set st x in dom (F | [:N2,S:]) holds
(F | [:N2,S:]) . x = (CircleMap * Fn) . x
proof
let x be set ; ::_thesis: ( x in dom (F | [:N2,S:]) implies (F | [:N2,S:]) . x = (CircleMap * Fn) . x )
assume A40: x in dom (F | [:N2,S:]) ; ::_thesis: (F | [:N2,S:]) . x = (CircleMap * Fn) . x
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 ; ::_thesis: verum
end;
hence F | [:N2,S:] = CircleMap * Fn by A35, A37, A38, FUNCT_1:2; ::_thesis: Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]
A41: dom (Fn | [: the carrier of Y,{0}:]) = [:N2,S:] /\ [: the carrier of Y,{0}:] by A35, RELAT_1:61;
A42: for x being set st x in dom (Fn | [: the carrier of Y,{0}:]) holds
(Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x
proof
A43: [:N2,{0}:] c= [:N2, the carrier of I[01]:] by Lm3, ZFMISC_1:95;
let x be set ; ::_thesis: ( x in dom (Fn | [: the carrier of Y,{0}:]) implies (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x )
assume A44: x in dom (Fn | [: the carrier of Y,{0}:]) ; ::_thesis: (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x
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, the carrier of I[01]:]) . x by A45, A43, FUNCT_1:49 ;
::_thesis: verum
end;
dom (Ft | [:N2, the carrier of I[01]:]) = [: the carrier of Y,{0}:] /\ [:N2, the carrier of I[01]:] by A8, RELAT_1:61
.= [:N2,S:] by A34, ZFMISC_1:101 ;
hence Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] by A34, A41, A42, FUNCT_1:2, ZFMISC_1:101; ::_thesis: verum
end;
supposeA46: i in dom TT ; ::_thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),(I[01] | S):],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
set SS = [.(TT . i),(TT . (i + 1)).];
consider Ui being non empty Subset of (Tunit_circle 2) such that
A47: Ui in UL and
A48: F .: [:N,[.(TT . i),(TT . (i + 1)).]:] 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 holds
for f being Function of (R^1 | d),((Tunit_circle 2) | Ui) st f = CircleMap | d holds
f is being_homeomorphism by A2, A47;
A51: the carrier of ((Tunit_circle 2) | Ui) = Ui by PRE_TOPC:8;
A52: TT . i < TT . (i + 1) by A19, A32, A46;
then TT . i in [.(TT . i),(TT . (i + 1)).] by XXREAL_1:1;
then A53: [y,(TT . i)] in [:N,[.(TT . i),(TT . (i + 1)).]:] 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, the carrier of I[01]:] by A31, A46;
reconsider N2 = 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 (Fn | [:N2,Ti:]) c= REAL ) by BORSUK_1:def_2, TOPMETR:17;
A66: [:N2,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:] 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 (Fn | [:N2,Ti:]) = [: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;
then reconsider FnT = Fn | [:N2,Ti:] as Function of [:(Y | N2),(I[01] | Ti):],R^1 by A67, A68, A65, 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;
[y,(TT . i)] in dom F by A6, A63, ZFMISC_1:87;
then A72: F . [y,(TT . i)] in F .: [:N,[.(TT . i),(TT . (i + 1)).]:] by A53, FUNCT_2:35;
A73: [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, A73, FUNCT_2:15 ;
then Fn . [y,(TT . i)] in CircleMap " Ui by A48, A72, FUNCT_2:38, TOPMETR:17;
then consider Uit being set such that
A74: Fn . [y,(TT . i)] in Uit and
A75: Uit in D by A49, TARSKI:def_4;
reconsider Uit = Uit as non empty Subset of R^1 by A74, A75;
( [#] R^1 <> {} & Uit is open ) by A75, 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
A76: FnT " Uit = union SF and
A77: for e being set st e in SF holds
ex X1 being Subset of (Y | N2) ex Y1 being Subset of (I[01] | Ti) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
A78: TT . i in {(TT . i)} by TARSKI:def_1;
then A79: [y,(TT . i)] in [:N2,{(TT . i)}:] by A55, ZFMISC_1:def_2;
then FnT . [y,(TT . i)] in Uit by A74, FUNCT_1:49;
then [y,(TT . i)] in FnT " Uit by A79, A68, FUNCT_1:def_7;
then consider N5 being set such that
A80: [y,(TT . i)] in N5 and
A81: N5 in SF by A76, TARSKI:def_4;
set f = CircleMap | Uit;
A82: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17;
A83: rng (CircleMap | Uit) c= Ui
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (CircleMap | Uit) or b in Ui )
assume b in rng (CircleMap | Uit) ; ::_thesis: b in Ui
then consider a being set such that
A84: a in dom (CircleMap | Uit) and
A85: (CircleMap | Uit) . a = b by FUNCT_1:def_3;
a in union D by A75, A82, A84, TARSKI:def_4;
then CircleMap . a in Ui by A49, FUNCT_2:38;
hence b in Ui by A82, A84, A85, FUNCT_1:49; ::_thesis: verum
end;
consider X1 being Subset of (Y | N2), Y1 being Subset of (I[01] | Ti) such that
A86: N5 = [:X1,Y1:] and
A87: X1 is open and
Y1 is open by A77, A81;
the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A51, A82, A83, FUNCT_2:2;
consider NY being Subset of Y such that
A88: NY is open and
A89: NY /\ ([#] (Y | N2)) = X1 by A87, TOPS_2:24;
consider y1, y2 being set such that
A90: y1 in X1 and
A91: y2 in Y1 and
A92: [y,(TT . i)] = [y1,y2] by A80, A86, ZFMISC_1:def_2;
set N1 = NY /\ N2;
y = y1 by A92, XTUPLE_0:1;
then A93: y in NY by A89, A90, XBOOLE_0:def_4;
then reconsider N1 = NY /\ N2 as non empty open Subset of Y by A55, A88, XBOOLE_0:def_4;
A94: N1 c= N2 by XBOOLE_1:17;
then [:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N2,[.(TT . i),(TT . (i + 1)).]:] by ZFMISC_1:96;
then [:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:] by A66, XBOOLE_1:1;
then A95: F .: [:N1,[.(TT . i),(TT . (i + 1)).]:] c= F .: [:N,[.(TT . i),(TT . (i + 1)).]:] by RELAT_1:123;
TT . (i + 1) <= 1 by A19, A32, A46;
then reconsider SS = [.(TT . i),(TT . (i + 1)).] as non empty Subset of I[01] by A25, A62, A52, XXREAL_1:1;
A96: 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, A75, TOPS_2:56;
then A97: dom (f ") = [#] ((Tunit_circle 2) | Ui) by TOPS_2:def_5;
A98: rng (F | [:N1,SS:]) c= dom (f ")
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (F | [:N1,SS:]) or b in dom (f ") )
assume b in rng (F | [:N1,SS:]) ; ::_thesis: b in dom (f ")
then consider a being set such that
A99: a in dom (F | [:N1,SS:]) and
A100: (F | [:N1,SS:]) . a = b by FUNCT_1:def_3;
b = F . a by A96, A99, A100, FUNCT_1:49;
then b in F .: [:N1,SS:] by A96, A99, FUNCT_2:35;
then b in F .: [:N,SS:] by A95;
then b in Ui by A48;
hence b in dom (f ") by A97, PRE_TOPC:8; ::_thesis: verum
end;
then A101: dom ((f ") * (F | [:N1,SS:])) = dom (F | [:N1,SS:]) by RELAT_1:27;
set Fn2 = Fn | [:N1,S:];
A102: the carrier of (Y | N1) = N1 by PRE_TOPC:8;
then A103: [:N1,S:] = the carrier of [:(Y | N1),(I[01] | S):] by A64, BORSUK_1:def_2;
then A104: dom (Fn | [:N1,S:]) = the carrier of [:(Y | N1),(I[01] | S):] by A64, A60, A67, A61, A94, RELAT_1:62, ZFMISC_1:96;
reconsider ff = f as Function ;
A105: f is being_homeomorphism by A50, A75;
then A106: f is one-to-one by TOPS_2:def_5;
A107: rng (Fn | [:N1,S:]) c= the carrier of R^1 ;
the carrier of (R^1 | Uit) is Subset of R^1 by TSEP_1:1;
then A108: rng ((f ") * (F | [:N1,SS:])) c= the carrier of R^1 by XBOOLE_1:1;
A109: the carrier of (I[01] | SS) = SS by PRE_TOPC:8;
then A110: [:N1,SS:] = the carrier of [:(Y | N1),(I[01] | SS):] by A102, BORSUK_1:def_2;
then reconsider Fni1 = (f ") * (F | [:N1,SS:]) as Function of [:(Y | N1),(I[01] | SS):],R^1 by A96, A101, A108, FUNCT_2:2;
set Fn1 = (Fn | [:N1,S:]) +* Fni1;
reconsider Fn2 = Fn | [:N1,S:] as Function of [:(Y | N1),(I[01] | S):],R^1 by A104, A107, FUNCT_2:2;
A111: rng ((Fn | [:N1,S:]) +* Fni1) c= (rng (Fn | [:N1,S:])) \/ (rng Fni1) by FUNCT_4:17;
dom (Fn | [:N1,S:]) = [:N1,S:] by A64, A60, A67, A61, A94, RELAT_1:62, ZFMISC_1:96;
then A112: dom ((Fn | [:N1,S:]) +* Fni1) = [:N1,S:] \/ [:N1,SS:] by A96, A101, FUNCT_4:def_1;
A113: rng f = [#] ((Tunit_circle 2) | Ui) by A105, TOPS_2:def_5;
then f is onto by FUNCT_2:def_3;
then A114: f " = ff " by A106, TOPS_2:def_4;
A115: Y1 = Ti
proof
thus Y1 c= Ti by A70; :: according to XBOOLE_0:def_10 ::_thesis: Ti c= Y1
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Ti or a in Y1 )
assume a in Ti ; ::_thesis: a in Y1
then a = TT . i by TARSKI:def_1;
hence a in Y1 by A91, A92, XTUPLE_0:1; ::_thesis: verum
end;
A116: Fn .: [:N1,{(TT . i)}:] c= Uit
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Fn .: [:N1,{(TT . i)}:] or b in Uit )
assume b in Fn .: [:N1,{(TT . i)}:] ; ::_thesis: b in Uit
then consider a being Point of [:(Y | N2),(I[01] | S):] such that
A117: a in [:N1,{(TT . i)}:] and
A118: Fn . a = b by FUNCT_2:65;
a in N5 by A86, A89, A115, A117, PRE_TOPC:def_5;
then A119: a in union SF by A81, TARSKI:def_4;
then a in dom FnT by A76, FUNCT_1:def_7;
then Fn . a = FnT . a by FUNCT_1:47;
hence b in Uit by A76, A118, A119, FUNCT_1:def_7; ::_thesis: verum
end;
A120: for p being set st p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) holds
Fn2 . p = Fni1 . p
proof
A121: the carrier of (Y | N2) = N2 by PRE_TOPC:8;
let p be set ; ::_thesis: ( p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) implies Fn2 . p = Fni1 . p )
assume A122: p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) ; ::_thesis: Fn2 . p = Fni1 . p
A123: p in ([#] [:(Y | N1),(I[01] | SS):]) /\ ([#] [:(Y | N1),(I[01] | S):]) by A122;
then A124: Fn . p = Fn2 . p by A103, FUNCT_1:49;
[:N1,S:] /\ [:N1,SS:] = [:N1,(S /\ SS):] by ZFMISC_1:99;
then A125: p in [:N1,{(TT . i)}:] by A54, A62, A52, A110, A103, A122, XXREAL_1:418;
then consider p1 being Element of N1, p2 being Element of {(TT . i)} such that
A126: p = [p1,p2] by DOMAIN_1:1;
A127: p1 in N1 ;
S /\ SS = {(TT . i)} by A54, A62, A52, XXREAL_1:418;
then p2 in S by XBOOLE_0:def_4;
then A128: p in [:N2,S:] by A94, A126, A127, ZFMISC_1:def_2;
then A129: Fn . p in Fn .: [:N1,{(TT . i)}:] by A64, A60, A67, A125, FUNCT_2:35;
(F | [:N1,SS:]) . p = F . p by A110, A122, FUNCT_1:49
.= (F | [:N2,S:]) . p by A128, FUNCT_1:49
.= CircleMap . (Fn . p) by A58, A64, A60, A61, A121, A128, FUNCT_1:13
.= (CircleMap | Uit) . (Fn . p) by A116, A129, FUNCT_1:49
.= ff . (Fn2 . p) by A103, A123, FUNCT_1:49 ;
hence Fn2 . p = (ff ") . ((F | [:N1,SS:]) . p) by A116, A82, A106, A124, A129, FUNCT_1:32
.= Fni1 . p by A114, A96, A110, A122, FUNCT_1:13 ;
::_thesis: verum
end;
A130: [:N1,S:] c= [:N2,S:] by A94, ZFMISC_1:96;
then reconsider K0 = [:N1,S:] as Subset of [:(Y | N2),(I[01] | S):] by A64, A60, PRE_TOPC:8;
A131: [:N1,SS:] c= dom F by A6, ZFMISC_1:96;
reconsider gF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],(Tunit_circle 2) by A96, A98, A110, FUNCT_2:2;
reconsider fF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],((Tunit_circle 2) | Ui) by A97, A96, A98, A110, 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 A132: fF is continuous by TOPMETR:6;
f " is continuous by A105, TOPS_2:def_5;
then (f ") * fF is continuous by A132;
then A133: Fni1 is continuous by PRE_TOPC:26;
reconsider aN1 = N1 as non empty Subset of (Y | N2) by A94, 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 A134: Fn2 is continuous by A57, TOPMETR:7;
take N1 ; ::_thesis: ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N1),(I[01] | S):],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn is continuous & F | [:N1,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
take S1 = S \/ SS; ::_thesis: ex Fn being Function of [:(Y | N1),(I[01] | S1):],R^1 st
( S1 = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn is continuous & F | [:N1,S1:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
A135: [:N1,S:] \/ [:N1,SS:] = [:N1,S1:] by ZFMISC_1:97;
A136: the carrier of (I[01] | S1) = S1 by PRE_TOPC:8;
then [:N1,S1:] = the carrier of [:(Y | N1),(I[01] | S1):] by A102, BORSUK_1:def_2;
then reconsider Fn1 = (Fn | [:N1,S:]) +* Fni1 as Function of [:(Y | N1),(I[01] | S1):],R^1 by A135, A112, A111, FUNCT_2:2, XBOOLE_1:1;
take Fn1 ; ::_thesis: ( S1 = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
thus A137: S1 = [.0,(TT . (i + 1)).] by A54, A62, A52, XXREAL_1:165; ::_thesis: ( y in N1 & N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
0 <= TT . (i + 1) by A19, A32;
then 0 in S1 by A137, XXREAL_1:1;
then A138: {0} c= S1 by ZFMISC_1:31;
A139: dom (Fn1 | [: the carrier of Y,{0}:]) = (dom Fn1) /\ [: the carrier of Y,{0}:] by RELAT_1:61;
then A140: dom (Fn1 | [: the carrier of Y,{0}:]) = [:(N1 /\ the carrier of Y),(S1 /\ {0}):] by A135, A112, ZFMISC_1:100
.= [:N1,(S1 /\ {0}):] by XBOOLE_1:28
.= [:N1,{0}:] by A138, XBOOLE_1:28 ;
A141: for a being set st a in dom (Fn1 | [: the carrier of Y,{0}:]) holds
(Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
proof
let a be set ; ::_thesis: ( a in dom (Fn1 | [: the carrier of Y,{0}:]) implies (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a )
A142: [:N1, the carrier of I[01]:] c= [:N2, the carrier of I[01]:] by A94, ZFMISC_1:96;
assume A143: a in dom (Fn1 | [: the carrier of Y,{0}:]) ; ::_thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
then A144: a in [: the carrier of Y,{0}:] by A139, XBOOLE_0:def_4;
then consider a1, a2 being set such that
a1 in the carrier of Y and
A145: a2 in {0} and
A146: a = [a1,a2] by ZFMISC_1:def_2;
A147: a2 = 0 by A145, TARSKI:def_1;
0 in S by A54, A62, XXREAL_1:1;
then {0} c= S by ZFMISC_1:31;
then A148: [:N1,{0}:] c= [:N1,S:] by ZFMISC_1:96;
then A149: a in [:N1,S:] by A140, A143;
A150: [:N1,S:] c= [:N1, the carrier of I[01]:] by ZFMISC_1:96;
then A151: a in [:N1, the carrier of I[01]:] by A149;
percases ( not a in dom Fni1 or a in dom Fni1 ) ;
supposeA152: not a in dom Fni1 ; ::_thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
thus (Fn1 | [: the carrier of Y,{0}:]) . a = Fn1 . a by A144, FUNCT_1:49
.= (Fn | [:N1,S:]) . a by A152, FUNCT_4:11
.= Fn . a by A140, A143, A148, FUNCT_1:49
.= (Ft | [:N2, the carrier of I[01]:]) . a by A59, A144, FUNCT_1:49
.= Ft . a by A151, A142, FUNCT_1:49
.= (Ft | [:N1, the carrier of I[01]:]) . a by A149, A150, FUNCT_1:49 ; ::_thesis: verum
end;
supposeA153: a in dom Fni1 ; ::_thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
set e = (Ft | [:N1, the carrier of I[01]:]) . a;
a in [:N1,SS:] by A6, A101, A153, RELAT_1:62, ZFMISC_1:96;
then consider b1, b2 being set such that
A154: b1 in N1 and
A155: b2 in SS and
A156: a = [b1,b2] by ZFMISC_1:def_2;
a2 = b2 by A146, A156, XTUPLE_0:1;
then A157: a2 = TT . i by A62, A147, A155, XXREAL_1:1;
a1 = b1 by A146, A156, XTUPLE_0:1;
then A158: ( [a1,(TT . i)] in [:N1,S:] & [a1,(TT . i)] in [:N1,{(TT . i)}:] ) by A63, A78, A154, ZFMISC_1:87;
(Ft | [:N1, the carrier of I[01]:]) . a = Ft . a by A149, A150, FUNCT_1:49
.= (Ft | [:N2, the carrier of I[01]:]) . a by A151, A142, FUNCT_1:49
.= Fn . a by A59, A144, FUNCT_1:49 ;
then A159: (Ft | [:N1, the carrier of I[01]:]) . a in Fn .: [:N1,{(TT . i)}:] by A64, A60, A67, A61, A130, A146, A157, A158, FUNCT_1:def_6;
then A160: ff . ((Ft | [:N1, the carrier of I[01]:]) . a) = CircleMap . ((Ft | [:N1, the carrier of I[01]:]) . a) by A116, FUNCT_1:49
.= CircleMap . (Ft . a) by A149, A150, FUNCT_1:49
.= (CircleMap * Ft) . a by A8, A144, FUNCT_1:13
.= F . a by A5, A144, FUNCT_1:49 ;
thus (Fn1 | [: the carrier of Y,{0}:]) . a = Fn1 . a by A144, FUNCT_1:49
.= Fni1 . a by A153, FUNCT_4:13
.= (ff ") . ((F | [:N1,SS:]) . a) by A114, A101, A153, FUNCT_1:13
.= (ff ") . (F . a) by A96, A101, A153, FUNCT_1:49
.= (Ft | [:N1, the carrier of I[01]:]) . a by A116, A82, A106, A159, A160, FUNCT_1:32 ; ::_thesis: verum
end;
end;
end;
A161: rng Fn1 c= dom CircleMap by Lm12, TOPMETR:17;
then A162: dom (CircleMap * Fn1) = dom Fn1 by RELAT_1:27;
A163: for a being set st a in dom (CircleMap * Fn1) holds
(CircleMap * Fn1) . a = F . a
proof
let a be set ; ::_thesis: ( a in dom (CircleMap * Fn1) implies (CircleMap * Fn1) . a = F . a )
assume A164: a in dom (CircleMap * Fn1) ; ::_thesis: (CircleMap * Fn1) . a = F . a
percases ( a in dom Fni1 or not a in dom Fni1 ) ;
supposeA165: a in dom Fni1 ; ::_thesis: (CircleMap * Fn1) . a = F . a
A166: [:N1,SS:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
A167: a in [:N1,SS:] by A6, A101, A165, RELAT_1:62, ZFMISC_1:96;
then F . a in F .: [:N1,SS:] by A6, A166, FUNCT_1:def_6;
then A168: F . a in F .: [:N,SS:] by A95;
then a in F " (dom (ff ")) by A6, A48, A51, A97, A114, A167, A166, FUNCT_1:def_7;
then A169: a in dom ((ff ") * F) by RELAT_1:147;
thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by A164, FUNCT_2:15
.= CircleMap . (Fni1 . a) by A165, FUNCT_4:13
.= CircleMap . ((f ") . ((F | [:N1,SS:]) . a)) by A101, A165, FUNCT_1:13
.= CircleMap . ((f ") . (F . a)) by A96, A101, A165, FUNCT_1:49
.= CircleMap . (((ff ") * F) . a) by A131, A114, A96, A101, A165, FUNCT_1:13
.= (CircleMap * ((ff ") * F)) . a by A169, FUNCT_1:13
.= ((CircleMap * (ff ")) * F) . a by RELAT_1:36
.= (CircleMap * (ff ")) . (F . a) by A131, A96, A101, A165, FUNCT_1:13
.= F . a by A48, A51, A113, A106, A168, TOPALG_3:2 ; ::_thesis: verum
end;
supposeA170: not a in dom Fni1 ; ::_thesis: (CircleMap * Fn1) . a = F . a
then A171: a in [:N1,S:] by A96, A101, A112, A162, A164, XBOOLE_0:def_3;
thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by A164, FUNCT_2:15
.= CircleMap . ((Fn | [:N1,S:]) . a) by A170, FUNCT_4:11
.= CircleMap . (Fn . a) by A171, FUNCT_1:49
.= (CircleMap * Fn) . a by A64, A60, A67, A130, A171, FUNCT_2:15
.= F . a by A58, A130, A171, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
A172: S c= S1 by XBOOLE_1:7;
then A173: ( [#] (I[01] | S1) = the carrier of (I[01] | S1) & I[01] | S is SubSpace of I[01] | S1 ) by A64, A136, TSEP_1:4;
A174: SS c= S1 by XBOOLE_1:7;
then reconsider F1 = [#] (I[01] | S), F2 = [#] (I[01] | SS) as Subset of (I[01] | S1) by A136, A172, 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 A175: F1 is closed by TSEP_1:8;
thus y in N1 by A55, A93, XBOOLE_0:def_4; ::_thesis: ( N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
thus N1 c= N by A56, A94, XBOOLE_1:1; ::_thesis: ( Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
hSS is closed by BORSUK_4:23, PRE_TOPC:8;
then A176: F2 is closed by TSEP_1:8;
I[01] | SS is SubSpace of I[01] | S1 by A109, A136, A174, 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, A109, A136, A173, A175, A176, A134, A133, A120, TOPALG_3:19;
hence Fn1 is continuous ; ::_thesis: ( F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
dom Fn1 = (dom F) /\ [:N1,S1:] by A6, A135, A112, XBOOLE_1:28, ZFMISC_1:96;
hence F | [:N1,S1:] = CircleMap * Fn1 by A161, A163, FUNCT_1:46, RELAT_1:27; ::_thesis: Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:]
dom (Ft | [:N1, the carrier of I[01]:]) = (dom Ft) /\ [:N1, the carrier of I[01]:] by RELAT_1:61
.= [:( the carrier of Y /\ N1),({0} /\ the carrier of I[01]):] by A8, ZFMISC_1:100
.= [:N1,({0} /\ the carrier of I[01]):] by XBOOLE_1:28
.= [:N1,{0}:] by Lm3, XBOOLE_1:28 ;
hence Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] by A140, A141, FUNCT_1:2; ::_thesis: verum
end;
end;
end;
A177: S2[ 0 ] by FINSEQ_3:24;
for i being Element of NAT holds S2[i] from NAT_1:sch_1(A177, 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
A178: S = [.0,(TT . (len TT)).] and
A179: y in N2 and
A180: N2 c= N and
A181: Fn1 is continuous and
A182: F | [:N2,S:] = CircleMap * Fn1 and
A183: Fn1 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] by A17;
reconsider z = Fn1 . x as Point of R^1 by TOPMETR:17;
A184: I[01] | S = I[01] by A12, A178, Lm6, BORSUK_1:40, TSEP_1:3;
then reconsider Fn1 = Fn1 as Function of [:(Y | N2),I[01]:],R^1 ;
take z ; ::_thesis: S1[x,z]
take y ; ::_thesis: ex t being Point of I[01] ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st
( x = [y,t] & z = Fn . x & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H ) )
take t ; ::_thesis: ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st
( x = [y,t] & z = Fn . x & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H ) )
take N2 ; ::_thesis: ex Fn being Function of [:(Y | N2),I[01]:],R^1 st
( x = [y,t] & z = Fn . x & y in N2 & Fn is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & ( for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] holds
Fn = H ) )
take Fn1 ; ::_thesis: ( x = [y,t] & z = Fn1 . x & y in N2 & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & ( for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] holds
Fn1 = H ) )
thus ( x = [y,t] & z = Fn1 . x & y in N2 & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) by A10, A12, A178, A179, A181, A182, A183, A184, BORSUK_1:40; ::_thesis: for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] holds
Fn1 = H
let H be Function of [:(Y | N2),I[01]:],R^1; ::_thesis: ( H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] implies Fn1 = H )
assume that
A185: H is continuous and
A186: F | [:N2, the carrier of I[01]:] = CircleMap * H and
A187: H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ; ::_thesis: Fn1 = H
defpred S3[ Element of 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:] ) );
A188: dom Fn1 = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def_1;
A189: ( the carrier of [:(Y | N2),I[01]:] = [: the carrier of (Y | N2), the carrier of I[01]:] & the carrier of (Y | N2) = N2 ) by BORSUK_1:def_2, PRE_TOPC:8;
A190: dom H = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def_1;
A191: for i being Element of NAT st S3[i] holds
S3[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S3[i] implies S3[i + 1] )
assume that
A192: S3[i] and
A193: i + 1 in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )
percases ( i = 0 or i in dom TT ) by A193, TOPREALA:2;
supposeA194: i = 0 ; ::_thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )
set Z = [.0,(TT . (i + 1)).];
A195: [.0,(TT . (i + 1)).] = {0} by A11, A194, XXREAL_1:17;
reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A11, A194, Lm3, XXREAL_1:17;
A196: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then A197: dom (Fn1 | [:N2,Z:]) = [:N2,Z:] by A189, A188, RELAT_1:62;
A198: for x being set st x in dom (Fn1 | [:N2,Z:]) holds
(Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x
proof
let x be set ; ::_thesis: ( x in dom (Fn1 | [:N2,Z:]) implies (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x )
A199: [:N2,Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95;
assume A200: x in dom (Fn1 | [:N2,Z:]) ; ::_thesis: (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x
hence (Fn1 | [:N2,Z:]) . x = Fn1 . x by A197, FUNCT_1:49
.= (Fn1 | [: the carrier of Y,{0}:]) . x by A195, A197, A200, A199, FUNCT_1:49
.= H . x by A183, A187, A195, A197, A200, A199, FUNCT_1:49
.= (H | [:N2,Z:]) . x by A197, A200, FUNCT_1:49 ;
::_thesis: verum
end;
take Z ; ::_thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )
thus Z = [.0,(TT . (i + 1)).] ; ::_thesis: Fn1 | [:N2,Z:] = H | [:N2,Z:]
dom (H | [:N2,Z:]) = [:N2,Z:] by A190, A189, A196, RELAT_1:62;
hence Fn1 | [:N2,Z:] = H | [:N2,Z:] by A188, A198, FUNCT_1:2, RELAT_1:62; ::_thesis: verum
end;
supposeA201: i in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )
set ZZ = [.(TT . i),(TT . (i + 1)).];
A202: 0 <= TT . i by A19, A201;
A203: TT . (i + 1) <= 1 by A19, A193, A201;
then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by A25, A202;
consider Z being non empty Subset of I[01] such that
A204: Z = [.0,(TT . i).] and
A205: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A192, A201;
take Z1 = Z \/ ZZ; ::_thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z1:] = H | [:N2,Z1:] )
A206: TT . i < TT . (i + 1) by A19, A193, A201;
hence Z1 = [.0,(TT . (i + 1)).] by A204, A202, XXREAL_1:165; ::_thesis: Fn1 | [:N2,Z1:] = H | [:N2,Z1:]
A207: [:N2,Z1:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then A208: dom (Fn1 | [:N2,Z1:]) = [:N2,Z1:] by A189, A188, RELAT_1:62;
A209: for x being set st x in dom (Fn1 | [:N2,Z1:]) holds
(Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
proof
0 <= TT . (i + 1) by A19, A193;
then A210: TT . (i + 1) is Point of I[01] by A203, BORSUK_1:43;
( 0 <= TT . i & TT . i <= 1 ) by A19, A193, A201;
then TT . i is Point of I[01] by BORSUK_1:43;
then A211: ZZ is connected by A206, A210, BORSUK_4:24;
consider Ui being non empty Subset of (Tunit_circle 2) such that
A212: Ui in UL and
A213: F .: [:N,ZZ:] c= Ui by A16, A193, A201;
consider D being mutually-disjoint open Subset-Family of R^1 such that
A214: union D = CircleMap " Ui and
A215: for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | Ui) st f = CircleMap | d holds
f is being_homeomorphism by A2, A212;
let x be set ; ::_thesis: ( x in dom (Fn1 | [:N2,Z1:]) implies (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x )
assume A216: x in dom (Fn1 | [:N2,Z1:]) ; ::_thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
consider x1, x2 being set such that
A217: x1 in N2 and
A218: x2 in Z1 and
A219: x = [x1,x2] by A208, A216, ZFMISC_1:def_2;
A220: TT . i in ZZ by A206, XXREAL_1:1;
then [x1,(TT . i)] in [:N,ZZ:] by A180, A217, ZFMISC_1:87;
then A221: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35;
reconsider xy = {x1} as non empty Subset of Y by A217, ZFMISC_1:31;
A222: xy c= N2 by A217, ZFMISC_1:31;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by A189, ZFMISC_1:96;
A223: dom (H | [:xy,ZZ:]) = [:xy,ZZ:] by A190, A189, A222, RELAT_1:62, ZFMISC_1:96;
A224: D is Cover of Fn1 .: xZZ
proof
let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in Fn1 .: xZZ or b in union D )
A225: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn1 .: xZZ ; ::_thesis: b in union D
then consider a being Point of [:(Y | N2),I[01]:] such that
A226: a in xZZ and
A227: Fn1 . a = b by FUNCT_2:65;
xy c= N by A180, A217, ZFMISC_1:31;
then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95;
then a in [:N,ZZ:] by A226;
then A228: F . a in F .: [:N,ZZ:] by A6, A225, FUNCT_1:def_6;
CircleMap . (Fn1 . a) = (CircleMap * Fn1) . a by FUNCT_2:15
.= F . a by A12, A178, A182, A189, BORSUK_1:40, FUNCT_1:49 ;
hence b in union D by A213, A214, A227, A228, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum
end;
A229: D is Cover of H .: xZZ
proof
let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in H .: xZZ or b in union D )
A230: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in H .: xZZ ; ::_thesis: b in union D
then consider a being Point of [:(Y | N2),I[01]:] such that
A231: a in xZZ and
A232: H . a = b by FUNCT_2:65;
A233: CircleMap . (H . a) = (CircleMap * H) . a by FUNCT_2:15
.= F . a by A186, A189, FUNCT_1:49 ;
xy c= N by A180, A217, ZFMISC_1:31;
then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95;
then a in [:N,ZZ:] by A231;
then F . a in F .: [:N,ZZ:] by A6, A230, FUNCT_1:def_6;
hence b in union D by A213, A214, A232, A233, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum
end;
TT . i in Z by A204, A202, XXREAL_1:1;
then A234: [x1,(TT . i)] in [:N2,Z:] by A217, ZFMISC_1:87;
then A235: Fn1 . [x1,(TT . i)] = (Fn1 | [:N2,Z:]) . [x1,(TT . i)] by FUNCT_1:49
.= H . [x1,(TT . i)] by A205, A234, FUNCT_1:49 ;
A236: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then F . [x1,(TT . i)] = (CircleMap * H) . [x1,(TT . i)] by A186, A234, FUNCT_1:49
.= CircleMap . (H . [x1,(TT . i)]) by A190, A189, A234, A236, FUNCT_1:13 ;
then H . [x1,(TT . i)] in CircleMap " Ui by A213, A221, FUNCT_2:38, TOPMETR:17;
then consider Uith being set such that
A237: H . [x1,(TT . i)] in Uith and
A238: Uith in D by A214, TARSKI:def_4;
F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by A12, A178, A182, A234, A236, BORSUK_1:40, FUNCT_1:49
.= CircleMap . (Fn1 . [x1,(TT . i)]) by A189, A188, A234, A236, FUNCT_1:13 ;
then Fn1 . [x1,(TT . i)] in CircleMap " Ui by A213, A221, FUNCT_2:38, TOPMETR:17;
then consider Uit being set such that
A239: Fn1 . [x1,(TT . i)] in Uit and
A240: Uit in D by A214, TARSKI:def_4;
I[01] is SubSpace of I[01] by TSEP_1:2;
then A241: [:(Y | N2),I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21;
xy is connected by A217;
then [:xy,ZZ:] is connected by A211, TOPALG_3:16;
then A242: xZZ is connected by A241, CONNSP_1:23;
reconsider Uith = Uith as non empty Subset of R^1 by A237, A238;
A243: x1 in xy by TARSKI:def_1;
then A244: [x1,(TT . i)] in xZZ by A220, ZFMISC_1:87;
then H . [x1,(TT . i)] in H .: xZZ by FUNCT_2:35;
then Uith meets H .: xZZ by A237, XBOOLE_0:3;
then A245: H .: xZZ c= Uith by A185, A242, A238, A229, TOPALG_3:12, TOPS_2:61;
reconsider Uit = Uit as non empty Subset of R^1 by A239, A240;
set f = CircleMap | Uit;
A246: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17;
A247: rng (CircleMap | Uit) c= Ui
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (CircleMap | Uit) or b in Ui )
assume b in rng (CircleMap | Uit) ; ::_thesis: b in Ui
then consider a being set such that
A248: a in dom (CircleMap | Uit) and
A249: (CircleMap | Uit) . a = b by FUNCT_1:def_3;
a in union D by A240, A246, A248, TARSKI:def_4;
then CircleMap . a in Ui by A214, FUNCT_2:38;
hence b in Ui by A246, A248, A249, FUNCT_1:49; ::_thesis: verum
end;
( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A246, A247, FUNCT_2:2;
A250: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A189, A188, A222, RELAT_1:62, ZFMISC_1:96;
H . [x1,(TT . i)] in H .: xZZ by A190, A244, FUNCT_1:def_6;
then Uit meets Uith by A239, A245, A235, XBOOLE_0:3;
then A251: Uit = Uith by A240, A238, TAXONOM2:def_5;
A252: rng (H | [:xy,ZZ:]) c= dom f
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (H | [:xy,ZZ:]) or b in dom f )
assume b in rng (H | [:xy,ZZ:]) ; ::_thesis: b in dom f
then consider a being set such that
A253: a in dom (H | [:xy,ZZ:]) and
A254: (H | [:xy,ZZ:]) . a = b by FUNCT_1:def_3;
H . a = b by A223, A253, A254, FUNCT_1:49;
then b in H .: xZZ by A190, A223, A253, FUNCT_1:def_6;
hence b in dom f by A245, A251, A246; ::_thesis: verum
end;
Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by A244, FUNCT_2:35;
then Uit meets Fn1 .: xZZ by A239, XBOOLE_0:3;
then A255: Fn1 .: xZZ c= Uit by A181, A184, A240, A242, A224, TOPALG_3:12, TOPS_2:61;
A256: rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f )
assume b in rng (Fn1 | [:xy,ZZ:]) ; ::_thesis: b in dom f
then consider a being set such that
A257: a in dom (Fn1 | [:xy,ZZ:]) and
A258: (Fn1 | [:xy,ZZ:]) . a = b by FUNCT_1:def_3;
Fn1 . a = b by A250, A257, A258, FUNCT_1:49;
then b in Fn1 .: xZZ by A188, A250, A257, FUNCT_1:def_6;
hence b in dom f by A255, A246; ::_thesis: verum
end;
then A259: dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27;
A260: for x being set st x in dom (f * (Fn1 | [:xy,ZZ:])) holds
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x
proof
let x be set ; ::_thesis: ( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x )
assume A261: x in dom (f * (Fn1 | [:xy,ZZ:])) ; ::_thesis: (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x
A262: Fn1 . x in Fn1 .: [:xy,ZZ:] by A188, A250, A259, A261, FUNCT_1:def_6;
A263: H . x in H .: [:xy,ZZ:] by A190, A250, A259, A261, FUNCT_1:def_6;
thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83
.= (f * Fn1) . x by A250, A259, A261, FUNCT_1:49
.= f . (Fn1 . x) by A188, A261, FUNCT_1:13
.= CircleMap . (Fn1 . x) by A255, A262, FUNCT_1:49
.= (CircleMap * Fn1) . x by A188, A261, FUNCT_1:13
.= CircleMap . (H . x) by A12, A178, A182, A186, A190, A261, BORSUK_1:40, FUNCT_1:13
.= f . (H . x) by A245, A251, A263, FUNCT_1:49
.= (f * H) . x by A190, A261, FUNCT_1:13
.= ((f * H) | [:xy,ZZ:]) . x by A250, A259, A261, FUNCT_1:49
.= (f * (H | [:xy,ZZ:])) . x by RELAT_1:83 ; ::_thesis: verum
end;
f is being_homeomorphism by A215, A240;
then A264: f is one-to-one by TOPS_2:def_5;
dom (f * (H | [:xy,ZZ:])) = dom (H | [:xy,ZZ:]) by A252, RELAT_1:27;
then A265: f * (Fn1 | [:xy,ZZ:]) = f * (H | [:xy,ZZ:]) by A250, A223, A256, A260, FUNCT_1:2, RELAT_1:27;
percases ( x2 in ZZ or not x2 in ZZ ) ;
suppose x2 in ZZ ; ::_thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
then A266: x in [:xy,ZZ:] by A219, A243, ZFMISC_1:87;
thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by A208, A216, FUNCT_1:49
.= (Fn1 | [:xy,ZZ:]) . x by A266, FUNCT_1:49
.= (H | [:xy,ZZ:]) . x by A264, A250, A223, A256, A252, A265, FUNCT_1:27
.= H . x by A266, FUNCT_1:49
.= (H | [:N2,Z1:]) . x by A208, A216, FUNCT_1:49 ; ::_thesis: verum
end;
suppose not x2 in ZZ ; ::_thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
then x2 in Z by A218, XBOOLE_0:def_3;
then A267: x in [:N2,Z:] by A217, A219, ZFMISC_1:87;
thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by A208, A216, FUNCT_1:49
.= (Fn1 | [:N2,Z:]) . x by A267, FUNCT_1:49
.= H . x by A205, A267, FUNCT_1:49
.= (H | [:N2,Z1:]) . x by A208, A216, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
dom (H | [:N2,Z1:]) = [:N2,Z1:] by A190, A189, A207, RELAT_1:62;
hence Fn1 | [:N2,Z1:] = H | [:N2,Z1:] by A188, A209, FUNCT_1:2, RELAT_1:62; ::_thesis: verum
end;
end;
end;
A268: S3[ 0 ] by FINSEQ_3:24;
for i being Element of NAT holds S3[i] from NAT_1:sch_1(A268, A191);
then consider Z being non empty Subset of I[01] such that
A269: Z = [.0,(TT . (len TT)).] and
A270: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A17;
thus Fn1 = Fn1 | [:N2,Z:] by A12, A189, A188, A269, BORSUK_1:40, RELAT_1:69
.= H by A12, A190, A189, A269, A270, BORSUK_1:40, RELAT_1:69 ; ::_thesis: verum
end;
consider G being Function of [:Y,I[01]:],R^1 such that
A271: for x being Point of [:Y,I[01]:] holds S1[x,G . x] from FUNCT_2:sch_3(A9);
take G ; ::_thesis: ( 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 ) )
A272: now__::_thesis:_for_N_being_Subset_of_Y
for_F_being_Function_of_[:(Y_|_N),I[01]:],R^1_holds_dom_F_=_[:N,_the_carrier_of_I[01]:]
let N be Subset of Y; ::_thesis: for F being Function of [:(Y | N),I[01]:],R^1 holds dom F = [:N, the carrier of I[01]:]
let F be Function of [:(Y | N),I[01]:],R^1; ::_thesis: dom F = [:N, the carrier of I[01]:]
thus dom F = the carrier of [:(Y | N),I[01]:] by FUNCT_2:def_1
.= [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2
.= [:N, the carrier of I[01]:] by PRE_TOPC:8 ; ::_thesis: verum
end;
A273: for p being Point of [:Y,I[01]:]
for y being Point of Y
for t being Point of I[01]
for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
proof
let p be Point of [:Y,I[01]:]; ::_thesis: for y being Point of Y
for t being Point of I[01]
for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
let y be Point of Y; ::_thesis: for t being Point of I[01]
for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
let t be Point of I[01]; ::_thesis: for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
let N1, N2 be non empty open Subset of Y; ::_thesis: for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
let Fn1 be Function of [:(Y | N1),I[01]:],R^1; ::_thesis: for 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, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
let Fn2 be Function of [:(Y | N2),I[01]:],R^1; ::_thesis: ( p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] implies Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] )
assume that
p = [y,t] and
A274: y in N1 and
A275: y in N2 and
A276: Fn2 is continuous and
A277: Fn1 is continuous and
A278: F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 and
A279: Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] and
A280: F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 and
A281: Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] ; ::_thesis: Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
A282: {y} c= N1 by A274, ZFMISC_1:31;
consider TT being non empty FinSequence of REAL such that
A283: TT . 1 = 0 and
A284: TT . (len TT) = 1 and
A285: TT is increasing and
A286: 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 holds
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
A287: y in N and
A288: for i being Nat st i in dom TT & i + 1 in dom TT holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui ) by A286;
reconsider N = N as non empty open Subset of Y by A287;
defpred S2[ Element of 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:] ) );
A289: len TT in dom TT by FINSEQ_5:6;
A290: dom Fn2 = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def_1;
A291: dom Fn2 = [:N2, the carrier of I[01]:] by A272;
A292: {y} c= N2 by A275, ZFMISC_1:31;
A293: ( the carrier of [:(Y | N1),I[01]:] = [: the carrier of (Y | N1), the carrier of I[01]:] & the carrier of (Y | N1) = N1 ) by BORSUK_1:def_2, PRE_TOPC:8;
A294: ( the carrier of [:(Y | N2),I[01]:] = [: the carrier of (Y | N2), the carrier of I[01]:] & the carrier of (Y | N2) = N2 ) by BORSUK_1:def_2, PRE_TOPC:8;
A295: dom Fn1 = [:N1, the carrier of I[01]:] by A272;
A296: dom Fn1 = the carrier of [:(Y | N1),I[01]:] by FUNCT_2:def_1;
A297: 1 in dom TT by FINSEQ_5:6;
A298: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume that
A299: S2[i] and
A300: i + 1 in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )
percases ( i = 0 or i in dom TT ) by A300, TOPREALA:2;
supposeA301: i = 0 ; ::_thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )
set Z = [.0,(TT . (i + 1)).];
A302: [.0,(TT . (i + 1)).] = {0} by A283, A301, XXREAL_1:17;
reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A283, A301, Lm3, XXREAL_1:17;
A303: [:{y},Z:] c= [:N2, the carrier of I[01]:] by A292, ZFMISC_1:96;
A304: dom (Fn1 | [:{y},Z:]) = [:{y},Z:] by A282, A295, RELAT_1:62, ZFMISC_1:96;
A305: [:{y},Z:] c= [:N1, the carrier of I[01]:] by A282, ZFMISC_1:96;
A306: for x being set st x in dom (Fn1 | [:{y},Z:]) holds
(Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x
proof
let x be set ; ::_thesis: ( x in dom (Fn1 | [:{y},Z:]) implies (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x )
A307: [:{y},Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95;
assume A308: x in dom (Fn1 | [:{y},Z:]) ; ::_thesis: (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x
hence (Fn1 | [:{y},Z:]) . x = Fn1 . x by A304, FUNCT_1:49
.= (Fn1 | [: the carrier of Y,{0}:]) . x by A302, A304, A308, A307, FUNCT_1:49
.= Ft . x by A281, A305, A304, A308, FUNCT_1:49
.= (Ft | [:N2, the carrier of I[01]:]) . x by A304, A303, A308, FUNCT_1:49
.= Fn2 . x by A279, A302, A304, A308, A307, FUNCT_1:49
.= (Fn2 | [:{y},Z:]) . x by A304, A308, FUNCT_1:49 ;
::_thesis: verum
end;
take Z ; ::_thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )
thus Z = [.0,(TT . (i + 1)).] ; ::_thesis: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]
dom (Fn2 | [:{y},Z:]) = [:{y},Z:] by A292, A291, RELAT_1:62, ZFMISC_1:96;
hence Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A304, A306, FUNCT_1:2; ::_thesis: verum
end;
supposeA309: i in dom TT ; ::_thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )
A310: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_TT_holds_
(_0_<=_TT_._i_&_(_i_+_1_in_dom_TT_implies_(_TT_._i_<_TT_._(i_+_1)_&_TT_._(i_+_1)_<=_1_&_TT_._i_<_1_&_0_<_TT_._(i_+_1)_)_)_)
let i be Element of NAT ; ::_thesis: ( i in dom TT implies ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) )
assume A311: i in dom TT ; ::_thesis: ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) )
1 <= i by A311, FINSEQ_3:25;
then ( 1 = i or 1 < i ) by XXREAL_0:1;
hence A312: 0 <= TT . i by A283, A285, A297, A311, SEQM_3:def_1; ::_thesis: ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) )
assume A313: i + 1 in dom TT ; ::_thesis: ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
A314: i + 0 < i + 1 by XREAL_1:8;
hence A315: TT . i < TT . (i + 1) by A285, A311, A313, SEQM_3:def_1; ::_thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
i + 1 <= len TT by A313, FINSEQ_3:25;
then ( i + 1 = len TT or i + 1 < len TT ) by XXREAL_0:1;
hence TT . (i + 1) <= 1 by A284, A285, A289, A313, SEQM_3:def_1; ::_thesis: ( TT . i < 1 & 0 < TT . (i + 1) )
hence TT . i < 1 by A315, XXREAL_0:2; ::_thesis: 0 < TT . (i + 1)
thus 0 < TT . (i + 1) by A285, A311, A312, A313, A314, SEQM_3:def_1; ::_thesis: verum
end;
then A316: 0 <= TT . i by A309;
A317: TT . (i + 1) <= 1 by A300, A309, A310;
set ZZ = [.(TT . i),(TT . (i + 1)).];
consider Z being non empty Subset of I[01] such that
A318: Z = [.0,(TT . i).] and
A319: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A299, A309;
now__::_thesis:_for_i_being_Element_of_NAT_st_0_<=_TT_._i_&_TT_._(i_+_1)_<=_1_holds_
[.(TT_._i),(TT_._(i_+_1)).]_c=_the_carrier_of_I[01]
let i be Element of NAT ; ::_thesis: ( 0 <= TT . i & TT . (i + 1) <= 1 implies [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] )
assume that
A320: 0 <= TT . i and
A321: TT . (i + 1) <= 1 ; ::_thesis: [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01]
thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [.(TT . i),(TT . (i + 1)).] or a in the carrier of I[01] )
assume A322: a in [.(TT . i),(TT . (i + 1)).] ; ::_thesis: a in the carrier of I[01]
then reconsider a = a as Real ;
a <= TT . (i + 1) by A322, XXREAL_1:1;
then A323: a <= 1 by A321, XXREAL_0:2;
0 <= a by A320, A322, XXREAL_1:1;
hence a in the carrier of I[01] by A323, BORSUK_1:43; ::_thesis: verum
end;
end;
then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by A316, A317;
take Z1 = Z \/ ZZ; ::_thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] )
A324: TT . i < TT . (i + 1) by A300, A309, A310;
hence Z1 = [.0,(TT . (i + 1)).] by A318, A316, XXREAL_1:165; ::_thesis: Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:]
A325: dom (Fn1 | [:{y},Z1:]) = [:{y},Z1:] by A282, A295, RELAT_1:62, ZFMISC_1:96;
A326: for x being set st x in dom (Fn1 | [:{y},Z1:]) holds
(Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
proof
0 <= TT . (i + 1) by A300, A310;
then A327: TT . (i + 1) is Point of I[01] by A317, BORSUK_1:43;
( 0 <= TT . i & TT . i <= 1 ) by A300, A309, A310;
then TT . i is Point of I[01] by BORSUK_1:43;
then A328: ZZ is connected by A324, A327, BORSUK_4:24;
A329: TT . i in ZZ by A324, XXREAL_1:1;
consider Ui being non empty Subset of (Tunit_circle 2) such that
A330: Ui in UL and
A331: F .: [:N,ZZ:] c= Ui by A288, A300, A309;
consider D being mutually-disjoint open Subset-Family of R^1 such that
A332: union D = CircleMap " Ui and
A333: for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | Ui) st f = CircleMap | d holds
f is being_homeomorphism by A2, A330;
let x be set ; ::_thesis: ( x in dom (Fn1 | [:{y},Z1:]) implies (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x )
assume A334: x in dom (Fn1 | [:{y},Z1:]) ; ::_thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
consider x1, x2 being set such that
A335: x1 in {y} and
A336: x2 in Z1 and
A337: x = [x1,x2] by A325, A334, ZFMISC_1:def_2;
reconsider xy = {x1} as non empty Subset of Y by A335, ZFMISC_1:31;
A338: xy c= N2 by A292, A335, ZFMISC_1:31;
then A339: [:xy,ZZ:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:96;
A340: x1 = y by A335, TARSKI:def_1;
then [x1,(TT . i)] in [:N,ZZ:] by A287, A329, ZFMISC_1:87;
then A341: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35;
A342: xy c= N1 by A282, A335, ZFMISC_1:31;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N1),I[01]:] by A293, ZFMISC_1:96;
xy is connected by A335;
then A343: [:xy,ZZ:] is connected by A328, TOPALG_3:16;
A344: xy c= N by A287, A340, ZFMISC_1:31;
A345: D is Cover of Fn1 .: xZZ
proof
let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in Fn1 .: xZZ or b in union D )
A346: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn1 .: xZZ ; ::_thesis: b in union D
then consider a being Point of [:(Y | N1),I[01]:] such that
A347: a in xZZ and
A348: Fn1 . a = b by FUNCT_2:65;
A349: CircleMap . (Fn1 . a) = (CircleMap * Fn1) . a by FUNCT_2:15
.= F . a by A280, A293, FUNCT_1:49 ;
[:xy,ZZ:] c= [:N,ZZ:] by A344, ZFMISC_1:95;
then a in [:N,ZZ:] by A347;
then F . a in F .: [:N,ZZ:] by A6, A346, FUNCT_1:def_6;
hence b in union D by A331, A332, A348, A349, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum
end;
A350: 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 A351: xZZ is connected by A343, CONNSP_1:23;
reconsider XZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by A294, A338, ZFMISC_1:96;
[:(Y | N2),I[01]:] is SubSpace of [:Y,I[01]:] by A350, BORSUK_3:21;
then A352: XZZ is connected by A343, CONNSP_1:23;
A353: D is Cover of Fn2 .: xZZ
proof
let b be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not b in Fn2 .: xZZ or b in union D )
A354: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn2 .: xZZ ; ::_thesis: b in union D
then consider a being Point of [:(Y | N2),I[01]:] such that
A355: a in xZZ and
A356: Fn2 . a = b by FUNCT_2:65;
A357: CircleMap . (Fn2 . a) = (CircleMap * Fn2) . a by FUNCT_2:15
.= F . a by A278, A294, FUNCT_1:49 ;
[:xy,ZZ:] c= [:N,ZZ:] by A344, ZFMISC_1:95;
then a in [:N,ZZ:] by A355;
then F . a in F .: [:N,ZZ:] by A6, A354, FUNCT_1:def_6;
hence b in union D by A331, A332, A356, A357, Lm12, FUNCT_1:def_7, TOPMETR:17; ::_thesis: verum
end;
A358: TT . i in Z by A318, A316, XXREAL_1:1;
then A359: [x1,(TT . i)] in [:{y},Z:] by A335, ZFMISC_1:87;
A360: [:{y},Z:] c= [:N1, the carrier of I[01]:] by A282, ZFMISC_1:96;
then F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by A280, A359, FUNCT_1:49
.= CircleMap . (Fn1 . [x1,(TT . i)]) by A295, A359, A360, FUNCT_1:13 ;
then Fn1 . [x1,(TT . i)] in CircleMap " Ui by A331, A341, FUNCT_2:38, TOPMETR:17;
then consider Uit being set such that
A361: Fn1 . [x1,(TT . i)] in Uit and
A362: Uit in D by A332, TARSKI:def_4;
reconsider Uit = Uit as non empty Subset of R^1 by A361, A362;
set f = CircleMap | Uit;
A363: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17;
A364: rng (CircleMap | Uit) c= Ui
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (CircleMap | Uit) or b in Ui )
assume b in rng (CircleMap | Uit) ; ::_thesis: b in Ui
then consider a being set such that
A365: a in dom (CircleMap | Uit) and
A366: (CircleMap | Uit) . a = b by FUNCT_1:def_3;
a in union D by A362, A363, A365, TARSKI:def_4;
then CircleMap . a in Ui by A332, FUNCT_2:38;
hence b in Ui by A363, A365, A366, FUNCT_1:49; ::_thesis: verum
end;
( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A363, A364, FUNCT_2:2;
A367: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
A368: [x1,(TT . i)] in [:N2,Z:] by A292, A335, A358, ZFMISC_1:87;
then F . [x1,(TT . i)] = (CircleMap * Fn2) . [x1,(TT . i)] by A278, A367, FUNCT_1:49
.= CircleMap . (Fn2 . [x1,(TT . i)]) by A290, A294, A368, A367, FUNCT_1:13 ;
then Fn2 . [x1,(TT . i)] in CircleMap " Ui by A331, A341, FUNCT_2:38, TOPMETR:17;
then consider Uith being set such that
A369: Fn2 . [x1,(TT . i)] in Uith and
A370: Uith in D by A332, TARSKI:def_4;
reconsider Uith = Uith as non empty Subset of R^1 by A369, A370;
A371: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A293, A296, A342, RELAT_1:62, ZFMISC_1:96;
A372: x1 in xy by TARSKI:def_1;
then A373: [x1,(TT . i)] in xZZ by A329, ZFMISC_1:87;
then Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by FUNCT_2:35;
then Uit meets Fn1 .: xZZ by A361, XBOOLE_0:3;
then A374: Fn1 .: xZZ c= Uit by A277, A362, A351, A345, TOPALG_3:12, TOPS_2:61;
A375: rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f )
assume b in rng (Fn1 | [:xy,ZZ:]) ; ::_thesis: b in dom f
then consider a being set such that
A376: a in dom (Fn1 | [:xy,ZZ:]) and
A377: (Fn1 | [:xy,ZZ:]) . a = b by FUNCT_1:def_3;
Fn1 . a = b by A371, A376, A377, FUNCT_1:49;
then b in Fn1 .: xZZ by A296, A371, A376, FUNCT_1:def_6;
hence b in dom f by A374, A363; ::_thesis: verum
end;
then A378: dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27;
[x1,(TT . i)] in [:xy,ZZ:] by A335, A340, A329, ZFMISC_1:87;
then [x1,(TT . i)] in dom Fn2 by A291, A339;
then A379: Fn2 . [x1,(TT . i)] in Fn2 .: xZZ by A373, FUNCT_2:35;
then Uith meets Fn2 .: xZZ by A369, XBOOLE_0:3;
then A380: Fn2 .: xZZ c= Uith by A276, A370, A352, A353, TOPALG_3:12, TOPS_2:61;
Fn1 . [x1,(TT . i)] = (Fn1 | [:{y},Z:]) . [x1,(TT . i)] by A359, FUNCT_1:49
.= Fn2 . [x1,(TT . i)] by A319, A359, FUNCT_1:49 ;
then Uit meets Uith by A361, A379, A380, XBOOLE_0:3;
then A381: Uit = Uith by A362, A370, TAXONOM2:def_5;
A382: for x being set st x in dom (f * (Fn1 | [:xy,ZZ:])) holds
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x
proof
A383: dom (Fn1 | [:xy,ZZ:]) c= dom Fn1 by RELAT_1:60;
let x be set ; ::_thesis: ( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x )
assume A384: x in dom (f * (Fn1 | [:xy,ZZ:])) ; ::_thesis: (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x
A385: Fn1 . x in Fn1 .: [:xy,ZZ:] by A296, A371, A378, A384, FUNCT_1:def_6;
A386: Fn2 . x in Fn2 .: [:xy,ZZ:] by A291, A339, A371, A378, A384, FUNCT_1:def_6;
dom (Fn1 | [:xy,ZZ:]) = (dom Fn1) /\ [:xy,ZZ:] by RELAT_1:61;
then A387: x in [:xy,ZZ:] by A378, A384, XBOOLE_0:def_4;
thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83
.= (f * Fn1) . x by A371, A378, A384, FUNCT_1:49
.= f . (Fn1 . x) by A296, A384, FUNCT_1:13
.= CircleMap . (Fn1 . x) by A374, A385, FUNCT_1:49
.= (CircleMap * Fn1) . x by A296, A384, FUNCT_1:13
.= F . x by A280, A295, A378, A384, A383, FUNCT_1:49
.= (CircleMap * Fn2) . x by A278, A339, A387, FUNCT_1:49
.= CircleMap . (Fn2 . x) by A291, A339, A387, FUNCT_1:13
.= f . (Fn2 . x) by A380, A381, A386, FUNCT_1:49
.= (f * Fn2) . x by A291, A339, A387, FUNCT_1:13
.= ((f * Fn2) | [:xy,ZZ:]) . x by A371, A378, A384, FUNCT_1:49
.= (f * (Fn2 | [:xy,ZZ:])) . x by RELAT_1:83 ; ::_thesis: verum
end;
A388: dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:] by A290, A294, A338, RELAT_1:62, ZFMISC_1:96;
A389: rng (Fn2 | [:xy,ZZ:]) c= dom f
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (Fn2 | [:xy,ZZ:]) or b in dom f )
assume b in rng (Fn2 | [:xy,ZZ:]) ; ::_thesis: b in dom f
then consider a being set such that
A390: a in dom (Fn2 | [:xy,ZZ:]) and
A391: (Fn2 | [:xy,ZZ:]) . a = b by FUNCT_1:def_3;
Fn2 . a = b by A388, A390, A391, FUNCT_1:49;
then b in Fn2 .: xZZ by A290, A388, A390, FUNCT_1:def_6;
hence b in dom f by A380, A381, A363; ::_thesis: verum
end;
then dom (f * (Fn2 | [:xy,ZZ:])) = dom (Fn2 | [:xy,ZZ:]) by RELAT_1:27;
then A392: f * (Fn1 | [:xy,ZZ:]) = f * (Fn2 | [:xy,ZZ:]) by A371, A388, A375, A382, FUNCT_1:2, RELAT_1:27;
f is being_homeomorphism by A333, A362;
then A393: f is one-to-one by TOPS_2:def_5;
percases ( x2 in ZZ or not x2 in ZZ ) ;
suppose x2 in ZZ ; ::_thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
then A394: x in [:xy,ZZ:] by A337, A372, ZFMISC_1:87;
thus (Fn1 | [:{y},Z1:]) . x = Fn1 . x by A325, A334, FUNCT_1:49
.= (Fn1 | [:xy,ZZ:]) . x by A394, FUNCT_1:49
.= (Fn2 | [:xy,ZZ:]) . x by A393, A371, A388, A375, A389, A392, FUNCT_1:27
.= Fn2 . x by A394, FUNCT_1:49
.= (Fn2 | [:{y},Z1:]) . x by A325, A334, FUNCT_1:49 ; ::_thesis: verum
end;
suppose not x2 in ZZ ; ::_thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
then x2 in Z by A336, XBOOLE_0:def_3;
then A395: x in [:{y},Z:] by A335, A337, ZFMISC_1:87;
thus (Fn1 | [:{y},Z1:]) . x = Fn1 . x by A325, A334, FUNCT_1:49
.= (Fn1 | [:{y},Z:]) . x by A395, FUNCT_1:49
.= Fn2 . x by A319, A395, FUNCT_1:49
.= (Fn2 | [:{y},Z1:]) . x by A325, A334, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
dom (Fn2 | [:{y},Z1:]) = [:{y},Z1:] by A292, A290, A294, RELAT_1:62, ZFMISC_1:96;
hence Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] by A325, A326, FUNCT_1:2; ::_thesis: verum
end;
end;
end;
A396: S2[ 0 ] by FINSEQ_3:24;
for i being Element of NAT holds S2[i] from NAT_1:sch_1(A396, A298);
then ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (len TT)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) by A289;
hence Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] by A284, BORSUK_1:40; ::_thesis: verum
end;
for p being Point of [:Y,I[01]:]
for 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]:]; ::_thesis: for 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 )
let V be Subset of R^1; ::_thesis: ( G . p in V & V is open implies ex W being Subset of [:Y,I[01]:] st
( p in W & W is open & G .: W c= V ) )
assume A397: ( G . p in V & V is open ) ; ::_thesis: ex W being Subset of [:Y,I[01]:] st
( p in W & W is open & G .: W c= V )
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
A398: p = [y,t] and
A399: G . p = Fn . p and
A400: y in N and
A401: Fn is continuous and
A402: ( F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] ) and
for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H by A271;
A403: the carrier of [:(Y | N),I[01]:] = [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2
.= [:N, the carrier of I[01]:] by PRE_TOPC:8 ;
then p in the carrier of [:(Y | N),I[01]:] by A398, A400, ZFMISC_1:87;
then consider W being Subset of [:(Y | N),I[01]:] such that
A404: p in W and
A405: W is open and
A406: Fn .: W c= V by A397, A399, A401, JGRAPH_2:10;
A407: dom Fn = [:N, the carrier of I[01]:] by A403, FUNCT_2:def_1;
A408: [#] (Y | N) = N by PRE_TOPC:def_5;
then A409: [#] [:(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
A410: C is open and
A411: C /\ ([#] [:(Y | N),I[01]:]) = W by A405, TOPS_2:24;
take WW = C /\ [:N,([#] I[01]):]; ::_thesis: ( p in WW & WW is open & G .: WW c= V )
thus p in WW by A404, A411, A408, BORSUK_3:1; ::_thesis: ( WW is open & G .: WW c= V )
[:N,([#] I[01]):] is open by BORSUK_1:6;
hence WW is open by A410; ::_thesis: G .: WW c= V
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G .: WW or y in V )
assume y in G .: WW ; ::_thesis: y in V
then consider x being Point of [:Y,I[01]:] such that
A412: x in WW and
A413: 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
A414: x = [y0,t0] and
A415: G . x = Fn0 . x and
A416: ( y0 in N0 & Fn0 is continuous & F | [:N0, the carrier of I[01]:] = CircleMap * Fn0 & Fn0 | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] ) and
for H being Function of [:(Y | N0),I[01]:],R^1 st H is continuous & F | [:N0, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] holds
Fn0 = H by A271;
x in [:N,([#] I[01]):] by A412, XBOOLE_0:def_4;
then A417: y0 in N by A414, ZFMISC_1:87;
A418: x in [:{y0}, the carrier of I[01]:] by A414, ZFMISC_1:105;
then Fn . x = (Fn | [:{y0}, the carrier of I[01]:]) . x by FUNCT_1:49
.= (Fn0 | [:{y0}, the carrier of I[01]:]) . x by A273, A401, A402, A414, A416, A417
.= Fn0 . x by A418, FUNCT_1:49 ;
then y in Fn .: W by A407, A411, A409, A412, A413, A415, FUNCT_1:def_6;
hence y in V by A406; ::_thesis: verum
end;
hence G is continuous by JGRAPH_2:10; ::_thesis: ( 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 ) )
for x being Point of [:Y,I[01]:] holds F . x = (CircleMap * G) . x
proof
let x be Point of [:Y,I[01]:]; ::_thesis: F . x = (CircleMap * G) . x
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
A419: x = [y,t] and
A420: G . x = Fn . x and
A421: y in N and
Fn is continuous and
A422: F | [:N, the carrier of I[01]:] = CircleMap * Fn and
Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] and
for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H by A271;
A423: the carrier of [:(Y | N),I[01]:] = [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2
.= [:N, the carrier of I[01]:] by PRE_TOPC:8 ;
then A424: x in the carrier of [:(Y | N),I[01]:] by A419, A421, ZFMISC_1:87;
thus (CircleMap * G) . x = CircleMap . (G . x) by FUNCT_2:15
.= (CircleMap * Fn) . x by A420, A424, FUNCT_2:15
.= F . x by A422, A423, A424, FUNCT_1:49 ; ::_thesis: verum
end;
hence F = CircleMap * G by FUNCT_2:63; ::_thesis: ( 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 ) )
A425: [: the carrier of Y,{0}:] c= [: the carrier of Y, the carrier of I[01]:] by Lm3, ZFMISC_1:95;
A426: the carrier of [:Y,I[01]:] = [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def_2;
then A427: dom G = [: the carrier of Y, the carrier of I[01]:] by FUNCT_2:def_1;
A428: for x being set st x in dom Ft holds
Ft . x = G . x
proof
let x be set ; ::_thesis: ( x in dom Ft implies Ft . x = G . x )
assume A429: x in dom Ft ; ::_thesis: Ft . x = G . x
then x in dom G by A8, A427, A425;
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
A430: x = [y,t] and
A431: G . x = Fn . x and
A432: y in N and
Fn is continuous and
F | [:N, the carrier of I[01]:] = CircleMap * Fn and
A433: Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] and
for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H by A271;
x in [:N, the carrier of I[01]:] by A430, A432, ZFMISC_1:87;
hence Ft . x = (Ft | [:N, the carrier of I[01]:]) . x by FUNCT_1:49
.= G . x by A7, A429, A431, A433, Lm14, FUNCT_1:49 ;
::_thesis: verum
end;
dom Ft = (dom G) /\ [: the carrier of Y,{0}:] by A8, A427, A425, XBOOLE_1:28;
hence G | [: the carrier of Y,{0}:] = Ft by A428, FUNCT_1:46; ::_thesis: 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
let H be Function of [:Y,I[01]:],R^1; ::_thesis: ( H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft implies G = H )
assume that
A434: ( H is continuous & F = CircleMap * H ) and
A435: H | [: the carrier of Y,{0}:] = Ft ; ::_thesis: G = H
for x being Point of [:Y,I[01]:] holds G . x = H . x
proof
let x be Point of [:Y,I[01]:]; ::_thesis: G . x = H . x
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
A436: x = [y,t] and
A437: G . x = Fn . x and
A438: y in N and
Fn is continuous and
F | [:N, the carrier of I[01]:] = CircleMap * Fn and
Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] and
A439: for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H by A271;
A440: the carrier of [:(Y | N),I[01]:] = [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def_2
.= [:N, the carrier of I[01]:] by PRE_TOPC:8 ;
then A441: x in the carrier of [:(Y | N),I[01]:] by A436, A438, ZFMISC_1:87;
dom H = the carrier of [:Y,I[01]:] by FUNCT_2:def_1;
then [:N, the carrier of I[01]:] c= dom H by A426, ZFMISC_1:95;
then A442: dom (H | [:N, the carrier of I[01]:]) = [:N, the carrier of I[01]:] by RELAT_1:62;
rng (H | [:N, the carrier of I[01]:]) c= the carrier of R^1 ;
then reconsider H1 = H | [:N, the carrier of I[01]:] as Function of [:(Y | N),I[01]:],R^1 by A440, A442, FUNCT_2:2;
A443: (H | [:N, the carrier of I[01]:]) | [: the carrier of Y,{0}:] = H | ([: the carrier of Y,{0}:] /\ [:N, the carrier of I[01]:]) by RELAT_1:71
.= Ft | [:N, the carrier of I[01]:] by A435, RELAT_1:71 ;
( H1 is continuous & F | [:N, the carrier of I[01]:] = CircleMap * (H | [:N, the carrier of I[01]:]) ) by A434, RELAT_1:83, TOPALG_3:17;
hence G . x = (H | [:N, the carrier of I[01]:]) . x by A437, A439, A443
.= H . x by A440, A441, FUNCT_1:49 ;
::_thesis: verum
end;
hence G = H by FUNCT_2:63; ::_thesis: verum
end;
theorem Th23: :: TOPALG_5:23
for x0, y0 being Point of (Tunit_circle 2)
for xt being Point of R^1
for f being Path of x0,y0 st xt in CircleMap " {x0} holds
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 (Tunit_circle 2); ::_thesis: for xt being Point of R^1
for f being Path of x0,y0 st xt in CircleMap " {x0} holds
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 ) )
let xt be Point of R^1; ::_thesis: for f being Path of x0,y0 st xt in CircleMap " {x0} holds
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 ) )
let f be Path of x0,y0; ::_thesis: ( xt in CircleMap " {x0} implies 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 ) ) )
deffunc H1( set , Element of the carrier of I[01]) -> Element of the carrier of (Tunit_circle 2) = f . $2;
consider F being Function of [: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of (Tunit_circle 2) such that
A1: for y being Element of (1TopSp {1})
for i being Element of the carrier of I[01] holds F . (y,i) = H1(y,i) from BINOP_1:sch_4();
reconsider j = 1 as Point of (1TopSp {1}) by TARSKI:def_1;
A2: [j,j0] in [: the carrier of (1TopSp {1}),{0}:] by Lm4, ZFMISC_1:87;
A3: the carrier of [:(1TopSp {1}),I[01]:] = [: the carrier of (1TopSp {1}), the carrier of I[01]:] by BORSUK_1:def_2;
then reconsider F = F as Function of [:(1TopSp {1}),I[01]:],(Tunit_circle 2) ;
set Ft = [:(1TopSp {1}),(Sspace 0[01]):] --> xt;
A4: the carrier of [:(1TopSp {1}),(Sspace 0[01]):] = [: the carrier of (1TopSp {1}), the carrier of (Sspace 0[01]):] by BORSUK_1:def_2;
then A5: for y being Element of (1TopSp {1})
for i being Element of {0} holds ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [y,i] = xt by Lm14, FUNCOP_1:7;
A6: [#] (1TopSp {1}) = the carrier of (1TopSp {1}) ;
for p being Point of [:(1TopSp {1}),I[01]:]
for V being Subset of (Tunit_circle 2) st F . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V )
proof
let p be Point of [:(1TopSp {1}),I[01]:]; ::_thesis: for V being Subset of (Tunit_circle 2) st F . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V )
let V be Subset of (Tunit_circle 2); ::_thesis: ( F . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V ) )
assume A7: ( F . p in V & V is open ) ; ::_thesis: ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V )
consider p1 being Point of (1TopSp {1}), 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:];
[:{1},S:] c= [: the carrier of (1TopSp {1}), the carrier of I[01]:] by ZFMISC_1:95;
then reconsider W = [:{1},S:] as Subset of [:(1TopSp {1}),I[01]:] by BORSUK_1:def_2;
take W ; ::_thesis: ( p in W & W is open & F .: W c= V )
thus p in W by A8, A9, ZFMISC_1:87; ::_thesis: ( W is open & F .: W c= V )
thus W is open by A6, A10, BORSUK_1:6; ::_thesis: F .: W c= V
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F .: W or y in V )
assume y in F .: W ; ::_thesis: y in V
then consider x being set such that
A12: x in the carrier of [:(1TopSp {1}),I[01]:] and
A13: x in W and
A14: y = F . x by FUNCT_2:64;
consider x1 being Point of (1TopSp {1}), 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 y in V by A11, A16; ::_thesis: verum
end;
then A17: F is continuous by JGRAPH_2:10;
assume xt in CircleMap " {x0} ; ::_thesis: 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 ) )
then A18: CircleMap . xt in {x0} by FUNCT_2:38;
A19: for x being set st x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) holds
(F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x
proof
let x be set ; ::_thesis: ( x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) implies (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x )
assume A20: x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) ; ::_thesis: (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x
consider x1, x2 being set such that
A21: x1 in the carrier of (1TopSp {1}) 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 (1TopSp {1}),{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 . (([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x) by A5, A21, A22, A23
.= (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x by A20, FUNCT_1:12 ; ::_thesis: verum
end;
A25: dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) = [: the carrier of (1TopSp {1}),{0}:] by A4, Lm14, FUNCT_2:def_1;
A26: dom F = the carrier of [:(1TopSp {1}),I[01]:] by FUNCT_2:def_1;
then A27: [: the carrier of (1TopSp {1}),{0}:] c= dom F by A3, Lm3, ZFMISC_1:95;
then dom (F | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:] by RELAT_1:62;
then consider G being Function of [:(1TopSp {1}),I[01]:],R^1 such that
A28: G is continuous and
A29: F = CircleMap * G and
A30: G | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt and
A31: for H being Function of [:(1TopSp {1}),I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt holds
G = H by A17, A25, A19, Th22, FUNCT_1:2;
take ft = Prj2 (j,G); ::_thesis: ( 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 ) )
thus ft . 0 = G . (j,j0) by Def3
.= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [j,j0] by A30, A2, FUNCT_1:49
.= xt by A5, Lm4 ; ::_thesis: ( 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 ) )
for i being Point of I[01] holds f . i = (CircleMap * ft) . i
proof
let i be Point of I[01]; ::_thesis: f . i = (CircleMap * ft) . i
A32: the carrier of [:(1TopSp {1}),I[01]:] = [: the carrier of (1TopSp {1}), 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 ; ::_thesis: verum
end;
hence f = CircleMap * ft by FUNCT_2:63; ::_thesis: ( 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 ) )
thus ft is continuous by A28; ::_thesis: for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1
let f1 be Function of I[01],R^1; ::_thesis: ( f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt implies ft = f1 )
deffunc H2( set , Element of the carrier of I[01]) -> Element of the carrier of R^1 = f1 . $2;
consider H being Function of [: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of R^1 such that
A33: for y being Element of (1TopSp {1})
for i being Element of the carrier of I[01] holds H . (y,i) = H2(y,i) from BINOP_1:sch_4();
reconsider H = H as Function of [:(1TopSp {1}),I[01]:],R^1 by A3;
assume that
A34: f1 is continuous and
A35: f = CircleMap * f1 and
A36: f1 . 0 = xt ; ::_thesis: ft = f1
for p being Point of [:(1TopSp {1}),I[01]:]
for V being Subset of R^1 st H . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V )
proof
let p be Point of [:(1TopSp {1}),I[01]:]; ::_thesis: for V being Subset of R^1 st H . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V )
let V be Subset of R^1; ::_thesis: ( H . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V ) )
assume A37: ( H . p in V & V is open ) ; ::_thesis: ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V )
consider p1 being Point of (1TopSp {1}), 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 = [:([#] (1TopSp {1})),W:]; ::_thesis: ( p in W1 & W1 is open & H .: W1 c= V )
thus p in W1 by A38, A39, ZFMISC_1:87; ::_thesis: ( W1 is open & H .: W1 c= V )
thus W1 is open by A40, BORSUK_1:6; ::_thesis: H .: W1 c= V
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in H .: W1 or y in V )
assume y in H .: W1 ; ::_thesis: y in V
then consider c being Element of [:(1TopSp {1}),I[01]:] such that
A42: c in W1 and
A43: y = H . c by FUNCT_2:65;
consider c1, c2 being set such that
A44: c1 in [#] (1TopSp {1}) 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 y in V by A41, A43, A47; ::_thesis: verum
end;
then A48: H is continuous by JGRAPH_2:10;
for x being Point of [:(1TopSp {1}),I[01]:] holds F . x = (CircleMap * H) . x
proof
let x be Point of [:(1TopSp {1}),I[01]:]; ::_thesis: F . x = (CircleMap * H) . x
consider x1 being Point of (1TopSp {1}), 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 ; ::_thesis: verum
end;
then A50: F = CircleMap * H by FUNCT_2:63;
for i being Point of I[01] holds ft . i = f1 . i
proof
let i be Point of I[01]; ::_thesis: ft . i = f1 . i
A51: dom H = the carrier of [:(1TopSp {1}),I[01]:] by FUNCT_2:def_1;
then A52: dom (H | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:] by A26, A27, RELAT_1:62;
A53: for x being set st x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) holds
(H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x
proof
let x be set ; ::_thesis: ( x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) implies (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x )
assume A54: x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) ; ::_thesis: (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x
then consider x1, x2 being set such that
A55: x1 in the carrier of (1TopSp {1}) 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 (1TopSp {1}),{0}:]) . x = H . (x1,x2) by A54, A57, FUNCT_1:47
.= f1 . x2 by A33, A55, A58
.= ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x by A5, A36, A55, A56, A57, A58 ; ::_thesis: verum
end;
dom ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) = [: the carrier of (1TopSp {1}),{0}:] by A4, Lm14, FUNCT_2:def_1;
then A59: H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt by A26, A27, A51, A53, FUNCT_1:2, RELAT_1:62;
thus ft . i = G . (j,i) by Def3
.= H . (j,i) by A31, A50, A48, A59
.= f1 . i by A33 ; ::_thesis: verum
end;
hence ft = f1 by FUNCT_2:63; ::_thesis: verum
end;
theorem Th24: :: TOPALG_5:24
for x0, y0 being Point of (Tunit_circle 2)
for P, Q being Path of x0,y0
for F being Homotopy of P,Q
for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 (Tunit_circle 2); ::_thesis: for P, Q being Path of x0,y0
for F being Homotopy of P,Q
for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) )
let P, Q be Path of x0,y0; ::_thesis: for F being Homotopy of P,Q
for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) )
let F be Homotopy of P,Q; ::_thesis: for xt being Point of R^1 st P,Q are_homotopic & xt in CircleMap " {x0} holds
ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) )
let xt be Point of R^1; ::_thesis: ( P,Q are_homotopic & xt in CircleMap " {x0} implies ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) )
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 ; ::_thesis: ( not xt in CircleMap " {x0} or ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) ) )
then A2: F is continuous by BORSUK_6:def_11;
assume A3: xt in CircleMap " {x0} ; ::_thesis: ex yt being Point of R^1 ex Pt, Qt being Path of xt,yt ex 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 ) )
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 S1[ set , set , set ] means $3 = ft . $1;
A7: for x being Element of the carrier of I[01]
for y being Element of {0} ex z being Element of REAL st S1[x,y,z] ;
consider Ft being Function of [: the carrier of I[01],{0}:],REAL such that
A8: for y being Element of the carrier of I[01]
for i being Element of {0} holds S1[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 the constant Loop of x0 . x = (CircleMap * (I[01] --> xt)) . x
proof
let x be Point of I[01]; ::_thesis: the constant Loop of x0 . x = (CircleMap * (I[01] --> xt)) . x
thus the constant Loop of x0 . x = x0 by TOPALG_3:21
.= CircleMap . ((I[01] --> xt) . x) by A9, TOPALG_3:4
.= (CircleMap * (I[01] --> xt)) . x by FUNCT_2:15 ; ::_thesis: verum
end;
consider ft1 being Function of I[01],R^1 such that
ft1 . 0 = xt and
the constant Loop of x0 = CircleMap * ft1 and
ft1 is continuous and
A11: for f1 being Function of I[01],R^1 st f1 is continuous & the constant Loop of x0 = CircleMap * f1 & f1 . 0 = xt holds
ft1 = f1 by A3, Th23;
(I[01] --> xt) . j0 = xt by TOPALG_3:4;
then A12: ft1 = I[01] --> xt by A11, A10, FUNCT_2:63;
A13: rng Ft c= REAL ;
A14: dom Ft = [: the carrier of I[01],{0}:] by FUNCT_2:def_1;
A15: the carrier of [:I[01],(Sspace 0[01]):] = [: the carrier of I[01], the carrier of (Sspace 0[01]):] by BORSUK_1:def_2;
then reconsider Ft = Ft as Function of [:I[01],(Sspace 0[01]):],R^1 by Lm14, TOPMETR:17;
A16: for x being set st x in dom (CircleMap * Ft) holds
(F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x
proof
let x be set ; ::_thesis: ( x in dom (CircleMap * Ft) implies (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x )
assume A17: x in dom (CircleMap * Ft) ; ::_thesis: (F | [: the carrier of I[01],{0}:]) . x = (CircleMap * Ft) . x
consider x1, x2 being set such that
A18: x1 in the carrier of I[01] 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 | [: the carrier of I[01],{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 ;
::_thesis: verum
end;
for p being Point of [:I[01],(Sspace 0[01]):]
for 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]):]; ::_thesis: for 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 )
let V be Subset of R^1; ::_thesis: ( Ft . p in V & V is open implies ex W being Subset of [:I[01],(Sspace 0[01]):] st
( p in W & W is open & Ft .: W c= V ) )
assume A21: ( Ft . p in V & V is open ) ; ::_thesis: ex W being Subset of [:I[01],(Sspace 0[01]):] st
( p in W & W is open & Ft .: W c= V )
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;
S1[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 = W1 as non empty Subset of I[01] by A23;
take W = [:W1,([#] (Sspace 0[01])):]; ::_thesis: ( p in W & W is open & Ft .: W c= V )
thus p in W by A22, A23, ZFMISC_1:def_2; ::_thesis: ( W is open & Ft .: W c= V )
thus W is open by A24, BORSUK_1:6; ::_thesis: Ft .: W c= V
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ft .: W or y in V )
assume y in Ft .: W ; ::_thesis: y in V
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;
( S1[x1,x2,Ft . (x1,x2)] & ft . x1 in ft .: W1 ) by A8, Lm14, FUNCT_2:35;
hence y in V by A25, A27, A28; ::_thesis: verum
end;
then A29: Ft is continuous by JGRAPH_2:10;
take yt = ft . j1; ::_thesis: ex Pt, Qt being Path of xt,yt ex 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 ) )
A30: [j1,j0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87;
reconsider ft = ft as Path of xt,yt by A4, A6, BORSUK_2:def_4;
A31: [j0,j0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87;
A32: dom F = the carrier of [:I[01],I[01]:] by FUNCT_2:def_1;
then A33: [: the carrier of I[01],{0}:] c= dom F by Lm3, Lm5, ZFMISC_1:95;
then dom (F | [: the carrier of I[01],{0}:]) = [: the carrier of I[01],{0}:] by RELAT_1:62;
then F | [: the carrier of I[01],{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 | [: the carrier of I[01],{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 the constant Loop of x0 . x = (CircleMap * (Prj2 (j0,G))) . x
proof
let x be Point of I[01]; ::_thesis: the constant Loop of x0 . x = (CircleMap * (Prj2 (j0,G))) . x
thus (CircleMap * (Prj2 (j0,G))) . x = CircleMap . ((Prj2 (j0,G)) . 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
.= the constant Loop of x0 . x by TOPALG_3:21 ; ::_thesis: verum
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 the constant Loop of y0 . x = (CircleMap * (I[01] --> yt)) . x
proof
let x be Point of I[01]; ::_thesis: the constant Loop of y0 . x = (CircleMap * (I[01] --> yt)) . x
thus the constant Loop of y0 . x = y0 by TOPALG_3:21
.= CircleMap . ((I[01] --> yt) . x) by A39, TOPALG_3:4
.= (CircleMap * (I[01] --> yt)) . x by FUNCT_2:15 ; ::_thesis: verum
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
the constant Loop of y0 = CircleMap * ft2 and
ft2 is continuous and
A42: for f1 being Function of I[01],R^1 st f1 is continuous & the constant Loop of y0 = CircleMap * f1 & f1 . 0 = yt holds
ft2 = f1 by Th23;
(I[01] --> yt) . j0 = yt by TOPALG_3:4;
then A43: ft2 = I[01] --> yt by A42, A40, FUNCT_2:63;
set sM1 = Prj2 (j1,G);
A44: for x being Point of I[01] holds the constant Loop of y0 . x = (CircleMap * (Prj2 (j1,G))) . x
proof
let x be Point of I[01]; ::_thesis: the constant Loop of y0 . x = (CircleMap * (Prj2 (j1,G))) . x
thus (CircleMap * (Prj2 (j1,G))) . x = CircleMap . ((Prj2 (j1,G)) . 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
.= the constant Loop of y0 . x by TOPALG_3:21 ; ::_thesis: verum
end;
(Prj2 (j1,G)) . 0 = G . (j1,j0) by Def3
.= Ft . (j1,j0) by A36, A30, FUNCT_1:49
.= yt by A8, Lm4 ;
then A45: ft2 = Prj2 (j1,G) by A34, A42, A44, FUNCT_2:63;
(Prj2 (j0,G)) . 0 = G . (j0,j0) by Def3
.= Ft . (j0,j0) by A36, A31, FUNCT_1:49
.= xt by A4, A8, Lm4 ;
then A46: ft1 = Prj2 (j0,G) by A34, A11, A38, FUNCT_2:63;
set Qt = Prj1 (j1,G);
A47: (Prj1 (j1,G)) . 0 = G . (j0,j1) by Def2
.= (Prj2 (j0,G)) . j1 by Def3
.= xt by A46, A12, TOPALG_3:4 ;
(Prj1 (j1,G)) . 1 = G . (j1,j1) by Def2
.= (Prj2 (j1,G)) . j1 by Def3
.= yt by A45, A43, TOPALG_3:4 ;
then reconsider Qt = Prj1 (j1,G) as Path of xt,yt by A34, A47, BORSUK_2:def_4;
A48: now__::_thesis:_for_s_being_Point_of_I[01]_holds_
(_G_._(s,0)_=_ft_._s_&_G_._(s,1)_=_Qt_._s_&_(_for_t_being_Point_of_I[01]_holds_
(_G_._(0,t)_=_xt_&_G_._(1,t)_=_yt_)_)_)
let s be Point of I[01]; ::_thesis: ( G . (s,0) = ft . s & G . (s,1) = Qt . s & ( for t being Point of I[01] holds
( G . (0,t) = xt & G . (1,t) = yt ) ) )
[s,0] in [: the carrier of I[01],{0}:] by Lm4, ZFMISC_1:87;
hence G . (s,0) = Ft . (s,j0) by A36, FUNCT_1:49
.= ft . s by A8, Lm4 ;
::_thesis: ( G . (s,1) = Qt . s & ( for t being Point of I[01] holds
( G . (0,t) = xt & G . (1,t) = yt ) ) )
thus G . (s,1) = Qt . s by Def2; ::_thesis: for t being Point of I[01] holds
( G . (0,t) = xt & G . (1,t) = yt )
let t be Point of I[01]; ::_thesis: ( G . (0,t) = xt & G . (1,t) = yt )
thus G . (0,t) = (Prj2 (j0,G)) . t by Def3
.= xt by A46, A12, TOPALG_3:4 ; ::_thesis: G . (1,t) = yt
thus G . (1,t) = (Prj2 (j1,G)) . t by Def3
.= yt by A45, A43, TOPALG_3:4 ; ::_thesis: verum
end;
then ft,Qt are_homotopic by A34, BORSUK_2:def_7;
then reconsider G = G as Homotopy of ft,Qt by A34, A48, BORSUK_6:def_11;
take ft ; ::_thesis: ex Qt being Path of xt,yt ex Ft being Homotopy of ft,Qt st
( ft,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
Ft = F1 ) )
take Qt ; ::_thesis: ex Ft being Homotopy of ft,Qt st
( ft,Qt are_homotopic & F = CircleMap * Ft & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
Ft = F1 ) )
take G ; ::_thesis: ( ft,Qt are_homotopic & F = CircleMap * G & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1 ) )
thus A49: ft,Qt are_homotopic by A34, A48, BORSUK_2:def_7; ::_thesis: ( F = CircleMap * G & yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1 ) )
thus F = CircleMap * G by A35; ::_thesis: ( yt in CircleMap " {y0} & ( for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1 ) )
thus yt in CircleMap " {y0} by A41, FUNCT_2:38; ::_thesis: for F1 being Homotopy of ft,Qt st F = CircleMap * F1 holds
G = F1
let F1 be Homotopy of ft,Qt; ::_thesis: ( F = CircleMap * F1 implies G = F1 )
assume A50: F = CircleMap * F1 ; ::_thesis: G = F1
A51: dom F1 = the carrier of [:I[01],I[01]:] by FUNCT_2:def_1;
then A52: dom (F1 | [: the carrier of I[01],{0}:]) = [: the carrier of I[01],{0}:] by A32, A33, RELAT_1:62;
for x being set st x in dom (F1 | [: the carrier of I[01],{0}:]) holds
(F1 | [: the carrier of I[01],{0}:]) . x = Ft . x
proof
let x be set ; ::_thesis: ( x in dom (F1 | [: the carrier of I[01],{0}:]) implies (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x )
assume A53: x in dom (F1 | [: the carrier of I[01],{0}:]) ; ::_thesis: (F1 | [: the carrier of I[01],{0}:]) . x = Ft . x
then consider x1, x2 being set such that
A54: x1 in the carrier of I[01] 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 | [: the carrier of I[01],{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 ; ::_thesis: verum
end;
then F1 | [: the carrier of I[01],{0}:] = Ft by A32, A33, A14, A51, FUNCT_1:2, RELAT_1:62;
hence G = F1 by A37, A50; ::_thesis: verum
end;
definition
func Ciso -> Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) means :Def5: :: TOPALG_5:def 5
for n being Integer holds it . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n));
existence
ex b1 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st
for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
proof
defpred S1[ Integer, set ] means $2 = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop $1));
A1: for x being Element of INT ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S1[x,y]
proof
let x be Element of INT ; ::_thesis: ex y being Element of (pi_1 ((Tunit_circle 2),c[10])) st S1[x,y]
reconsider y = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) as Element of (pi_1 ((Tunit_circle 2),c[10])) by TOPALG_1:47;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] ; ::_thesis: verum
end;
consider f being Function of INT, the carrier of (pi_1 ((Tunit_circle 2),c[10])) such that
A2: for x being Element of INT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
reconsider f = f as Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) ;
take f ; ::_thesis: for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
let n be Integer; ::_thesis: f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n))
n in INT by INT_1:def_2;
hence f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) st ( for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) & ( for n being Integer holds b2 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) holds
b1 = b2
proof
let f, g be Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])); ::_thesis: ( ( for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) & ( for n being Integer holds g . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ) implies f = g )
assume that
A3: for n being Integer holds f . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) and
A4: for n being Integer holds g . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) ; ::_thesis: f = g
for x being Element of INT.Group holds f . x = g . x
proof
let x be Element of INT.Group; ::_thesis: f . x = g . x
thus f . x = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop x)) by A3
.= g . x by A4 ; ::_thesis: verum
end;
hence f = g by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Ciso TOPALG_5:def_5_:_
for b1 being Function of INT.Group,(pi_1 ((Tunit_circle 2),c[10])) holds
( b1 = Ciso iff for n being Integer holds b1 . n = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop n)) );
theorem Th25: :: TOPALG_5:25
for i being Integer
for 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; ::_thesis: for f being Path of R^1 0, R^1 i holds Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f))
let f be Path of R^1 0, R^1 i; ::_thesis: Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f))
set P = CircleMap * f;
A1: (CircleMap * f) . 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 ;
(CircleMap * f) . 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 = CircleMap * f 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; :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = (cLoop i) . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] ) ) )
thus F is continuous ; ::_thesis: for b1 being Element of the carrier of I[01] holds
( F . (b1,0) = (cLoop i) . b1 & F . (b1,1) = P . b1 & F . (0,b1) = c[10] & F . (1,b1) = c[10] )
let s be Point of I[01]; ::_thesis: ( F . (s,0) = (cLoop i) . s & F . (s,1) = P . s & F . (0,s) = c[10] & F . (1,s) = c[10] )
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 ; ::_thesis: ( F . (s,1) = P . s & F . (0,s) = c[10] & F . (1,s) = c[10] )
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 ; ::_thesis: ( F . (0,s) = c[10] & F . (1,s) = c[10] )
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 ; ::_thesis: F . (1,s) = c[10]
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 ; ::_thesis: verum
end;
thus Ciso . i = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop i)) by Def5
.= Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * f)) by A3, TOPALG_1:46 ; ::_thesis: verum
end;
registration
cluster Ciso -> multiplicative ;
coherence
Ciso is multiplicative
proof
set f = Ciso ;
let x, y be Element of INT.Group; :: according to GROUP_6:def_6 ::_thesis: Ciso . (x * y) = (Ciso . x) * (Ciso . y)
consider fX, fY being Loop of c[10] such that
A1: Ciso . x = Class ((EqRel ((Tunit_circle 2),c[10])),fX) and
A2: Ciso . y = Class ((EqRel ((Tunit_circle 2),c[10])),fY) and
A3: the multF of (pi_1 ((Tunit_circle 2),c[10])) . ((Ciso . x),(Ciso . y)) = Class ((EqRel ((Tunit_circle 2),c[10])),(fX + fY)) by TOPALG_1:def_5;
Ciso . y = Class ((EqRel ((Tunit_circle 2),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: (tx * (ExtendInt y)) . 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: (tx * (ExtendInt y)) . 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 ;
x is Real by XREAL_0:def_1;
then tx is being_homeomorphism by JORDAN16:20;
then tx is continuous by TOPS_2:def_5;
then reconsider p = tx * (ExtendInt y) 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]; ::_thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a
percases ( a <= 1 / 2 or 1 / 2 <= a ) ;
supposeA8: a <= 1 / 2 ; ::_thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . a
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 ; ::_thesis: verum
end;
supposeA10: 1 / 2 <= a ; ::_thesis: (CircleMap * ((ExtendInt x) + p)) . a = ((cLoop x) + (cLoop y)) . 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 ; ::_thesis: verum
end;
end;
end;
Ciso . x = Class ((EqRel ((Tunit_circle 2),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 Ciso . (x * y) = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * ((ExtendInt x) + p))) by Th25
.= Class ((EqRel ((Tunit_circle 2),c[10])),((cLoop x) + (cLoop y))) by A7, FUNCT_2:63
.= (Ciso . x) * (Ciso . y) by A3, A12, TOPALG_1:46 ; ::_thesis: verum
end;
end;
registration
cluster Ciso -> one-to-one onto ;
coherence
( Ciso is one-to-one & Ciso is onto )
proof
thus Ciso is one-to-one ::_thesis: Ciso is onto
proof
set xt = R^1 0;
let m, n be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not m in dom Ciso or not n in dom Ciso or not Ciso . m = Ciso . n or m = n )
assume that
A1: ( m in dom Ciso & n in dom Ciso ) and
A2: Ciso . m = Ciso . n ; ::_thesis: m = n
reconsider m = m, n = n as Integer by A1;
( Ciso . m = Class ((EqRel ((Tunit_circle 2),c[10])),(cLoop m)) & Ciso . n = Class ((EqRel ((Tunit_circle 2),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]:],(Tunit_circle 2) 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] ) ) ) by BORSUK_2:def_7;
A6: R^1 0 in CircleMap " {c[10]} by Lm1, TOPREALB:33, TOPREALB:def_2;
then consider ftm being Function of I[01],R^1 such that
ftm . 0 = R^1 0 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 = R^1 0 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 R^1 0,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__::_thesis:_for_x_being_Point_of_I[01]_holds_(CircleMap_*_(Prj1_(j0,Ft)))_._x_=_(cLoop_m)_._x
let x be Point of I[01]; ::_thesis: (CircleMap * (Prj1 (j0,Ft))) . x = (cLoop m) . x
thus (CircleMap * (Prj1 (j0,Ft))) . x = CircleMap . ((Prj1 (j0,Ft)) . 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 ; ::_thesis: verum
end;
(Prj1 (j0,Ft)) . 0 = Ft . (j0,j0) by Def2
.= R^1 0 by A8, BORSUK_6:def_11 ;
then A12: Prj1 (j0,Ft) = ftm by A7, A11, FUNCT_2:63;
set ft1 = Prj1 (j1,Ft);
A13: now__::_thesis:_for_x_being_Point_of_I[01]_holds_(CircleMap_*_(Prj1_(j1,Ft)))_._x_=_(cLoop_n)_._x
let x be Point of I[01]; ::_thesis: (CircleMap * (Prj1 (j1,Ft))) . x = (cLoop n) . x
thus (CircleMap * (Prj1 (j1,Ft))) . x = CircleMap . ((Prj1 (j1,Ft)) . 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 ; ::_thesis: verum
end;
consider ftn being Function of I[01],R^1 such that
ftn . 0 = R^1 0 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 = R^1 0 holds
ftn = f1 by A6, Th23;
A15: cLoop m = CircleMap * (ExtendInt m) by Th20;
(Prj1 (j1,Ft)) . 0 = Ft . (j0,j1) by Def2
.= R^1 0 by A8, BORSUK_6:def_11 ;
then A16: Prj1 (j1,Ft) = ftn by A14, A13, FUNCT_2:63;
(ExtendInt n) . 0 = n * j0 by Def1
.= R^1 0 by TOPREALB:def_2 ;
then ExtendInt n = ftn by A14, A10;
then A17: (Prj1 (j1,Ft)) . j1 = n * 1 by A16, Def1;
(ExtendInt m) . 0 = m * j0 by Def1
.= R^1 0 by TOPREALB:def_2 ;
then ExtendInt m = ftm by A7, A15;
then A18: (Prj1 (j0,Ft)) . j1 = m * 1 by A12, Def1;
(Prj1 (j0,Ft)) . j1 = Ft . (j1,j0) by Def2
.= yt by A8, BORSUK_6:def_11
.= Ft . (j1,j1) by A8, BORSUK_6:def_11
.= (Prj1 (j1,Ft)) . j1 by Def2 ;
hence m = n by A18, A17; ::_thesis: verum
end;
thus rng Ciso c= the carrier of (pi_1 ((Tunit_circle 2),c[10])) ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of (pi_1 ((Tunit_circle 2),c[10])) c= rng Ciso
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in the carrier of (pi_1 ((Tunit_circle 2),c[10])) or q in rng Ciso )
assume q in the carrier of (pi_1 ((Tunit_circle 2),c[10])) ; ::_thesis: q in rng Ciso
then consider f being Loop of c[10] such that
A19: q = Class ((EqRel ((Tunit_circle 2),c[10])),f) by TOPALG_1:47;
R^1 0 in CircleMap " {c[10]} by Lm1, TOPREALB:33, TOPREALB: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;
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 A23: ft . 1 in INT by Lm12, FUNCT_1:def_7, TOPREALB:33;
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 ((Tunit_circle 2),c[10])),(CircleMap * ft)) ) by A23, Th25, FUNCT_2:def_1;
hence q in rng Ciso by A19, A21, A23, FUNCT_1:def_3; ::_thesis: verum
end;
end;
theorem :: TOPALG_5:26
Ciso is bijective ;
Lm16: for r being positive real number
for o being Point of (TOP-REAL 2)
for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
proof
let r be positive real number ; ::_thesis: for o being Point of (TOP-REAL 2)
for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
let o be Point of (TOP-REAL 2); ::_thesis: for x being Point of (Tcircle (o,r)) holds INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
let x be Point of (Tcircle (o,r)); ::_thesis: INT.Group , pi_1 ((Tcircle (o,r)),x) are_isomorphic
Tunit_circle 2 = Tcircle ((0. (TOP-REAL 2)),1) by TOPREALB:def_7;
then pi_1 ((Tunit_circle 2),c[10]), pi_1 ((Tcircle (o,r)),x) are_isomorphic by TOPALG_3:33, TOPREALB:20;
then consider h being Homomorphism of (pi_1 ((Tunit_circle 2),c[10])),(pi_1 ((Tcircle (o,r)),x)) such that
A1: h is bijective by GROUP_6:def_11;
take h * Ciso ; :: according to GROUP_6:def_11 ::_thesis: h * Ciso is bijective
thus h * Ciso is bijective by A1, GROUP_6:64; ::_thesis: verum
end;
theorem Th27: :: TOPALG_5:27
for S being being_simple_closed_curve SubSpace of TOP-REAL 2
for x being Point of S holds INT.Group , pi_1 (S,x) are_isomorphic
proof
set r = the positive real number ;
set o = the Point of (TOP-REAL 2);
set y = the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive real number ));
let S be being_simple_closed_curve SubSpace of TOP-REAL 2; ::_thesis: for x being Point of S holds INT.Group , pi_1 (S,x) are_isomorphic
let x be Point of S; ::_thesis: INT.Group , pi_1 (S,x) are_isomorphic
( INT.Group , pi_1 ((Tcircle ( the Point of (TOP-REAL 2), the positive real number )), the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive real number ))) are_isomorphic & pi_1 ((Tcircle ( the Point of (TOP-REAL 2), the positive real number )), the Point of (Tcircle ( the Point of (TOP-REAL 2), the positive real number ))), pi_1 (S,x) are_isomorphic ) by Lm16, TOPALG_3:33, TOPREALB:11;
hence INT.Group , pi_1 (S,x) are_isomorphic by GROUP_6:67; ::_thesis: verum
end;
registration
let S be being_simple_closed_curve SubSpace of TOP-REAL 2;
let x be Point of S;
cluster FundamentalGroup (S,x) -> infinite ;
coherence
not pi_1 (S,x) is finite
proof
INT.Group , pi_1 (S,x) are_isomorphic by Th27;
hence not pi_1 (S,x) is finite by GROUP_6:74; ::_thesis: verum
end;
end;