:: by Grzegorz Bancerek

::

:: Received September 24, 1999

:: Copyright (c) 1999-2018 Association of Mizar Users

notation
end;

notation

let I be set ;

let J be non-Empty TopStruct-yielding ManySortedSet of I;

synonym I -TOP_prod J for product J;

end;
let J be non-Empty TopStruct-yielding ManySortedSet of I;

synonym I -TOP_prod J for product J;

:: 4.1. DEFINITION (a)

definition
end;

:: deftheorem defines oContMaps WAYBEL26:def 1 :

for X, Y being non empty TopSpace holds oContMaps (X,Y) = ContMaps (X,(Omega Y));

for X, Y being non empty TopSpace holds oContMaps (X,Y) = ContMaps (X,(Omega Y));

registration

let X, Y be non empty TopSpace;

coherence

( oContMaps (X,Y) is reflexive & oContMaps (X,Y) is transitive & oContMaps (X,Y) is constituted-Functions ) ;

end;
coherence

( oContMaps (X,Y) is reflexive & oContMaps (X,Y) is transitive & oContMaps (X,Y) is constituted-Functions ) ;

registration

let X be non empty TopSpace;

let Y be non empty T_0 TopSpace;

coherence

oContMaps (X,Y) is antisymmetric ;

end;
let Y be non empty T_0 TopSpace;

coherence

oContMaps (X,Y) is antisymmetric ;

theorem Th1: :: WAYBEL26:1

for X, Y being non empty TopSpace

for a being set holds

( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )

for a being set holds

( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )

proof end;

theorem Th2: :: WAYBEL26:2

for X, Y being non empty TopSpace

for a being set holds

( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,Y )

for a being set holds

( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,Y )

proof end;

theorem Th3: :: WAYBEL26:3

for X, Y being non empty TopSpace

for a, b being Element of (oContMaps (X,Y))

for f, g being Function of X,(Omega Y) st a = f & b = g holds

( a <= b iff f <= g )

for a, b being Element of (oContMaps (X,Y))

for f, g being Function of X,(Omega Y) st a = f & b = g holds

( a <= b iff f <= g )

proof end;

definition

let X, Y be non empty TopSpace;

let x be Point of X;

let A be Subset of (oContMaps (X,Y));

:: original: pi

redefine func pi (A,x) -> Subset of (Omega Y);

coherence

pi (A,x) is Subset of (Omega Y)

end;
let x be Point of X;

let A be Subset of (oContMaps (X,Y));

:: original: pi

redefine func pi (A,x) -> Subset of (Omega Y);

coherence

pi (A,x) is Subset of (Omega Y)

proof end;

registration

let X, Y be non empty TopSpace;

let x be set ;

let A be non empty Subset of (oContMaps (X,Y));

coherence

not pi (A,x) is empty

end;
let x be set ;

let A be non empty Subset of (oContMaps (X,Y));

coherence

not pi (A,x) is empty

proof end;

theorem Th5: :: WAYBEL26:5

for X being non empty TopSpace ex f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) st

( f is isomorphic & ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )

( f is isomorphic & ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )

proof end;

theorem Th6: :: WAYBEL26:6

for X being non empty TopSpace holds InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic

proof end;

:: 4.1. DEFINITION (b)

definition

let X, Y, Z be non empty TopSpace;

let f be continuous Function of Y,Z;

for b_{1}, b_{2} being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st ( for g being continuous Function of X,Y holds b_{1} . g = f * g ) & ( for g being continuous Function of X,Y holds b_{2} . g = f * g ) holds

b_{1} = b_{2}

ex b_{1} being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st

for g being continuous Function of X,Y holds b_{1} . g = f * g

for b_{1}, b_{2} being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st ( for g being continuous Function of Z,X holds b_{1} . g = g * f ) & ( for g being continuous Function of Z,X holds b_{2} . g = g * f ) holds

b_{1} = b_{2}

ex b_{1} being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st

for g being continuous Function of Z,X holds b_{1} . g = g * f

end;
let f be continuous Function of Y,Z;

func oContMaps (X,f) -> Function of (oContMaps (X,Y)),(oContMaps (X,Z)) means :Def2: :: WAYBEL26:def 2

for g being continuous Function of X,Y holds it . g = f * g;

uniqueness for g being continuous Function of X,Y holds it . g = f * g;

