:: by Artur Korni{\l}owicz

::

:: Received July 30, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

set I = the carrier of I[01];

Lm1: 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;

theorem :: TOPALG_3:1

for A, B, a, b being set

for f being Function of A,B st a in A & b in B holds

f +* (a .--> b) is Function of A,B

for f being Function of A,B st a in A & b in B holds

f +* (a .--> b) is Function of A,B

proof end;

theorem :: TOPALG_3:2

for f being Function

for X, x being set st f | X is one-to-one & x in rng (f | X) holds

(f * ((f | X) ")) . x = x

for X, x being set st f | X is one-to-one & x in rng (f | X) holds

(f * ((f | X) ")) . x = x

proof end;

theorem :: TOPALG_3:4

:: Topological preliminaries

theorem :: TOPALG_3:5

for T being non empty TopStruct

for t being Point of T

for A being Subset of T st A = {t} holds

Sspace t = T | A

for t being Point of T

for A being Subset of T st A = {t} holds

Sspace t = T | A

proof end;

theorem Th7: :: TOPALG_3:7

for T being non empty TopSpace holds

( T is connected iff for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) )

( T is connected iff for f being Function of T,(1TopSp {0,1}) holds

( not f is continuous or not f is onto ) )

proof end;

theorem :: TOPALG_3:8

for T being TopSpace st TopStruct(# the carrier of T, the topology of T #) is connected holds

T is connected

T is connected

proof end;

registration

let T be connected TopSpace;

coherence

TopStruct(# the carrier of T, the topology of T #) is connected

end;
coherence

TopStruct(# the carrier of T, the topology of T #) is connected

proof end;

theorem :: TOPALG_3:9

for S, T being non empty TopSpace st S,T are_homeomorphic & S is pathwise_connected holds

T is pathwise_connected

T is pathwise_connected

proof end;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is trivial holds

b_{1} is pathwise_connected

end;
for b

b

proof end;

theorem :: TOPALG_3:10

for T being SubSpace of TOP-REAL 2 st the carrier of T is Simple_closed_curve holds

T is pathwise_connected

T is pathwise_connected

proof end;

theorem :: TOPALG_3:11

for T being TopSpace ex F being Subset-Family of T st

( F = { the carrier of T} & F is Cover of T & F is open )

( F = { the carrier of T} & F is Cover of T & F is open )

proof end;

registration

let T be TopSpace;

existence

ex b_{1} being Subset-Family of T st

( not b_{1} is empty & b_{1} is mutually-disjoint & b_{1} is open & b_{1} is closed )

end;
existence

ex b

( not b

proof end;

theorem :: TOPALG_3:12

for T being TopSpace

for D being open mutually-disjoint Subset-Family of T

for A being Subset of T

for X being set st A is connected & X in D & X meets A & D is Cover of A holds

A c= X

for D being open mutually-disjoint Subset-Family of T

for A being Subset of T

for X being set st A is connected & X in D & X meets A & D is Cover of A holds

A c= X

proof end;

theorem Th13: :: TOPALG_3:13

for S, T being TopSpace holds TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]

proof end;

theorem Th14: :: TOPALG_3:14

for S, T being TopSpace

for A being Subset of S

for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]

for A being Subset of S

for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]

proof end;

theorem Th15: :: TOPALG_3:15

for S, T being TopSpace

for A being closed Subset of S

for B being closed Subset of T holds [:A,B:] is closed

for A being closed Subset of S

for B being closed Subset of T holds [:A,B:] is closed

proof end;

theorem :: TOPALG_3:16

for S, T being TopSpace

for A being Subset of S

for B being Subset of T st A is connected & B is connected holds

[:A,B:] is connected

for A being Subset of S

for B being Subset of T st A is connected & B is connected holds

[:A,B:] is connected

proof end;

theorem :: TOPALG_3:17

for S, T being TopSpace

for Y being non empty TopSpace

for A being Subset of S

for f being Function of [:S,T:],Y

for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds

g is continuous

for Y being non empty TopSpace

for A being Subset of S

for f being Function of [:S,T:],Y

for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds

g is continuous

proof end;

theorem :: TOPALG_3:18

for S, T being TopSpace

for Y being non empty TopSpace

for A being Subset of T

for f being Function of [:S,T:],Y

for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds

g is continuous

for Y being non empty TopSpace

for A being Subset of T

for f being Function of [:S,T:],Y

for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds

g is continuous

proof end;

theorem :: TOPALG_3:19

for S, T, T1, T2, Y being non empty TopSpace

for f being Function of [:Y,T1:],S

for g being Function of [:Y,T2:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds

f . p = g . p ) holds

ex h being Function of [:Y,T:],S st

( h = f +* g & h is continuous )

for f being Function of [:Y,T1:],S

for g being Function of [:Y,T2:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds

f . p = g . p ) holds

ex h being Function of [:Y,T:],S st

( h = f +* g & h is continuous )

proof end;

theorem :: TOPALG_3:20

for S, T, T1, T2, Y being non empty TopSpace

for f being Function of [:T1,Y:],S

for g being Function of [:T2,Y:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

( h = f +* g & h is continuous )

for f being Function of [:T1,Y:],S

for g being Function of [:T2,Y:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

( h = f +* g & h is continuous )

proof end;

registration

let T be non empty TopSpace;

let t be Point of T;

coherence

for b_{1} being Loop of t holds b_{1} is continuous

end;
let t be Point of T;

coherence

for b

proof end;

theorem :: TOPALG_3:21

for T being non empty TopSpace

for t being Point of T

for x being Point of I[01]

for P being constant Loop of t holds P . x = t

for t being Point of T

for x being Point of I[01]

for P being constant Loop of t holds P . x = t

proof end;

theorem Th22: :: TOPALG_3:22

for T being non empty TopSpace

for t being Point of T

for P being Loop of t holds

( P . 0 = t & P . 1 = t )

for t being Point of T

for P being Loop of t holds

( P . 0 = t & P . 1 = t )

proof end;

theorem Th23: :: TOPALG_3:23

for S, T being non empty TopSpace

for f being continuous Function of S,T

for a, b being Point of S st a,b are_connected holds

f . a,f . b are_connected

for f being continuous Function of S,T

for a, b being Point of S st a,b are_connected holds

f . a,f . b are_connected

proof end;

theorem :: TOPALG_3:24

for S, T being non empty TopSpace

for f being continuous Function of S,T

for a, b being Point of S

for P being Path of a,b st a,b are_connected holds

f * P is Path of f . a,f . b

for f being continuous Function of S,T

for a, b being Point of S

for P being Path of a,b st a,b are_connected holds

f * P is Path of f . a,f . b

proof end;

theorem Th25: :: TOPALG_3:25

for S being non empty pathwise_connected TopSpace

for T being non empty TopSpace

for f being continuous Function of S,T

for a, b being Point of S

for P being Path of a,b holds f * P is Path of f . a,f . b

for T being non empty TopSpace

for f being continuous Function of S,T

for a, b being Point of S

for P being Path of a,b holds f * P is Path of f . a,f . b

proof end;

definition

let S be non empty pathwise_connected TopSpace;

let T be non empty TopSpace;

let a, b be Point of S;

let P be Path of a,b;

let f be continuous Function of S,T;

:: original: *

redefine func f * P -> Path of f . a,f . b;

coherence

P * f is Path of f . a,f . b by Th25;

end;
let T be non empty TopSpace;

let a, b be Point of S;

let P be Path of a,b;

let f be continuous Function of S,T;

:: original: *

redefine func f * P -> Path of f . a,f . b;

coherence

P * f is Path of f . a,f . b by Th25;

theorem Th26: :: TOPALG_3:26

for S, T being non empty TopSpace

for f being continuous Function of S,T

for a being Point of S

for P being Loop of a holds f * P is Loop of f . a

for f being continuous Function of S,T

for a being Point of S

for P being Loop of a holds f * P is Loop of f . a

proof end;

definition

let S, T be non empty TopSpace;

let a be Point of S;

let P be Loop of a;

let f be continuous Function of S,T;

:: original: *

redefine func f * P -> Loop of f . a;

coherence

P * f is Loop of f . a by Th26;

end;
let a be Point of S;

let P be Loop of a;

let f be continuous Function of S,T;

:: original: *

redefine func f * P -> Loop of f . a;

coherence

P * f is Loop of f . a by Th26;

theorem Th27: :: TOPALG_3:27

for S, T being non empty TopSpace

for f being continuous Function of S,T

for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

for f being continuous Function of S,T

for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

P1,Q1 are_homotopic

proof end;

theorem :: TOPALG_3:28

for S, T being non empty TopSpace

for f being continuous Function of S,T

for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b

for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

f * F is Homotopy of P1,Q1

for f being continuous Function of S,T

for a, b being Point of S

for P, Q being Path of a,b

for P1, Q1 being Path of f . a,f . b

for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds

f * F is Homotopy of P1,Q1

proof end;

theorem Th29: :: TOPALG_3:29

for S, T being non empty TopSpace

for f being continuous Function of S,T

for a, b, c being Point of S

for P being Path of a,b

for Q being Path of b,c

for P1 being Path of f . a,f . b

for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds

P1 + Q1 = f * (P + Q)

for f being continuous Function of S,T

for a, b, c being Point of S

for P being Path of a,b

for Q being Path of b,c

for P1 being Path of f . a,f . b

for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds

P1 + Q1 = f * (P + Q)

proof end;

definition

let S, T be non empty TopSpace;

let s be Point of S;

let f be Function of S,T;

assume A1: f is continuous ;

set pT = pi_1 (T,(f . s));

set pS = pi_1 (S,s);

ex b_{1} being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st

for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & b_{1} . x = Class ((EqRel (T,(f . s))),(f * ls)) )

for b_{1}, b_{2} being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & b_{1} . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) & ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & b_{2} . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) holds

b_{1} = b_{2}

end;
let s be Point of S;

let f be Function of S,T;

assume A1: f is continuous ;

set pT = pi_1 (T,(f . s));

set pS = pi_1 (S,s);

func FundGrIso (f,s) -> Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) means :Def1: :: TOPALG_3:def 1

for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & it . x = Class ((EqRel (T,(f . s))),(f * ls)) );

existence for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & it . x = Class ((EqRel (T,(f . s))),(f * ls)) );

