:: by Adam Grabowski

::

:: Received June 22, 1999

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

theorem :: WAYBEL24:1

for S, T being up-complete Scott TopLattice

for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T

for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T

proof end;

registration

let S be non empty RelStr ;

let T be non empty reflexive RelStr ;

for b_{1} being Function of S,T st b_{1} is constant holds

b_{1} is monotone

end;
let T be non empty reflexive RelStr ;

cluster Function-like constant quasi_total -> monotone for Element of bool [: the carrier of S, the carrier of T:];

coherence for b

b

proof end;

registration

let S be non empty RelStr ;

let T be non empty reflexive RelStr ;

let a be Element of T;

coherence

S --> a is monotone

end;
let T be non empty reflexive RelStr ;

let a be Element of T;

coherence

S --> a is monotone

proof end;

theorem :: WAYBEL24:2

for S being non empty RelStr

for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T)

for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T)

proof end;

theorem :: WAYBEL24:3

for S being non empty RelStr

for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T)

for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T)

proof end;

scheme :: WAYBEL24:sch 1

FuncFraenkelSL{ F_{1}() -> non empty RelStr , F_{2}() -> non empty RelStr , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Function, P_{1}[ set ] } :

FuncFraenkelSL{ F

F_{4}() .: { F_{3}(x) where x is Element of F_{1}() : P_{1}[x] } = { (F_{4}() . F_{3}(x)) where x is Element of F_{1}() : P_{1}[x] }

provided
proof end;

theorem Th4: :: WAYBEL24:4

for S, T being complete LATTICE

for f being monotone Function of S,T

for x being Element of S holds f . x = sup (f .: (downarrow x))

for f being monotone Function of S,T

for x being Element of S holds f . x = sup (f .: (downarrow x))

proof end;

theorem :: WAYBEL24:5

for S, T being lower-bounded complete LATTICE

for f being monotone Function of S,T

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)

for f being monotone Function of S,T

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)

proof end;

theorem Th6: :: WAYBEL24:6

for S being RelStr

for T being non empty RelStr

for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T

for T being non empty RelStr

for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T

proof end;

definition

let X1, X2, Y be non empty RelStr ;

let f be Function of [:X1,X2:],Y;

let x be Element of X1;

correctness

coherence

(curry f) . x is Function of X2,Y;

end;
let f be Function of [:X1,X2:],Y;

let x be Element of X1;

correctness

coherence

(curry f) . x is Function of X2,Y;

proof end;

:: deftheorem defines Proj WAYBEL24:def 1 :

for X1, X2, Y being non empty RelStr

for f being Function of [:X1,X2:],Y

for x being Element of X1 holds Proj (f,x) = (curry f) . x;

for X1, X2, Y being non empty RelStr

for f being Function of [:X1,X2:],Y

for x being Element of X1 holds Proj (f,x) = (curry f) . x;

theorem Th7: :: WAYBEL24:7

for X1, X2, Y being non empty RelStr

for f being Function of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)

for f being Function of [:X1,X2:],Y

for x being Element of X1

for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)

proof end;

definition

let X1, X2, Y be non empty RelStr ;

let f be Function of [:X1,X2:],Y;

let y be Element of X2;

correctness

coherence