for b

b

proof end;

existence ex b

for g being continuous Function of X,Y holds b

proof end;

func oContMaps (f,X) -> Function of (oContMaps (Z,X)),(oContMaps (Y,X)) means :Def3: :: WAYBEL26:def 3

for g being continuous Function of Z,X holds it . g = g * f;

uniqueness for g being continuous Function of Z,X holds it . g = g * f;

for b

b

proof end;

existence ex b

for g being continuous Function of Z,X holds b

proof end;

:: deftheorem Def2 defines oContMaps WAYBEL26:def 2 :

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z

for b_{5} being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) holds

( b_{5} = oContMaps (X,f) iff for g being continuous Function of X,Y holds b_{5} . g = f * g );

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z

for b

( b

:: deftheorem Def3 defines oContMaps WAYBEL26:def 3 :

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z

for b_{5} being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) holds

( b_{5} = oContMaps (f,X) iff for g being continuous Function of Z,X holds b_{5} . g = g * f );

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z

for b

( b

theorem Th7: :: WAYBEL26:7

for X being non empty TopSpace

for Y being monotone-convergence T_0-TopSpace holds oContMaps (X,Y) is up-complete

for Y being monotone-convergence T_0-TopSpace holds oContMaps (X,Y) is up-complete

proof end;

theorem Th8: :: WAYBEL26:8

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z holds oContMaps (X,f) is monotone

for f being continuous Function of Y,Z holds oContMaps (X,f) is monotone

proof end;

theorem :: WAYBEL26:9

for X, Y being non empty TopSpace

for f being continuous Function of Y,Y st f is idempotent holds

oContMaps (X,f) is idempotent

for f being continuous Function of Y,Y st f is idempotent holds

oContMaps (X,f) is idempotent

proof end;

theorem Th10: :: WAYBEL26:10

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z holds oContMaps (f,X) is monotone

for f being continuous Function of Y,Z holds oContMaps (f,X) is monotone

proof end;

theorem Th11: :: WAYBEL26:11

for X, Y being non empty TopSpace

for f being continuous Function of Y,Y st f is idempotent holds

oContMaps (f,X) is idempotent

for f being continuous Function of Y,Y st f is idempotent holds

oContMaps (f,X) is idempotent

proof end;

theorem Th12: :: WAYBEL26:12

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z

for x being Element of X

for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))

for f being continuous Function of Y,Z

for x being Element of X

for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))

proof end;

:: 4.2. LEMMA (ii)

theorem Th13: :: WAYBEL26:13

for X being non empty TopSpace

for Y, Z being monotone-convergence T_0-TopSpace

for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving

for Y, Z being monotone-convergence T_0-TopSpace

for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving

proof end;

theorem Th14: :: WAYBEL26:14

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z

for x being Element of Y

for A being Subset of (oContMaps (Z,X)) holds pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))

for f being continuous Function of Y,Z

for x being Element of Y

for A being Subset of (oContMaps (Z,X)) holds pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))

proof end;

theorem Th15: :: WAYBEL26:15

for Y, Z being non empty TopSpace

for X being monotone-convergence T_0-TopSpace

for f being continuous Function of Y,Z holds oContMaps (f,X) is directed-sups-preserving

for X being monotone-convergence T_0-TopSpace

for f being continuous Function of Y,Z holds oContMaps (f,X) is directed-sups-preserving

proof end;

:: 4.3. LEMMA (i) genralized

theorem Th16: :: WAYBEL26:16

for X, Z being non empty TopSpace

for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)

for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)

proof end;

theorem Th17: :: WAYBEL26:17

for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z

for f being continuous Function of Z,Y st f is being_a_retraction holds

Omega Y is directed-sups-inheriting SubRelStr of Omega Z

for Y being non empty SubSpace of Z

for f being continuous Function of Z,Y st f is being_a_retraction holds

Omega Y is directed-sups-inheriting SubRelStr of Omega Z

proof end;

Lm1: for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z

for f being continuous Function of Z,Y st f is being_a_retraction holds

Y is monotone-convergence

proof end;

theorem Th18: :: WAYBEL26:18

for X being non empty TopSpace

for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z

for f being continuous Function of Z,Y st f is being_a_retraction holds

oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)

for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z

for f being continuous Function of Z,Y st f is being_a_retraction holds

oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)

proof end;