ex b

for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & b

proof end;

uniqueness for b

( x = Class ((EqRel (S,s)),ls) & b

( x = Class ((EqRel (S,s)),ls) & b

b

proof end;

:: deftheorem Def1 defines FundGrIso TOPALG_3:def 1 :

for S, T being non empty TopSpace

for s being Point of S

for f being Function of S,T st f is continuous holds

for b_{5} being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) holds

( b_{5} = FundGrIso (f,s) iff for x being Element of (pi_1 (S,s)) ex ls being Loop of s st

( x = Class ((EqRel (S,s)),ls) & b_{5} . x = Class ((EqRel (T,(f . s))),(f * ls)) ) );

for S, T being non empty TopSpace

for s being Point of S

for f being Function of S,T st f is continuous holds

for b

( b

( x = Class ((EqRel (S,s)),ls) & b

theorem :: TOPALG_3:30

for S, T being non empty TopSpace

for s being Point of S

for f being continuous Function of S,T

for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))

for s being Point of S

for f being continuous Function of S,T

for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))

proof end;

registration

let S, T be non empty TopSpace;

let s be Point of S;

let f be continuous Function of S,T;

coherence

FundGrIso (f,s) is multiplicative

end;
let s be Point of S;

let f be continuous Function of S,T;

coherence

FundGrIso (f,s) is multiplicative

proof end;

theorem Th31: :: TOPALG_3:31

for S, T being non empty TopSpace

for s being Point of S

for f being continuous Function of S,T st f is being_homeomorphism holds

FundGrIso (f,s) is bijective

for s being Point of S

for f being continuous Function of S,T st f is being_homeomorphism holds

FundGrIso (f,s) is bijective

proof end;

theorem :: TOPALG_3:32

for S, T being non empty TopSpace

for s being Point of S

for t being Point of T

for f being continuous Function of S,T

for P being Path of t,f . s

for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds

h is bijective

for s being Point of S

for t being Point of T

for f being continuous Function of S,T

for P being Path of t,f . s

for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds

h is bijective

proof end;

theorem :: TOPALG_3:33

for S being non empty TopSpace

for T being non empty pathwise_connected TopSpace

for s being Point of S

for t being Point of T st S,T are_homeomorphic holds

pi_1 (S,s), pi_1 (T,t) are_isomorphic

for T being non empty pathwise_connected TopSpace

for s being Point of S

for t being Point of T st S,T are_homeomorphic holds

pi_1 (S,s), pi_1 (T,t) are_isomorphic

proof end;