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