:: by Zbigniew Karno

::

:: Received July 26, 1994

:: Copyright (c) 1994-2016 Association of Mizar Users

:: 1. Maximal T_{0} Subsets.

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds

MaxADSet a misses MaxADSet b )

end;
let A be Subset of X;

redefine attr A is T_0 means :: TSP_2:def 1

for a, b being Point of X st a in A & b in A & a <> b holds

MaxADSet a misses MaxADSet b;

compatibility for a, b being Point of X st a in A & b in A & a <> b holds

MaxADSet a misses MaxADSet b;

( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds

MaxADSet a misses MaxADSet b )

proof end;

:: deftheorem defines T_0 TSP_2:def 1 :

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds

MaxADSet a misses MaxADSet b );

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds

MaxADSet a misses MaxADSet b );

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is T_0 iff for a being Point of X st a in A holds

A /\ (MaxADSet a) = {a} )

end;
let A be Subset of X;

redefine attr A is T_0 means :: TSP_2:def 2

for a being Point of X st a in A holds

A /\ (MaxADSet a) = {a};

compatibility for a being Point of X st a in A holds

A /\ (MaxADSet a) = {a};

( A is T_0 iff for a being Point of X st a in A holds

A /\ (MaxADSet a) = {a} )

proof end;

:: deftheorem defines T_0 TSP_2:def 2 :

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for a being Point of X st a in A holds

A /\ (MaxADSet a) = {a} );

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for a being Point of X st a in A holds

A /\ (MaxADSet a) = {a} );

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is T_0 iff for a being Point of X st a in A holds

ex D being Subset of X st

( D is maximal_anti-discrete & A /\ D = {a} ) )

end;
let A be Subset of X;

redefine attr A is T_0 means :: TSP_2:def 3

for a being Point of X st a in A holds

ex D being Subset of X st

( D is maximal_anti-discrete & A /\ D = {a} );

compatibility for a being Point of X st a in A holds

ex D being Subset of X st

( D is maximal_anti-discrete & A /\ D = {a} );

( A is T_0 iff for a being Point of X st a in A holds

ex D being Subset of X st

( D is maximal_anti-discrete & A /\ D = {a} ) )

proof end;

:: deftheorem defines T_0 TSP_2:def 3 :

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for a being Point of X st a in A holds

ex D being Subset of X st

( D is maximal_anti-discrete & A /\ D = {a} ) );

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for a being Point of X st a in A holds

ex D being Subset of X st

( D is maximal_anti-discrete & A /\ D = {a} ) );

definition

let Y be TopStruct ;

let IT be Subset of Y;

end;
let IT be Subset of Y;

attr IT is maximal_T_0 means :: TSP_2:def 4

( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds

IT = D ) );

( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds

IT = D ) );

:: deftheorem defines maximal_T_0 TSP_2:def 4 :

for Y being TopStruct

for IT being Subset of Y holds

( IT is maximal_T_0 iff ( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds

IT = D ) ) );

for Y being TopStruct

for IT being Subset of Y holds

( IT is maximal_T_0 iff ( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds

IT = D ) ) );

theorem :: TSP_2:1

for Y0, Y1 being TopStruct

for D0 being Subset of Y0

for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_T_0 holds

D1 is maximal_T_0

for D0 being Subset of Y0

for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_T_0 holds

D1 is maximal_T_0

proof end;

definition

let X be non empty TopSpace;

let M be Subset of X;

compatibility

( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) )

end;
let M be Subset of X;

compatibility

( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) )

proof end;

:: deftheorem defines maximal_T_0 TSP_2:def 5 :

for X being non empty TopSpace

for M being Subset of X holds

( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) );

for X being non empty TopSpace

for M being Subset of X holds

( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) );

theorem Th5: :: TSP_2:5

for X being non empty TopSpace

for M being Subset of X st M is maximal_T_0 holds

for A being Subset of X st A is closed holds

A = MaxADSet (M /\ A)

for M being Subset of X st M is maximal_T_0 holds