theorem Th19: :: WAYBEL26:19

for X being non empty TopSpace

for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds

oContMaps (X,Y) is_a_retract_of oContMaps (X,Z)

for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds

oContMaps (X,Y) is_a_retract_of oContMaps (X,Z)

proof end;

theorem Th20: :: WAYBEL26:20

for X, Y, Z being non empty TopSpace

for f being continuous Function of Y,Z st f is being_homeomorphism holds

oContMaps (X,f) is isomorphic

for f being continuous Function of Y,Z st f is being_homeomorphism holds

oContMaps (X,f) is isomorphic

proof end;

theorem Th21: :: WAYBEL26:21

for X, Y, Z being non empty TopSpace st Y,Z are_homeomorphic holds

oContMaps (X,Y), oContMaps (X,Z) are_isomorphic

oContMaps (X,Y), oContMaps (X,Z) are_isomorphic

proof end;

:: 4.3. LEMMA (ii)

theorem Th22: :: WAYBEL26:22

for X being non empty TopSpace

for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z st Y is_a_retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by Th19, YELLOW16:21, YELLOW16:22;

for Z being monotone-convergence T_0-TopSpace

for Y being non empty SubSpace of Z st Y is_a_retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by Th19, YELLOW16:21, YELLOW16:22;

theorem Th23: :: WAYBEL26:23

for X being non empty TopSpace

for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

proof end;

theorem Th25: :: WAYBEL26:25

for X being non empty TopSpace

for Y being non trivial T_0-TopSpace st oContMaps (X,Y) is with_suprema holds

not Y is T_1

for Y being non trivial T_0-TopSpace st oContMaps (X,Y) is with_suprema holds

not Y is T_1

proof end;

registration
end;

registration

existence

ex b_{1} being T_0-TopSpace st

( b_{1} is injective & b_{1} is monotone-convergence & not b_{1} is trivial )

end;
ex b

( b

proof end;

:: 4.4. PROPOSITION

theorem Th26: :: WAYBEL26:26

for X being non empty TopSpace

for Y being non trivial monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds

InclPoset the topology of X is continuous

for Y being non trivial monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds

InclPoset the topology of X is continuous

proof end;

theorem Th27: :: WAYBEL26:27

for X being non empty TopSpace

for x being Point of X

for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st

( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st

( h = X --> x & F = oContMaps (h,Y) ) )

for x being Point of X

for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st

( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st

( h = X --> x & F = oContMaps (h,Y) ) )

proof end;

:: 4.5. PROPOSITION

theorem Th28: :: WAYBEL26:28

for X being non empty TopSpace

for Y being monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds

( Omega Y is complete & Omega Y is continuous )

for Y being monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds

( Omega Y is complete & Omega Y is continuous )

proof end;

theorem Th29: :: WAYBEL26:29

for X being non empty 1-sorted

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being Function of X,(I -TOP_prod J)

for i being Element of I holds (commute f) . i = (proj (J,i)) * f

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I

for f being Function of X,(I -TOP_prod J)

for i being Element of I holds (commute f) . i = (proj (J,i)) * f

proof end;

theorem Th31: :: WAYBEL26:31

for X, Y being non empty TopSpace

for M being non empty set

for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M, the carrier of (oContMaps (X,Y))

for M being non empty set

for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M, the carrier of (oContMaps (X,Y))

proof end;

theorem Th32: :: WAYBEL26:32

for X, Y being non empty TopSpace holds the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y)

proof end;

theorem Th33: :: WAYBEL26:33

for X, Y being non empty TopSpace

for M being non empty set

for f being Function of M, the carrier of (oContMaps (X,Y)) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))

for M being non empty set

for f being Function of M, the carrier of (oContMaps (X,Y)) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))

proof end;

theorem Th34: :: WAYBEL26:34

for X being non empty TopSpace

for M being non empty set ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st

( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )

for M being non empty set ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st

( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )

proof end;

theorem Th35: :: WAYBEL26:35

for X being non empty TopSpace

for M being non empty set holds oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))),M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))) are_isomorphic

for M being non empty set holds oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))),M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))) are_isomorphic

proof end;

:: 4.6. PROPOSITION

theorem Th36: :: WAYBEL26:36

for X being non empty TopSpace st InclPoset the topology of X is continuous holds

