:: by Zbigniew Karno

::

:: Received April 6, 1993

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

theorem Th1: :: TOPS_3:1

for X being TopStruct

for A being Subset of X holds

( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )

for A being Subset of X holds

( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )

proof end;

theorem Th6: :: TOPS_3:6

for X being TopSpace

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

Int (A \/ B) = Int (A \/ (Int B))

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

Int (A \/ B) = Int (A \/ (Int B))

proof end;

theorem :: TOPS_3:8

for X being TopSpace

for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds

Cl (Int A) = the carrier of X

for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds

Cl (Int A) = the carrier of X

proof end;

:: 2. Special Subsets of a Topological Space.

definition

let X be TopStruct ;

let A be Subset of X;

compatibility

( A is boundary iff Int A = {} ) by TOPS_1:48;

end;
let A be Subset of X;

compatibility

( A is boundary iff Int A = {} ) by TOPS_1:48;

:: deftheorem Def1 defines boundary TOPS_3:def 1 :

for X being TopStruct

for A being Subset of X holds

( A is boundary iff Int A = {} );

for X being TopStruct

for A being Subset of X holds

( A is boundary iff Int A = {} );

theorem :: TOPS_3:12

for X being TopSpace

for A being Subset of X holds

( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds

C = the carrier of X )

for A being Subset of X holds

( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds

C = the carrier of X )

proof end;

theorem :: TOPS_3:13

for X being TopSpace

for A being Subset of X holds

( A is boundary iff for G being Subset of X st G <> {} & G is open holds

A ` meets G )

for A being Subset of X holds

( A is boundary iff for G being Subset of X st G <> {} & G is open holds

A ` meets G )

proof end;

theorem :: TOPS_3:14

for X being TopSpace

for A being Subset of X holds

( A is boundary iff for F being Subset of X st F is closed holds

Int F = Int (F \/ A) )

for A being Subset of X holds

( A is boundary iff for F being Subset of X st F is closed holds

Int F = Int (F \/ A) )

proof end;

theorem :: TOPS_3:15

definition

let X be TopStruct ;

let A be Subset of X;

compatibility

( A is dense iff Cl A = the carrier of X )

end;
let A be Subset of X;

compatibility

( A is dense iff Cl A = the carrier of X )

proof end;

:: deftheorem defines dense TOPS_3:def 2 :

for X being TopStruct

for A being Subset of X holds

( A is dense iff Cl A = the carrier of X );

for X being TopStruct

for A being Subset of X holds

( A is dense iff Cl A = the carrier of X );

theorem :: TOPS_3:19

theorem :: TOPS_3:20

for X being non empty TopSpace

for A being Subset of X holds

( A is dense iff for G being Subset of X st G is open holds

Cl G = Cl (G /\ A) )

for A being Subset of X holds

( A is dense iff for G being Subset of X st G is open holds

Cl G = Cl (G /\ A) )

proof end;

theorem :: TOPS_3:21

definition

let X be TopStruct ;

let A be Subset of X;

compatibility

( A is nowhere_dense iff Int (Cl A) = {} ) by Def1, TOPS_1:def 5;

end;
let A be Subset of X;

compatibility

( A is nowhere_dense iff Int (Cl A) = {} ) by Def1, TOPS_1:def 5;

:: deftheorem defines nowhere_dense TOPS_3:def 3 :

for X being TopStruct

for A being Subset of X holds

( A is nowhere_dense iff Int (Cl A) = {} );

for X being TopStruct

for A being Subset of X holds

( A is nowhere_dense iff Int (Cl A) = {} );

theorem :: TOPS_3:23

theorem :: TOPS_3:24

for X being non empty TopSpace

for A being Subset of X st A is nowhere_dense holds

Cl A is nowhere_dense ;

for A being Subset of X st A is nowhere_dense holds

Cl A is nowhere_dense ;

theorem Th26: :: TOPS_3:26

for X being non empty TopSpace

for A, B being Subset of X st B is nowhere_dense & A c= B holds

A is nowhere_dense

for A, B being Subset of X st B is nowhere_dense & A c= B holds

A is nowhere_dense

proof end;

theorem Th27: :: TOPS_3:27

for X being non empty TopSpace

for A being Subset of X holds

( A is nowhere_dense iff ex C being Subset of X st

( A c= C & C is closed & C is boundary ) )

for A being Subset of X holds

( A is nowhere_dense iff ex C being Subset of X st

( A c= C & C is closed & C is boundary ) )

proof end;

theorem Th28: :: TOPS_3:28

for X being non empty TopSpace

for A being Subset of X holds

( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds

ex H being Subset of X st

( H c= G & H <> {} & H is open & A misses H ) )

for A being Subset of X holds

( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds

ex H being Subset of X st

( H c= G & H <> {} & H is open & A misses H ) )

proof end;

theorem :: TOPS_3:29

for X being non empty TopSpace

for A, B being Subset of X st A is nowhere_dense holds

A /\ B is nowhere_dense by Th26, XBOOLE_1:17;

for A, B being Subset of X st A is nowhere_dense holds

A /\ B is nowhere_dense by Th26, XBOOLE_1:17;

theorem Th30: :: TOPS_3:30

for X being non empty TopSpace

for A, B being Subset of X st A is nowhere_dense & B is boundary holds

A \/ B is boundary

for A, B being Subset of X st A is nowhere_dense & B is boundary holds

A \/ B is boundary

proof end;

:: deftheorem defines everywhere_dense TOPS_3:def 4 :

for X being TopStruct

for A being Subset of X holds

( A is everywhere_dense iff Cl (Int A) = [#] X );

for X being TopStruct

for A being Subset of X holds

( A is everywhere_dense iff Cl (Int A) = [#] X );

definition

let X be TopStruct ;

let A be Subset of X;

compatibility

( A is everywhere_dense iff Cl (Int A) = the carrier of X ) ;

end;
let A be Subset of X;

compatibility

( A is everywhere_dense iff Cl (Int A) = the carrier of X ) ;

:: deftheorem defines everywhere_dense TOPS_3:def 5 :

for X being TopStruct

for A being Subset of X holds

( A is everywhere_dense iff Cl (Int A) = the carrier of X );

for X being TopStruct

for A being Subset of X holds

( A is everywhere_dense iff Cl (Int A) = the carrier of X );

theorem :: TOPS_3:32

for X being non empty TopSpace

for A being Subset of X st A is everywhere_dense holds

Int A is everywhere_dense ;

for A being Subset of X st A is everywhere_dense holds

Int A is everywhere_dense ;

theorem :: TOPS_3:34

theorem :: TOPS_3:35

theorem :: TOPS_3:37

for X being non empty TopSpace

for A being Subset of X st A is everywhere_dense holds

not A is boundary by PRE_TOPC:22;

for A being Subset of X st A is everywhere_dense holds

not A is boundary by PRE_TOPC:22;

theorem Th38: :: TOPS_3:38

for X being non empty TopSpace

for A, B being Subset of X st A is everywhere_dense & A c= B holds

B is everywhere_dense

for A, B being Subset of X st A is everywhere_dense & A c= B holds

B is everywhere_dense

proof end;

theorem Th39: :: TOPS_3:39

for X being non empty TopSpace

for A being Subset of X holds

( A is everywhere_dense iff A ` is nowhere_dense )

for A being Subset of X holds

( A is everywhere_dense iff A ` is nowhere_dense )

proof end;

theorem Th40: :: TOPS_3:40

for X being non empty TopSpace

for A being Subset of X holds

( A is nowhere_dense iff A ` is everywhere_dense )

for A being Subset of X holds

( A is nowhere_dense iff A ` is everywhere_dense )

proof end;

theorem Th41: :: TOPS_3:41

for X being non empty TopSpace

for A being Subset of X holds

( A is everywhere_dense iff ex C being Subset of X st

( C c= A & C is open & C is dense ) )

for A being Subset of X holds

( A is everywhere_dense iff ex C being Subset of X st

( C c= A & C is open & C is dense ) )

proof end;

theorem :: TOPS_3:42

for X being non empty TopSpace

for A being Subset of X holds

( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds

ex H being Subset of X st

( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )

for A being Subset of X holds

( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds

ex H being Subset of X st

( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )

proof end;

theorem :: TOPS_3:43

for X being non empty TopSpace

for A, B being Subset of X st A is everywhere_dense holds

A \/ B is everywhere_dense by Th38, XBOOLE_1:7;

for A, B being Subset of X st A is everywhere_dense holds

A \/ B is everywhere_dense by Th38, XBOOLE_1:7;

theorem Th44: :: TOPS_3:44

for X being non empty TopSpace

for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds

A /\ B is everywhere_dense

for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds

A /\ B is everywhere_dense

proof end;

theorem Th45: :: TOPS_3:45

for X being non empty TopSpace

for A, B being Subset of X st A is everywhere_dense & B is dense holds

A /\ B is dense

for A, B being Subset of X st A is everywhere_dense & B is dense holds

A /\ B is dense

proof end;

theorem :: TOPS_3:46

for X being non empty TopSpace

for A, B being Subset of X st A is dense & B is nowhere_dense holds

A \ B is dense

for A, B being Subset of X st A is dense & B is nowhere_dense holds

A \ B is dense

proof end;

theorem :: TOPS_3:47

for X being non empty TopSpace

for A, B being Subset of X st A is everywhere_dense & B is boundary holds

A \ B is dense

for A, B being Subset of X st A is everywhere_dense & B is boundary holds

A \ B is dense

proof end;

theorem :: TOPS_3:48

for X being non empty TopSpace

for A, B being Subset of X st A is everywhere_dense & B is nowhere_dense holds

A \ B is everywhere_dense

for A, B being Subset of X st A is everywhere_dense & B is nowhere_dense holds

A \ B is everywhere_dense

proof end;

theorem :: TOPS_3:49

for X being non empty TopSpace

for D being Subset of X st D is everywhere_dense holds

ex C, B being Subset of X st

( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )

for D being Subset of X st D is everywhere_dense holds

ex C, B being Subset of X st

( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )

proof end;

theorem :: TOPS_3:50

for X being non empty TopSpace

for D being Subset of X st D is everywhere_dense holds

ex C, B being Subset of X st

( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )

for D being Subset of X st D is everywhere_dense holds

ex C, B being Subset of X st

( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )

proof end;

theorem :: TOPS_3:51

for X being non empty TopSpace

for D being Subset of X st D is nowhere_dense holds

ex C, B being Subset of X st

( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )

for D being Subset of X st D is nowhere_dense holds

ex C, B being Subset of X st

( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )

proof end;

theorem :: TOPS_3:52

for X being non empty TopSpace

for D being Subset of X st D is nowhere_dense holds

ex C, B being Subset of X st

( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )

for D being Subset of X st D is nowhere_dense holds

ex C, B being Subset of X st

( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )

proof end;

theorem Th53: :: TOPS_3:53

for X being non empty TopSpace

for Y0 being SubSpace of X

for A being Subset of X

for B being Subset of Y0 st B c= A holds

Cl B c= Cl A

for Y0 being SubSpace of X

for A being Subset of X

for B being Subset of Y0 st B c= A holds

Cl B c= Cl A

proof end;

theorem Th54: :: TOPS_3:54

for X being non empty TopSpace

for Y0 being SubSpace of X

for C, A being Subset of X

for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds

Cl A = Cl B

for Y0 being SubSpace of X

for C, A being Subset of X

for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds

Cl A = Cl B

proof end;

theorem :: TOPS_3:55

for X being non empty TopSpace

for Y0 being non empty closed SubSpace of X

for A being Subset of X

for B being Subset of Y0 st A = B holds

Cl A = Cl B

for Y0 being non empty closed SubSpace of X

for A being Subset of X

for B being Subset of Y0 st A = B holds

Cl A = Cl B

proof end;

theorem Th56: :: TOPS_3:56

for X being non empty TopSpace

for Y0 being SubSpace of X

for A being Subset of X

for B being Subset of Y0 st A c= B holds

Int A c= Int B

for Y0 being SubSpace of X

for A being Subset of X

for B being Subset of Y0 st A c= B holds

Int A c= Int B

proof end;

theorem Th57: :: TOPS_3:57

for X being non empty TopSpace

for Y0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds

Int A = Int B

for Y0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds

Int A = Int B

proof end;

theorem :: TOPS_3:58

for X being non empty TopSpace

for Y0 being non empty open SubSpace of X

for A being Subset of X

for B being Subset of Y0 st A = B holds

Int A = Int B

for Y0 being non empty open SubSpace of X

for A being Subset of X

for B being Subset of Y0 st A = B holds

Int A = Int B

proof end;

theorem Th59: :: TOPS_3:59

for X being non empty TopSpace

for X0 being SubSpace of X

for A being Subset of X

for B being Subset of X0 st A c= B & A is dense holds

B is dense

for X0 being SubSpace of X

for A being Subset of X

for B being Subset of X0 st A c= B & A is dense holds

B is dense

proof end;

theorem Th60: :: TOPS_3:60

for X being non empty TopSpace

for X0 being SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds

( ( C is dense & B is dense ) iff A is dense )

for X0 being SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds

( ( C is dense & B is dense ) iff A is dense )

proof end;

theorem Th61: :: TOPS_3:61

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for A being Subset of X

for B being Subset of X0 st A c= B & A is everywhere_dense holds

B is everywhere_dense

for X0 being non empty SubSpace of X

for A being Subset of X

for B being Subset of X0 st A c= B & A is everywhere_dense holds

B is everywhere_dense

proof end;

theorem Th62: :: TOPS_3:62

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds

( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )

for X0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds

( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )

proof end;

theorem :: TOPS_3:63

for X being non empty TopSpace

for X0 being non empty open SubSpace of X

for A, C being Subset of X

for B being Subset of X0 st C = the carrier of X0 & A = B holds

( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )

for X0 being non empty open SubSpace of X

for A, C being Subset of X

for B being Subset of X0 st C = the carrier of X0 & A = B holds

( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )

proof end;

theorem :: TOPS_3:64

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds

( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )

for X0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds

( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )

proof end;

theorem :: TOPS_3:67

for X being non empty TopSpace

for X0 being non empty open SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( A is boundary iff B is boundary )

for X0 being non empty open SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( A is boundary iff B is boundary )

proof end;

theorem Th68: :: TOPS_3:68

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for A being Subset of X

for B being Subset of X0 st A c= B & B is nowhere_dense holds

A is nowhere_dense

for X0 being non empty SubSpace of X

for A being Subset of X

for B being Subset of X0 st A c= B & B is nowhere_dense holds

A is nowhere_dense

proof end;

Lm1: for X being non empty TopSpace

for X0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds

B is nowhere_dense

proof end;

theorem Th69: :: TOPS_3:69

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds

B is nowhere_dense

for X0 being non empty SubSpace of X

for C, A being Subset of X

for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds

B is nowhere_dense

proof end;

theorem :: TOPS_3:70

for X being non empty TopSpace

for X0 being non empty open SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( A is nowhere_dense iff B is nowhere_dense )

for X0 being non empty open SubSpace of X

for A being Subset of X

for B being Subset of X0 st A = B holds

( A is nowhere_dense iff B is nowhere_dense )

proof end;

:: 4. Subsets in Topological Spaces with the same Topological Structures.

theorem :: TOPS_3:71

for X1, X2 being 1-sorted st the carrier of X1 = the carrier of X2 holds

for C1 being Subset of X1

for C2 being Subset of X2 holds

( C1 = C2 iff C1 ` = C2 ` )

for C1 being Subset of X1

for C2 being Subset of X2 holds

( C1 = C2 iff C1 ` = C2 ` )

proof end;

theorem Th72: :: TOPS_3:72

for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1

for C2 being Subset of X2 st C1 = C2 holds

( C1 is open iff C2 is open ) ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

for C2 being Subset of X2 st C1 = C2 holds

( C1 is open iff C2 is open ) ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

proof end;

theorem Th73: :: TOPS_3:73

for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1

for C2 being Subset of X2 st C1 = C2 holds

( C1 is closed iff C2 is closed ) ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

for C2 being Subset of X2 st C1 = C2 holds

( C1 is closed iff C2 is closed ) ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

proof end;

theorem :: TOPS_3:74

for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1

for C2 being Subset of X2 st C1 = C2 holds

Int C1 = Int C2 ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

for C2 being Subset of X2 st C1 = C2 holds

Int C1 = Int C2 ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

proof end;

theorem :: TOPS_3:75

for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1

for C2 being Subset of X2 st C1 = C2 holds

Cl C1 = Cl C2 ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

for C2 being Subset of X2 st C1 = C2 holds

Cl C1 = Cl C2 ) holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

proof end;

theorem Th77: :: TOPS_3:77

for X1, X2 being TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Int D1 = Int D2

for D1 being Subset of X1

for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Int D1 = Int D2

proof end;

theorem Th78: :: TOPS_3:78

for X1, X2 being TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Int D1 c= Int D2

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Int D1 c= Int D2

proof end;

theorem Th80: :: TOPS_3:80

for X1, X2 being TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Cl D1 = Cl D2

for D1 being Subset of X1

for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Cl D1 = Cl D2

proof end;

theorem Th81: :: TOPS_3:81

for X1, X2 being TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Cl D1 c= Cl D2

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds

Cl D1 c= Cl D2

proof end;

theorem Th82: :: TOPS_3:82

for X1, X2 being TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds

D2 is boundary

for D1 being Subset of X1

for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds

D2 is boundary

proof end;

theorem Th83: :: TOPS_3:83

for X1, X2 being TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds

D2 is dense

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds

D2 is dense

proof end;

theorem :: TOPS_3:84

for X1, X2 being TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds

D2 is nowhere_dense

for D1 being Subset of X1

for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds

D2 is nowhere_dense

proof end;

theorem :: TOPS_3:85

for X1, X2 being non empty TopSpace

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds

D2 is everywhere_dense

for D1 being Subset of X1

for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds

D2 is everywhere_dense

proof end;