:: Subsets of Topological Spaces
:: by Miros{\l}aw Wysocki and Agata Darmochwa\l
::
:: Received April 28, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem :: TOPS_1:1

for TS being 1-sorted
for K, Q being Subset of TS st K ` = Q ` holds
K = Q by SUBSET_1:42;

theorem Th2: :: TOPS_1:2

for GX being TopStruct holds Cl ([#] GX) = [#] GX by PRE_TOPC:18;

registration

let T be TopSpace;
let P be Subset of T;

cluster Cl P -> closed ;

coherence
Cl P is closed

proof end;

end;

theorem Th3: :: TOPS_1:3

for GX being TopStruct
for R being Subset of GX holds
( R is closed iff R ` is open )

proof end;

registration

let T be TopSpace;
let R be closed Subset of T;

cluster R ` -> open ;

coherence
R ` is open by Th3;

end;

theorem Th4: :: TOPS_1:4

for GX being TopStruct
for R being Subset of GX holds
( R is open iff R ` is closed )

proof end;

registration

let T be TopSpace;

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

existence
ex b₁ being Subset of T st b₁ is open

proof end;

end;

registration

let T be TopSpace;
let R be open Subset of T;

cluster R ` -> closed ;

coherence
R ` is closed by Th4;

end;

theorem :: TOPS_1:5

for GX being TopStruct
for S, T being Subset of GX st S is closed & T c= S holds
Cl T c= S

proof end;

theorem Th6: :: TOPS_1:6

for TS being TopSpace
for K, L being Subset of TS holds (Cl K) \ (Cl L) c= Cl (K \ L)

proof end;

theorem Th7: :: TOPS_1:7

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)

proof end;

registration

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

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

coherence
for b₁ being Subset of TS st b₁ = P /\ Q holds
b₁ is closed

proof end;

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

coherence
for b₁ being Subset of TS st b₁ = P \/ Q holds
b₁ is closed

proof end;

end;

theorem :: TOPS_1:8

for TS being TopSpace
for P, Q being Subset of TS st P is closed & Q is closed holds
P /\ Q is closed ;

theorem :: TOPS_1:9

for TS being TopSpace
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 for Subset of TS;

coherence
for b₁ being Subset of TS st b₁ = P /\ Q holds
b₁ is open

proof end;

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

coherence
for b₁ being Subset of TS st b₁ = P \/ Q holds
b₁ is open

proof end;

end;

theorem :: TOPS_1:10

for TS being TopSpace
for P, Q being Subset of TS st P is open & Q is open holds
P \/ Q is open ;

theorem :: TOPS_1:11

for TS being TopSpace
for P, Q being Subset of TS st P is open & Q is open holds
P /\ Q is open ;

theorem Th12: :: TOPS_1:12

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 )

proof end;

theorem Th13: :: TOPS_1:13

for TS being TopSpace
for Q, K being Subset of TS st Q is open holds
Q /\ (Cl K) c= Cl (Q /\ K)

proof end;

theorem :: TOPS_1:14

for TS being TopSpace
for Q, K being Subset of TS st Q is open holds
Cl (Q /\ (Cl K)) = Cl (Q /\ K)

proof end;

