:: by Beata Padlewska and Agata Darmochwa\l

::

:: Received April 14, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct TopStruct -> 1-sorted ;

aggr TopStruct(# carrier, topology #) -> TopStruct ;

sel topology c_{1} -> Subset-Family of the carrier of c_{1};

end;
struct TopStruct -> 1-sorted ;

aggr TopStruct(# carrier, topology #) -> TopStruct ;

sel topology c

definition

let IT be TopStruct ;

end;
attr IT is TopSpace-like means :Def1: :: PRE_TOPC:def 1

( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds

union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds

a /\ b in the topology of IT ) );

( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds

union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds

a /\ b in the topology of IT ) );

:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def 1 :

for IT being TopStruct holds

( IT is TopSpace-like iff ( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds

union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds

a /\ b in the topology of IT ) ) );

for IT being TopStruct holds

( IT is TopSpace-like iff ( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds

union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds

a /\ b in the topology of IT ) ) );

registration

existence

ex b_{1} being TopStruct st

( not b_{1} is empty & b_{1} is strict & b_{1} is TopSpace-like )

end;
ex b

( not b

proof end;

theorem :: PRE_TOPC:5

for T being 1-sorted

for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds

Q = ([#] T) \ P

for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds

Q = ([#] T) \ P

proof end;

:: deftheorem Def2 defines open PRE_TOPC:def 2 :

for T being TopStruct

for P being Subset of T holds

( P is open iff P in the topology of T );

for T being TopStruct

for P being Subset of T holds

( P is open iff P in the topology of T );

:: deftheorem Def3 defines closed PRE_TOPC:def 3 :

for T being TopStruct

for P being Subset of T holds

( P is closed iff ([#] T) \ P is open );

for T being TopStruct

for P being Subset of T holds

( P is closed iff ([#] T) \ P is open );

definition

let T be TopStruct ;

ex b_{1} being TopStruct st

( [#] b_{1} c= [#] T & ( for P being Subset of b_{1} holds

( P in the topology of b_{1} iff ex Q being Subset of T st

( Q in the topology of T & P = Q /\ ([#] b_{1}) ) ) ) )

end;
mode SubSpace of T -> TopStruct means :Def4: :: PRE_TOPC:def 4

( [#] it c= [#] T & ( for P being Subset of it holds

( P in the topology of it iff ex Q being Subset of T st

( Q in the topology of T & P = Q /\ ([#] it) ) ) ) );

existence ( [#] it c= [#] T & ( for P being Subset of it holds

( P in the topology of it iff ex Q being Subset of T st

( Q in the topology of T & P = Q /\ ([#] it) ) ) ) );

ex b

( [#] b

( P in the topology of b

( Q in the topology of T & P = Q /\ ([#] b

proof end;

:: deftheorem Def4 defines SubSpace PRE_TOPC:def 4 :

for T, b_{2} being TopStruct holds

( b_{2} is SubSpace of T iff ( [#] b_{2} c= [#] T & ( for P being Subset of b_{2} holds

( P in the topology of b_{2} iff ex Q being Subset of T st

( Q in the topology of T & P = Q /\ ([#] b_{2}) ) ) ) ) );

for T, b

( b

( P in the topology of b

( Q in the topology of T & P = Q /\ ([#] b

Lm1: for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T

proof end;

registration
end;

registration

let T be non empty TopStruct ;

existence

ex b_{1} being SubSpace of T st

( b_{1} is strict & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

registration
end;

definition

let T be TopStruct ;

let P be Subset of T;

existence

ex b_{1} being strict SubSpace of T st [#] b_{1} = P

for b_{1}, b_{2} being strict SubSpace of T st [#] b_{1} = P & [#] b_{2} = P holds

b_{1} = b_{2}

end;
let P be Subset of T;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines | PRE_TOPC:def 5 :

for T being TopStruct

for P being Subset of T

for b_{3} being strict SubSpace of T holds

( b_{3} = T | P iff [#] b_{3} = P );

for T being TopStruct

for P being Subset of T

for b

( b

registration

let T be non empty TopStruct ;

let P be non empty Subset of T;

coherence

not T | P is empty

end;
let P be non empty Subset of T;

coherence

not T | P is empty

proof end;

registration

let T be TopSpace;

existence

ex b_{1} being SubSpace of T st

( b_{1} is TopSpace-like & b_{1} is strict )

end;
existence

ex b

( b

proof end;

theorem :: PRE_TOPC:7

for S being TopSpace

for P1, P2 being Subset of S

for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds

S | P1 = (S | P2) | P19

for P1, P2 being Subset of S

for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds

S | P1 = (S | P2) | P19

proof end;

theorem :: PRE_TOPC:9

for X being TopStruct

for Y being non empty TopStruct

for f being Function of X,Y

for P being Subset of X holds f | P is Function of (X | P),Y

for Y being non empty TopStruct

for f being Function of X,Y

for P being Subset of X holds f | P is Function of (X | P),Y

proof end;

definition

let S, T be TopStruct ;

let f be Function of S,T;

end;
let f be Function of S,T;

attr f is continuous means :Def6: :: PRE_TOPC:def 6

for P1 being Subset of T st P1 is closed holds

f " P1 is closed ;

for P1 being Subset of T st P1 is closed holds

f " P1 is closed ;

:: deftheorem Def6 defines continuous PRE_TOPC:def 6 :

for S, T being TopStruct

for f being Function of S,T holds

( f is continuous iff for P1 being Subset of T st P1 is closed holds

f " P1 is closed );

for S, T being TopStruct

for f being Function of S,T holds

( f is continuous iff for P1 being Subset of T st P1 is closed holds

f " P1 is closed );

theorem :: PRE_TOPC:10

for T1, T2, S1, S2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & S1 is SubSpace of T1 holds

S2 is SubSpace of T2

S2 is SubSpace of T2

proof end;

registration
end;

registration

let T be non empty TopSpace;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is closed )

end;
existence

ex b

( not b

proof end;

theorem Th13: :: PRE_TOPC:13

for T being TopStruct

for X9 being SubSpace of T

for B being Subset of X9 holds

( B is closed iff ex C being Subset of T st

( C is closed & C /\ ([#] X9) = B ) )

for X9 being SubSpace of T

for B being Subset of X9 holds

( B is closed iff ex C being Subset of T st

( C is closed & C /\ ([#] X9) = B ) )

proof end;

theorem Th14: :: PRE_TOPC:14

for GX being TopSpace

for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds

A is closed ) holds

meet F is closed

for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds

A is closed ) holds

meet F is closed

proof end;

::

:: The closure of a set

::

:: The closure of a set

::

definition

let GX be TopStruct ;

let A be Subset of GX;

ex b_{1} being Subset of GX st

for p being set st p in the carrier of GX holds

( p in b_{1} iff for G being Subset of GX st G is open & p in G holds

A meets G )

for b_{1}, b_{2} being Subset of GX st ( for p being set st p in the carrier of GX holds

( p in b_{1} iff for G being Subset of GX st G is open & p in G holds

A meets G ) ) & ( for p being set st p in the carrier of GX holds

( p in b_{2} iff for G being Subset of GX st G is open & p in G holds

A meets G ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Subset of GX st ( for p being set st p in the carrier of GX holds

( p in b_{1} iff for G being Subset of GX st G is open & p in G holds

b_{2} meets G ) ) holds

for p being set st p in the carrier of GX holds

( p in b_{1} iff for G being Subset of GX st G is open & p in G holds

b_{1} meets G )

end;
let A be Subset of GX;

func Cl A -> Subset of GX means :Def7: :: PRE_TOPC:def 7

for p being set st p in the carrier of GX holds

( p in it iff for G being Subset of GX st G is open & p in G holds

A meets G );

existence for p being set st p in the carrier of GX holds

( p in it iff for G being Subset of GX st G is open & p in G holds

A meets G );

ex b

for p being set st p in the carrier of GX holds

( p in b

A meets G )

proof end;

uniqueness for b

( p in b

A meets G ) ) & ( for p being set st p in the carrier of GX holds

( p in b

A meets G ) ) holds

b

proof end;

projectivity for b

( p in b

b

for p being set st p in the carrier of GX holds

( p in b

b

proof end;

:: deftheorem Def7 defines Cl PRE_TOPC:def 7 :

for GX being TopStruct

for A, b_{3} being Subset of GX holds

( b_{3} = Cl A iff for p being set st p in the carrier of GX holds

( p in b_{3} iff for G being Subset of GX st G is open & p in G holds

A meets G ) );

for GX being TopStruct

for A, b

( b

( p in b

A meets G ) );

theorem Th15: :: PRE_TOPC:15

for T being TopStruct

for A being Subset of T

for p being set st p in the carrier of T holds

( p in Cl A iff for C being Subset of T st C is closed & A c= C holds

p in C )

for A being Subset of T

for p being set st p in the carrier of T holds

( p in Cl A iff for C being Subset of T st C is closed & A c= C holds

p in C )

proof end;

theorem Th16: :: PRE_TOPC:16

for GX being TopSpace

for A being Subset of GX ex F being Subset-Family of GX st

( ( for C being Subset of GX holds

( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )

for A being Subset of GX ex F being Subset-Family of GX st

( ( for C being Subset of GX holds

( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )

proof end;

theorem :: PRE_TOPC:17

for T being TopStruct

for X9 being SubSpace of T

for A being Subset of T

for A1 being Subset of X9 st A = A1 holds

Cl A1 = (Cl A) /\ ([#] X9)

for X9 being SubSpace of T

for A being Subset of T

for A1 being Subset of X9 st A = A1 holds

Cl A1 = (Cl A) /\ ([#] X9)

proof end;

theorem Th22: :: PRE_TOPC:22

for T being TopStruct

for A being Subset of T holds

( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )

for A being Subset of T holds

( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )

proof end;

theorem :: PRE_TOPC:23

for T being TopStruct

for A being Subset of T holds

( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )

for A being Subset of T holds

( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )

proof end;

theorem :: PRE_TOPC:24

begin

:: from TOPMETR, 2008.07.06, A.T.

theorem :: PRE_TOPC:25

for T being non empty TopStruct

for A being non empty SubSpace of T

for p being Point of A holds p is Point of T

for A being non empty SubSpace of T

for p being Point of A holds p is Point of T

proof end;

theorem :: PRE_TOPC:26

for A, B, C being TopSpace

for f being Function of A,C st f is continuous & C is SubSpace of B holds

for h being Function of A,B st h = f holds

h is continuous

for f being Function of A,C st f is continuous & C is SubSpace of B holds

for h being Function of A,B st h = f holds

h is continuous

proof end;

theorem :: PRE_TOPC:27

for A being TopSpace

for B being non empty TopSpace

for f being Function of A,B

for C being SubSpace of B st f is continuous holds

for h being Function of A,C st h = f holds

h is continuous

for B being non empty TopSpace

for f being Function of A,B

for C being SubSpace of B st f is continuous holds

for h being Function of A,C st h = f holds

h is continuous

proof end;

registration

let T be TopSpace;

coherence

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

b_{1} is closed

end;
coherence

for b

b

proof end;

:: from BORSUK_1, 2008.07.07, A.T.

registration

let X be TopSpace;

let Y be non empty TopStruct ;

let y be Point of Y;

coherence

X --> y is continuous

end;
let Y be non empty TopStruct ;

let y be Point of Y;

coherence

X --> y is continuous

proof end;

registration

let S be TopSpace;

let T be non empty TopSpace;

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

end;
let T be non empty TopSpace;

cluster V7() V10( the carrier of S) V11( the carrier of T) V12() V21( the carrier of S, the carrier of T) continuous for Element of bool [: the carrier of S, the carrier of T:];

existence ex b

proof end;

:: from TSP_1, T_0TOPSP, COMPTS_1, URYSOHN1 2008.07.16, A.T.

definition

let T be TopStruct ;

end;
attr T is T_0 means :: PRE_TOPC:def 8

for x, y being Point of T st ( for G being Subset of T st G is open holds

( x in G iff y in G ) ) holds

x = y;

for x, y being Point of T st ( for G being Subset of T st G is open holds

( x in G iff y in G ) ) holds

x = y;

attr T is T_1 means :Def9: :: PRE_TOPC:def 9

for p, q being Point of T st p <> q holds

ex G being Subset of T st

( G is open & p in G & q in G ` );

for p, q being Point of T st p <> q holds

ex G being Subset of T st

( G is open & p in G & q in G ` );

attr T is T_2 means :Def10: :: PRE_TOPC:def 10

for p, q being Point of T st p <> q holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 );

for p, q being Point of T st p <> q holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 );

attr T is regular means :: PRE_TOPC:def 11

for p being Point of T

for F being Subset of T st F is closed & p in F ` holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 );

for p being Point of T

for F being Subset of T st F is closed & p in F ` holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 );

:: deftheorem defines T_0 PRE_TOPC:def 8 :

for T being TopStruct holds

( T is T_0 iff for x, y being Point of T st ( for G being Subset of T st G is open holds

( x in G iff y in G ) ) holds

x = y );

for T being TopStruct holds

( T is T_0 iff for x, y being Point of T st ( for G being Subset of T st G is open holds

( x in G iff y in G ) ) holds

x = y );

:: deftheorem Def9 defines T_1 PRE_TOPC:def 9 :

for T being TopStruct holds

( T is T_1 iff for p, q being Point of T st p <> q holds

ex G being Subset of T st

( G is open & p in G & q in G ` ) );

for T being TopStruct holds

( T is T_1 iff for p, q being Point of T st p <> q holds

ex G being Subset of T st

( G is open & p in G & q in G ` ) );

:: deftheorem Def10 defines T_2 PRE_TOPC:def 10 :

for T being TopStruct holds

( T is T_2 iff for p, q being Point of T st p <> q holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) );

for T being TopStruct holds

( T is T_2 iff for p, q being Point of T st p <> q holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) );

:: deftheorem defines regular PRE_TOPC:def 11 :

for T being TopStruct holds

( T is regular iff for p being Point of T

for F being Subset of T st F is closed & p in F ` holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 ) );

for T being TopStruct holds

( T is regular iff for p being Point of T

for F being Subset of T st F is closed & p in F ` holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 ) );

:: deftheorem defines normal PRE_TOPC:def 12 :

for T being TopStruct holds

( T is normal iff for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) );

for T being TopStruct holds

( T is normal iff for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds

ex G1, G2 being Subset of T st

( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) );

:: deftheorem Def13 defines T_3 PRE_TOPC:def 13 :

for T being TopStruct holds

( T is T_3 iff ( T is T_1 & T is regular ) );

for T being TopStruct holds

( T is T_3 iff ( T is T_1 & T is regular ) );

:: deftheorem Def14 defines T_4 PRE_TOPC:def 14 :

for T being TopStruct holds

( T is T_4 iff ( T is T_1 & T is normal ) );

for T being TopStruct holds

( T is T_4 iff ( T is T_1 & T is normal ) );

registration

coherence

for b_{1} being TopStruct st b_{1} is T_3 holds

( b_{1} is T_1 & b_{1} is regular )
by Def13;

coherence

for b_{1} being TopStruct st b_{1} is T_1 & b_{1} is regular holds

b_{1} is T_3
by Def13;

coherence

for b_{1} being TopStruct st b_{1} is T_4 holds

( b_{1} is T_1 & b_{1} is normal )
by Def14;

coherence

for b_{1} being TopStruct st b_{1} is T_1 & b_{1} is normal holds

b_{1} is T_4
by Def14;

end;
for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

registration

coherence

for b_{1} being TopStruct st b_{1} is T_1 holds

b_{1} is T_0

for b_{1} being TopStruct st b_{1} is T_2 holds

b_{1} is T_1

end;
for b

b

proof end;

coherence for b

b

proof end;

:: missing, 2009.02.14, A.T.

registration

let T be TopSpace;

coherence

TopStruct(# the carrier of T, the topology of T #) is TopSpace-like

end;
coherence

TopStruct(# the carrier of T, the topology of T #) is TopSpace-like

proof end;

registration

let T be non empty TopStruct ;

coherence

not TopStruct(# the carrier of T, the topology of T #) is empty ;

end;
coherence

not TopStruct(# the carrier of T, the topology of T #) is empty ;

theorem :: PRE_TOPC:28

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

T is TopSpace-like

T is TopSpace-like

proof end;

theorem :: PRE_TOPC:29

for T being TopStruct

for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T

for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T

proof end;

registration
end;

theorem :: PRE_TOPC:30

for T being TopSpace

for X being set holds

( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )

for X being set holds

( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )

proof end;

theorem Th31: :: PRE_TOPC:31

for T being TopSpace

for X being set holds

( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )

for X being set holds

( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )

proof end;

theorem Th32: :: PRE_TOPC:32

for S, T being TopSpace

for f being Function of S,T

for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds

( f is continuous iff g is continuous )

for f being Function of S,T

for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds

( f is continuous iff g is continuous )

proof end;

theorem Th33: :: PRE_TOPC:33

for S, T being TopSpace

for f being Function of S,T

for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds

( f is continuous iff g is continuous )

for f being Function of S,T

for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds

( f is continuous iff g is continuous )

proof end;

theorem :: PRE_TOPC:34

for S, T being TopSpace

for f being Function of S,T

for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds

( f is continuous iff g is continuous )

for f being Function of S,T

for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds

( f is continuous iff g is continuous )

proof end;

:: from BORSUK_3, 2009.03.15, A.T.

theorem Th35: :: PRE_TOPC:35

for S, T being TopStruct holds

( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )

( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )

proof end;

theorem :: PRE_TOPC:36

for T being TopStruct

for X being Subset of T

for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds

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

for X being Subset of T

for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds

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

proof end;

:: missing, 2009.05.26, A.T.

registration
end;

:: from COMPLSP1, 2010.02.25, A.T.

registration
end;

:: from BORSUK_3, 2011.07.08. A.T.

registration
end;

registration
end;

:: The topological space

::