:: The Properties of Supercondensed Sets, Subcondensed Sets and Condensed Sets
::  by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 31, 2005
:: Copyright (c) 2005-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 NUMBERS, PRE_TOPC, SUBSET_1, ZFMISC_1, TEX_1, TDLAT_3, XBOOLE_0,
      STRUCT_0, TOPS_1, RCOMP_1, TARSKI, DECOMP_1, TOPMETR, XXREAL_1, XXREAL_0,
      BORSUK_5, ARYTM_3, LIMFUNC1, ISOMICHI, REAL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, LIMFUNC1, RCOMP_1,
      NUMBERS, DOMAIN_1, ZFMISC_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TEX_1,
      TOPMETR, BORSUK_5, SEQ_4, DECOMP_1, XXREAL_0;
 constructors PROB_1, SEQ_4, RCOMP_1, LIMFUNC1, TOPS_1, TDLAT_3, TEX_1,
      TOPMETR, BORSUK_5, DECOMP_1;
 registrations XBOOLE_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, ZFMISC_1,
      STRUCT_0, TOPS_1, TEX_1, TEX_2, TOPMETR, FCONT_3, PRE_TOPC;
 requirements BOOLE, SUBSET, NUMERALS, REAL;


begin :: Preliminaries

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

registration
  let D be non trivial set;
  cluster ADTS D -> non trivial;
end;

registration
  cluster anti-discrete non trivial strict for TopSpace;
end;

theorem :: ISOMICHI:1
  Int Cl Int A /\ Int Cl Int B = Int Cl Int (A /\ B);

theorem :: ISOMICHI:2
  Cl Int Cl (A \/ B) = Cl Int Cl A \/ Cl Int Cl B;

begin :: Connections between Supercondensed, Condensed and Subcondensed Sets

definition
  let T be TopStruct, A be Subset of T;
  attr A is supercondensed means
:: ISOMICHI:def 1

  Int Cl A = Int A;
  attr A is subcondensed means
:: ISOMICHI:def 2

  Cl Int A = Cl A;
end;

registration
  let T;
  cluster closed -> supercondensed for Subset of T;
end;

theorem :: ISOMICHI:3 :: Remark 1
  A is closed implies A is supercondensed;

theorem :: ISOMICHI:4
  A is open implies A is subcondensed;

definition
  let T be TopSpace, A be Subset of T;
  redefine attr A is condensed means
:: ISOMICHI:def 3

  Cl Int A = Cl A & Int Cl A = Int A;
end;

theorem :: ISOMICHI:5  :: Remark 2
  A is condensed iff A is subcondensed & A is supercondensed;

registration
  let T be TopSpace;
  cluster condensed -> subcondensed supercondensed for Subset of T;
  cluster subcondensed supercondensed -> condensed for Subset of T;
end;

registration
  let T be TopSpace;
  cluster condensed subcondensed supercondensed for Subset of T;
end;

theorem :: ISOMICHI:6 :: Theorem 1
  A is supercondensed implies A` is subcondensed;

theorem :: ISOMICHI:7 :: Theorem 1
  A is subcondensed implies A` is supercondensed;

:: Corollary to Theorem 1
::  A is condensed implies A` is condensed = TDLAT_1:16;

theorem :: ISOMICHI:8  :: Theorem 2
  A is supercondensed iff Int Cl A c= A;

theorem :: ISOMICHI:9  :: Theorem 2
  A is subcondensed iff A c= Cl Int A;

registration
  let T be TopSpace;
  cluster subcondensed -> semi-open for Subset of T;
  cluster semi-open -> subcondensed for Subset of T;
end;

theorem :: ISOMICHI:10  :: Corollary to Theorem 2
  A is condensed iff Int Cl A c= A & A c= Cl Int A;

begin :: Regular Open and Regular Closed Sets

notation
  let T be TopStruct, A be Subset of T;
  synonym A is regular_open for A is open_condensed;
end;

notation
  let T be TopStruct, A be Subset of T;
  synonym A is regular_closed for A is closed_condensed;
end;

theorem :: ISOMICHI:11 :: Remark 1
  for T being TopSpace holds [#]T is regular_open & [#]T is regular_closed;

registration
  let T be TopSpace;
  cluster [#]T -> regular_open regular_closed;
end;

registration
  let T be TopSpace;
  cluster empty -> regular_open regular_closed for Subset of T;
end;

theorem :: ISOMICHI:12
  Int Cl {}T = {}T;

theorem :: ISOMICHI:13  :: Remark 2
  A is regular_open implies A` is regular_closed;

registration
  let T be TopSpace;
  cluster regular_open regular_closed for Subset of T;
