:: by Zbigniew Karno

::

:: Received July 26, 1994

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

:: 1. Properties of the Closure and the Interior Operations.

registration

let X be non empty TopSpace;

let A be non empty Subset of X;

coherence

not Cl A is empty by PCOMPS_1:2;

end;
let A be non empty Subset of X;

coherence

not Cl A is empty by PCOMPS_1:2;

registration
end;

registration

let X be non empty TopSpace;

let A be non proper Subset of X;

coherence

not Cl A is proper

end;
let A be non proper Subset of X;

coherence

not Cl A is proper

proof end;

registration

let X be non trivial TopSpace;

let A be non trivial Subset of X;

coherence

not Cl A is trivial

end;
let A be non trivial Subset of X;

coherence

not Cl A is trivial

proof end;

theorem Th1: :: TEX_4:1

for X being non empty TopSpace

for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }

for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) }

proof end;

theorem Th2: :: TEX_4:2

for X being non empty TopSpace

for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }

for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }

proof end;

registration

let X be non empty TopSpace;

let A be non proper Subset of X;

coherence

not Int A is proper

end;
let A be non proper Subset of X;

coherence

not Int A is proper

proof end;

registration
end;

registration
end;

theorem :: TEX_4:3

for X being non empty TopSpace

for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) }

for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) }

proof end;

:: 2. Anti-discrete Subsets of Topological Structures.

definition

let Y be TopStruct ;

let IT be Subset of Y;

end;
let IT be Subset of Y;

attr IT is anti-discrete means :: TEX_4:def 1

for x being Point of Y

for G being Subset of Y st G is open & x in G & x in IT holds

IT c= G;

for x being Point of Y

for G being Subset of Y st G is open & x in G & x in IT holds

IT c= G;

:: deftheorem defines anti-discrete TEX_4:def 1 :

for Y being TopStruct

for IT being Subset of Y holds

( IT is anti-discrete iff for x being Point of Y

for G being Subset of Y st G is open & x in G & x in IT holds

IT c= G );

for Y being TopStruct

for IT being Subset of Y holds

( IT is anti-discrete iff for x being Point of Y

for G being Subset of Y st G is open & x in G & x in IT holds

IT c= G );

definition

let Y be non empty TopStruct ;

let A be Subset of Y;

( A is anti-discrete iff for x being Point of Y

for F being Subset of Y st F is closed & x in F & x in A holds

A c= F )

end;
let A be Subset of Y;

redefine attr A is anti-discrete means :: TEX_4:def 2

for x being Point of Y

for F being Subset of Y st F is closed & x in F & x in A holds

A c= F;

compatibility for x being Point of Y

for F being Subset of Y st F is closed & x in F & x in A holds

A c= F;

( A is anti-discrete iff for x being Point of Y

for F being Subset of Y st F is closed & x in F & x in A holds

A c= F )

proof end;

:: deftheorem defines anti-discrete TEX_4:def 2 :

for Y being non empty TopStruct

for A being Subset of Y holds

( A is anti-discrete iff for x being Point of Y

for F being Subset of Y st F is closed & x in F & x in A holds

A c= F );

for Y being non empty TopStruct

for A being Subset of Y holds

( A is anti-discrete iff for x being Point of Y

for F being Subset of Y st F is closed & x in F & x in A holds

A c= F );

definition

let Y be TopStruct ;

let A be Subset of Y;

( A is anti-discrete iff for G being Subset of Y holds

( not G is open or A misses G or A c= G ) )

end;
let A be Subset of Y;

redefine attr A is anti-discrete means :: TEX_4:def 3

for G being Subset of Y holds

( not G is open or A misses G or A c= G );

compatibility for G being Subset of Y holds

( not G is open or A misses G or A c= G );

( A is anti-discrete iff for G being Subset of Y holds

( not G is open or A misses G or A c= G ) )

proof end;

:: deftheorem defines anti-discrete TEX_4:def 3 :

for Y being TopStruct

for A being Subset of Y holds

( A is anti-discrete iff for G being Subset of Y holds

( not G is open or A misses G or A c= G ) );

for Y being TopStruct

for A being Subset of Y holds