for A being Subset of X st A is closed holds

A = MaxADSet (M /\ A)

proof end;

theorem Th6: :: TSP_2:6

for X being non empty TopSpace

for M being Subset of X st M is maximal_T_0 holds

for A being Subset of X st A is open holds

A = MaxADSet (M /\ A)

for M being Subset of X st M is maximal_T_0 holds

for A being Subset of X st A is open holds

A = MaxADSet (M /\ A)

proof end;

theorem :: TSP_2:7

theorem :: TSP_2:8

definition

let X be non empty TopSpace;

let M be Subset of X;

( M is maximal_T_0 iff for x being Point of X ex a being Point of X st

( a in M & M /\ (MaxADSet x) = {a} ) )

end;
let M be Subset of X;

redefine attr M is maximal_T_0 means :: TSP_2:def 6

for x being Point of X ex a being Point of X st

( a in M & M /\ (MaxADSet x) = {a} );

compatibility for x being Point of X ex a being Point of X st

( a in M & M /\ (MaxADSet x) = {a} );

( M is maximal_T_0 iff for x being Point of X ex a being Point of X st

( a in M & M /\ (MaxADSet x) = {a} ) )

proof end;

:: deftheorem defines maximal_T_0 TSP_2:def 6 :

for X being non empty TopSpace

for M being Subset of X holds

( M is maximal_T_0 iff for x being Point of X ex a being Point of X st

( a in M & M /\ (MaxADSet x) = {a} ) );

for X being non empty TopSpace

for M being Subset of X holds

( M is maximal_T_0 iff for x being Point of X ex a being Point of X st

( a in M & M /\ (MaxADSet x) = {a} ) );

theorem Th9: :: TSP_2:9

for X being non empty TopSpace

for A being Subset of X st A is T_0 holds

ex M being Subset of X st

( A c= M & M is maximal_T_0 )

for A being Subset of X st A is T_0 holds

ex M being Subset of X st

( A c= M & M is maximal_T_0 )

proof end;

:: 2. Maximal Kolmogorov Subspaces.

definition

let Y be non empty TopStruct ;

let IT be SubSpace of Y;

end;
let IT be SubSpace of Y;

attr IT is maximal_T_0 means :: TSP_2:def 7

for A being Subset of Y st A = the carrier of IT holds

A is maximal_T_0 ;

for A being Subset of Y st A = the carrier of IT holds

A is maximal_T_0 ;

:: deftheorem defines maximal_T_0 TSP_2:def 7 :

for Y being non empty TopStruct

for IT being SubSpace of Y holds

( IT is maximal_T_0 iff for A being Subset of Y st A = the carrier of IT holds

A is maximal_T_0 );

for Y being non empty TopStruct

for IT being SubSpace of Y holds

( IT is maximal_T_0 iff for A being Subset of Y st A = the carrier of IT holds

A is maximal_T_0 );

theorem Th11: :: TSP_2:11

for Y being non empty TopStruct

for Y0 being SubSpace of Y

for A being Subset of Y st A = the carrier of Y0 holds

( A is maximal_T_0 iff Y0 is maximal_T_0 ) ;

for Y0 being SubSpace of Y

for A being Subset of Y st A = the carrier of Y0 holds

( A is maximal_T_0 iff Y0 is maximal_T_0 ) ;

Lm1: now :: thesis: for Z being non empty TopStruct

for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

let Z be non empty TopStruct ; :: thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

let Z0 be SubSpace of Z; :: thesis: the carrier of Z0 is Subset of Z

