:: by Jaros{\l}aw Gryko and Artur Korni{\l}owicz

::

:: Received June 22, 1999

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

theorem :: YELLOW14:3

theorem :: YELLOW14:4

theorem :: YELLOW14:5

theorem :: YELLOW14:6

definition

let S be non empty reflexive RelStr ;

let T be non empty RelStr ;

let f be Function of S,T;

( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X ) ;

end;
let T be non empty RelStr ;

let f be Function of S,T;

redefine attr f is directed-sups-preserving means :: YELLOW14:def 1

for X being non empty directed Subset of S holds f preserves_sup_of X;

compatibility for X being non empty directed Subset of S holds f preserves_sup_of X;

( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X ) ;

:: deftheorem defines directed-sups-preserving YELLOW14:def 1 :

for S being non empty reflexive RelStr

for T being non empty RelStr

for f being Function of S,T holds

( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X );

for S being non empty reflexive RelStr

for T being non empty RelStr

for f being Function of S,T holds

( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X );

:: deftheorem Def2 defines Function-yielding YELLOW14:def 2 :

for R being 1-sorted

for N being NetStr over R holds

( N is Function-yielding iff the mapping of N is Function-yielding );

for R being 1-sorted

for N being NetStr over R holds

( N is Function-yielding iff the mapping of N is Function-yielding );

registration

existence

ex b_{1} being 1-sorted st

( not b_{1} is empty & b_{1} is constituted-Functions )

end;
ex b