(curry' f) . y is Function of X1,Y;

end;
let f be Function of [:X1,X2:],Y;

let y be Element of X2;

correctness

coherence

(curry' f) . y is Function of X1,Y;

proof end;

:: deftheorem defines Proj WAYBEL24:def 2 :

for X1, X2, Y being non empty RelStr

for f being Function of [:X1,X2:],Y

for y being Element of X2 holds Proj (f,y) = (curry' f) . y;

for X1, X2, Y being non empty RelStr

for f being Function of [:X1,X2:],Y

for y being Element of X2 holds Proj (f,y) = (curry' f) . y;

theorem Th8: :: WAYBEL24:8

for X1, X2, Y being non empty RelStr

for f being Function of [:X1,X2:],Y

for y being Element of X2

for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)

for f being Function of [:X1,X2:],Y

for y being Element of X2

for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)

proof end;

theorem Th9: :: WAYBEL24:9

for R, S, T being non empty RelStr

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

for a being Element of R

for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a

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

for a being Element of R

for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a

proof end;

registration

let S be non empty RelStr ;

let T be non empty reflexive RelStr ;

ex b_{1} being Function of S,T st b_{1} is antitone

end;
let T be non empty reflexive RelStr ;

cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total antitone for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

proof end;

theorem Th10: :: WAYBEL24:10

for R, S, T being non empty reflexive RelStr

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

for a being Element of R

for b being Element of S st f is monotone holds

( Proj (f,a) is monotone & Proj (f,b) is monotone )

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

for a being Element of R

for b being Element of S st f is monotone holds

( Proj (f,a) is monotone & Proj (f,b) is monotone )

proof end;

theorem Th11: :: WAYBEL24:11

for R, S, T being non empty reflexive RelStr

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

for a being Element of R

for b being Element of S st f is antitone holds

( Proj (f,a) is antitone & Proj (f,b) is antitone )

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

for a being Element of R

for b being Element of S st f is antitone holds

( Proj (f,a) is antitone & Proj (f,b) is antitone )

proof end;

registration

let R, S, T be non empty reflexive RelStr ;

let f be monotone Function of [:R,S:],T;

let a be Element of R;

coherence

Proj (f,a) is monotone by Th10;

end;
let f be monotone Function of [:R,S:],T;

let a be Element of R;

coherence

Proj (f,a) is monotone by Th10;

registration

let R, S, T be non empty reflexive RelStr ;

let f be monotone Function of [:R,S:],T;

let b be Element of S;

coherence

Proj (f,b) is monotone by Th10;

end;
let f be monotone Function of [:R,S:],T;

let b be Element of S;

coherence

Proj (f,b) is monotone by Th10;

registration

let R, S, T be non empty reflexive RelStr ;

let f be antitone Function of [:R,S:],T;

let a be Element of R;

coherence

Proj (f,a) is antitone by Th11;

end;
let f be antitone Function of [:R,S:],T;

let a be Element of R;

coherence

Proj (f,a) is antitone by Th11;

registration

let R, S, T be non empty reflexive RelStr ;

let f be antitone Function of [:R,S:],T;

let b be Element of S;

coherence

Proj (f,b) is antitone by Th11;

end;
let f be antitone Function of [:R,S:],T;

let b be Element of S;

coherence

Proj (f,b) is antitone by Th11;

theorem Th12: :: WAYBEL24:12

for R, S, T being LATTICE

for f being Function of [:R,S:],T st ( for a being Element of R

for b being Element of S holds

( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds

f is monotone

for f being Function of [:R,S:],T st ( for a being Element of R

for b being Element of S holds

( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds

f is monotone

proof end;

theorem :: WAYBEL24:13

for R, S, T being LATTICE

for f being Function of [:R,S:],T st ( for a being Element of R

for b being Element of S holds

( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds

f is antitone

for f being Function of [:R,S:],T st ( for a being Element of R

for b being Element of S holds

( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds

f is antitone

proof end;

theorem Th14: :: WAYBEL24:14

for R, S, T being LATTICE

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

for b being Element of S

for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]

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

for b being Element of S

for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]

proof end;

theorem Th15: :: WAYBEL24:15

for R, S, T being LATTICE

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

for b being Element of R

for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]

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

for b being Element of R

for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]

proof end;

theorem :: WAYBEL24:16

for R, S, T being LATTICE

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

for a being Element of R

for b being Element of S st f is directed-sups-preserving holds

( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )

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

for a being Element of R

for b being Element of S st f is directed-sups-preserving holds

( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )

proof end;

theorem Th17: :: WAYBEL24:17

for R, S, T being LATTICE

for f being monotone Function of [:R,S:],T

for a being Element of R

for b being Element of S

for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds

f . [a,b] <= sup (f .: X)

for f being monotone Function of [:R,S:],T

for a being Element of R

for b being Element of S

for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds

f . [a,b] <= sup (f .: X)

proof end;

theorem :: WAYBEL24:18

for R, S, T being complete LATTICE

for f being Function of [:R,S:],T st ( for a being Element of R

for b being Element of S holds

( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds

f is directed-sups-preserving

for f being Function of [:R,S:],T st ( for a being Element of R

for b being Element of S holds

( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds

f is directed-sups-preserving

proof end;

theorem Th19: :: WAYBEL24:19

for S being set

for T being non empty RelStr

for f being set holds

( f is Element of (T |^ S) iff f is Function of S, the carrier of T )

for T being non empty RelStr

for f being set holds

( f is Element of (T |^ S) iff f is Function of S, the carrier of T )

proof end;

definition

let S be TopStruct ;

let T be non empty TopRelStr ;

ex b_{1} being strict RelStr st

( b_{1} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{1} iff ex f being Function of S,T st

( x = f & f is continuous ) ) ) )

for b_{1}, b_{2} being strict RelStr st b_{1} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{1} iff ex f being Function of S,T st

( x = f & f is continuous ) ) ) & b_{2} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{2} iff ex f being Function of S,T st

( x = f & f is continuous ) ) ) holds

b_{1} = b_{2}

end;
let T be non empty TopRelStr ;

func ContMaps (S,T) -> strict RelStr means :Def3: :: WAYBEL24:def 3

( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of it iff ex f being Function of S,T st

( x = f & f is continuous ) ) ) );

existence ( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of it iff ex f being Function of S,T st

( x = f & f is continuous ) ) ) );

