:: by Miros{\l}aw Wysocki and Agata Darmochwa\l

::

:: Received April 28, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: TOPS_1:1

canceled;

theorem :: TOPS_1:2

canceled;

theorem :: TOPS_1:3

canceled;

theorem :: TOPS_1:4

canceled;

theorem :: TOPS_1:5

canceled;

theorem :: TOPS_1:6

canceled;

theorem :: TOPS_1:7

canceled;

theorem :: TOPS_1:8

canceled;

theorem :: TOPS_1:9

canceled;

theorem :: TOPS_1:10

canceled;

theorem :: TOPS_1:11

canceled;

theorem :: TOPS_1:12

canceled;

theorem :: TOPS_1:13

canceled;

theorem :: TOPS_1:14

canceled;

theorem :: TOPS_1:15

canceled;

theorem :: TOPS_1:16

canceled;

theorem :: TOPS_1:17

canceled;

theorem :: TOPS_1:18

canceled;

theorem :: TOPS_1:19

canceled;

theorem :: TOPS_1:20

canceled;

theorem :: TOPS_1:21

theorem :: TOPS_1:22

canceled;

theorem :: TOPS_1:23

canceled;

theorem :: TOPS_1:24

canceled;

theorem :: TOPS_1:25

canceled;

theorem :: TOPS_1:26

canceled;

theorem Th27: :: TOPS_1:27

proof end;

registration

let T be TopSpace;

let P be Subset of T;

cluster Cl P -> closed ;

coherence

Cl P is closed

end;
let P be Subset of T;

cluster Cl P -> closed ;

coherence

Cl P is closed

proof end;

theorem :: TOPS_1:28

canceled;

theorem Th29: :: TOPS_1:29

proof end;

registration
end;

theorem Th30: :: TOPS_1:30

proof end;

registration

let T be TopSpace;

cluster open Element of K10( the carrier of T);

existence

ex b_{1} being Subset of T st b_{1} is open

end;
cluster open Element of K10( the carrier of T);

existence

ex b

proof end;

registration

let T be TopSpace;

let R be open Subset of T;

cluster R ` -> closed ;

coherence

R ` is closed by Th30;

end;
let R be open Subset of T;

cluster R ` -> closed ;

coherence

R ` is closed by Th30;

theorem :: TOPS_1:31

proof end;

theorem Th32: :: TOPS_1:32

proof end;

theorem :: TOPS_1:33

canceled;

theorem Th34: :: TOPS_1:34

for GX being TopStruct

for R, S being Subset of GX st R is closed & S is closed holds

Cl (R /\ S) = (Cl R) /\ (Cl S)

for R, S being Subset of GX st R is closed & S is closed holds

Cl (R /\ S) = (Cl R) /\ (Cl S)

proof end;

registration

let TS be TopSpace;

let P, Q be closed Subset of TS;

cluster P /\ Q -> closed Subset of TS;

coherence

for b_{1} being Subset of TS st b_{1} = P /\ Q holds

b_{1} is closed

coherence

for b_{1} being Subset of TS st b_{1} = P \/ Q holds

b_{1} is closed

end;
let P, Q be closed Subset of TS;

cluster P /\ Q -> closed Subset of TS;

coherence

for b

b

proof end;

cluster P \/ Q -> closed Subset of TS;coherence

for b

b

proof end;

theorem :: TOPS_1:35

for TS being TopSpace

for P, Q being Subset of TS st P is closed & Q is closed holds

P /\ Q is closed ;

for P, Q being Subset of TS st P is closed & Q is closed holds

P /\ Q is closed ;

theorem :: TOPS_1:36

for TS being TopSpace

for P, Q being Subset of TS st P is closed & Q is closed holds

P \/ Q is closed ;

for P, Q being Subset of TS st P is closed & Q is closed holds

P \/ Q is closed ;

registration

let TS be TopSpace;

let P, Q be open Subset of TS;

cluster P /\ Q -> open Subset of TS;

coherence

