:: by Jaros{\l}aw Gryko

::

:: Received April 17, 1998

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

theorem Th1: :: WAYBEL18:1

for X being set

for A, B being Subset-Family of X st ( B = A \ {{}} or A = B \/ {{}} ) holds

UniCl A = UniCl B

for A, B being Subset-Family of X st ( B = A \ {{}} or A = B \/ {{}} ) holds

UniCl A = UniCl B

proof end;

theorem Th2: :: WAYBEL18:2

for T being TopSpace

for K being Subset-Family of T holds

( K is Basis of T iff K \ {{}} is Basis of T )

for K being Subset-Family of T holds

( K is Basis of T iff K \ {{}} is Basis of T )

proof end;

definition

let F be Relation;

end;
attr F is TopStruct-yielding means :Def1: :: WAYBEL18:def 1

for x being set st x in rng F holds

x is TopStruct ;

for x being set st x in rng F holds

x is TopStruct ;

:: deftheorem Def1 defines TopStruct-yielding WAYBEL18:def 1 :

for F being Relation holds

( F is TopStruct-yielding iff for x being set st x in rng F holds

x is TopStruct );

for F being Relation holds

( F is TopStruct-yielding iff for x being set st x in rng F holds

x is TopStruct );

registration

coherence

for b_{1} being Function st b_{1} is TopStruct-yielding holds

b_{1} is 1-sorted-yielding

end;
for b

b

proof end;

registration

let I be set ;

existence

ex b_{1} being ManySortedSet of I st b_{1} is TopStruct-yielding

end;
existence

ex b

proof end;

registration

let I be set ;

ex b_{1} being ManySortedSet of I st

( b_{1} is TopStruct-yielding & b_{1} is non-Empty )

end;
cluster Relation-like I -defined Function-like total non-Empty TopStruct-yielding for ManySortedSet of ;

existence ex b

( b

proof end;

definition

let J be non empty set ;

let A be TopStruct-yielding ManySortedSet of J;

let j be Element of J;

:: original: .

redefine func A . j -> TopStruct ;

coherence

A . j is TopStruct

end;
let A be TopStruct-yielding ManySortedSet of J;

let j be Element of J;

:: original: .

redefine func A . j -> TopStruct ;

coherence

A . j is TopStruct

proof end;

definition

let I be set ;

let J be TopStruct-yielding ManySortedSet of I;

ex b_{1} being Subset-Family of (product (Carrier J)) st

for x being Subset of (product (Carrier J)) holds

( x in b_{1} iff ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) )

for b_{1}, b_{2} being Subset-Family of (product (Carrier J)) st ( for x being Subset of (product (Carrier J)) holds

( x in b_{1} iff ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) & ( for x being Subset of (product (Carrier J)) holds

( x in b_{2} iff ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) holds

b_{1} = b_{2}

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

func product_prebasis J -> Subset-Family of (product (Carrier J)) means :Def2: :: WAYBEL18:def 2

for x being Subset of (product (Carrier J)) holds

( x in it iff ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) );

existence for x being Subset of (product (Carrier J)) holds

( x in it iff ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) );

ex b

for x being Subset of (product (Carrier J)) holds

( x in b

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) )

proof end;

uniqueness for b

( x in b

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) & ( for x being Subset of (product (Carrier J)) holds

( x in b

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) ) holds

b

proof end;

:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :

for I being set

for J being TopStruct-yielding ManySortedSet of I

for b_{3} being Subset-Family of (product (Carrier J)) holds

( b_{3} = product_prebasis J iff for x being Subset of (product (Carrier J)) holds

( x in b_{3} iff ex i being set ex T being TopStruct ex V being Subset of T st

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) );

for I being set

for J being TopStruct-yielding ManySortedSet of I

for b

( b

( x in b

( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) );

theorem Th3: :: WAYBEL18:3

for X being set

for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like

for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like

proof end;

definition

let I be set ;

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

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = product (Carrier J) & product_prebasis J is prebasis of b_{1} )

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = product (Carrier J) & product_prebasis J is prebasis of b_{1} & the carrier of b_{2} = product (Carrier J) & product_prebasis J is prebasis of b_{2} holds

b_{1} = b_{2}

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

func product J -> strict TopSpace means :Def3: :: WAYBEL18:def 3

( the carrier of it = product (Carrier J) & product_prebasis J is prebasis of it );

existence ( the carrier of it = product (Carrier J) & product_prebasis J is prebasis of it );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines product WAYBEL18:def 3 :

for I being set

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

for b_{3} being strict TopSpace holds

( b_{3} = product J iff ( the carrier of b_{3} = product (Carrier J) & product_prebasis J is prebasis of b_{3} ) );

for I being set

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

for b