ex b

( b

( x in the carrier of b

( x = f & f is continuous ) ) ) )

proof end;

uniqueness for b

( x in the carrier of b

( x = f & f is continuous ) ) ) & b

( x in the carrier of b

( x = f & f is continuous ) ) ) holds

b

proof end;

:: deftheorem Def3 defines ContMaps WAYBEL24:def 3 :

for S being TopStruct

for T being non empty TopRelStr

for b_{3} being strict RelStr holds

( b_{3} = ContMaps (S,T) iff ( b_{3} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{3} iff ex f being Function of S,T st

( x = f & f is continuous ) ) ) ) );

for S being TopStruct

for T being non empty TopRelStr

for b

( b

( x in the carrier of b

( x = f & f is continuous ) ) ) ) );

registration

let S be non empty TopSpace;

let T be non empty TopSpace-like TopRelStr ;

coherence

not ContMaps (S,T) is empty

end;
let T be non empty TopSpace-like TopRelStr ;

coherence

not ContMaps (S,T) is empty

proof end;

registration

let S be non empty TopSpace;

let T be non empty TopSpace-like TopRelStr ;

coherence

ContMaps (S,T) is constituted-Functions

end;
let T be non empty TopSpace-like TopRelStr ;

coherence

ContMaps (S,T) is constituted-Functions

proof end;

theorem Th20: :: WAYBEL24:20

for S being non empty TopSpace

for T being non empty TopSpace-like reflexive TopRelStr

for x, y being Element of (ContMaps (S,T)) holds

( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )

for T being non empty TopSpace-like reflexive TopRelStr

for x, y being Element of (ContMaps (S,T)) holds

( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )

proof end;

theorem Th21: :: WAYBEL24:21

for S being non empty TopSpace

for T being non empty TopSpace-like reflexive TopRelStr

for x being set holds

( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )

for T being non empty TopSpace-like reflexive TopRelStr

for x being set holds

( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )

proof end;

registration

let S be non empty TopSpace;

let T be non empty TopSpace-like reflexive TopRelStr ;

coherence

ContMaps (S,T) is reflexive

end;
let T be non empty TopSpace-like reflexive TopRelStr ;

coherence

ContMaps (S,T) is reflexive

proof end;

registration

let S be non empty TopSpace;

let T be non empty TopSpace-like transitive TopRelStr ;

coherence

ContMaps (S,T) is transitive

end;
let T be non empty TopSpace-like transitive TopRelStr ;

coherence

ContMaps (S,T) is transitive

proof end;

registration

let S be non empty TopSpace;

let T be non empty TopSpace-like antisymmetric TopRelStr ;

coherence