end;

registration
  let T be TopSpace;
  let A be regular_open Subset of T;
  cluster A` -> regular_closed;
end;

theorem :: ISOMICHI:14  :: Remark 2
  A is regular_closed implies A` is regular_open;

registration
  let T be TopSpace;
  let A be regular_closed Subset of T;
  cluster A` -> regular_open;
end;

registration
  let T be TopSpace;
  cluster regular_open -> open for Subset of T;
  cluster regular_closed -> closed for Subset of T;
end;

:: (A is regular_open & B is regular_open) implies
::   A /\ B is regular_open by TOPS_1:109;
:: A is regular_closed & B is regular_closed implies
::   A \/ B is regular_closed by TOPS_1:108;

theorem :: ISOMICHI:15  :: Remark 3
  Int Cl A is regular_open & Cl Int A is regular_closed;

registration
  let T be TopSpace, A be Subset of T;
  cluster Int Cl A -> regular_open;
  cluster Cl Int A -> regular_closed;
end;

theorem :: ISOMICHI:16 :: Theorem 3
  A is regular_open iff A is supercondensed & A is open;

theorem :: ISOMICHI:17 :: Theorem 3
  A is regular_closed iff A is subcondensed & A is closed;

registration
  let T be TopSpace;
  cluster regular_open -> condensed open for Subset of T;
  cluster condensed open -> regular_open for Subset of T;
  cluster regular_closed -> condensed closed for Subset of T;
  cluster condensed closed -> regular_closed for Subset of T;
end;

theorem :: ISOMICHI:18 :: Corollary to Theorem 3:: Theorem 4
  A is condensed iff ex B st B is regular_open & B c= A & A c= Cl B;

theorem :: ISOMICHI:19 :: Theorem 4
  A is condensed iff ex B st B is regular_closed & Int B c= A & A c= B;

begin :: Boundaries and Borders

definition
  let T be TopStruct, A be Subset of T;
  redefine func Fr A equals
:: ISOMICHI:def 4
  Cl A \ Int A;
end;

theorem :: ISOMICHI:20 :: Theorem 5
  A is condensed iff Fr A = Cl Int A \ Int Cl A & Fr A = Cl Int A /\ Cl Int A`;

definition
  let T be TopStruct, A be Subset of T;
  func Border A -> Subset of T equals
:: ISOMICHI:def 5
  Int Fr A;
end;