( A is anti-discrete iff for G being Subset of Y holds

( not G is open or A misses G or A c= G ) );

definition

let Y be TopStruct ;

let A be Subset of Y;

( A is anti-discrete iff for F being Subset of Y holds

( not F is closed or A misses F or A c= F ) )

end;
let A be Subset of Y;

redefine attr A is anti-discrete means :: TEX_4:def 4

for F being Subset of Y holds

( not F is closed or A misses F or A c= F );

compatibility for F being Subset of Y holds

( not F is closed or A misses F or A c= F );

( A is anti-discrete iff for F being Subset of Y holds

( not F is closed or A misses F or A c= F ) )

proof end;

:: deftheorem defines anti-discrete TEX_4:def 4 :

for Y being TopStruct

for A being Subset of Y holds

( A is anti-discrete iff for F being Subset of Y holds

( not F is closed or A misses F or A c= F ) );

for Y being TopStruct

for A being Subset of Y holds

( A is anti-discrete iff for F being Subset of Y holds

( not F is closed or A misses F or A c= F ) );

theorem Th4: :: TEX_4:4

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 anti-discrete holds

D1 is anti-discrete

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 anti-discrete holds

D1 is anti-discrete

proof end;

theorem Th5: :: TEX_4:5

for Y being non empty TopStruct

for A, B being Subset of Y st B c= A & A is anti-discrete holds

B is anti-discrete

for A, B being Subset of Y st B c= A & A is anti-discrete holds

B is anti-discrete

proof end;

theorem :: TEX_4:7

definition

let Y be TopStruct ;

let IT be Subset-Family of Y;

end;
let IT be Subset-Family of Y;

attr IT is anti-discrete-set-family means :: TEX_4:def 5

for A being Subset of Y st A in IT holds

A is anti-discrete ;

for A being Subset of Y st A in IT holds

A is anti-discrete ;

:: deftheorem defines anti-discrete-set-family TEX_4:def 5 :

for Y being TopStruct

for IT being Subset-Family of Y holds

( IT is anti-discrete-set-family iff for A being Subset of Y st A in IT holds

A is anti-discrete );

for Y being TopStruct

for IT being Subset-Family of Y holds

( IT is anti-discrete-set-family iff for A being Subset of Y st A in IT holds

A is anti-discrete );

theorem Th8: :: TEX_4:8

for Y being non empty TopStruct

for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds

union F is anti-discrete

for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds

union F is anti-discrete

proof end;

theorem :: TEX_4:9

for Y being non empty TopStruct

for F being Subset-Family of Y st F is anti-discrete-set-family holds

meet F is anti-discrete

for F being Subset-Family of Y st F is anti-discrete-set-family holds

meet F is anti-discrete

proof end;

definition

let Y be TopStruct ;

let x be Point of Y;

{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y

end;
let x be Point of Y;

func MaxADSF x -> Subset-Family of Y equals :: TEX_4:def 6

{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;

coherence { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;

{ A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y

proof end;

:: deftheorem defines MaxADSF TEX_4:def 6 :

for Y being TopStruct

for x being Point of Y holds MaxADSF x = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;

for Y being TopStruct

for x being Point of Y holds MaxADSF x = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ;

registration
end;

:: 3. Maximal Anti-discrete Subsets of Topological Structures.

definition

let Y be TopStruct ;

let IT be Subset of Y;

end;
let IT be Subset of Y;

attr IT is maximal_anti-discrete means :: TEX_4:def 7

( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds

IT = D ) );

( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds

IT = D ) );

:: deftheorem defines maximal_anti-discrete TEX_4:def 7 :

for Y being TopStruct

for IT being Subset of Y holds

( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds

IT = D ) ) );

for Y being TopStruct

for IT being Subset of Y holds

( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds

IT = D ) ) );

theorem :: TEX_4:14

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_anti-discrete holds

D1 is maximal_anti-discrete

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_anti-discrete holds

D1 is maximal_anti-discrete

proof end;

theorem Th16: :: TEX_4:16

for Y being non empty TopStruct

for A being non empty Subset of Y st A is anti-discrete & A is open holds

A is maximal_anti-discrete

for A being non empty Subset of Y st A is anti-discrete & A is open holds