ContMaps (S,T) is antisymmetric

end;
let T be non empty TopSpace-like antisymmetric TopRelStr ;

coherence

ContMaps (S,T) is antisymmetric

proof end;

registration
end;

theorem :: WAYBEL24:22

for S being non empty 1-sorted

for T being complete LATTICE

for f, g, h being Function of S,T

for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds

h . i = sup {(f . i),(g . i)}

for T being complete LATTICE

for f, g, h being Function of S,T

for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds

h . i = sup {(f . i),(g . i)}

proof end;

theorem Th23: :: WAYBEL24:23

for I being non empty set

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

for X being Subset of (product J)

for i being Element of I holds (inf X) . i = inf (pi (X,i))

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

for X being Subset of (product J)

for i being Element of I holds (inf X) . i = inf (pi (X,i))

proof end;

theorem :: WAYBEL24:24

for S being non empty 1-sorted

for T being complete LATTICE

for f, g, h being Function of S,T

for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds

h . i = inf {(f . i),(g . i)}

for T being complete LATTICE

for f, g, h being Function of S,T

for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds

h . i = inf {(f . i),(g . i)}

proof end;

theorem Th25: :: WAYBEL24:25

for S being non empty RelStr

for T being complete LATTICE

for F being non empty Subset of (T |^ the carrier of S)

for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)

for T being complete LATTICE

for F being non empty Subset of (T |^ the carrier of S)

for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)

proof end;

theorem Th26: :: WAYBEL24:26

for S, T being complete TopLattice

for F being non empty Subset of (ContMaps (S,T))

for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)

for F being non empty Subset of (ContMaps (S,T))

for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)

proof end;

theorem Th27: :: WAYBEL24:27

for S being non empty RelStr

for T being complete LATTICE

for F being non empty Subset of (T |^ the carrier of S)

for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }

for T being complete LATTICE

for F being non empty Subset of (T |^ the carrier of S)

for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }

proof end;

theorem Th28: :: WAYBEL24:28

for S, T being complete Scott TopLattice

for F being non empty Subset of (ContMaps (S,T))

for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }

for F being non empty Subset of (ContMaps (S,T))

for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }

proof end;

scheme :: WAYBEL24:sch 5

FuncFraenkelS{ F_{1}() -> non empty TopRelStr , F_{2}() -> non empty TopRelStr , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Function, P_{1}[ set ] } :

FuncFraenkelS{ F

F_{4}() .: { F_{3}(x) where x is Element of F_{1}() : P_{1}[x] } = { (F_{4}() . F_{3}(x)) where x is Element of F_{1}() : P_{1}[x] }

provided
proof end;

Lm1: for S being non empty RelStr

for D being non empty Subset of S holds D = { i where i is Element of S : i in D }

proof end;

theorem Th29: :: WAYBEL24:29

for S, T being complete Scott TopLattice

for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T

for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T

proof end;

theorem Th30: :: WAYBEL24:30

for S, T being complete Scott TopLattice

for F being non empty Subset of (ContMaps (S,T))

for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T)

for F being non empty Subset of (ContMaps (S,T))

for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T)

proof end;

theorem Th31: :: WAYBEL24:31

for S, T being complete Scott TopLattice

for F being non empty Subset of (ContMaps (S,T))

for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)

for F being non empty Subset of (ContMaps (S,T))

for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)

proof end;

theorem Th32: :: WAYBEL24:32

for S, T being complete Scott TopLattice

for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))

for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))

proof end;

theorem Th33: :: WAYBEL24:33

for S being non empty RelStr

for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)

for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)

proof end;

theorem :: WAYBEL24:34

for S being non empty RelStr

for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T)

for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T)

proof end;

registration

let S be non empty reflexive RelStr ;

let T be complete LATTICE;

let a be Element of T;

coherence

S --> a is directed-sups-preserving

end;
let T be complete LATTICE;

let a be Element of T;

coherence

S --> a is directed-sups-preserving

proof end;

theorem Th35: :: WAYBEL24:35

for S, T being complete Scott TopLattice holds ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S

proof end;

registration
end;