for Y being injective T_0-TopSpace holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

for Y being injective T_0-TopSpace holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

proof end;

registration

ex b_{1} being TopLattice st

( not b_{1} is trivial & b_{1} is complete & b_{1} is Scott )
end;

cluster non empty non trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott for TopLattice;

existence ex b

( not b

proof end;

:: 4.7. THEOREM p.129.

theorem :: WAYBEL26:37

for X being non empty TopSpace

for L being non trivial complete Scott TopLattice holds

( oContMaps (X,L) is complete & oContMaps (X,L) is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )

for L being non trivial complete Scott TopLattice holds

( oContMaps (X,L) is complete & oContMaps (X,L) is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )

proof end;

:: deftheorem defines *graph WAYBEL26:def 4 :

for f being Function holds *graph f = (Union (disjoin f)) ~ ;

for f being Function holds *graph f = (Union (disjoin f)) ~ ;

theorem Th38: :: WAYBEL26:38

for x, y being object

for f being Function holds

( [x,y] in *graph f iff ( x in dom f & y in f . x ) )

for f being Function holds

( [x,y] in *graph f iff ( x in dom f & y in f . x ) )

proof end;

:: 4.8. LEMMA p.130.

theorem Th40: :: WAYBEL26:40

for X, Y being non empty TopSpace

for S being Scott TopAugmentation of InclPoset the topology of Y

for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds

f is continuous

for S being Scott TopAugmentation of InclPoset the topology of Y

for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds

f is continuous

proof end;

definition

let W be Relation;

let X be set ;

ex b_{1} being Function st

( dom b_{1} = X & ( for x being object st x in X holds

b_{1} . x = Im (W,x) ) )

uniqueness

for b_{1}, b_{2} being Function st dom b_{1} = X & ( for x being object st x in X holds

b_{1} . x = Im (W,x) ) & dom b_{2} = X & ( for x being object st x in X holds

b_{2} . x = Im (W,x) ) holds

b_{1} = b_{2};

end;
let X be set ;

func (W,X) *graph -> Function means :Def5: :: WAYBEL26:def 5

( dom it = X & ( for x being object st x in X holds

it . x = Im (W,x) ) );

existence ( dom it = X & ( for x being object st x in X holds

it . x = Im (W,x) ) );

ex b

( dom b

b

proof end;

correctness uniqueness

for b

b

b

b

proof end;

:: deftheorem Def5 defines *graph WAYBEL26:def 5 :

for W being Relation

for X being set

for b_{3} being Function holds

( b_{3} = (W,X) *graph iff ( dom b_{3} = X & ( for x being object st x in X holds

b_{3} . x = Im (W,x) ) ) );

for W being Relation

for X being set

for b

( b

b

registration

let X, Y be TopSpace;

coherence

for b_{1} being Subset of [:X,Y:] holds b_{1} is Relation-like

for b_{1} being Element of the topology of [:X,Y:] holds b_{1} is Relation-like
;

end;
coherence

for b

proof end;

coherence for b

theorem Th42: :: WAYBEL26:42

for X, Y being non empty TopSpace

for W being open Subset of [:X,Y:]

for x being Point of X holds Im (W,x) is open Subset of Y

for W being open Subset of [:X,Y:]

for x being Point of X holds Im (W,x) is open Subset of Y

proof end;

:: 4.9. PROPOSITION a) p.130.

theorem Th43: :: WAYBEL26:43

for X, Y being non empty TopSpace

for S being Scott TopAugmentation of InclPoset the topology of Y

for W being open Subset of [:X,Y:] holds (W, the carrier of X) *graph is continuous Function of X,S

for S being Scott TopAugmentation of InclPoset the topology of Y

for W being open Subset of [:X,Y:] holds (W, the carrier of X) *graph is continuous Function of X,S

proof end;

:: 4.9. PROPOSITION b) p.130.

theorem Th44: :: WAYBEL26:44

for X, Y being non empty TopSpace

for S being Scott TopAugmentation of InclPoset the topology of Y

for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds

for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

for S being Scott TopAugmentation of InclPoset the topology of Y

for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds

for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds

f1 <= f2

proof end;

:: 4.9. PROPOSITION p.130.

theorem :: WAYBEL26:45

for X, Y being non empty TopSpace

for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) st

( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )

for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) st

( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )

proof end;