( b

registration

let I be set ;

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

coherence

not product J is empty

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

coherence

not product J is empty

proof end;

definition

let I be non empty set ;

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

let i be Element of I;

:: original: .

redefine func J . i -> non empty TopStruct ;

coherence

J . i is non empty TopStruct

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

let i be Element of I;

:: original: .

redefine func J . i -> non empty TopStruct ;

coherence

J . i is non empty TopStruct

proof end;

registration

let I be set ;

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

coherence

product J is constituted-Functions

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

coherence

product J is constituted-Functions

proof end;

definition

let I be non empty set ;

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

let x be Element of (product J);

let i be Element of I;

:: original: .

redefine func x . i -> Element of (J . i);

coherence

x . i is Element of (J . i)

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

let x be Element of (product J);

let i be Element of I;

:: original: .

redefine func x . i -> Element of (J . i);

coherence

x . i is Element of (J . i)

proof end;

definition

let I be non empty set ;

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

let i be Element of I;

coherence

proj ((Carrier J),i) is Function of (product J),(J . i)

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

let i be Element of I;

coherence

proj ((Carrier J),i) is Function of (product J),(J . i)

proof end;

:: deftheorem defines proj WAYBEL18:def 4 :

for I being non empty set

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

for i being Element of I holds proj (J,i) = proj ((Carrier J),i);

for I being non empty set

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

for i being Element of I holds proj (J,i) = proj ((Carrier J),i);

theorem Th4: :: WAYBEL18:4

for I being non empty set

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

for i being Element of I

for P being Subset of (J . i) holds (proj (J,i)) " P = product ((Carrier J) +* (i,P))

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

for i being Element of I

for P being Subset of (J . i) holds (proj (J,i)) " P = product ((Carrier J) +* (i,P))

proof end;

theorem Th5: :: WAYBEL18:5

for I being non empty set

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

for i being Element of I holds proj (J,i) is continuous

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

for i being Element of I holds proj (J,i) is continuous

proof end;

theorem Th6: :: WAYBEL18:6

for X being non empty TopSpace

for I being non empty set

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

for f being Function of X,(product J) holds

( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )

for I being non empty set

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

for f being Function of X,(product J) holds

( f is continuous iff for i being Element of I holds (proj (J,i)) * f is continuous )

proof end;

definition

let Z be TopStruct ;

end;
attr Z is injective means :: WAYBEL18:def 5

for X being non empty TopSpace

for f being Function of X,Z st f is continuous holds

for Y being non empty TopSpace st X is SubSpace of Y holds

ex g being Function of Y,Z st

( g is continuous & g | the carrier of X = f );

for X being non empty TopSpace

for f being Function of X,Z st f is continuous holds

for Y being non empty TopSpace st X is SubSpace of Y holds

ex g being Function of Y,Z st

( g is continuous & g | the carrier of X = f );

:: deftheorem defines injective WAYBEL18:def 5 :

for Z being TopStruct holds

( Z is injective iff for X being non empty TopSpace

for f being Function of X,Z st f is continuous holds

for Y being non empty TopSpace st X is SubSpace of Y holds

ex g being Function of Y,Z st

( g is continuous & g | the carrier of X = f ) );

for Z being TopStruct holds

( Z is injective iff for X being non empty TopSpace

for f being Function of X,Z st f is continuous holds

for Y being non empty TopSpace st X is SubSpace of Y holds

ex g being Function of Y,Z st

( g is continuous & g | the carrier of X = f ) );

theorem Th7: :: WAYBEL18:7

for I being non empty set

for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds

product J is injective

for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is injective ) holds

product J is injective

proof end;

theorem :: WAYBEL18:8

for T being non empty TopSpace st T is injective holds

for S being non empty SubSpace of T st S is_a_retract_of T holds

S is injective

for S being non empty SubSpace of T st S is_a_retract_of T holds

S is injective

proof end;

definition

let X be 1-sorted ;

let Y be TopStruct ;

let f be Function of X,Y;

coherence

Y | (rng f) is SubSpace of Y ;

end;
let Y be TopStruct ;

let f be Function of X,Y;

coherence

Y | (rng f) is SubSpace of Y ;

:: deftheorem defines Image WAYBEL18:def 6 :

for X being 1-sorted

for Y being TopStruct

for f being Function of X,Y holds Image f = Y | (rng f);

for X being 1-sorted

for Y being TopStruct

for f being Function of X,Y holds Image f = Y | (rng f);

registration

let X be non empty 1-sorted ;

let Y be non empty TopStruct ;

let f be Function of X,Y;

coherence

not Image f is empty ;

end;
let Y be non empty TopStruct ;

let f be Function of X,Y;

coherence

not Image f is empty ;

theorem Th9: :: WAYBEL18:9

for X being 1-sorted

for Y being TopStruct

for f being Function of X,Y holds the carrier of (Image f) = rng f

for Y being TopStruct

for f being Function of X,Y holds the carrier of (Image f) = rng f

proof end;

definition

let X be 1-sorted ;

let Y be non empty TopStruct ;

let f be Function of X,Y;

coherence

f is Function of X,(Image f)

end;
let Y be non empty TopStruct ;

let f be Function of X,Y;

coherence

f is Function of X,(Image f)

proof end;

:: deftheorem defines corestr WAYBEL18:def 7 :