A is maximal_anti-discrete

proof end;

theorem Th17: :: TEX_4:17

for Y being non empty TopStruct

for A being non empty Subset of Y st A is anti-discrete & A is closed holds

A is maximal_anti-discrete

for A being non empty Subset of Y st A is anti-discrete & A is closed holds

A is maximal_anti-discrete

proof end;

definition
end;

:: deftheorem defines MaxADSet TEX_4:def 8 :

for Y being TopStruct

for x being Point of Y holds MaxADSet x = union (MaxADSF x);

for Y being TopStruct

for x being Point of Y holds MaxADSet x = union (MaxADSF x);

registration
end;

theorem :: TEX_4:18

theorem Th19: :: TEX_4:19

for Y being non empty TopStruct

for D being Subset of Y

for x being Point of Y st D is anti-discrete & x in D holds

D c= MaxADSet x

for D being Subset of Y

for x being Point of Y st D is anti-discrete & x in D holds

D c= MaxADSet x

proof end;

theorem Th21: :: TEX_4:21

for Y being non empty TopStruct

for x, y being Point of Y holds

( y in MaxADSet x iff MaxADSet y = MaxADSet x )

for x, y being Point of Y holds

( y in MaxADSet x iff MaxADSet y = MaxADSet x )

proof end;

theorem Th22: :: TEX_4:22

for Y being non empty TopStruct

for x, y being Point of Y holds

( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )

for x, y being Point of Y holds

( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )

proof end;

theorem Th23: :: TEX_4:23

for Y being non empty TopStruct

for F being Subset of Y

for x being Point of Y st F is closed & x in F holds

MaxADSet x c= F

for F being Subset of Y

for x being Point of Y st F is closed & x in F holds

MaxADSet x c= F

proof end;

theorem Th24: :: TEX_4:24

for Y being non empty TopStruct

for G being Subset of Y

for x being Point of Y st G is open & x in G holds

MaxADSet x c= G

for G being Subset of Y

for x being Point of Y st G is open & x in G holds

MaxADSet x c= G

proof end;

theorem :: TEX_4:25

for Y being non empty TopSpace

for x being Point of Y holds MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) }

for x being Point of Y holds MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) }

proof end;

theorem :: TEX_4:26

for Y being non empty TopSpace

for x being Point of Y holds MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }

for x being Point of Y holds MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) }

proof end;

definition

let Y be non empty TopStruct ;

let A be Subset of Y;

( A is maximal_anti-discrete iff ex x being Point of Y st

( x in A & A = MaxADSet x ) )

end;
let A be Subset of Y;

redefine attr A is maximal_anti-discrete means :: TEX_4:def 9

ex x being Point of Y st

( x in A & A = MaxADSet x );

compatibility ex x being Point of Y st

( x in A & A = MaxADSet x );

( A is maximal_anti-discrete iff ex x being Point of Y st

( x in A & A = MaxADSet x ) )

proof end;

:: deftheorem defines maximal_anti-discrete TEX_4:def 9 :

for Y being non empty TopStruct

for A being Subset of Y holds

( A is maximal_anti-discrete iff ex x being Point of Y st

( x in A & A = MaxADSet x ) );

for Y being non empty TopStruct

for A being Subset of Y holds

( A is maximal_anti-discrete iff ex x being Point of Y st

( x in A & A = MaxADSet x ) );

definition

let Y be non empty TopStruct ;

let A be non empty Subset of Y;

( A is maximal_anti-discrete iff for x being Point of Y st x in A holds

A = MaxADSet x )

end;
let A be non empty Subset of Y;

redefine attr A is maximal_anti-discrete means :: TEX_4:def 10

for x being Point of Y st x in A holds

A = MaxADSet x;

compatibility for x being Point of Y st x in A holds

A = MaxADSet x;

( A is maximal_anti-discrete iff for x being Point of Y st x in A holds

A = MaxADSet x )

proof end;

:: deftheorem defines maximal_anti-discrete TEX_4:def 10 :

for Y being non empty TopStruct

for A being non empty Subset of Y holds

( A is maximal_anti-discrete iff for x being Point of Y st x in A holds

A = MaxADSet x );

for Y being non empty TopStruct