[#] Z0 c= [#] Z by PRE_TOPC:def 4;

hence the carrier of Z0 is Subset of Z ; :: thesis: verum

end;
let Z0 be SubSpace of Z; :: thesis: the carrier of Z0 is Subset of Z

[#] Z0 c= [#] Z by PRE_TOPC:def 4;

hence the carrier of Z0 is Subset of Z ; :: thesis: verum

registration

let Y be non empty TopStruct ;

coherence

for b_{1} being non empty SubSpace of Y st b_{1} is maximal_T_0 holds

b_{1} is V59()

for b_{1} being non empty SubSpace of Y st b_{1} is V59() holds

not b_{1} is maximal_T_0
;

end;
coherence

for b

b

proof end;

coherence for b

not b

definition

let X be non empty TopSpace;

let X0 be non empty SubSpace of X;

( X0 is maximal_T_0 iff ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds

TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) )

end;
let X0 be non empty SubSpace of X;

redefine attr X0 is maximal_T_0 means :: TSP_2:def 8

( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds

TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) );

compatibility ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds

TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) );

( X0 is maximal_T_0 iff ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds

TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) )

proof end;

:: deftheorem defines maximal_T_0 TSP_2:def 8 :

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds

( X0 is maximal_T_0 iff ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds

TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) );

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds

( X0 is maximal_T_0 iff ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds

TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) );

theorem Th12: :: TSP_2:12

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is maximal_T_0 holds

ex X0 being non empty strict SubSpace of X st

( X0 is maximal_T_0 & A0 = the carrier of X0 )

for A0 being non empty Subset of X st A0 is maximal_T_0 holds

ex X0 being non empty strict SubSpace of X st

( X0 is maximal_T_0 & A0 = the carrier of X0 )

proof end;

registration

let X be non empty TopSpace;

coherence

for b_{1} being SubSpace of X st b_{1} is maximal_T_0 holds

b_{1} is dense

for b_{1} being SubSpace of X st not b_{1} is dense holds

not b_{1} is maximal_T_0
;

coherence

for b_{1} being SubSpace of X st b_{1} is open & b_{1} is maximal_T_0 holds

not b_{1} is proper

for b_{1} being SubSpace of X st b_{1} is open & b_{1} is proper holds

not b_{1} is maximal_T_0
;

coherence

for b_{1} being SubSpace of X st b_{1} is proper & b_{1} is maximal_T_0 holds

not b_{1} is open
;

coherence

for b_{1} being SubSpace of X st b_{1} is closed & b_{1} is maximal_T_0 holds

not b_{1} is proper

for b_{1} being SubSpace of X st b_{1} is closed & b_{1} is proper holds

not b_{1} is maximal_T_0
;

coherence

for b_{1} being SubSpace of X st b_{1} is proper & b_{1} is maximal_T_0 holds

not b_{1} is closed
;

end;
coherence

for b

b

proof end;

coherence for b

not b

coherence

for b

not b

proof end;

coherence for b

not b

coherence

for b

not b

coherence

for b

not b

proof end;

coherence for b

not b

coherence

for b

not b

theorem :: TSP_2:13

for X being non empty TopSpace

for Y0 being non empty V59() SubSpace of X ex X0 being strict SubSpace of X st

( Y0 is SubSpace of X0 & X0 is maximal_T_0 )

for Y0 being non empty V59() SubSpace of X ex X0 being strict SubSpace of X st

( Y0 is SubSpace of X0 & X0 is maximal_T_0 )

proof end;

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

definition
end;

theorem Th14: :: TSP_2:14

for X being non empty TopSpace

for X0 being maximal_Kolmogorov_subspace of X

for G being Subset of X

for G0 being Subset of X0 st G0 = G holds

( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )

for X0 being maximal_Kolmogorov_subspace of X

for G being Subset of X

for G0 being Subset of X0 st G0 = G holds

( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )

proof end;

theorem :: TSP_2:15

for X being non empty TopSpace

for X0 being maximal_Kolmogorov_subspace of X

for G being Subset of X holds

( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st

( G0 is open & G0 = G /\ the carrier of X0 ) ) )

for X0 being maximal_Kolmogorov_subspace of X

for G being Subset of X holds

( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st

( G0 is open & G0 = G /\ the carrier of X0 ) ) )

proof end;

theorem Th16: :: TSP_2:16

for X being non empty TopSpace

for X0 being maximal_Kolmogorov_subspace of X