( not b

proof end;

registration

existence

ex b_{1} being RelStr st

( b_{1} is strict & not b_{1} is empty & b_{1} is constituted-Functions )

end;
ex b

( b

proof end;

registration

let R be constituted-Functions 1-sorted ;

coherence

for b_{1} being NetStr over R holds b_{1} is Function-yielding

end;
coherence

for b

proof end;

registration

let R be constituted-Functions 1-sorted ;

existence

ex b_{1} being NetStr over R st

( b_{1} is strict & b_{1} is Function-yielding )

end;
existence

ex b

( b

proof end;

registration

let R be non empty constituted-Functions 1-sorted ;

existence

ex b_{1} being NetStr over R st

( b_{1} is strict & not b_{1} is empty & b_{1} is Function-yielding )

end;
existence

ex b

( b

proof end;

registration

let R be constituted-Functions 1-sorted ;

let N be Function-yielding NetStr over R;

coherence

the mapping of N is Function-yielding by Def2;

end;
let N be Function-yielding NetStr over R;

coherence

the mapping of N is Function-yielding by Def2;

registration

let R be non empty constituted-Functions 1-sorted ;

existence

ex b_{1} being net of R st

( b_{1} is strict & b_{1} is Function-yielding )

end;
existence

ex b

( b

proof end;

registration

let S be non empty 1-sorted ;

let N be non empty NetStr over S;

coherence

not rng the mapping of N is empty ;

end;
let N be non empty NetStr over S;

coherence

not rng the mapping of N is empty ;

registration

let S be non empty 1-sorted ;

let N be non empty NetStr over S;

coherence

not rng (netmap (N,S)) is empty ;

end;
let N be non empty NetStr over S;

coherence

not rng (netmap (N,S)) is empty ;

theorem :: YELLOW14:7

for A, B, C being non empty RelStr

for f being Function of B,C

for g, h being Function of A,B st g <= h & f is monotone holds

f * g <= f * h

for f being Function of B,C

for g, h being Function of A,B st g <= h & f is monotone holds

f * g <= f * h

proof end;

theorem :: YELLOW14:8

for S being non empty TopSpace

for T being non empty TopSpace-like TopRelStr

for f, g being Function of S,T

for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds

( x <= y iff f <= g )

for T being non empty TopSpace-like TopRelStr

for f, g being Function of S,T

for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds

( x <= y iff f <= g )

proof end;

definition

let I be non empty set ;

let R be non empty RelStr ;

let f be Element of (R |^ I);

let i be Element of I;

:: original: .

redefine func f . i -> Element of R;

coherence

f . i is Element of R

end;
let R be non empty RelStr ;

let f be Element of (R |^ I);

let i be Element of I;

:: original: .

redefine func f . i -> Element of R;

coherence

f . i is Element of R

proof end;

registration

let S, T be RelStr ;

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

b_{1} is onto
by Th9;

end;
cluster Function-like quasi_total isomorphic -> onto for Element of K6(K7( the carrier of S, the carrier of T));

coherence for b

b

theorem Th10: :: YELLOW14:10

for S, T being non empty RelStr

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

f /" is isomorphic

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

f /" is isomorphic

proof end;

registration
end;

theorem :: YELLOW14:16

for S, T being non empty RelStr

for A being Subset of S

for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds

ex_sup_of f .: A,T

for A being Subset of S

for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds

ex_sup_of f .: A,T

proof end;

theorem :: YELLOW14:17

for S, T being non empty RelStr

for A being Subset of S

for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds

ex_inf_of f .: A,T

for A being Subset of S

for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds

ex_inf_of f .: A,T

proof end;

theorem :: YELLOW14:18

for S, T being TopStruct st ( S,T are_homeomorphic or ex f being Function of S,T st

( dom f = [#] S & rng f = [#] T ) ) holds

( S is empty iff T is empty )

( dom f = [#] S & rng f = [#] T ) ) holds

( S is empty iff T is empty )

proof end;

theorem :: YELLOW14:19

for T being non empty TopSpace holds T, TopStruct(# the carrier of T, the topology of T #) are_homeomorphic

proof end;

registration

let T be non empty reflexive Scott TopRelStr ;

coherence

for b_{1} being Subset of T st b_{1} is open holds

( b_{1} is inaccessible & b_{1} is upper )
by WAYBEL11:def 4;

coherence

for b_{1} being Subset of T st b_{1} is inaccessible & b_{1} is upper holds

b_{1} is open
by WAYBEL11:def 4;

end;
coherence

for b

( b

coherence

for b

b

theorem :: YELLOW14:20

for T being TopStruct

for x, y being Point of T

for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds

x in Cl Y

for x, y being Point of T

for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds

x in Cl Y

proof end;

theorem :: YELLOW14:21

for T being TopStruct

for x, y being Point of T

for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds

y in V

for x, y being Point of T

for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds

y in V

proof end;

theorem :: YELLOW14:22

for T being TopStruct

for x, y being Point of T

for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds

y in V ) holds

Cl X c= Cl Y

for x, y being Point of T

for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds

y in V ) holds

Cl X c= Cl Y

proof end;

theorem Th23: :: YELLOW14:23

for S, T being non empty TopSpace

for A being irreducible Subset of S

for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds

B is irreducible

for A being irreducible Subset of S

for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds

B is irreducible

proof end;

theorem Th24: :: YELLOW14:24

for S, T being non empty TopSpace

for a being Point of S

for b being Point of T

for A being Subset of S

for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds

b is_dense_point_of B

for a being Point of S

for b being Point of T

for A being Subset of S

for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds

b is_dense_point_of B

proof end;

theorem Th25: :: YELLOW14:25

for S, T being TopStruct

for A being Subset of S

for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds

B is compact

for A being Subset of S

for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds

B is compact

proof end;

theorem :: YELLOW14:26

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 sober holds

T is sober

T is sober

proof end;

theorem :: YELLOW14:27

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-compact holds

T is locally-compact

T is locally-compact

proof end;

theorem :: YELLOW14:28

for S, T being TopStruct st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is compact holds

T is compact

T is compact

proof end;

definition

let I be non empty set ;

let T be non empty TopSpace;

let x be Point of (product (I --> T));

let i be Element of I;

:: original: .

redefine func x . i -> Element of T;

coherence

x . i is Element of T

end;
let T be non empty TopSpace;

let x be Point of (product (I --> T));

let i be Element of I;

:: original: .

redefine func x . i -> Element of T;

coherence

x . i is Element of T

proof end;

theorem Th29: :: YELLOW14:29

for M being non empty set

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

for x, y being Point of (product J) holds

( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )

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

for x, y being Point of (product J) holds

( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )

proof end;

theorem :: YELLOW14:30

for M being non empty set

for T being non empty TopSpace

for x, y being Point of (product (M --> T)) holds

( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )

for T being non empty TopSpace

for x, y being Point of (product (M --> T)) holds

( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )

proof end;

theorem Th31: :: YELLOW14:31

for M being non empty set

for i being Element of M

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

for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}

for i being Element of M

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

for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}

proof end;

theorem :: YELLOW14:32

for M being non empty set

for i being Element of M

for T being non empty TopSpace

for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}

for i being Element of M

for T being non empty TopSpace

for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}

proof end;

theorem :: YELLOW14:33

for X, Y being non empty TopStruct

for f being Function of X,Y

for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds

TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)

for f being Function of X,Y

for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds

TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)

proof end;

theorem :: YELLOW14:34

for X, Y being non empty TopSpace

for f being Function of X,Y st corestr f is continuous holds

f is continuous

for f being Function of X,Y st corestr f is continuous holds

f is continuous

proof end;

registration

let X be non empty TopSpace;

let Y be non empty SubSpace of X;

coherence

incl Y is continuous by TMAP_1:87;

end;
let Y be non empty SubSpace of X;

coherence

incl Y is continuous by TMAP_1:87;

theorem :: YELLOW14:35

for T being non empty TopSpace

for f being Function of T,T st f * f = f holds

(corestr f) * (incl (Image f)) = id (Image f)

for f being Function of T,T st f * f = f holds

(corestr f) * (incl (Image f)) = id (Image f)

proof end;

theorem :: YELLOW14:36

for Y being non empty TopSpace

for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism

for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism

proof end;

theorem Th37: :: YELLOW14:37

for M being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds

product J is T_0

for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds

product J is T_0

proof end;

registration

let I be non empty set ;

let T be non empty T_0 TopSpace;

coherence

product (I --> T) is T_0

end;
let T be non empty T_0 TopSpace;

coherence

product (I --> T) is T_0

proof end;

theorem Th38: :: YELLOW14:38

for M being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds

( J . i is T_1 & J . i is TopSpace-like ) ) holds

product J is T_1

for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds

( J . i is T_1 & J . i is TopSpace-like ) ) holds

product J is T_1

proof end;

registration

let I be non empty set ;

let T be non empty T_1 TopSpace;

coherence

product (I --> T) is T_1

end;
let T be non empty T_1 TopSpace;

coherence

product (I --> T) is T_1

proof end;