theorem :: ISOMICHI:21  :: Theorem 6
  Border A is regular_open & Border A = (Int Cl A) \ (Cl Int A) &
  Border A = Int Cl A /\ (Int Cl A`);

registration
  let T be TopSpace, A be Subset of T;
  cluster Border A -> regular_open;
end;

theorem :: ISOMICHI:22  :: Theorem 7
  A is supercondensed iff Int A is regular_open & Border A is empty;

theorem :: ISOMICHI:23  :: Theorem 7
  A is subcondensed iff Cl A is regular_closed & Border A is empty;

registration
  let T be TopSpace, A be Subset of T;
  cluster Border Border A -> empty;
end;

theorem :: ISOMICHI:24 :: Remark:: Corollary to Theorem 7
  A is condensed iff Int A is regular_open & Cl A is regular_closed &
  Border A is empty;

begin :: Auxiliary Theorems

theorem :: ISOMICHI:25
  for A being Subset of R^1, a being Real st A = ]. -infty, a.]
  holds Int A = ]. -infty, a.[;

theorem :: ISOMICHI:26
  for A being Subset of R^1, a being Real st A = [.a,+infty .[
  holds Int A = ].a,+infty .[;

theorem :: ISOMICHI:27
  for A being Subset of R^1, a, b being Real st A = ].
  -infty,a.] \/ IRRAT (a,b) \/ [.b,+infty .[ holds Cl A = the carrier of R^1;

theorem :: ISOMICHI:28
  for A being Subset of R^1, a, b being Real st A = RAT (a,b)
  holds Int A = {};

theorem :: ISOMICHI:29
  for A being Subset of R^1, a, b being Real st A = IRRAT (a,b)
  holds Int A = {};

theorem :: ISOMICHI:30
  for a,b being Real st a >= b holds IRRAT (a,b) = {};

theorem :: ISOMICHI:31
  for a,b being Real holds IRRAT (a,b) c= [.a,+infty .[;

theorem :: ISOMICHI:32
  for A being Subset of R^1, a, b, c being Real st A = ].
  -infty, a .[ \/ RAT (b,c) & a < b & b < c holds Int A = ]. -infty, a .[;

theorem :: ISOMICHI:33
  for a,b being Real st a < b holds REAL = ]. -infty,a.[ \/ [.a,b
  .] \/ ].b,+infty .[;

theorem :: ISOMICHI:34
  for A being Subset of R^1, a, b, c being Real st A = ].
-infty, a .] \/ [.b,c.] & a < b & b < c holds Int A = ]. -infty, a .[ \/ ].b,c
  .[;

begin :: Classification of Subsets

notation
  let A, B be set;
  antonym A, B are_c=-incomparable for A, B are_c=-comparable;
end;

theorem :: ISOMICHI:35
  for A, B being set holds A, B are_c=-incomparable or A c= B or B c< A;

definition
  let T, A;
  attr A is 1st_class means
:: ISOMICHI:def 6

  Int Cl A c= Cl Int A;
  attr A is 2nd_class means
:: ISOMICHI:def 7

  Cl Int A c< Int Cl A;
  attr A is 3rd_class means
:: ISOMICHI:def 8

  Cl Int A, Int Cl A are_c=-incomparable;
end;

theorem :: ISOMICHI:36
  A is 1st_class or A is 2nd_class or A is 3rd_class;

registration
  let T be TopSpace;
  cluster 1st_class -> non 2nd_class non 3rd_class for Subset of T;
  cluster 2nd_class -> non 1st_class non 3rd_class for Subset of T;
  cluster 3rd_class -> non 1st_class non 2nd_class for Subset of T;
end;

theorem :: ISOMICHI:37  :: Remark 1
  A is 1st_class iff Border A is empty;

registration
  let T be TopSpace;
  cluster supercondensed -> 1st_class for Subset of T;
  cluster subcondensed -> 1st_class for Subset of T;
end;

definition
  let T be TopSpace;
  attr T is with_1st_class_subsets means
:: ISOMICHI:def 9

  ex A being Subset of T st A is 1st_class;
  attr T is with_2nd_class_subsets means
:: ISOMICHI:def 10

  ex A being Subset of T st A is 2nd_class;
  attr T is with_3rd_class_subsets means
:: ISOMICHI:def 11

  ex A being Subset of T st A is 3rd_class;
end;

registration
  let T be anti-discrete non empty TopSpace;
  cluster proper non empty -> 2nd_class for Subset of T;
end;

registration
  let T be anti-discrete non trivial strict TopSpace;
  cluster 2nd_class for Subset of T;
end;

registration
  cluster with_1st_class_subsets with_2nd_class_subsets
      strict non trivial for TopSpace;
  cluster with_3rd_class_subsets non empty strict for TopSpace;
end;

registration
  let T;
  cluster 1st_class for Subset of T;
end;

registration
  let T be with_2nd_class_subsets TopSpace;
  cluster 2nd_class for Subset of T;
end;

registration
  let T be with_3rd_class_subsets TopSpace;
  cluster 3rd_class for Subset of T;
end;

theorem :: ISOMICHI:38  :: Theorem 8
  A is 1st_class iff A` is 1st_class;

theorem :: ISOMICHI:39  :: Theorem 8
  A is 2nd_class iff A` is 2nd_class;

theorem :: ISOMICHI:40  :: Theorem 8
  A is 3rd_class iff A` is 3rd_class;

registration
  let T;
  let A be 1st_class Subset of T;
  cluster A` -> 1st_class;
end;

registration
  let T be with_2nd_class_subsets TopSpace;
  let A be 2nd_class Subset of T;
  cluster A` -> 2nd_class;
end;

registration
  let T be with_3rd_class_subsets TopSpace;
  let A be 3rd_class Subset of T;
  cluster A` -> 3rd_class;
end;

theorem :: ISOMICHI:41  :: Theorem 9
  A is 1st_class implies Int Cl A = Int Cl Int A & Cl Int A = Cl Int Cl A;

theorem :: ISOMICHI:42  :: Theorem 9
  (Int Cl A = Int Cl Int A or Cl Int A = Cl Int Cl A) implies A is 1st_class;

theorem :: ISOMICHI:43  :: Theorem 10
  A is 1st_class & B is 1st_class implies Int Cl A /\ Int Cl B =
  Int Cl (A /\ B) & Cl Int A \/ Cl Int B = Cl Int (A \/ B);

theorem :: ISOMICHI:44 :: Theorem 11
  A is 1st_class & B is 1st_class implies A \/ B is 1st_class & A /\ B
  is 1st_class;
 
:: TODO: Remark 2 from Isomichi's paper
:: condensed = domain    Int Cl A c= Cl Int A 
:: closed domain:   A = Cl Int A:  regular_closed = closed_condensed 
:: open domain:     A = Int Cl A:  regular_open = open_condensed