:: Remarks on Special Subsets of Topological Spaces
::  by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies PRE_TOPC, SUBSET_1, XBOOLE_0, STRUCT_0, TOPS_1, TARSKI, RCOMP_1,
      TOPS_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1,
      TSEP_1;
 constructors TOPS_1, BORSUK_1, TSEP_1;
 registrations PRE_TOPC, TOPS_1, BORSUK_1, TSEP_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 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 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 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 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);