for A being non empty Subset of Y holds

( A is maximal_anti-discrete iff for x being Point of Y st x in A holds

A = MaxADSet x );

definition

let Y be non empty TopStruct ;

let A be Subset of Y;

union { (MaxADSet a) where a is Point of Y : a in A } is Subset of Y

end;
let A be Subset of Y;

func MaxADSet A -> Subset of Y equals :: TEX_4:def 11

union { (MaxADSet a) where a is Point of Y : a in A } ;

coherence union { (MaxADSet a) where a is Point of Y : a in A } ;

union { (MaxADSet a) where a is Point of Y : a in A } is Subset of Y

proof end;

:: deftheorem defines MaxADSet TEX_4:def 11 :

for Y being non empty TopStruct

for A being Subset of Y holds MaxADSet A = union { (MaxADSet a) where a is Point of Y : a in A } ;

for Y being non empty TopStruct

for A being Subset of Y holds MaxADSet A = union { (MaxADSet a) where a is Point of Y : a in A } ;

theorem Th29: :: TEX_4:29

for Y being non empty TopStruct

for A being Subset of Y

for x being Point of Y st MaxADSet x meets MaxADSet A holds

MaxADSet x meets A

for A being Subset of Y

for x being Point of Y st MaxADSet x meets MaxADSet A holds

MaxADSet x meets A

proof end;

theorem Th30: :: TEX_4:30

for Y being non empty TopStruct

for A being Subset of Y

for x being Point of Y st MaxADSet x meets MaxADSet A holds

MaxADSet x c= MaxADSet A

for A being Subset of Y

for x being Point of Y st MaxADSet x meets MaxADSet A holds

MaxADSet x c= MaxADSet A

proof end;

theorem Th34: :: TEX_4:34

for Y being non empty TopStruct

for A, B being Subset of Y st A c= MaxADSet B holds

MaxADSet A c= MaxADSet B

for A, B being Subset of Y st A c= MaxADSet B holds

MaxADSet A c= MaxADSet B

proof end;

theorem :: TEX_4:36

for Y being non empty TopStruct

for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)

for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B)

proof end;

theorem Th37: :: TEX_4:37

for Y being non empty TopStruct

for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)

for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B)

proof end;

registration

let Y be non empty TopStruct ;

let A be non empty Subset of Y;

coherence

not MaxADSet A is empty by Th32, XBOOLE_1:3;

end;
let A be non empty Subset of Y;

coherence

not MaxADSet A is empty by Th32, XBOOLE_1:3;

registration
end;

registration

let Y be non empty TopStruct ;

let A be non proper Subset of Y;

coherence

not MaxADSet A is proper

end;
let A be non proper Subset of Y;

coherence

not MaxADSet A is proper

proof end;

registration

let Y be non trivial TopStruct ;

let A be non trivial Subset of Y;

coherence

not MaxADSet A is trivial

end;
let A be non trivial Subset of Y;

coherence

not MaxADSet A is trivial

proof end;

theorem Th38: :: TEX_4:38

for Y being non empty TopStruct

for G, A being Subset of Y st G is open & A c= G holds

MaxADSet A c= G

for G, A being Subset of Y st G is open & A c= G holds

MaxADSet A c= G

proof end;

theorem Th39: :: TEX_4:39

for Y being non empty TopSpace

for A being Subset of Y holds MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }

for A being Subset of Y holds MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) }

proof end;

theorem Th40: :: TEX_4:40

for Y being non empty TopStruct

for F, A being Subset of Y st F is closed & A c= F holds

MaxADSet A c= F

for F, A being Subset of Y st F is closed & A c= F holds

MaxADSet A c= F

proof end;

theorem Th41: :: TEX_4:41

for Y being non empty TopSpace

for A being Subset of Y holds MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) }

for A being Subset of Y holds MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) }

proof end;

:: 4. Anti-discrete and Maximal Anti-discrete Subsets of Topological Spaces.

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is anti-discrete iff for x being Point of X st x in A holds

A c= Cl {x} )

end;
let A be Subset of X;

redefine attr A is anti-discrete means :: TEX_4:def 12

for x being Point of X st x in A holds

A c= Cl {x};

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

A c= Cl {x};