::
:: INTERIOR OF A SET
::

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₁, b₂ being Subset of GX st b₁ = (Cl (b₂ `)) ` holds
b₁ = (Cl (b₁ `)) ` ;

end;

:: deftheorem defines Int TOPS_1:def 1 :
for GX being TopStruct
for R being Subset of GX holds Int R = (Cl (R `)) ` ;

theorem Th15: :: TOPS_1:15

for TS being TopSpace holds Int ([#] TS) = [#] TS

proof end;

theorem Th16: :: TOPS_1:16

for GX being TopStruct
for T being Subset of GX holds Int T c= T

proof end;

theorem Th17: :: TOPS_1:17

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

proof end;

registration

let GX be TopStruct ;

cluster Int ({} GX) -> empty ;

coherence
Int ({} GX) is empty

proof end;

end;

theorem :: TOPS_1:18

for GX being TopStruct holds Int ({} GX) = {} GX ;

theorem Th19: :: TOPS_1:19

for GX being TopStruct
for T, W being Subset of GX st T c= W holds
Int T c= Int W

proof end;

theorem Th20: :: TOPS_1:20

for GX being TopStruct
for T, W being Subset of GX holds (Int T) \/ (Int W) c= Int (T \/ W)

proof end;

theorem :: TOPS_1:21

for TS being TopSpace
for K, L being Subset of TS holds Int (K \ L) c= (Int K) \ (Int L)

proof end;

registration

let T be TopSpace;
let K be Subset of T;

cluster Int K -> open ;

coherence
Int K is open ;

end;

registration

let T be TopSpace;

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

coherence
for b₁ being Subset of T st b₁ is empty holds
b₁ is open

proof end;

cluster [#] T -> open ;

coherence
[#] T is open

proof end;

end;

registration

let T be TopSpace;

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

existence
ex b₁ being Subset of T st
( b₁ is open & b₁ is closed )

proof end;

end;

registration

let T be non empty TopSpace;

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

existence
ex b₁ being Subset of T st
( not b₁ is empty & b₁ is open & b₁ is closed )

proof end;

end;

theorem Th22: :: TOPS_1:22

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 ) )

proof end;

theorem Th23: :: TOPS_1:23

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 ) )

proof end;

theorem :: TOPS_1:24

for GX being TopStruct
for S, T being Subset of GX st S is open & S c= T holds
S c= Int T

proof end;

theorem :: TOPS_1:25

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 ) ) )

proof end;

theorem Th26: :: TOPS_1:26

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

proof end;

theorem :: TOPS_1:27

for GX being TopStruct
for R being Subset of GX st R is open holds
Cl (Int (Cl R)) = Cl R

proof end;

::
:: FRONTIER OF A SET
::

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;

:: deftheorem defines Fr TOPS_1:def 2 :
for GX being TopStruct
for R being Subset of GX holds Fr R = (Cl R) /\ (Cl (R `));

registration

let T be TopSpace;
let A be Subset of T;

cluster Fr A -> closed ;

coherence
Fr A is closed ;

end;

theorem Th28: :: TOPS_1:28

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 ) )

proof end;

theorem :: TOPS_1:29

for GX being TopStruct
for T being Subset of GX holds Fr T = Fr (T `) ;

theorem :: TOPS_1:30

for GX being TopStruct
for T being Subset of GX holds Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)

proof end;

theorem Th31: :: TOPS_1:31

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

proof end;

theorem Th32: :: TOPS_1:32

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

proof end;

theorem Th33: :: TOPS_1:33

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

proof end;

theorem Th34: :: TOPS_1:34

for GX being TopStruct
for T being Subset of GX holds Fr (Fr T) c= Fr T

proof end;

theorem :: TOPS_1:35

for GX being TopStruct
for R being Subset of GX st R is closed holds
Fr R c= R

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:36

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))

proof end;

theorem :: TOPS_1:37

for GX being TopStruct
for T being Subset of GX holds Fr (Int T) c= Fr T

proof end;

theorem :: TOPS_1:38

for GX being TopStruct
for T being Subset of GX holds Fr (Cl T) c= Fr T

proof end;

theorem Th39: :: TOPS_1:39

for GX being TopStruct
for T being Subset of GX holds Int T misses Fr T

proof end;

theorem Th40: :: TOPS_1:40

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

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:41

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

proof end;

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

proof end;

theorem Th42: :: TOPS_1:42

for TS being TopSpace
for P being Subset of TS holds
( P is open iff Fr P = (Cl P) \ P )

proof end;

theorem Th43: :: TOPS_1:43

for TS being TopSpace
for P being Subset of TS holds
( P is closed iff Fr P = P \ (Int P) )

proof end;

::
:: DENSE, BOUNDARY AND NOWHEREDENSE SETS
::

definition

let GX be TopStruct ;
let R be Subset of GX;

attr R is dense means :: TOPS_1:def 3
Cl R = [#] GX;

end;

:: deftheorem 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 by Th2;

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

existence
ex b₁ being Subset of GX st b₁ is dense

proof end;

end;

theorem :: TOPS_1:44

for GX being TopStruct
for R, S being Subset of GX st R is dense & R c= S holds
S is dense

proof end;

theorem Th45: :: TOPS_1:45

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 )

proof end;

theorem Th46: :: TOPS_1:46

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)

proof end;

theorem :: TOPS_1:47

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 by Th46;

definition

let GX be TopStruct ;
let R be Subset of GX;