for F being Subset of X

for F0 being Subset of X0 st F0 = F holds

( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )

for X0 being maximal_Kolmogorov_subspace of X

for F being Subset of X

for F0 being Subset of X0 st F0 = F holds

( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )

proof end;

theorem :: TSP_2:17

for X being non empty TopSpace

for X0 being maximal_Kolmogorov_subspace of X

for F being Subset of X holds

( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st

( F0 is closed & F0 = F /\ the carrier of X0 ) ) )

for X0 being maximal_Kolmogorov_subspace of X

for F being Subset of X holds

( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st

( F0 is closed & F0 = F /\ the carrier of X0 ) ) )

proof end;

theorem Th18: :: TSP_2:18

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being Function of X,X0

for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds

r is continuous Function of X,X0

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being Function of X,X0

for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds

r is continuous Function of X,X0

proof end;

theorem :: TSP_2:19

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds

r is continuous Function of X,X0

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds

r is continuous Function of X,X0

proof end;

theorem Th20: :: TSP_2:20

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0

for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds

r is being_a_retraction

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0

for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds

r is being_a_retraction

proof end;

theorem Th21: :: TSP_2:21

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds

r is being_a_retraction

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds

r is being_a_retraction

proof end;

theorem Th22: :: TSP_2:22

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction

for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction

proof end;

theorem :: TSP_2:23

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X holds X0 is_a_retract_of X

for X0 being non empty maximal_Kolmogorov_subspace of X holds X0 is_a_retract_of X

proof end;

Lm2: for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0 st r is being_a_retraction holds

for a being Point of X

for b being Point of X0 st a = b holds

r " (Cl {b}) = Cl {a}

proof end;

Lm3: for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0 st r is being_a_retraction holds

for A being Subset of X st A = the carrier of X0 holds

for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}

proof end;

Lm4: for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0 st r is being_a_retraction holds

for a being Point of X

for b being Point of X0 st a = b holds

MaxADSet a c= r " {b}

proof end;

Lm5: for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0 st r is being_a_retraction holds

for a being Point of X

for b being Point of X0 st a = b holds

r " {b} = MaxADSet a

proof end;

Lm6: for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for r being continuous Function of X,X0 st r is being_a_retraction holds

for E being Subset of X

for F being Subset of X0 st F = E holds

r " F = MaxADSet E

proof end;

definition

let X be non empty TopSpace;

let X0 be non empty maximal_Kolmogorov_subspace of X;

ex b_{1} being continuous Function of X,X0 st b_{1} is being_a_retraction
by Th22;

uniqueness

for b_{1}, b_{2} being continuous Function of X,X0 st b_{1} is being_a_retraction & b_{2} is being_a_retraction holds

b_{1} = b_{2}

end;
let X0 be non empty maximal_Kolmogorov_subspace of X;

func Stone-retraction (X,X0) -> continuous Function of X,X0 means :Def9: :: TSP_2:def 9

it is being_a_retraction ;

existence it is being_a_retraction ;

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def9 defines Stone-retraction TSP_2:def 9 :

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b_{3} being continuous Function of X,X0 holds

( b_{3} = Stone-retraction (X,X0) iff b_{3} is being_a_retraction );

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b