( A is anti-discrete iff for x being Point of X st x in A holds

A c= Cl {x} )

proof end;

:: deftheorem defines anti-discrete TEX_4:def 12 :

for X being non empty TopSpace

for A being Subset of X holds

( A is anti-discrete iff for x being Point of X st x in A holds

A c= Cl {x} );

for X being non empty TopSpace

for A being Subset of X holds

( A is anti-discrete iff for x being Point of X st x in A holds

A c= Cl {x} );

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is anti-discrete iff for x being Point of X st x in A holds

Cl A = Cl {x} )

end;
let A be Subset of X;

redefine attr A is anti-discrete means :: TEX_4:def 13

for x being Point of X st x in A holds

Cl A = Cl {x};

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

Cl A = Cl {x};

( A is anti-discrete iff for x being Point of X st x in A holds

Cl A = Cl {x} )

proof end;

:: deftheorem defines anti-discrete TEX_4:def 13 :

for X being non empty TopSpace

for A being Subset of X holds

( A is anti-discrete iff for x being Point of X st x in A holds

Cl A = Cl {x} );

for X being non empty TopSpace

for A being Subset of X holds

( A is anti-discrete iff for x being Point of X st x in A holds

Cl A = Cl {x} );

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} )

end;
let A be Subset of X;

redefine attr A is anti-discrete means :: TEX_4:def 14

for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y};

compatibility for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y};

( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} )

proof end;

:: deftheorem defines anti-discrete TEX_4:def 14 :

for X being non empty TopSpace

for A being Subset of X holds

( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} );

for X being non empty TopSpace

for A being Subset of X holds

( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds

Cl {x} = Cl {y} );

theorem :: TEX_4:42

for X being non empty TopSpace

for x being Point of X

for D being Subset of X st D is anti-discrete & Cl {x} c= D holds

D = Cl {x}

for x being Point of X

for D being Subset of X st D is anti-discrete & Cl {x} c= D holds

D = Cl {x}

proof end;

theorem :: TEX_4:43

for X being non empty TopSpace

for A being Subset of X holds

( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds

A = Cl {x} )

for A being Subset of X holds

( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds

A = Cl {x} )

proof end;

theorem :: TEX_4:44

for X being non empty TopSpace

for A being Subset of X st A is anti-discrete & not A is open holds

A is boundary

for A being Subset of X st A is anti-discrete & not A is open holds

A is boundary

proof end;

theorem Th45: :: TEX_4:45

for X being non empty TopSpace

for x being Point of X st Cl {x} = {x} holds

{x} is maximal_anti-discrete

for x being Point of X st Cl {x} = {x} holds

{x} is maximal_anti-discrete

proof end;

theorem Th46: :: TEX_4:46

for X being non empty TopSpace

for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }

for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) }

proof end;

theorem Th47: :: TEX_4:47

for X being non empty TopSpace

for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }

for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) }

proof end;

Lm1: for X being non empty TopSpace

for x, y being Point of X st MaxADSet x = MaxADSet y holds

Cl {x} = Cl {y}

proof end;

theorem Th49: :: TEX_4:49

for X being non empty TopSpace

for x, y being Point of X holds

( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )

for x, y being Point of X holds

( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} )

proof end;

theorem :: TEX_4:50

definition

let X be non empty TopSpace;

let x be Point of X;

for b_{1} being non empty Subset of X holds

( b_{1} = MaxADSet x iff b_{1} = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) )

MaxADSet x is non empty Subset of X ;

end;
let x be Point of X;

:: original: MaxADSet

redefine func MaxADSet x -> non empty Subset of X equals :: TEX_4:def 15

(Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } );

compatibility redefine func MaxADSet x -> non empty Subset of X equals :: TEX_4:def 15

(Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } );

for b

( b

proof end;

coherence MaxADSet x is non empty Subset of X ;

:: deftheorem defines MaxADSet TEX_4:def 15 :

for X being non empty TopSpace

for x being Point of X holds MaxADSet x = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } );

for X being non empty TopSpace

for x being Point of X holds MaxADSet x = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } );

theorem Th51: :: TEX_4:51

for X being non empty TopSpace

for x, y being Point of X holds

( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } )

for x, y being Point of X holds

( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } )

proof end;

theorem :: TEX_4:52

for X being non empty TopSpace

for x, y being Point of X holds

( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )

for x, y being Point of X holds

( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )

proof end;

theorem Th53: :: TEX_4:53

for X being non empty TopSpace

for x, y being Point of X holds

( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st

( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st

( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )

for x, y being Point of X holds

( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st

( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st

( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )

proof end;

theorem :: TEX_4:54

for X being non empty TopSpace

for x, y being Point of X holds

( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st

( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st

( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )

for x, y being Point of X holds

( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st

( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st

( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) )

proof end;

theorem :: TEX_4:57

theorem :: TEX_4:61

theorem :: TEX_4:62

theorem :: TEX_4:63

for X being non empty TopSpace

for A, B being Subset of X st MaxADSet A = MaxADSet B holds

Cl A = Cl B

for A, B being Subset of X st MaxADSet A = MaxADSet B holds

Cl A = Cl B

proof end;

theorem :: TEX_4:64

for X being non empty TopSpace

for P, Q being Subset of X st ( P is closed or Q is closed ) holds

MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

for P, Q being Subset of X st ( P is closed or Q is closed ) holds

MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

proof end;

theorem :: TEX_4:65

for X being non empty TopSpace

for P, Q being Subset of X st ( P is open or Q is open ) holds

MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

for P, Q being Subset of X st ( P is open or Q is open ) holds

MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q)

proof end;

theorem Th66: :: TEX_4:66

for Y being non empty TopStruct

for Y0 being SubSpace of Y

for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds

A is anti-discrete

for Y0 being SubSpace of Y

for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds

A is anti-discrete

proof end;

theorem Th67: :: TEX_4:67

for Y being non empty TopStruct

for Y0 being SubSpace of Y st Y0 is TopSpace-like holds

for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds

Y0 is anti-discrete

for Y0 being SubSpace of Y st Y0 is TopSpace-like holds

for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds

Y0 is anti-discrete

proof end;

theorem :: TEX_4:68

for X being non empty TopSpace

for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds

Y0 is anti-discrete

for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds

Y0 is anti-discrete

proof end;

theorem :: TEX_4:69

for X being non empty TopSpace

for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds

Y0 is anti-discrete

for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds

Y0 is anti-discrete

proof end;

theorem :: TEX_4:70

for X being non empty TopSpace

for Y0 being anti-discrete SubSpace of X

for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

for Y0 being anti-discrete SubSpace of X

for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

proof end;

theorem :: TEX_4:71

for X being non empty TopSpace

for Y0 being anti-discrete SubSpace of X

for X0 being closed SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

for Y0 being anti-discrete SubSpace of X

for X0 being closed SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

proof end;

definition

let Y be non empty TopStruct ;

let IT be SubSpace of Y;

end;
let IT be SubSpace of Y;

attr IT is maximal_anti-discrete means :: TEX_4:def 16

( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds

the carrier of IT = the carrier of Y0 ) );

( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds

the carrier of IT = the carrier of Y0 ) );

:: deftheorem defines maximal_anti-discrete TEX_4:def 16 :

for Y being non empty TopStruct

for IT being SubSpace of Y holds

( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds

the carrier of IT = the carrier of Y0 ) ) );

for Y being non empty TopStruct

for IT being SubSpace of Y holds

( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds

the carrier of IT = the carrier of Y0 ) ) );

registration

let Y be non empty TopStruct ;

coherence

for b_{1} being SubSpace of Y st b_{1} is maximal_anti-discrete holds

b_{1} is anti-discrete
;

coherence

for b_{1} being SubSpace of Y st not b_{1} is anti-discrete holds

not b_{1} is maximal_anti-discrete
;

end;
coherence

for b

b

coherence

for b

not b

theorem Th72: :: TEX_4:72

for X being non empty TopSpace

for Y0 being non empty SubSpace of X

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

( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

for Y0 being non empty SubSpace of X

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

( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

proof end;

registration

let X be non empty TopSpace;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is open & b_{1} is anti-discrete holds

b_{1} is maximal_anti-discrete

for b_{1} being non empty SubSpace of X st b_{1} is open & not b_{1} is maximal_anti-discrete holds

not b_{1} is anti-discrete
;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is anti-discrete & not b_{1} is maximal_anti-discrete holds

not b_{1} is open
;

coherence

for b_{1} being non empty SubSpace of X st b_{1} is closed & b_{1} is anti-discrete holds

b_{1} is maximal_anti-discrete

for b_{1} being non empty SubSpace of X st b_{1} is closed & not b_{1} is maximal_anti-discrete holds

not b_{1} is anti-discrete
;

for b_{1} being non empty SubSpace of X st b_{1} is anti-discrete & not b_{1} is maximal_anti-discrete holds

not b_{1} is closed
;

end;
coherence

for b

b

proof end;

coherence for b

not b

coherence

for b

not b

coherence

for b

b

proof end;

cluster non empty closed non maximal_anti-discrete -> non empty non anti-discrete for SubSpace of X;

coherence for b

not b

cluster non empty anti-discrete non maximal_anti-discrete -> non empty non closed for SubSpace of X;

coherence for b

not b

definition

let Y be TopStruct ;

let x be Point of Y;

ex b_{1} being strict SubSpace of Y st the carrier of b_{1} = MaxADSet x

for b_{1}, b_{2} being strict SubSpace of Y st the carrier of b_{1} = MaxADSet x & the carrier of b_{2} = MaxADSet x holds

b_{1} = b_{2}

end;
let x be Point of Y;

func MaxADSspace x -> strict SubSpace of Y means :Def17: :: TEX_4:def 17

the carrier of it = MaxADSet x;

existence the carrier of it = MaxADSet x;

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def17 defines MaxADSspace TEX_4:def 17 :

for Y being TopStruct

for x being Point of Y

for b_{3} being strict SubSpace of Y holds

( b_{3} = MaxADSspace x iff the carrier of b_{3} = MaxADSet x );

for Y being TopStruct

for x being Point of Y

for b

( b

registration
end;

Lm2: for Y being non empty TopStruct

for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds

X1 is SubSpace of X2

proof end;

theorem :: TEX_4:74

for Y being non empty TopStruct

for x, y being Point of Y holds

( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )

for x, y being Point of Y holds

( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) )

proof end;

theorem :: TEX_4:75

for Y being non empty TopStruct

for x, y being Point of Y holds

( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )

for x, y being Point of Y holds

( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) )

proof end;

registration

let X be non empty TopSpace;

existence

ex b_{1} being SubSpace of X st

( b_{1} is maximal_anti-discrete & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let X be non empty TopSpace;

let x be Point of X;

coherence

MaxADSspace x is maximal_anti-discrete

end;
let x be Point of X;

coherence

MaxADSspace x is maximal_anti-discrete

proof end;

theorem :: TEX_4:76

for X being non empty TopSpace

for X0 being non empty closed SubSpace of X

for x being Point of X st x is Point of X0 holds

MaxADSspace x is SubSpace of X0

for X0 being non empty closed SubSpace of X

for x being Point of X st x is Point of X0 holds

MaxADSspace x is SubSpace of X0

proof end;

theorem :: TEX_4:77

for X being non empty TopSpace

for X0 being non empty open SubSpace of X

for x being Point of X st x is Point of X0 holds

MaxADSspace x is SubSpace of X0

for X0 being non empty open SubSpace of X

for x being Point of X st x is Point of X0 holds

MaxADSspace x is SubSpace of X0

proof end;

theorem :: TEX_4:78

for X being non empty TopSpace

for x being Point of X st Cl {x} = {x} holds

Sspace x is maximal_anti-discrete

for x being Point of X st Cl {x} = {x} holds

Sspace x is maximal_anti-discrete

proof end;

Lm3: for Y being TopStruct

for A being Subset of Y holds the carrier of (Y | A) = A

proof end;

theorem :: TEX_4:80

for Y being non empty TopStruct

for Y0 being SubSpace of Y

for A being non empty Subset of Y st A is Subset of Y0 holds

Sspace A is SubSpace of Y0

for Y0 being SubSpace of Y

for A being non empty Subset of Y st A is Subset of Y0 holds

Sspace A is SubSpace of Y0

proof end;

registration

let Y be non trivial TopStruct ;

existence

ex b_{1} being SubSpace of Y st

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

end;
existence

ex b

( not b

proof end;

registration

let Y be non trivial TopStruct ;

let A be non trivial Subset of Y;

coherence

not Sspace A is trivial by Lm3;

end;
let A be non trivial Subset of Y;

coherence

not Sspace A is trivial by Lm3;

registration

let Y be non empty TopStruct ;

let A be non proper Subset of Y;

coherence

not Sspace A is proper

end;
let A be non proper Subset of Y;

coherence

not Sspace A is proper

proof end;

definition

let Y be non empty TopStruct ;

let A be Subset of Y;

ex b_{1} being strict SubSpace of Y st the carrier of b_{1} = MaxADSet A

for b_{1}, b_{2} being strict SubSpace of Y st the carrier of b_{1} = MaxADSet A & the carrier of b_{2} = MaxADSet A holds

b_{1} = b_{2}

end;
let A be Subset of Y;

func MaxADSspace A -> strict SubSpace of Y means :Def18: :: TEX_4:def 18

the carrier of it = MaxADSet A;

existence the carrier of it = MaxADSet A;

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines MaxADSspace TEX_4:def 18 :

for Y being non empty TopStruct

for A being Subset of Y

for b_{3} being strict SubSpace of Y holds

( b_{3} = MaxADSspace A iff the carrier of b_{3} = MaxADSet A );

for Y being non empty TopStruct

for A being Subset of Y

for b

( b

registration

let Y be non empty TopStruct ;

let A be non empty Subset of Y;

coherence

not MaxADSspace A is empty

end;
let A be non empty Subset of Y;

coherence

not MaxADSspace A is empty

proof end;

theorem :: TEX_4:81

for Y being non empty TopStruct

for A being non empty Subset of Y holds A is Subset of (MaxADSspace A)

for A being non empty Subset of Y holds A is Subset of (MaxADSspace A)

proof end;

theorem :: TEX_4:82

for Y being non empty TopStruct

for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A

for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A

proof end;

theorem :: TEX_4:83

for Y being non empty TopStruct

for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #)

for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #)

proof end;

theorem :: TEX_4:84

for Y being non empty TopStruct

for A, B being non empty Subset of Y st A c= B holds

MaxADSspace A is SubSpace of MaxADSspace B

for A, B being non empty Subset of Y st A c= B holds

MaxADSspace A is SubSpace of MaxADSspace B

proof end;

theorem :: TEX_4:85

for Y being non empty TopStruct

for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)

for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #)

proof end;

theorem :: TEX_4:86

for Y being non empty TopStruct

for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds

MaxADSspace A is SubSpace of MaxADSspace B

for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds

MaxADSspace A is SubSpace of MaxADSspace B

proof end;

theorem :: TEX_4:87

for Y being non empty TopStruct

for A, B being non empty Subset of Y holds

( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) )

for A, B being non empty Subset of Y holds

( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) )

proof end;

registration

let Y be non trivial TopStruct ;

let A be non trivial Subset of Y;

coherence

not MaxADSspace A is trivial

end;
let A be non trivial Subset of Y;

coherence

not MaxADSspace A is trivial

proof end;

registration

let Y be non empty TopStruct ;

let A be non proper Subset of Y;

coherence

not MaxADSspace A is proper

end;
let A be non proper Subset of Y;

coherence

not MaxADSspace A is proper

proof end;

theorem :: TEX_4:88

for X being non empty TopSpace

for X0 being open SubSpace of X

for A being non empty Subset of X st A is Subset of X0 holds

MaxADSspace A is SubSpace of X0

for X0 being open SubSpace of X

for A being non empty Subset of X st A is Subset of X0 holds

MaxADSspace A is SubSpace of X0

proof end;

theorem :: TEX_4:89

for X being non empty TopSpace

for X0 being closed SubSpace of X

for A being non empty Subset of X st A is Subset of X0 holds

MaxADSspace A is SubSpace of X0

for X0 being closed SubSpace of X

for A being non empty Subset of X st A is Subset of X0 holds

MaxADSspace A is SubSpace of X0

proof end;