for X being 1-sorted

for Y being non empty TopStruct

for f being Function of X,Y holds corestr f = f;

for X being 1-sorted

for Y being non empty TopStruct

for f being Function of X,Y holds corestr f = f;

theorem Th10: :: WAYBEL18:10

for X, Y being non empty TopSpace

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

corestr f is continuous

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

corestr f is continuous

proof end;

registration

let X be 1-sorted ;

let Y be non empty TopStruct ;

let f be Function of X,Y;

coherence

corestr f is onto

end;
let Y be non empty TopStruct ;

let f be Function of X,Y;

coherence

corestr f is onto

proof end;

definition

let X, Y be TopStruct ;

end;
pred X is_Retract_of Y means :: WAYBEL18:def 8

ex f being Function of Y,Y st

( f is continuous & f * f = f & Image f,X are_homeomorphic );

ex f being Function of Y,Y st

( f is continuous & f * f = f & Image f,X are_homeomorphic );

:: deftheorem defines is_Retract_of WAYBEL18:def 8 :

for X, Y being TopStruct holds

( X is_Retract_of Y iff ex f being Function of Y,Y st

( f is continuous & f * f = f & Image f,X are_homeomorphic ) );

for X, Y being TopStruct holds

( X is_Retract_of Y iff ex f being Function of Y,Y st

( f is continuous & f * f = f & Image f,X are_homeomorphic ) );

theorem Th11: :: WAYBEL18:11

for T, S being non empty TopSpace st T is injective holds

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

T is_Retract_of S

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

T is_Retract_of S

proof end;

definition

ex b_{1} being strict TopStruct st

( the carrier of b_{1} = {0,1} & the topology of b_{1} = {{},{1},{0,1}} )

for b_{1}, b_{2} being strict TopStruct st the carrier of b_{1} = {0,1} & the topology of b_{1} = {{},{1},{0,1}} & the carrier of b_{2} = {0,1} & the topology of b_{2} = {{},{1},{0,1}} holds

b_{1} = b_{2}
;

end;

func Sierpinski_Space -> strict TopStruct means :Def9: :: WAYBEL18:def 9

( the carrier of it = {0,1} & the topology of it = {{},{1},{0,1}} );

existence ( the carrier of it = {0,1} & the topology of it = {{},{1},{0,1}} );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def 9 :

for b_{1} being strict TopStruct holds

( b_{1} = Sierpinski_Space iff ( the carrier of b_{1} = {0,1} & the topology of b_{1} = {{},{1},{0,1}} ) );

for b

( b

registration
end;

Lm1: Sierpinski_Space is T_0

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let I be non empty set ;

let L be non empty antisymmetric RelStr ;

coherence

product (I --> L) is antisymmetric

end;
let L be non empty antisymmetric RelStr ;

coherence

product (I --> L) is antisymmetric

proof end;

registration

let I be non empty set ;

let L be non empty transitive RelStr ;

coherence

product (I --> L) is transitive

end;
let L be non empty transitive RelStr ;

coherence

product (I --> L) is transitive

proof end;

theorem :: WAYBEL18:12

for T being Scott TopAugmentation of BoolePoset {0} holds the topology of T = the topology of Sierpinski_Space

proof end;

theorem Th13: :: WAYBEL18:13

for I being non empty set holds { (product ((Carrier (I --> Sierpinski_Space)) +* (i,{1}))) where i is Element of I : verum } is prebasis of (product (I --> Sierpinski_Space))

proof end;

registration

let I be non empty set ;

let L be complete LATTICE;

coherence

( product (I --> L) is with_suprema & product (I --> L) is complete )

end;
let L be complete LATTICE;

coherence

( product (I --> L) is with_suprema & product (I --> L) is complete )

proof end;

registration

let I be non empty set ;

let X be lower-bounded algebraic LATTICE;

coherence

product (I --> X) is algebraic

end;
let X be lower-bounded algebraic LATTICE;

coherence

product (I --> X) is algebraic

proof end;

theorem Th14: :: WAYBEL18:14

for X being non empty set ex f being Function of (BoolePoset X),(product (X --> (BoolePoset {0}))) st

( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )

( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )

proof end;

theorem Th15: :: WAYBEL18:15

for I being non empty set

for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds the topology of T = the topology of (product (I --> Sierpinski_Space))

for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds the topology of T = the topology of (product (I --> Sierpinski_Space))

proof end;

theorem Th16: :: WAYBEL18:16

for T, S being non empty TopSpace st the carrier of T = the carrier of S & the topology of T = the topology of S & T is injective holds

S is injective

S is injective

proof end;

theorem :: WAYBEL18:17

for I being non empty set

for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds T is injective

for T being Scott TopAugmentation of product (I --> (BoolePoset {0})) holds T is injective

proof end;

theorem Th18: :: WAYBEL18:18

for T being T_0-TopSpace ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism

proof end;

theorem :: WAYBEL18:19

for T being T_0-TopSpace st T is injective holds

ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space)

ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space)

proof end;