( b

theorem :: TSP_2:24

definition

let X be non empty TopSpace;

let X0 be non empty maximal_Kolmogorov_subspace of X;

for b_{1} being continuous Function of X,X0 holds

( b_{1} = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds

for a being Point of X holds M /\ (MaxADSet a) = {(b_{1} . a)} )

end;
let X0 be non empty maximal_Kolmogorov_subspace of X;

redefine func Stone-retraction (X,X0) means :Def10: :: TSP_2:def 10

for M being Subset of X st M = the carrier of X0 holds

for a being Point of X holds M /\ (MaxADSet a) = {(it . a)};

compatibility for M being Subset of X st M = the carrier of X0 holds

for a being Point of X holds M /\ (MaxADSet a) = {(it . a)};

for b

( b

for a being Point of X holds M /\ (MaxADSet a) = {(b

proof end;

:: deftheorem Def10 defines Stone-retraction TSP_2:def 10 :

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b_{3} being continuous Function of X,X0 holds

( b_{3} = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds

for a being Point of X holds M /\ (MaxADSet a) = {(b_{3} . a)} );

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b

( b

for a being Point of X holds M /\ (MaxADSet a) = {(b

definition

let X be non empty TopSpace;

let X0 be non empty maximal_Kolmogorov_subspace of X;

for b_{1} being continuous Function of X,X0 holds

( b_{1} = Stone-retraction (X,X0) iff for a being Point of X holds b_{1} . a in MaxADSet a )

end;
let X0 be non empty maximal_Kolmogorov_subspace of X;

redefine func Stone-retraction (X,X0) means :Def11: :: TSP_2:def 11

for a being Point of X holds it . a in MaxADSet a;

compatibility for a being Point of X holds it . a in MaxADSet a;

for b

( b

proof end;

:: deftheorem Def11 defines Stone-retraction TSP_2:def 11 :

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b_{3} being continuous Function of X,X0 holds

( b_{3} = Stone-retraction (X,X0) iff for a being Point of X holds b_{3} . a in MaxADSet a );

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b

( b

theorem Th27: :: TSP_2:27

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a

for X0 being non empty maximal_Kolmogorov_subspace of X

for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a

proof end;

theorem :: TSP_2:28

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)

for X0 being non empty maximal_Kolmogorov_subspace of X

for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)

proof end;

definition

let X be non empty TopSpace;

let X0 be non empty maximal_Kolmogorov_subspace of X;

for b_{1} being continuous Function of X,X0 holds

( b_{1} = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds

for A being Subset of X holds M /\ (MaxADSet A) = b_{1} .: A )

end;
let X0 be non empty maximal_Kolmogorov_subspace of X;

redefine func Stone-retraction (X,X0) means :Def12: :: TSP_2:def 12

for M being Subset of X st M = the carrier of X0 holds

for A being Subset of X holds M /\ (MaxADSet A) = it .: A;

compatibility for M being Subset of X st M = the carrier of X0 holds

for A being Subset of X holds M /\ (MaxADSet A) = it .: A;

for b

( b

for A being Subset of X holds M /\ (MaxADSet A) = b

proof end;

:: deftheorem Def12 defines Stone-retraction TSP_2:def 12 :

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b_{3} being continuous Function of X,X0 holds

( b_{3} = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds

for A being Subset of X holds M /\ (MaxADSet A) = b_{3} .: A );

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for b

( b

for A being Subset of X holds M /\ (MaxADSet A) = b

theorem Th29: :: TSP_2:29

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A

proof end;

theorem :: TSP_2:30

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A)

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A)

proof end;

theorem :: TSP_2:31

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B)

for X0 being non empty maximal_Kolmogorov_subspace of X

for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B)

proof end;

theorem :: TSP_2:32

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for A, B being Subset of X st ( A is open or B is open ) holds

(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)

for X0 being non empty maximal_Kolmogorov_subspace of X

for A, B being Subset of X st ( A is open or B is open ) holds

(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)

proof end;

theorem :: TSP_2:33

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for A, B being Subset of X st ( A is closed or B is closed ) holds

(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)

for X0 being non empty maximal_Kolmogorov_subspace of X

for A, B being Subset of X st ( A is closed or B is closed ) holds

(Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B)

proof end;

theorem :: TSP_2:34

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X st A is open holds

(Stone-retraction (X,X0)) .: A is open

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X st A is open holds

(Stone-retraction (X,X0)) .: A is open

proof end;

theorem :: TSP_2:35

for X being non empty TopSpace

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X st A is closed holds

(Stone-retraction (X,X0)) .: A is closed

for X0 being non empty maximal_Kolmogorov_subspace of X

for A being Subset of X st A is closed holds

(Stone-retraction (X,X0)) .: A is closed

proof end;