for b_{1} being Subset of TS st b_{1} = P /\ Q holds

b_{1} is open

coherence

for b_{1} being Subset of TS st b_{1} = P \/ Q holds

b_{1} is open

end;
let P, Q be open Subset of TS;

cluster P /\ Q -> open Subset of TS;

coherence

for b

b

proof end;

cluster P \/ Q -> open Subset of TS;coherence

for b

b

proof end;

theorem :: TOPS_1:37

theorem :: TOPS_1:38

theorem Th39: :: TOPS_1:39

for GX being non empty TopSpace

for R being Subset of GX

for p being Point of GX holds

( p in Cl R iff for T being Subset of GX st T is open & p in T holds

R meets T )

for R being Subset of GX

for p being Point of GX holds

( p in Cl R iff for T being Subset of GX st T is open & p in T holds

R meets T )

proof end;

theorem Th40: :: TOPS_1:40

proof end;

theorem :: TOPS_1:41

proof end;

definition

let GX be TopStruct ;

let R be Subset of GX;

func Int R -> Subset of GX equals :: TOPS_1:def 1

(Cl (R `)) ` ;

coherence

(Cl (R `)) ` is Subset of GX ;

projectivity

for b_{1}, b_{2} being Subset of GX st b_{1} = (Cl (b_{2} `)) ` holds

b_{1} = (Cl (b_{1} `)) `
;

end;
let R be Subset of GX;

func Int R -> Subset of GX equals :: TOPS_1:def 1

(Cl (R `)) ` ;

coherence

(Cl (R `)) ` is Subset of GX ;

projectivity

for b

b

:: deftheorem defines Int TOPS_1:def 1 :

for GX being TopStruct

for R being Subset of GX holds Int R = (Cl (R `)) ` ;

theorem :: TOPS_1:42

canceled;

theorem Th43: :: TOPS_1:43

proof end;

theorem Th44: :: TOPS_1:44

proof end;

theorem :: TOPS_1:45

canceled;

theorem Th46: :: TOPS_1:46

proof end;

registration
end;

theorem :: TOPS_1:47

theorem Th48: :: TOPS_1:48

proof end;

theorem Th49: :: TOPS_1:49

proof end;

theorem :: TOPS_1:50

proof end;

registration
end;

theorem :: TOPS_1:51

canceled;

theorem :: TOPS_1:52

canceled;

theorem :: TOPS_1:53

canceled;

registration

let T be TopSpace;

cluster empty -> open Element of K10( the carrier of T);

coherence

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

b_{1} is open

coherence

[#] T is open

end;
cluster empty -> open Element of K10( the carrier of T);

coherence

for b

b

proof end;

cluster [#] T -> open ;coherence

[#] T is open

proof end;

registration

let T be TopSpace;

cluster open closed Element of K10( the carrier of T);

existence

ex b_{1} being Subset of T st

( b_{1} is open & b_{1} is closed )

end;
cluster open closed Element of K10( the carrier of T);

existence

ex b

( b

proof end;

registration

let T be non empty TopSpace;

cluster non empty open closed Element of K10( the carrier of T);

existence

ex b_{1} being Subset of T st

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

end;
cluster non empty open closed Element of K10( the carrier of T);

existence

ex b

( not b

proof end;

theorem Th54: :: TOPS_1:54

for TS being TopSpace

for x being set

for K being Subset of TS holds

( x in Int K iff ex Q being Subset of TS st

( Q is open & Q c= K & x in Q ) )

for x being set

for K being Subset of TS holds

( x in Int K iff ex Q being Subset of TS st

( Q is open & Q c= K & x in Q ) )

proof end;

theorem Th55: :: TOPS_1:55

for TS being TopSpace

for GX being TopStruct

for P being Subset of TS

for R being Subset of GX holds

( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )

for GX being TopStruct

for P being Subset of TS

for R being Subset of GX holds

( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )

proof end;

theorem :: TOPS_1:56

proof end;

theorem :: TOPS_1:57

for TS being TopSpace

for P being Subset of TS holds

( P is open iff for x being set holds

( x in P iff ex Q being Subset of TS st

( Q is open & Q c= P & x in Q ) ) )

for P being Subset of TS holds

( P is open iff for x being set holds

( x in P iff ex Q being Subset of TS st

( Q is open & Q c= P & x in Q ) ) )

proof end;

theorem Th58: :: TOPS_1:58

proof end;

theorem :: TOPS_1:59

proof end;

definition

let GX be TopStruct ;

let R be Subset of GX;

func Fr R -> Subset of GX equals :: TOPS_1:def 2

(Cl R) /\ (Cl (R `));

coherence

(Cl R) /\ (Cl (R `)) is Subset of GX ;

end;
let R be Subset of GX;

func Fr R -> Subset of GX equals :: TOPS_1:def 2

(Cl R) /\ (Cl (R `));

coherence

(Cl R) /\ (Cl (R `)) is Subset of GX ;

:: deftheorem defines Fr TOPS_1:def 2 :

for GX being TopStruct

for R being Subset of GX holds Fr R = (Cl R) /\ (Cl (R `));

theorem :: TOPS_1:60

canceled;

registration
end;

theorem Th61: :: TOPS_1:61

for GX being non empty TopSpace

for R being Subset of GX

for p being Point of GX holds

( p in Fr R iff for S being Subset of GX st S is open & p in S holds

( R meets S & R ` meets S ) )

for R being Subset of GX

for p being Point of GX holds

( p in Fr R iff for S being Subset of GX st S is open & p in S holds

( R meets S & R ` meets S ) )

proof end;

theorem :: TOPS_1:62

theorem :: TOPS_1:63

canceled;

theorem :: TOPS_1:64

proof end;

theorem Th65: :: TOPS_1:65

proof end;

theorem Th66: :: TOPS_1:66

proof end;

theorem Th67: :: TOPS_1:67

proof end;

theorem Th68: :: TOPS_1:68

proof end;

theorem :: TOPS_1:69

proof end;

Lm1: for TS being TopSpace

for K, L being Subset of TS holds Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))

proof end;

theorem :: TOPS_1:70

for TS being TopSpace

for K, L being Subset of TS holds (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))

for K, L being Subset of TS holds (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))

proof end;

theorem :: TOPS_1:71

proof end;

theorem :: TOPS_1:72

proof end;

theorem Th73: :: TOPS_1:73

proof end;

theorem Th74: :: TOPS_1:74

proof end;

Lm2: for GX being TopStruct

for T being Subset of GX holds Fr T = (Cl T) \ (Int T)

proof end;

Lm3: for TS being TopSpace

for K being Subset of TS holds Cl (Fr K) = Fr K

proof end;

Lm4: for TS being TopSpace

for K being Subset of TS holds Int (Fr (Fr K)) = {}

proof end;

theorem :: TOPS_1:75

proof end;

Lm5: for X, Y, Z being set st X c= Z & Y = Z \ X holds

X c= Z \ Y

proof end;

theorem Th76: :: TOPS_1:76

proof end;

theorem Th77: :: TOPS_1:77

proof end;

definition

let GX be TopStruct ;

let R be Subset of GX;

attr R is dense means :Def3: :: TOPS_1:def 3

Cl R = [#] GX;

end;
let R be Subset of GX;

attr R is dense means :Def3: :: TOPS_1:def 3

Cl R = [#] GX;

:: deftheorem Def3 defines dense TOPS_1:def 3 :

for GX being TopStruct

for R being Subset of GX holds

( R is dense iff Cl R = [#] GX );

registration

let GX be TopStruct ;

cluster [#] GX -> dense ;

coherence

[#] GX is dense

existence

ex b_{1} being Subset of GX st b_{1} is dense

end;
cluster [#] GX -> dense ;

coherence

[#] GX is dense

proof end;

cluster dense Element of K10( the carrier of GX);existence

ex b

proof end;

theorem :: TOPS_1:78

canceled;

theorem :: TOPS_1:79

proof end;

theorem Th80: :: TOPS_1:80

for TS being TopSpace

for P being Subset of TS holds

( P is dense iff for Q being Subset of TS st Q <> {} & Q is open holds

P meets Q )

for P being Subset of TS holds

( P is dense iff for Q being Subset of TS st Q <> {} & Q is open holds

P meets Q )

proof end;

theorem Th81: :: TOPS_1:81

for TS being TopSpace

for P being Subset of TS st P is dense holds

for Q being Subset of TS st Q is open holds

Cl Q = Cl (Q /\ P)

for P being Subset of TS st P is dense holds

for Q being Subset of TS st Q is open holds

Cl Q = Cl (Q /\ P)

proof end;

theorem :: TOPS_1:82

for TS being TopSpace

for P, Q being Subset of TS st P is dense & Q is dense & Q is open holds

P /\ Q is dense

for P, Q being Subset of TS st P is dense & Q is dense & Q is open holds

P /\ Q is dense

proof end;

definition

let GX be TopStruct ;

let R be Subset of GX;

attr R is boundary means :Def4: :: TOPS_1:def 4

R ` is dense ;

end;
let R be Subset of GX;

attr R is boundary means :Def4: :: TOPS_1:def 4

R ` is dense ;

:: deftheorem Def4 defines boundary TOPS_1:def 4 :

for GX being TopStruct

for R being Subset of GX holds

( R is boundary iff R ` is dense );

registration

let GX be TopStruct ;

cluster empty -> boundary Element of K10( the carrier of GX);

coherence

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

b_{1} is boundary

end;
cluster empty -> boundary Element of K10( the carrier of GX);

coherence

for b

b

proof end;

theorem :: TOPS_1:83

canceled;

theorem Th84: :: TOPS_1:84

proof end;

registration

let GX be TopStruct ;

cluster boundary Element of K10( the carrier of GX);

existence

ex b_{1} being Subset of GX st b_{1} is boundary

end;
cluster boundary Element of K10( the carrier of GX);

existence

ex b

proof end;

registration

let GX be TopStruct ;

let R be boundary Subset of GX;

cluster Int R -> empty ;

coherence

Int R is empty by Th84;

end;
let R be boundary Subset of GX;

cluster Int R -> empty ;

coherence

Int R is empty by Th84;

theorem Th85: :: TOPS_1:85

for TS being TopSpace

for P, Q being Subset of TS st P is boundary & Q is boundary & Q is closed holds

P \/ Q is boundary

for P, Q being Subset of TS st P is boundary & Q is boundary & Q is closed holds

P \/ Q is boundary

proof end;

theorem :: TOPS_1:86

for TS being TopSpace

for P being Subset of TS holds

( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds

Q = {} )

for P being Subset of TS holds

( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds

Q = {} )

proof end;

theorem :: TOPS_1:87

for TS being TopSpace

for P being Subset of TS st P is closed holds

( P is boundary iff for Q being Subset of TS st Q <> {} & Q is open holds

ex G being Subset of TS st

( G c= Q & G <> {} & G is open & P misses G ) )

for P being Subset of TS st P is closed holds

( P is boundary iff for Q being Subset of TS st Q <> {} & Q is open holds

ex G being Subset of TS st

( G c= Q & G <> {} & G is open & P misses G ) )

proof end;

theorem :: TOPS_1:88

proof end;

registration

let GX be non empty TopSpace;

cluster [#] GX -> non boundary ;

coherence

not [#] GX is boundary

existence

ex b_{1} being Subset of GX st

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

end;
cluster [#] GX -> non boundary ;

coherence

not [#] GX is boundary

proof end;

cluster non empty non boundary Element of K10( the carrier of GX);existence

ex b

( not b

proof end;

definition

let GX be TopStruct ;

let R be Subset of GX;

attr R is nowhere_dense means :Def5: :: TOPS_1:def 5

Cl R is boundary ;

end;
let R be Subset of GX;

attr R is nowhere_dense means :Def5: :: TOPS_1:def 5

Cl R is boundary ;

:: deftheorem Def5 defines nowhere_dense TOPS_1:def 5 :

for GX being TopStruct

for R being Subset of GX holds

( R is nowhere_dense iff Cl R is boundary );

registration

let TS be TopSpace;

cluster empty -> nowhere_dense Element of K10( the carrier of TS);

coherence

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

b_{1} is nowhere_dense

end;
cluster empty -> nowhere_dense Element of K10( the carrier of TS);

coherence

for b

b

proof end;

registration

let TS be TopSpace;

cluster nowhere_dense Element of K10( the carrier of TS);

existence

ex b_{1} being Subset of TS st b_{1} is nowhere_dense

end;
cluster nowhere_dense Element of K10( the carrier of TS);

existence

ex b

proof end;

theorem :: TOPS_1:89

canceled;

theorem :: TOPS_1:90

for TS being TopSpace

for P, Q being Subset of TS st P is nowhere_dense & Q is nowhere_dense holds

P \/ Q is nowhere_dense

for P, Q being Subset of TS st P is nowhere_dense & Q is nowhere_dense holds

P \/ Q is nowhere_dense

proof end;

theorem Th91: :: TOPS_1:91

proof end;

registration

let TS be TopSpace;

let R be nowhere_dense Subset of TS;

cluster R ` -> dense ;

coherence

R ` is dense by Th91;

end;
let R be nowhere_dense Subset of TS;

cluster R ` -> dense ;

coherence

R ` is dense by Th91;

theorem Th92: :: TOPS_1:92

proof end;

registration

let TS be TopSpace;

cluster nowhere_dense -> boundary Element of K10( the carrier of TS);

coherence

for b_{1} being Subset of TS st b_{1} is nowhere_dense holds

b_{1} is boundary
by Th92;

end;
cluster nowhere_dense -> boundary Element of K10( the carrier of TS);

coherence

for b

b

theorem Th93: :: TOPS_1:93

for GX being TopStruct

for S being Subset of GX st S is boundary & S is closed holds

S is nowhere_dense

for S being Subset of GX st S is boundary & S is closed holds

S is nowhere_dense

proof end;

registration

let TS be TopSpace;

cluster closed boundary -> nowhere_dense Element of K10( the carrier of TS);

coherence

for b_{1} being Subset of TS st b_{1} is boundary & b_{1} is closed holds

b_{1} is nowhere_dense
by Th93;

end;
cluster closed boundary -> nowhere_dense Element of K10( the carrier of TS);

coherence

for b

b

theorem :: TOPS_1:94

for GX being TopStruct

for R being Subset of GX st R is closed holds

( R is nowhere_dense iff R = Fr R )

for R being Subset of GX st R is closed holds

( R is nowhere_dense iff R = Fr R )

proof end;

theorem Th95: :: TOPS_1:95

proof end;

registration

let TS be TopSpace;

let P be open Subset of TS;

cluster Fr P -> nowhere_dense ;

coherence

Fr P is nowhere_dense by Th95;

end;
let P be open Subset of TS;

cluster Fr P -> nowhere_dense ;

coherence

Fr P is nowhere_dense by Th95;

theorem Th96: :: TOPS_1:96

proof end;

registration

let TS be TopSpace;

let P be closed Subset of TS;

cluster Fr P -> nowhere_dense ;

coherence

Fr P is nowhere_dense by Th96;

end;
let P be closed Subset of TS;

cluster Fr P -> nowhere_dense ;

coherence

Fr P is nowhere_dense by Th96;

theorem Th97: :: TOPS_1:97

proof end;

registration

let TS be TopSpace;

cluster open nowhere_dense -> empty Element of K10( the carrier of TS);

coherence

for b_{1} being Subset of TS st b_{1} is open & b_{1} is nowhere_dense holds

b_{1} is empty
by Th97;

end;
cluster open nowhere_dense -> empty Element of K10( the carrier of TS);

coherence

for b

b

definition

let GX be TopStruct ;

let R be Subset of GX;

attr R is condensed means :Def6: :: TOPS_1:def 6

( Int (Cl R) c= R & R c= Cl (Int R) );

attr R is closed_condensed means :Def7: :: TOPS_1:def 7

R = Cl (Int R);

attr R is open_condensed means :Def8: :: TOPS_1:def 8

R = Int (Cl R);

end;
let R be Subset of GX;

attr R is condensed means :Def6: :: TOPS_1:def 6

( Int (Cl R) c= R & R c= Cl (Int R) );

attr R is closed_condensed means :Def7: :: TOPS_1:def 7

R = Cl (Int R);

attr R is open_condensed means :Def8: :: TOPS_1:def 8

R = Int (Cl R);

:: deftheorem Def6 defines condensed TOPS_1:def 6 :

for GX being TopStruct

for R being Subset of GX holds

( R is condensed iff ( Int (Cl R) c= R & R c= Cl (Int R) ) );

:: deftheorem Def7 defines closed_condensed TOPS_1:def 7 :

for GX being TopStruct

for R being Subset of GX holds

( R is closed_condensed iff R = Cl (Int R) );

:: deftheorem Def8 defines open_condensed TOPS_1:def 8 :

for GX being TopStruct

for R being Subset of GX holds

( R is open_condensed iff R = Int (Cl R) );

theorem :: TOPS_1:98

canceled;

theorem :: TOPS_1:99

canceled;

theorem :: TOPS_1:100

canceled;

theorem Th101: :: TOPS_1:101

for GX being TopStruct

for R being Subset of GX holds

( R is open_condensed iff R ` is closed_condensed )

for R being Subset of GX holds

( R is open_condensed iff R ` is closed_condensed )

proof end;

theorem Th102: :: TOPS_1:102

proof end;

theorem :: TOPS_1:103

proof end;

theorem Th104: :: TOPS_1:104

for GX being TopStruct

for R being Subset of GX st R is open_condensed holds

( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R )

for R being Subset of GX st R is open_condensed holds

( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R )

proof end;

theorem :: TOPS_1:105

for GX being TopStruct

for R being Subset of GX st R is open & R is closed holds

( R is closed_condensed iff R is open_condensed )

for R being Subset of GX st R is open & R is closed holds

( R is closed_condensed iff R is open_condensed )

proof end;

theorem Th106: :: TOPS_1:106

for TS being TopSpace

for GX being TopStruct

for P being Subset of TS

for R being Subset of GX holds

( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )

for GX being TopStruct

for P being Subset of TS

for R being Subset of GX holds

( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )

proof end;

theorem :: TOPS_1:107

for TS being TopSpace

for GX being TopStruct

for P being Subset of TS

for R being Subset of GX holds

( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )

for GX being TopStruct

for P being Subset of TS

for R being Subset of GX holds

( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )

proof end;

theorem Th108: :: TOPS_1:108

for TS being TopSpace

for P, Q being Subset of TS st P is closed_condensed & Q is closed_condensed holds

P \/ Q is closed_condensed

for P, Q being Subset of TS st P is closed_condensed & Q is closed_condensed holds

P \/ Q is closed_condensed

proof end;

theorem :: TOPS_1:109

for TS being TopSpace

for P, Q being Subset of TS st P is open_condensed & Q is open_condensed holds

P /\ Q is open_condensed

for P, Q being Subset of TS st P is open_condensed & Q is open_condensed holds

P /\ Q is open_condensed

proof end;

theorem :: TOPS_1:110

proof end;

theorem :: TOPS_1:111

for GX being TopStruct

for R being Subset of GX st R is condensed holds

( Int R is condensed & Cl R is condensed )

for R being Subset of GX st R is condensed holds

( Int R is condensed & Cl R is condensed )

proof end;