The abstract of the Mizar article:

Remarks on Special Subsets of Topological Spaces

by

Zbigniew Karno

Received April 6, 1993

MML identifier: TOPS_3

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, BOOLE, SUBSET_1, TOPS_1, TOPS_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
      TSEP_1;
 constructors TOPS_1, BORSUK_1, TSEP_1, MEMBERED;
 clusters BORSUK_1, TSEP_1, PRE_TOPC, TOPS_1, MEMBERED, ZFMISC_1;
 requirements BOOLE, SUBSET;


begin
:: 1. Selected Properties of Subsets of a Topological Space.
reserve X for TopStruct, A for Subset of X;

theorem :: TOPS_3:1
 (A = {}X iff  A` = [#]X) &
   (A = {} iff  A` = the carrier of X);

theorem :: TOPS_3:2
 (A = [#]X iff  A` = {}X) &
   (A = the carrier of X iff  A` = {});

theorem :: TOPS_3:3
 for X being TopSpace, A,B being Subset of X holds
  Int A /\ Cl B c= Cl(A /\ B);

reserve X for TopSpace, A,B for Subset of X;

theorem :: TOPS_3:4
 Int(A \/ B) c= (Cl A) \/ Int B;

theorem :: TOPS_3:5
 for A being Subset of X st A is closed holds Int(A \/ B) c= A \/ Int B;

theorem :: TOPS_3:6
 for A being Subset of X st A is closed holds Int(A \/ B) = Int(A \/ Int B);

theorem :: TOPS_3:7
 A misses Int Cl A implies Int Cl A = {};

theorem :: TOPS_3:8
   A \/ Cl Int A = the carrier of X implies Cl Int A = the carrier of X;

begin
:: 2. Special Subsets of a Topological Space.

definition let X be TopStruct, A be Subset of X;
 redefine attr A is boundary means
:: TOPS_3:def 1
 Int A = {};
end;

theorem :: TOPS_3:9
 {}X is boundary;

reserve X for non empty TopSpace, A for Subset of X;

theorem :: TOPS_3:10
 A is boundary implies A <> the carrier of X;

reserve X for TopSpace, A,B for Subset of X;

theorem :: TOPS_3:11
 B is boundary & A c= B implies A is boundary;

theorem :: TOPS_3:12
   A is boundary iff
  for C being Subset of X st  A` c= C & C is closed
   holds C = the carrier of X;

theorem :: TOPS_3:13
    A is boundary iff
   for G being Subset of X st G <> {} & G is open holds ( A`) meets G;

theorem :: TOPS_3:14
    A is boundary iff
   for F being Subset of X holds F is closed
    implies Int F = Int(F \/ A);

theorem :: TOPS_3:15
   A is boundary or B is boundary implies A /\ B is boundary;

definition let X be TopStruct, A be Subset of X;
 redefine attr A is dense means
:: TOPS_3:def 2
 Cl A = the carrier of X;
end;

theorem :: TOPS_3:16
   [#]X is dense;

reserve X for non empty TopSpace, A, B for Subset of X;

theorem :: TOPS_3:17
 A is dense implies A <> {};

theorem :: TOPS_3:18
 A is dense iff  A` is boundary;

theorem :: TOPS_3:19
   A is dense iff
  for C being Subset of X st A c= C & C is closed
   holds C = the carrier of X;

theorem :: TOPS_3:20
   A is dense iff
  for G being Subset of X holds G is open
   implies Cl G = Cl(G /\ A);

theorem :: TOPS_3:21
   A is dense or B is dense implies A \/ B is dense;

definition let X be TopStruct, A be Subset of X;
 redefine attr A is nowhere_dense means
:: TOPS_3:def 3
 Int(Cl A) = {};
end;

theorem :: TOPS_3:22
 {}X is nowhere_dense;

theorem :: TOPS_3:23
   A is nowhere_dense implies A <> the carrier of X;

theorem :: TOPS_3:24
   A is nowhere_dense implies Cl A is nowhere_dense;

theorem :: TOPS_3:25
   A is nowhere_dense implies A is not dense;

theorem :: TOPS_3:26
 B is nowhere_dense & A c= B implies A is nowhere_dense;

theorem :: TOPS_3:27
 A is nowhere_dense iff ex C being Subset of X st
                          A c= C & C is closed & C is boundary;

theorem :: TOPS_3:28
 A is nowhere_dense iff
  for G being Subset of X st G <> {} & G is open
   ex H being Subset of X
    st H c= G & H <> {} & H is open & A misses H;

theorem :: TOPS_3:29
   A is nowhere_dense or B is nowhere_dense implies A /\ B is nowhere_dense;

theorem :: TOPS_3:30
 A is nowhere_dense & B is boundary implies A \/ B is boundary;

definition let X be TopStruct, A be Subset of X;
 attr A is everywhere_dense means
:: TOPS_3:def 4
 Cl(Int A) = [#]X;
end;

definition let X be TopStruct, A be Subset of X;
 redefine attr A is everywhere_dense means
:: TOPS_3:def 5
    Cl(Int A) = the carrier of X;
end;

theorem :: TOPS_3:31
   [#]X is everywhere_dense;

theorem :: TOPS_3:32
 A is everywhere_dense implies Int A is everywhere_dense;

theorem :: TOPS_3:33
 A is everywhere_dense implies A is dense;

theorem :: TOPS_3:34
   A is everywhere_dense implies A <> {};

theorem :: TOPS_3:35
 A is everywhere_dense iff Int A is dense;

theorem :: TOPS_3:36
 A is open & A is dense implies A is everywhere_dense;

theorem :: TOPS_3:37
   A is everywhere_dense implies A is not boundary;

theorem :: TOPS_3:38
 A is everywhere_dense & A c= B implies B is everywhere_dense;

theorem :: TOPS_3:39
 A is everywhere_dense iff  A` is nowhere_dense;

theorem :: TOPS_3:40
 A is nowhere_dense iff  A` is everywhere_dense;

theorem :: TOPS_3:41
 A is everywhere_dense iff ex C being Subset of X st
                             C c= A & C is open & C is dense;

theorem :: TOPS_3:42
   A is everywhere_dense iff
  for F being Subset of X st F <> the carrier of X & F is closed
   ex H being Subset of X st
    F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X;

theorem :: TOPS_3:43
   A is everywhere_dense or B is everywhere_dense implies
  A \/ B is everywhere_dense;

theorem :: TOPS_3:44
 A is everywhere_dense & B is everywhere_dense implies
  A /\ B is everywhere_dense;

theorem :: TOPS_3:45
 A is everywhere_dense & B is dense implies A /\ B is dense;

theorem :: TOPS_3:46
   A is dense & B is nowhere_dense implies A \ B is dense;

theorem :: TOPS_3:47
   A is everywhere_dense & B is boundary implies A \ B is dense;

theorem :: TOPS_3:48
   A is everywhere_dense & B is nowhere_dense implies A \ B is everywhere_dense
;

reserve D for Subset of X;

theorem :: TOPS_3:49
   D is everywhere_dense implies
   ex C,B being Subset of X st
     C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B;

theorem :: TOPS_3:50
   D is everywhere_dense implies
  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;

theorem :: TOPS_3:51
   D is nowhere_dense implies
  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;

theorem :: TOPS_3:52
   D is nowhere_dense implies
  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;


begin
:: 3. Properties of Subsets in Subspaces.
reserve Y0 for SubSpace of X;

theorem :: TOPS_3:53
 for A being Subset of X, B being Subset of Y0
  st B c= A holds Cl B c= Cl A;

theorem :: TOPS_3:54
 for C, A being Subset of X,
     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;

theorem :: TOPS_3:55
   for Y0 being closed non empty SubSpace of X
  for A being Subset of X, B being Subset of Y0
   st A = B holds Cl A = Cl B;

theorem :: TOPS_3:56
 for A being Subset of X, B being Subset of Y0
  st A c= B holds Int A c= Int B;

theorem :: TOPS_3:57
 for Y0 being non empty SubSpace of X,
     C, A being Subset of X,
     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;

theorem :: TOPS_3:58
   for Y0 being open non empty SubSpace of X
  for A being Subset of X, B being Subset of Y0
   st A = B holds Int A = Int B;

reserve X0 for SubSpace of X;

theorem :: TOPS_3:59
 for A being Subset of X, B being Subset of X0 st A c= B holds
  A is dense implies B is dense;

theorem :: TOPS_3:60
 for C, A being Subset of X, 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;

reserve X0 for non empty SubSpace of X;

theorem :: TOPS_3:61
 for A being Subset of X, B being Subset of X0 st A c= B holds
  A is everywhere_dense implies B is everywhere_dense;

theorem :: TOPS_3:62
 for C, A being Subset of X,
     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;

theorem :: TOPS_3:63
   for X0 being open non empty SubSpace of X
  for A,C being Subset of X,
      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;

theorem :: TOPS_3:64
   for C, A being Subset of X,
     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;

theorem :: TOPS_3:65
 for A being Subset of X,
     B being Subset of X0 st A c= B holds
  B is boundary implies A is boundary;

theorem :: TOPS_3:66
 for C, A being Subset of X,
     B being Subset of X0 st
   C is open & C c= the carrier of X0 & A c= C & A = B holds
  A is boundary implies B is boundary;

theorem :: TOPS_3:67
   for X0 being open non empty SubSpace of X
  for A being Subset of X,
      B being Subset of X0 st A = B holds
   A is boundary iff B is boundary;

theorem :: TOPS_3:68
 for A being Subset of X,
     B being Subset of X0 st A c= B holds
   B is nowhere_dense implies A is nowhere_dense;

theorem :: TOPS_3:69
 for C, A being Subset of X,
     B being Subset of X0 st
   C is open & C c= the carrier of X0 & A c= C & A = B holds
  A is nowhere_dense implies B is nowhere_dense;

theorem :: TOPS_3:70
   for X0 being open non empty SubSpace of X
  for A being Subset of X,
      B being Subset of X0 st A = B holds
   A is nowhere_dense iff B is nowhere_dense;


begin
:: 4. Subsets in Topological Spaces with the same Topological Structures.
theorem :: TOPS_3:71
   for X1, X2 being 1-sorted holds
 the carrier of X1 = the carrier of X2 implies
  for C1 being Subset of X1,
      C2 being Subset of X2 holds
    C1 = C2 iff  C1` =  C2`;

reserve X1,X2 for TopStruct;

theorem :: TOPS_3:72
 the carrier of X1 = the carrier of X2 &
  (for C1 being Subset of X1,
       C2 being Subset of X2 st C1 = C2 holds
    (C1 is open iff C2 is open)) implies
  the TopStruct of X1 = the TopStruct of X2;

theorem :: TOPS_3:73
 the carrier of X1 = the carrier of X2 &
  (for C1 being Subset of X1,
       C2 being Subset of X2 st C1 = C2 holds
    (C1 is closed iff C2 is closed)) implies
  the TopStruct of X1 = the TopStruct of X2;

reserve X1,X2 for TopSpace;

theorem :: TOPS_3:74
   the carrier of X1 = the carrier of X2 &
  (for C1 being Subset of X1,
       C2 being Subset of X2 st C1 = C2 holds
    Int C1 = Int C2) implies
  the TopStruct of X1 = the TopStruct of X2;

theorem :: TOPS_3:75
   the carrier of X1 = the carrier of X2 &
  (for C1 being Subset of X1,
       C2 being Subset of X2 st C1 = C2 holds
    Cl C1 = Cl C2) implies
  the TopStruct of X1 = the TopStruct of X2;

reserve D1 for Subset of X1, D2 for Subset of X2;

theorem :: TOPS_3:76
 D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies
   (D1 is open implies D2 is open);

theorem :: TOPS_3:77
 D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies Int D1 = Int D2;

theorem :: TOPS_3:78
 D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies Int D1 c= Int D2;

theorem :: TOPS_3:79
 D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies
   (D1 is closed implies D2 is closed);

theorem :: TOPS_3:80
 D1 = D2 & the TopStruct of X1 = the TopStruct of X2 implies Cl D1 = Cl D2;

theorem :: TOPS_3:81
 D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies Cl D1 c= Cl D2;

theorem :: TOPS_3:82
 D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies
   (D1 is boundary implies D2 is boundary);

theorem :: TOPS_3:83
 D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies
   (D1 is dense implies D2 is dense);

theorem :: TOPS_3:84
   D2 c= D1 & the TopStruct of X1 = the TopStruct of X2 implies
   (D1 is nowhere_dense implies D2 is nowhere_dense);

reserve X1,X2 for non empty TopSpace;
reserve D1 for Subset of X1, D2 for Subset of X2;

theorem :: TOPS_3:85
   D1 c= D2 & the TopStruct of X1 = the TopStruct of X2 implies
   (D1 is everywhere_dense implies D2 is everywhere_dense);