attr R is boundary means :: TOPS_1:def 4
R ` is dense ;

end;

:: deftheorem 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 for Element of K10( the carrier of GX);

coherence
for b₁ being Subset of GX st b₁ is empty holds
b₁ is boundary

proof end;

end;

theorem Th48: :: TOPS_1:48

for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff Int R = {} )

proof end;

registration

let GX be TopStruct ;

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

existence
ex b₁ being Subset of GX st b₁ is boundary

proof end;

end;

registration

let GX be TopStruct ;
let R be boundary Subset of GX;

cluster Int R -> empty ;

coherence
Int R is empty by Th48;

end;

theorem Th49: :: TOPS_1:49

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

proof end;

theorem :: TOPS_1:50

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 = {} )

proof end;

theorem :: TOPS_1:51

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 ) )

proof end;

theorem :: TOPS_1:52

for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff R c= Fr R )

proof end;

registration

let GX be non empty TopSpace;

cluster [#] GX -> non boundary ;

coherence
not [#] GX is boundary

proof end;

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

existence
ex b₁ being Subset of GX st
( not b₁ is boundary & not b₁ is empty )

proof end;

end;

definition

let GX be TopStruct ;
let R be Subset of GX;

attr R is nowhere_dense means :: TOPS_1:def 5
Cl R is boundary ;

end;

:: deftheorem 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 for Element of K10( the carrier of TS);

coherence
for b₁ being Subset of TS st b₁ is empty holds
b₁ is nowhere_dense by PRE_TOPC:22;

end;

registration

let TS be TopSpace;

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

existence
ex b₁ being Subset of TS st b₁ is nowhere_dense

proof end;

end;

theorem :: TOPS_1:53

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

proof end;

theorem Th54: :: TOPS_1:54

for GX being TopStruct
for R being Subset of GX st R is nowhere_dense holds
R ` is dense

proof end;

registration

let TS be TopSpace;
let R be nowhere_dense Subset of TS;

cluster R ` -> dense ;

coherence
R ` is dense by Th54;

end;

theorem :: TOPS_1:55

for GX being TopStruct
for R being Subset of GX st R is nowhere_dense holds
R is boundary by Th54;

registration

let TS be TopSpace;

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

coherence
for b₁ being Subset of TS st b₁ is nowhere_dense holds
b₁ is boundary ;

end;

theorem Th56: :: TOPS_1:56

for GX being TopStruct
for S being Subset of GX st S is boundary & S is closed holds
S is nowhere_dense by PRE_TOPC:22;

registration

let TS be TopSpace;

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

coherence
for b₁ being Subset of TS st b₁ is boundary & b₁ is closed holds
b₁ is nowhere_dense by Th56;

end;

theorem :: TOPS_1:57

for GX being TopStruct
for R being Subset of GX st R is closed holds
( R is nowhere_dense iff R = Fr R )

proof end;

theorem Th58: :: TOPS_1:58

for TS being TopSpace
for P being Subset of TS st P is open holds
Fr P is nowhere_dense

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 Th58;

end;

theorem Th59: :: TOPS_1:59

for TS being TopSpace
for P being Subset of TS st P is closed holds
Fr P is nowhere_dense

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 Th59;

end;

theorem Th60: :: TOPS_1:60

for TS being TopSpace
for P being Subset of TS st P is open & P is nowhere_dense holds
P = {}

proof end;

registration

let TS be TopSpace;

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

coherence
for b₁ being Subset of TS st b₁ is open & b₁ is nowhere_dense holds
b₁ is empty by Th60;

end;

::
:: CLOSED AND OPEN DOMAIN, DOMAIN
::

definition

let GX be TopStruct ;
let R be Subset of GX;

attr R is condensed means :: TOPS_1:def 6
( Int (Cl R) c= R & R c= Cl (Int R) );

attr R is closed_condensed means :: TOPS_1:def 7
R = Cl (Int R);

attr R is open_condensed means :: TOPS_1:def 8
R = Int (Cl R);

end;

:: deftheorem 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 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 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:61

for GX being TopStruct
for R being Subset of GX holds
( R is open_condensed iff R ` is closed_condensed ) ;

theorem :: TOPS_1:62

for GX being TopStruct
for R being Subset of GX st R is closed_condensed holds
Fr (Int R) = Fr R ;

theorem :: TOPS_1:63

for GX being TopStruct
for R being Subset of GX st R is closed_condensed holds
Fr R c= Cl (Int R) by XBOOLE_1:17;

theorem Th64: :: TOPS_1:64

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 ) by Lm2;

theorem :: TOPS_1:65

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 ) by PRE_TOPC:22, Th23;

theorem :: TOPS_1:66

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 ) ) )

proof end;

theorem :: TOPS_1:67

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 ) ) )

proof end;

theorem Th68: :: TOPS_1:68

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

proof end;

theorem :: TOPS_1:69

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

proof end;

theorem :: TOPS_1:70

for TS being TopSpace
for P being Subset of TS st P is condensed holds
Int (Fr P) = {}

proof end;

theorem :: TOPS_1:71

for GX being TopStruct
for R being Subset of GX st R is condensed holds
( Int R is condensed & Cl R is condensed )

proof end;