:: 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;
definitions TARSKI;
equalities SUBSET_1, STRUCT_0, LIMFUNC1, PROB_1;
expansions SUBSET_1;
theorems SUBSET_1, XBOOLE_0, XBOOLE_1, PRE_TOPC, TOPS_1, TDLAT_1, TDLAT_3,
PCOMPS_1, TEX_1, BORSUK_5, TOPMETR, DECOMP_1, TOPGEN_1, TOPS_3, XXREAL_0,
XXREAL_1, JORDAN5A;
begin :: Preliminaries
reserve T for TopSpace,
A, B for Subset of T;
registration
let D be non trivial set;
cluster ADTS D -> non trivial;
coherence
proof
ADTS D = TopStruct (# D,cobool D #) by TEX_1:def 3;
hence thesis;
end;
end;
registration
cluster anti-discrete non trivial strict for TopSpace;
existence
proof
set D = the non trivial set;
take ADTS D;
thus thesis;
end;
end;
theorem Th1:
Int Cl Int A /\ Int Cl Int B = Int Cl Int (A /\ B)
proof
set C = Int A, D = Int B;
Int Cl C /\ Int Cl D = Int Cl(C /\ D) by TDLAT_1:7;
hence thesis by TOPS_1:17;
end;
theorem Th2:
Cl Int Cl (A \/ B) = Cl Int Cl A \/ Cl Int Cl B
proof
set C = Cl A, D = Cl B;
Cl Int C \/ Cl Int D = Cl Int(C \/ D) by TDLAT_1:6;
hence thesis by PRE_TOPC:20;
end;
begin :: Connections between Supercondensed, Condensed and Subcondensed Sets
definition
let T be TopStruct, A be Subset of T;
attr A is supercondensed means
:Def1:
Int Cl A = Int A;
attr A is subcondensed means
:Def2:
Cl Int A = Cl A;
end;
registration
let T;
cluster closed -> supercondensed for Subset of T;
coherence
by PRE_TOPC:22;
end;
theorem :: Remark 1
A is closed implies A is supercondensed;
theorem
A is open implies A is subcondensed
by TOPS_1:23;
definition
let T be TopSpace, A be Subset of T;
redefine attr A is condensed means
Cl Int A = Cl A & Int Cl A = Int A;
compatibility
proof
thus A is condensed implies Cl Int A = Cl A & Int Cl A = Int A by TDLAT_3:9
;
assume that
A1: Cl Int A = Cl A and
A2: Int Cl A = Int A;
A3: Int A c= A by TOPS_1:16;
A c= Cl Int A by A1,PRE_TOPC:18;
hence thesis by A2,A3,TOPS_1:def 6;
end;
end;
theorem :: 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;
coherence;
cluster subcondensed supercondensed -> condensed for Subset of T;
coherence;
end;
registration
let T be TopSpace;
cluster condensed subcondensed supercondensed for Subset of T;
existence
proof
set A = {}T;
take A;
A is supercondensed subcondensed;
hence thesis;
end;
end;
theorem :: Theorem 1
A is supercondensed implies A` is subcondensed
proof
A1: (Int A)` = Cl (A`) by TDLAT_3:2;
assume A is supercondensed;
then
A2: (Int Cl A)` = (Int A)`;
(Int Cl A)` = Cl (Cl A)` by TDLAT_3:2
.= Cl Int (A`) by TDLAT_3:3;
hence thesis by A2,A1;
end;
theorem :: Theorem 1
A is subcondensed implies A` is supercondensed
proof
A1: (Cl A)` = Int A` by TDLAT_3:3;
assume A is subcondensed;
then
A2: (Cl Int A)` = (Cl A)`;
(Cl Int A)` = Int ((Int A)`) by TDLAT_3:3
.= Int (Cl A`) by TDLAT_3:2;
hence thesis by A2,A1;
end;
:: Corollary to Theorem 1
:: A is condensed implies A` is condensed = TDLAT_1:16;
theorem Th8: :: Theorem 2
A is supercondensed iff Int Cl A c= A
proof
thus A is supercondensed implies Int Cl A c= A
by TOPS_1:16;
assume Int Cl A c= A;
then
A1: Int Int Cl A c= Int A by TOPS_1:19;
Int A c= Int Cl A by PRE_TOPC:18,TOPS_1:19;
then Int A = Int Cl A by A1,XBOOLE_0:def 10;
hence thesis;
end;
theorem Th9: :: Theorem 2
A is subcondensed iff A c= Cl Int A
proof
thus A is subcondensed implies A c= Cl Int A
by PRE_TOPC:18;
assume A c= Cl Int A;
then
A1: Cl A c= Cl Cl Int A by PRE_TOPC:19;
Cl Int A c= Cl A by PRE_TOPC:19,TOPS_1:16;
then Cl Int A = Cl A by A1,XBOOLE_0:def 10;
hence thesis;
end;
registration
let T be TopSpace;
cluster subcondensed -> semi-open for Subset of T;
coherence
by Th9,DECOMP_1:def 2;
cluster semi-open -> subcondensed for Subset of T;
coherence
by DECOMP_1:def 2,Th9;
end;
theorem Th10: :: Corollary to Theorem 2
A is condensed iff Int Cl A c= A & A c= Cl Int A
proof
thus A is condensed implies Int Cl A c= A & A c= Cl Int A by Th8,Th9;
assume that
A1: Int Cl A c= A and
A2: A c= Cl Int A;
A3: A is subcondensed by A2,Th9;
A is supercondensed by A1,Th8;
hence thesis by A3;
end;
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 :: Remark 1
for T being TopSpace holds [#]T is regular_open & [#]T is regular_closed
proof
let T be TopSpace;
A1: Int [#]T = [#]T by TOPS_1:15;
Cl [#]T = [#]T by TOPS_1:2;
hence thesis by A1,TOPS_1:def 7,def 8;
end;
registration
let T be TopSpace;
cluster [#]T -> regular_open regular_closed;
coherence
proof
A1: Int [#]T = [#]T by TOPS_1:15;
Cl [#]T = [#]T by TOPS_1:2;
hence thesis by A1,TOPS_1:def 7,def 8;
end;
end;
registration
let T be TopSpace;
cluster empty -> regular_open regular_closed for Subset of T;
coherence
proof
let S be Subset of T;
assume
A1: S is empty;
then
A2: S = Int S;
S = Cl S by A1,PCOMPS_1:2;
hence thesis by A2,TOPS_1:def 7,def 8;
end;
end;
theorem
Int Cl {}T = {}T
proof
Int Cl {}T = Int {}T by PCOMPS_1:2
.= {}T;
hence thesis;
end;
theorem Th13: :: Remark 2
A is regular_open implies A` is regular_closed
proof
assume A is regular_open;
then Int Cl A = A by TOPS_1:def 8;
then Cl (Cl A)` = A` by TDLAT_3:2;
then Cl Int (A`) = A` by TDLAT_3:3;
hence thesis by TOPS_1:def 7;
end;
registration
let T be TopSpace;
cluster regular_open regular_closed for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
registration
let T be TopSpace;
let A be regular_open Subset of T;
cluster A` -> regular_closed;
coherence by Th13;
end;
theorem Th14: :: Remark 2
A is regular_closed implies A` is regular_open
proof
assume A is regular_closed;
then Cl Int A = A by TOPS_1:def 7;
then Int (Int A)` = A` by TDLAT_3:3;
then Int Cl(A`) = A` by TDLAT_3:2;
hence thesis by TOPS_1:def 8;
end;
registration
let T be TopSpace;
let A be regular_closed Subset of T;
cluster A` -> regular_open;
coherence by Th14;
end;
registration
let T be TopSpace;
cluster regular_open -> open for Subset of T;
coherence by TOPS_1:67;
cluster regular_closed -> closed for Subset of T;
coherence by TOPS_1:66;
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 Th15: :: Remark 3
Int Cl A is regular_open & Cl Int A is regular_closed
proof
A1: Cl Int Cl Int A = Cl Int A by TOPS_1:26;
Int Cl Int Cl A = Int Cl A by TDLAT_1:5;
hence thesis by A1,TOPS_1:def 7,def 8;
end;
registration
let T be TopSpace, A be Subset of T;
cluster Int Cl A -> regular_open;
coherence by Th15;
cluster Cl Int A -> regular_closed;
coherence by Th15;
end;
theorem :: Theorem 3
A is regular_open iff A is supercondensed & A is open
proof
thus A is regular_open implies A is supercondensed & A is open
proof
assume A is regular_open;
then
A1: Int Cl A = A by TOPS_1:def 8;
thus thesis by A1;
end;
assume that
A2: A is supercondensed and
A3: A is open;
Int Cl A = Int A by A2;
hence thesis by A3,TOPS_1:23;
end;
theorem :: Theorem 3
A is regular_closed iff A is subcondensed & A is closed
proof
thus A is regular_closed implies A is subcondensed & A is closed
proof
assume A is regular_closed;
then
A1: Cl Int A = A by TOPS_1:def 7;
thus thesis by A1;
end;
assume that
A2: A is subcondensed and
A3: A is closed;
Cl Int A = Cl A by A2;
hence thesis by A3,PRE_TOPC:22;
end;
registration
let T be TopSpace;
cluster regular_open -> condensed open for Subset of T;
coherence by TOPS_1:67;
cluster condensed open -> regular_open for Subset of T;
coherence by TOPS_1:67;
cluster regular_closed -> condensed closed for Subset of T;
coherence by TOPS_1:66;
cluster condensed closed -> regular_closed for Subset of T;
coherence by TOPS_1:66;
end;
theorem :: Corollary to Theorem 3:: Theorem 4
A is condensed iff ex B st B is regular_open & B c= A & A c= Cl B
proof
thus A is condensed implies ex B st B is regular_open & B c= A & A c= Cl B
proof
assume
A1: A is condensed;
then
A2: Cl Int A = Cl A;
take Int Cl A;
Int Cl A = Int A by A1;
hence thesis by A2,PRE_TOPC:18,TOPS_1:16;
end;
given B such that
A3: B is regular_open and
A4: B c= A and
A5: A c= Cl B;
A6: Int Cl B = B by A3,TOPS_1:def 8;
Int B c= Int A by A4,TOPS_1:19;
then
A7: Cl Int B c= Cl Int A by PRE_TOPC:19;
A8: Cl Int B = Cl B by A3,Def2;
Int A c= Int Cl B by A5,TOPS_1:19;
then Cl Int A c= Cl B by A6,PRE_TOPC:19;
then
A9: Cl B = Cl Int A by A7,A8,XBOOLE_0:def 10;
Cl B c= Cl A by A4,PRE_TOPC:19;
then
A10: Int Cl B c= Int Cl A by TOPS_1:19;
Cl A c= Cl Cl B by A5,PRE_TOPC:19;
then Int Cl A c= Int Cl Cl B by TOPS_1:19;
then B = Int Cl A by A6,A10,XBOOLE_0:def 10;
hence thesis by A4,A5,A9,Th10;
end;
theorem :: Theorem 4
A is condensed iff ex B st B is regular_closed & Int B c= A & A c= B
proof
thus A is condensed implies ex B st B is regular_closed & Int B c= A & A c= B
proof
assume
A1: A is condensed;
then
A2: Cl Int A = Cl A;
take Cl Int A;
Int Cl A = Int A by A1;
hence thesis by A2,PRE_TOPC:18,TOPS_1:16;
end;
given B such that
A3: B is regular_closed and
A4: Int B c= A and
A5: A c= B;
A6: Cl Int B = B by A3,TOPS_1:def 7;
Cl A c= Cl B by A5,PRE_TOPC:19;
then Int Cl A c= Int Cl B by TOPS_1:19;
then
A7: Int Cl A c= Int B by A3,Def1;
Cl Int B c= Cl A by A4,PRE_TOPC:19;
then Int B c= Int Cl A by A6,TOPS_1:19;
then
A8: Int B = Int Cl A by A7,XBOOLE_0:def 10;
Int A c= Int B by A5,TOPS_1:19;
then
A9: Cl Int A c= Cl Int B by PRE_TOPC:19;
Int Int B c= Int A by A4,TOPS_1:19;
then Cl Int Int B c= Cl Int A by PRE_TOPC:19;
then Cl Int A = B by A6,A9,XBOOLE_0:def 10;
hence thesis by A4,A5,A8,Th10;
end;
begin :: Boundaries and Borders
definition
let T be TopStruct, A be Subset of T;
redefine func Fr A equals
Cl A \ Int A;
compatibility by TOPGEN_1:8;
end;
theorem :: Theorem 5
A is condensed iff Fr A = Cl Int A \ Int Cl A & Fr A = Cl Int A /\ Cl Int A`
proof
A1: A c= Cl A by PRE_TOPC:18;
Cl Int A /\ Cl Int A` c= Cl Int A by XBOOLE_1:17;
then
A2: Int A \/ (Cl Int A /\ Cl Int A`) c= Int A \/ Cl Int A by XBOOLE_1:13;
thus A is condensed implies Fr A = Cl Int A \ Int Cl A & Fr A = Cl Int A /\
Cl Int A`
proof
assume
A3: A is condensed;
then A` is condensed by TDLAT_1:16;
then
A4: Cl Int A` = Cl A`;
thus thesis by A3,A4,TOPS_1:def 2;
end;
assume that
Fr A = Cl Int A \ Int Cl A and
A5: Fr A = Cl Int A /\ Cl Int A`;
A6: Cl A \/ Int A = Int A \/ Fr A by XBOOLE_1:39;
Int A c= A by TOPS_1:16;
then Cl A = Int A \/ (Cl Int A /\ Cl Int A`) by A5,A1,A6,XBOOLE_1:1,12;
then
A7: Cl A c= Cl Int A by A2,PRE_TOPC:18,XBOOLE_1:12;
Cl Int A c= Cl A by PRE_TOPC:19,TOPS_1:16;
then Cl Int A = Cl A by A7,XBOOLE_0:def 10;
then
A8: A is subcondensed;
A9: A` c= Cl A` by PRE_TOPC:18;
A10: Cl A` \/ Int A` = Int A` \/ Fr A` by XBOOLE_1:39;
A11: Fr A = Fr A` by TOPS_1:29;
Cl Int A` /\ Cl Int A`` c= Cl Int A` by XBOOLE_1:17;
then
A12: Int A` \/ (Cl Int A` /\ Cl Int A``) c= Int A` \/ Cl Int A` by XBOOLE_1:13;
A13: Cl Int A` c= Cl A` by PRE_TOPC:19,TOPS_1:16;
A14: Cl Int A` = Cl (Cl A)` by TDLAT_3:3
.= (Int Cl A)` by TDLAT_3:2;
A15: Int A` \/ Cl Int A` = Cl Int A` by PRE_TOPC:18,XBOOLE_1:12;
Int A` c= A` by TOPS_1:16;
then Cl A` = Int A` \/ (Cl Int A` /\ Cl Int A``) by A5,A9,A11,A10,XBOOLE_1:1
,12;
then
A16: Cl A` = Cl Int A` by A13,A12,A15,XBOOLE_0:def 10;
Cl A` = (Int A)` by TDLAT_3:2;
then Int A = (Int Cl A)`` by A16,A14;
then A is supercondensed;
hence thesis by A8;
end;
definition
let T be TopStruct, A be Subset of T;
func Border A -> Subset of T equals
Int Fr A;
coherence;
end;
theorem Th21: :: Theorem 6
Border A is regular_open & Border A = (Int Cl A) \ (Cl Int A) &
Border A = Int Cl A /\ (Int Cl A`)
proof
Fr A = Cl Fr A by PRE_TOPC:22;
hence Border A is regular_open;
(Int Cl A) \ (Cl Int A) = (Int Cl A) \ ((Cl Int A)`)`
.= (Int Cl A) \ (Int (Int A)`)` by TDLAT_3:3
.= (Int Cl A) \ (Int Cl A`)` by TDLAT_3:2
.= Int Cl A /\ (Int Cl A`)`` by SUBSET_1:13
.= Int (Cl A /\ Cl A`) by TOPS_1:17
.= Int Fr A by TOPS_1:def 2;
hence Border A = (Int Cl A) \ (Cl Int A);
Int Cl A /\ (Int Cl A`) = Int (Cl A /\ Cl A`) by TOPS_1:17
.= Int Fr A by TOPS_1:def 2;
hence thesis;
end;
registration
let T be TopSpace, A be Subset of T;
cluster Border A -> regular_open;
coherence by Th21;
end;
theorem Th22: :: Theorem 7
A is supercondensed iff Int A is regular_open & Border A is empty
proof
A1: Int A c= Int Cl A by PRE_TOPC:18,TOPS_1:19;
thus A is supercondensed implies Int A is regular_open & Border A is empty
proof
assume
A2: A is supercondensed;
then Int Cl A = Int A;
then Int Cl A c= Cl Int A by PRE_TOPC:18;
then (Int Cl A) \ (Cl Int A) is empty by XBOOLE_1:37;
hence thesis by A2,Th21;
end;
assume that
A3: Int A is regular_open and
A4: Border A is empty;
(Int Cl A) \ (Cl Int A) is empty by A4,Th21;
then Int Cl A c= Cl Int A by XBOOLE_1:37;
then
A5: Int Int Cl A c= Int Cl Int A by TOPS_1:19;
Int A = Int Cl Int A by A3,TOPS_1:def 8;
then Int Cl A = Int A by A5,A1,XBOOLE_0:def 10;
hence thesis;
end;
theorem Th23: :: Theorem 7
A is subcondensed iff Cl A is regular_closed & Border A is empty
proof
A1: Cl Int A c= Cl A by PRE_TOPC:19,TOPS_1:16;
thus A is subcondensed implies Cl A is regular_closed & Border A is empty
proof
assume
A2: A is subcondensed;
then Cl Int A = Cl A;
then Int Cl A c= Cl Int A by TOPS_1:16;
then (Int Cl A) \ (Cl Int A) is empty by XBOOLE_1:37;
hence thesis by A2,Th21;
end;
assume that
A3: Cl A is regular_closed and
A4: Border A is empty;
(Int Cl A) \ (Cl Int A) is empty by A4,Th21;
then Int Cl A c= Cl Int A by XBOOLE_1:37;
then
A5: Cl Int Cl A c= Cl Cl Int A by PRE_TOPC:19;
Cl A = Cl Int Cl A by A3,TOPS_1:def 7;
then Cl Int A = Cl A by A5,A1,XBOOLE_0:def 10;
hence thesis;
end;
registration
let T be TopSpace, A be Subset of T;
cluster Border Border A -> empty;
coherence;
end;
theorem :: Remark:: Corollary to Theorem 7
A is condensed iff Int A is regular_open & Cl A is regular_closed &
Border A is empty
proof
thus A is condensed implies Int A is regular_open & Cl A is regular_closed &
Border A is empty by Th22;
assume that
A1: Int A is regular_open and
A2: Cl A is regular_closed and
A3: Border A is empty;
A4: A is subcondensed by A2,A3,Th23;
A is supercondensed by A1,A3,Th22;
hence thesis by A4;
end;
begin :: Auxiliary Theorems
theorem
for A being Subset of R^1, a being Real st A = ]. -infty, a.]
holds Int A = ]. -infty, a.[
proof
let A be Subset of R^1, a be Real;
assume A = ]. -infty, a.];
then A` = ].a,+infty .[ by TOPMETR:17,XXREAL_1:224,288;
then Cl A` = [.a,+infty .[ by BORSUK_5:49;
then (Cl A`)` = ]. -infty, a.[ by TOPMETR:17,XXREAL_1:224,294;
hence thesis by TOPS_1:def 1;
end;
theorem
for A being Subset of R^1, a being Real st A = [.a,+infty .[
holds Int A = ].a,+infty .[
proof
let A be Subset of R^1, a be Real;
assume A = [.a,+infty .[;
then A` = ]. -infty,a.[ by TOPMETR:17,XXREAL_1:224,294;
then Cl A` = ]. -infty,a.] by BORSUK_5:51;
then (Cl A`)` = ].a,+infty .[ by TOPMETR:17,XXREAL_1:224,288;
hence thesis by TOPS_1:def 1;
end;
theorem Th27:
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
proof
reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
let A be Subset of R^1, a, b be Real;
assume
A1: A = ]. -infty,a.] \/ IRRAT (a,b) \/ [.b,+infty .[;
B c= A
proof
let x be object;
assume
A2: x in B;
then reconsider x9 = x as Real;
per cases;
suppose
x9 <= a;
then x9 in ]. -infty,a.] by XXREAL_1:234;
then x9 in ]. -infty,a.] \/ IRRAT (a,b) by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
suppose
x9 > a & x9 < b;
then x9 in ]. a, b .[ by XXREAL_1:4;
then x9 in IRRAT /\ ]. a, b .[ by A2,XBOOLE_0:def 4;
then x9 in IRRAT (a, b) by BORSUK_5:def 3;
then x9 in ]. -infty,a.] \/ IRRAT (a,b) by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
suppose
x9 >= b;
then x9 in [.b,+infty .[ by XXREAL_1:236;
hence thesis by A1,XBOOLE_0:def 3;
end;
end;
then
A3: Cl B c= Cl A by PRE_TOPC:19;
Cl B = the carrier of R^1 by BORSUK_5:28;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
for A being Subset of R^1, a, b being Real st A = RAT (a,b)
holds Int A = {}
proof
let A be Subset of R^1, a, b be Real;
assume
A1: A = RAT (a,b);
A` = REAL \ A by TOPMETR:17
.= ]. -infty,a.] \/ IRRAT (a,b) \/ [.b,+infty .[ by A1,BORSUK_5:58;
then Cl A` = [#]R^1 by Th27;
then (Cl A`)` = {}R^1 by XBOOLE_1:37;
hence thesis by TOPS_1:def 1;
end;
theorem
for A being Subset of R^1, a, b being Real st A = IRRAT (a,b)
holds Int A = {}
proof
reconsider B = IRRAT as Subset of R^1 by TOPMETR:17;
let A be Subset of R^1, a, b be Real;
assume A = IRRAT (a,b);
then A = IRRAT /\ ]. a, b .[ by BORSUK_5:def 3;
then A c= B by XBOOLE_1:17;
then A is boundary by TOPGEN_1:54,TOPS_3:11;
hence thesis;
end;
theorem
for a,b being Real st a >= b holds IRRAT (a,b) = {}
proof
let a, b be Real;
assume
A1: a >= b;
IRRAT (a,b) = IRRAT /\ ]. a, b .[ by BORSUK_5:def 3
.= IRRAT /\ {} by A1,XXREAL_1:28;
hence thesis;
end;
theorem Th31:
for a,b being Real holds IRRAT (a,b) c= [.a,+infty .[
proof
let a,b be Real;
let x be object;
assume
A1: x in IRRAT (a,b);
then reconsider x as Real;
a < x by A1,BORSUK_5:30;
hence thesis by XXREAL_1:236;
end;
theorem Th32:
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 .[
proof
let A be Subset of R^1, a, b, c be Real;
reconsider B = [. a, b .], C = IRRAT (b,c), D = [. c,+infty .[ as Subset of
R^1 by TOPMETR:17;
assume that
A1: A = ]. -infty, a.[ \/ RAT (b,c) and
A2: a < b and
A3: b < c;
A4: a < c by A2,A3,XXREAL_0:2;
A` = REAL \ ( ]. -infty, a.[ \/ RAT (b,c)) by A1,TOPMETR:17
.= (REAL \ RAT (b,c)) \ ]. -infty, a.[ by XBOOLE_1:41
.= (]. -infty,b.] \/ IRRAT (b, c) \/ [.c,+infty .[) \ ]. -infty,a.[ by
BORSUK_5:58
.= (]. -infty,b.] \/ (IRRAT (b, c) \/ [.c,+infty .[)) \ ]. -infty,a.[ by
XBOOLE_1:4
.= (]. -infty,b.] \ ]. -infty,a.[) \/ ((IRRAT (b, c) \/ [.c,+infty .[) \
]. -infty,a.[) by XBOOLE_1:42;
then
A5: A` = [.a,b.] \/ ((IRRAT (b, c) \/ [.c,+infty .[) \ ]. -infty,a.[) by
XXREAL_1:289
.= [.a,b.] \/ ((IRRAT (b,c) \ ]. -infty,a.[) \/ ([.c,+infty .[ \ ].
-infty,a.[)) by XBOOLE_1:42;
right_closed_halfline c is closed;
then D is closed by JORDAN5A:23;
then
A6: Cl D = D by PRE_TOPC:22;
[.b,+infty .[ misses ]. -infty,a.[ by A2,XXREAL_1:94;
then IRRAT (b,c) misses ]. -infty,a.[ by Th31,XBOOLE_1:63;
then
A7: IRRAT (b,c) \ ]. -infty,a.[ = IRRAT (b,c) by XBOOLE_1:83;
B is closed by JORDAN5A:23;
then
A8: Cl B = B by PRE_TOPC:22;
[.c,+infty .[ misses ]. -infty,a.[ by A2,A3,XXREAL_0:2,XXREAL_1:94;
then A` = [.a,b.] \/ (IRRAT (b,c) \/ [.c,+infty .[) by A5,A7,XBOOLE_1:83
.= [.a,b.] \/ (IRRAT (b,c) \/ ({c} \/ ].c,+infty .[)) by BORSUK_5:43
.= [.a,b.] \/ IRRAT (b,c) \/ ({c} \/ ].c,+infty .[) by XBOOLE_1:4
.= [. a, b .] \/ IRRAT (b,c) \/ [. c,+infty .[ by BORSUK_5:43;
then Cl A` = Cl (B \/ C) \/ Cl D by PRE_TOPC:20
.= Cl B \/ Cl C \/ Cl D by PRE_TOPC:20
.= B \/ [.b,c.] \/ D by A8,A6,A3,BORSUK_5:32
.= [.a,c.] \/ D by A2,A3,XXREAL_1:165
.= [. a,+infty .[ by A4,BORSUK_5:11;
then (Cl A`)` = ]. -infty, a .[ by TOPMETR:17,XXREAL_1:224,294;
hence thesis by TOPS_1:def 1;
end;
Lm1: for a,b being Real st a < b holds [.a,b.] \/ {b} = [.a,b.]
proof
let a,b be Real;
assume
A1: a < b;
then [. a, b .] = [. a, b .[ \/ { b } by XXREAL_1:129
.= [. a, b .[ \/ { b } \/ {b} by XBOOLE_1:6;
hence thesis by A1,XXREAL_1:129;
end;
theorem
for a,b being Real st a < b holds REAL = ]. -infty,a.[ \/ [.a,b
.] \/ ].b,+infty .[
proof
let a,b be Real;
assume
A1: a < b;
REAL = (REAL \ {a}) \/ {a} by XBOOLE_1:45
.= (]. -infty,a.[ \/ ].a,+infty .[) \/ {a} by XXREAL_1:389
.= ]. -infty,a.[ \/ (].a,+infty .[ \/ {a}) by XBOOLE_1:4
.= ]. -infty,a.[ \/ [.a,+infty .[ by BORSUK_5:43
.= ]. -infty,a.[ \/ ([.a,b.] \/ [.b,+infty .[) by A1,BORSUK_5:11
.= ]. -infty,a.[ \/ ([.a,b.] \/ ({b} \/ ].b,+infty .[)) by BORSUK_5:43
.= ]. -infty,a.[ \/ ([.a,b.] \/ {b} \/ ].b,+infty .[) by XBOOLE_1:4
.= ]. -infty,a.[ \/ ([.a,b.] \/ {b}) \/ ].b,+infty .[ by XBOOLE_1:4;
hence thesis by A1,Lm1;
end;
theorem Th34:
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
.[
proof
let A be Subset of R^1, a, b, c be Real;
assume that
A1: A = ]. -infty, a .] \/ [.b,c.] and
A2: a < b and
A3: b < c;
a < c by A2,A3,XXREAL_0:2;
then
A4: ].c,+infty .[ /\ ].a,+infty .[ = ].c,+infty .[ by XBOOLE_1:28,XXREAL_1:46;
reconsider B = ]. a,b .[, C = ].c,+infty .[ as Subset of R^1 by TOPMETR:17;
A5: Cl B = [. a,b .] by A2,BORSUK_5:16;
A6: Cl C = [. c,+infty .[ by BORSUK_5:49;
A` = REAL \ (]. -infty, a .] \/ [.b,c.]) by A1,TOPMETR:17
.= (REAL \ left_closed_halfline a) \ [.b,c.] by XBOOLE_1:41
.= right_open_halfline a \ [.b,c.] by XXREAL_1:224,288
.= ].a,+infty .[ \ ([.b,+infty .[ \ ].c,+infty .[) by XXREAL_1:295
.= ( ].a,+infty .[ \ [.b,+infty .[) \/ ( ].a,+infty .[ /\ ].c,+infty .[)
by XBOOLE_1:52
.= ]. a,b .[ \/ ]. c,+infty .[ by A4,XXREAL_1:294;
then (Cl A`)` = REAL \ ([. c,+infty .[ \/ [.a,b.]) by A5,A6,PRE_TOPC:20
,TOPMETR:17
.= (REAL \ right_closed_halfline c) \ [.a,b.] by XBOOLE_1:41
.= left_open_halfline c \ [.a,b.] by XXREAL_1:224,294
.= ]. -infty, a .[ \/ ].b,c.[ by A2,A3,XXREAL_0:2,XXREAL_1:339;
hence thesis by TOPS_1:def 1;
end;
begin :: Classification of Subsets
notation
let A, B be set;
antonym A, B are_c=-incomparable for A, B are_c=-comparable;
end;
theorem Th35:
for A, B being set holds A, B are_c=-incomparable or A c= B or B c< A
proof
let A, B be set;
assume that
A1: A, B are_c=-comparable and
A2: not A c= B and
A3: not B c< A;
A c= B or B c= A by A1,XBOOLE_0:def 9;
hence thesis by A2,A3,XBOOLE_0:def 8;
end;
definition
let T, A;
attr A is 1st_class means
Int Cl A c= Cl Int A;
attr A is 2nd_class means
Cl Int A c< Int Cl A;
attr A is 3rd_class means
Cl Int A, Int Cl A are_c=-incomparable;
end;
theorem
A is 1st_class or A is 2nd_class or A is 3rd_class
by Th35;
registration
let T be TopSpace;
cluster 1st_class -> non 2nd_class non 3rd_class for Subset of T;
coherence
by XBOOLE_0:def 9,XBOOLE_1:60;
cluster 2nd_class -> non 1st_class non 3rd_class for Subset of T;
coherence
proof
let A be Subset of T;
assume A is 2nd_class;
then
A1: Cl Int A c< Int Cl A;
then Cl Int A c= Int Cl A by XBOOLE_0:def 8;
then
A2: Cl Int A, Int Cl A are_c=-comparable by XBOOLE_0:def 9;
not Int Cl A c= Cl Int A by A1,XBOOLE_0:def 8;
hence thesis by A2;
end;
cluster 3rd_class -> non 1st_class non 2nd_class for Subset of T;
coherence;
end;
theorem Th37: :: Remark 1
A is 1st_class iff Border A is empty
proof
A1: Border A is empty implies A is 1st_class
proof
assume Border A is empty;
then Int Cl A \ Cl Int A = {} by Th21;
then Int Cl A c= Cl Int A by XBOOLE_1:37;
hence thesis;
end;
A is 1st_class implies Border A is empty
proof
assume A is 1st_class;
then Int Cl A c= Cl Int A;
then Int Cl A \ Cl Int A = {} by XBOOLE_1:37;
hence thesis by Th21;
end;
hence thesis by A1;
end;
registration
let T be TopSpace;
cluster supercondensed -> 1st_class for Subset of T;
coherence
proof
let A be Subset of T;
assume A is supercondensed;
then Border A is empty by Th22;
hence thesis by Th37;
end;
cluster subcondensed -> 1st_class for Subset of T;
coherence
proof
let A be Subset of T;
assume A is subcondensed;
then Border A is empty by Th23;
hence thesis by Th37;
end;
end;
definition
let T be TopSpace;
attr T is with_1st_class_subsets means
ex A being Subset of T st A is 1st_class;
attr T is with_2nd_class_subsets means
:Def10:
ex A being Subset of T st A is 2nd_class;
attr T is with_3rd_class_subsets means
:Def11:
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;
coherence
proof
let A be Subset of T;
assume
A1: A is proper non empty;
then A <> the carrier of T;
then Int A = {} by TEX_1:10;
then
A2: Cl Int A = {} by TEX_1:9;
Cl A = the carrier of T by A1,TEX_1:9;
then Int Cl A = the carrier of T by TEX_1:10;
then Cl Int A c< Int Cl A by A2,XBOOLE_0:def 8;
hence thesis;
end;
end;
registration
let T be anti-discrete non trivial strict TopSpace;
cluster 2nd_class for Subset of T;
existence
proof
set x = the Element of T;
reconsider A = {x} as Subset of T;
Cl A = the carrier of T by TEX_1:9;
hence thesis;
end;
end;
registration
cluster with_1st_class_subsets with_2nd_class_subsets
strict non trivial for TopSpace;
existence
proof
set T = the anti-discrete non trivial strict TopSpace;
set B = the 2nd_class Subset of T;
B is 2nd_class;
then
A1: T is with_2nd_class_subsets;
{}T is 1st_class;
then T is with_1st_class_subsets;
hence thesis by A1;
end;
cluster with_3rd_class_subsets non empty strict for TopSpace;
existence
proof
set B = ]. -infty, 1 .[, C = RAT(2,4);
take R^1;
set A = B \/ C;
reconsider A, B, C as Subset of R^1 by TOPMETR:17;
A2: Cl C = [. 2,4 .] by BORSUK_5:31;
Cl B = ]. -infty, 1 .] by BORSUK_5:51;
then Cl A = ]. -infty, 1 .] \/ [. 2,4 .] by A2,PRE_TOPC:20;
then
A3: Int Cl A = ]. -infty, 1 .[ \/ ]. 2,4 .[ by Th34;
A4: Cl Int A = ]. -infty, 1 .] by Th32,BORSUK_5:51;
3 in ]. 2, 4 .[ by XXREAL_1:4;
then 3 in Int Cl A by A3,XBOOLE_0:def 3;
then
A5: not Int Cl A c= Cl Int A by A4,XXREAL_1:234;
A6: not 1 in ].2,4.[ by XXREAL_1:4;
A7: not 1 in ]. -infty,1.[ by XXREAL_1:4;
1 in Cl Int A by A4,XXREAL_1:234;
then not Cl Int A c= Int Cl A by A3,A7,A6,XBOOLE_0:def 3;
then Int Cl A, Cl Int A are_c=-incomparable by A5,XBOOLE_0:def 9;
then A is 3rd_class;
hence thesis;
end;
end;
registration
let T;
cluster 1st_class for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
registration
let T be with_2nd_class_subsets TopSpace;
cluster 2nd_class for Subset of T;
existence by Def10;
end;
registration
let T be with_3rd_class_subsets TopSpace;
cluster 3rd_class for Subset of T;
existence by Def11;
end;
theorem Th38: :: Theorem 8
A is 1st_class iff A` is 1st_class
proof
A1: A` is 1st_class implies A is 1st_class
proof
assume A` is 1st_class;
then Int Cl A` c= Cl Int A`;
then Int (Int A)` c= Cl Int A` by TDLAT_3:2;
then (Cl Int A)` c= Cl Int A` by TDLAT_3:3;
then (Cl Int A)` c= Cl (Cl A)` by TDLAT_3:3;
then (Cl Int A)` c= (Int Cl A)` by TDLAT_3:2;
then Int Cl A c= Cl Int A by SUBSET_1:12;
hence thesis;
end;
A is 1st_class implies A` is 1st_class
proof
assume A is 1st_class;
then Int Cl A c= Cl Int A;
then (Cl Int A)` c= (Int Cl A)` by SUBSET_1:12;
then Int (Int A)` c= (Int Cl A)` by TDLAT_3:3;
then Int (Int A)` c= Cl (Cl A)` by TDLAT_3:2;
then Int (Int A)` c= Cl Int A` by TDLAT_3:3;
then Int Cl A` c= Cl Int A` by TDLAT_3:2;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th39: :: Theorem 8
A is 2nd_class iff A` is 2nd_class
proof
A1: for A being Subset of T st A` is 2nd_class holds A is 2nd_class
proof
let A be Subset of T;
assume A` is 2nd_class;
then
A2: Cl Int A` c< Int Cl A`;
then Cl Int A` c= Int Cl A` by XBOOLE_0:def 8;
then Cl Int A` c= Int (Int A)` by TDLAT_3:2;
then Cl Int A` c= (Cl Int A)` by TDLAT_3:3;
then Cl (Cl A)` c= (Cl Int A)` by TDLAT_3:3;
then (Int Cl A)` c= (Cl Int A)` by TDLAT_3:2;
then
A3: Cl Int A c= Int Cl A by SUBSET_1:12;
Cl (Cl A)` <> Int Cl A` by A2,TDLAT_3:3;
then Cl (Cl A)` <> Int (Int A)` by TDLAT_3:2;
then (Cl Int A)` <> Cl (Cl A)` by TDLAT_3:3;
then Cl Int A <> Int Cl A by TDLAT_3:2;
then Cl Int A c< Int Cl A by A3,XBOOLE_0:def 8;
hence thesis;
end;
A is 2nd_class implies A` is 2nd_class
proof
assume A is 2nd_class;
then A`` is 2nd_class;
hence thesis by A1;
end;
hence thesis by A1;
end;
theorem Th40: :: Theorem 8
A is 3rd_class iff A` is 3rd_class
proof
(Int Cl A)` = Cl (Cl A)` by TDLAT_3:2
.= Cl Int A` by TDLAT_3:3;
then
A1: Int Cl A = (Cl Int A`)`;
(Cl Int A)` = Int (Int A)` by TDLAT_3:3
.= Int Cl A` by TDLAT_3:2;
then
A2: Cl Int A = (Int Cl A`)`;
A3: A` is 3rd_class implies A is 3rd_class
proof
assume A` is 3rd_class;
then
A4: Cl Int A`, Int Cl A` are_c=-incomparable;
then not Int Cl A` c= Cl Int A` by XBOOLE_0:def 9;
then
A5: not Int Cl A c= Cl Int A by A2,A1,SUBSET_1:12;
not Cl Int A` c= Int Cl A` by A4,XBOOLE_0:def 9;
then not Cl Int A c= Int Cl A by A2,A1,SUBSET_1:12;
then Cl Int A, Int Cl A are_c=-incomparable by A5,XBOOLE_0:def 9;
hence thesis;
end;
A is 3rd_class implies A` is 3rd_class
proof
assume A is 3rd_class;
then
A6: Cl Int A, Int Cl A are_c=-incomparable;
then not Int Cl A c= Cl Int A by XBOOLE_0:def 9;
then
A7: not Int Cl A` c= Cl Int A` by A2,A1,SUBSET_1:12;
not Cl Int A c= Int Cl A by A6,XBOOLE_0:def 9;
then not Cl Int A` c= Int Cl A` by A2,A1,SUBSET_1:12;
then Cl Int A`, Int Cl A` are_c=-incomparable by A7,XBOOLE_0:def 9;
hence thesis;
end;
hence thesis by A3;
end;
registration
let T;
let A be 1st_class Subset of T;
cluster A` -> 1st_class;
coherence by Th38;
end;
registration
let T be with_2nd_class_subsets TopSpace;
let A be 2nd_class Subset of T;
cluster A` -> 2nd_class;
coherence by Th39;
end;
registration
let T be with_3rd_class_subsets TopSpace;
let A be 3rd_class Subset of T;
cluster A` -> 3rd_class;
coherence by Th40;
end;
theorem Th41: :: Theorem 9
A is 1st_class implies Int Cl A = Int Cl Int A & Cl Int A = Cl Int Cl A
proof
Cl Int A c= Cl A by PRE_TOPC:19,TOPS_1:16;
then
A1: Int Cl Int A c= Int Cl A by TOPS_1:19;
Int A c= Int Cl A by PRE_TOPC:18,TOPS_1:19;
then
A2: Cl Int A c= Cl Int Cl A by PRE_TOPC:19;
assume A is 1st_class;
then
A3: Int Cl A c= Cl Int A;
then
A4: Cl Int Cl A c= Cl Cl Int A by PRE_TOPC:19;
Int Int Cl A c= Int Cl Int A by A3,TOPS_1:19;
hence thesis by A1,A4,A2,XBOOLE_0:def 10;
end;
theorem Th42: :: Theorem 9
(Int Cl A = Int Cl Int A or Cl Int A = Cl Int Cl A) implies A is 1st_class
proof
assume
A1: Int Cl A = Int Cl Int A or Cl Int A = Cl Int Cl A;
per cases by A1;
suppose
A2: Int Cl A = Int Cl Int A;
Int Cl Int A c= Cl Int A by TOPS_1:16;
hence thesis by A2;
end;
suppose
A3: Cl Int A = Cl Int Cl A;
Int Cl A c= Cl Int Cl A by PRE_TOPC:18;
hence thesis by A3;
end;
end;
theorem Th43: :: 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)
proof
assume that
A1: A is 1st_class and
A2: B is 1st_class;
A3: Cl Int B = Cl Int Cl B by A2,Th41;
Cl Int A = Cl Int Cl A by A1,Th41;
then
A4: Cl Int A \/ Cl Int B = Cl Int Cl (A \/ B) by A3,Th2;
Int Cl (A /\ B) c= Int (Cl A /\ Cl B) by PRE_TOPC:21,TOPS_1:19;
then
A5: Int Cl (A /\ B) c= Int Cl A /\ Int Cl B by TOPS_1:17;
Int (A \/ B) c= Int Cl (A \/ B) by PRE_TOPC:18,TOPS_1:19;
then
A6: Cl Int (A \/ B) c= Cl Int Cl (A \/ B) by PRE_TOPC:19;
Cl (Int A \/ Int B) c= Cl Int (A \/ B) by PRE_TOPC:19,TOPS_1:20;
then
A7: Cl Int A \/ Cl Int B c= Cl Int (A \/ B) by PRE_TOPC:20;
A8: Int Cl B = Int Cl Int B by A2,Th41;
Cl Int (A /\ B) c= Cl (A /\ B) by PRE_TOPC:19,TOPS_1:16;
then
A9: Int Cl Int (A /\ B) c= Int Cl (A /\ B) by TOPS_1:19;
Int Cl A = Int Cl Int A by A1,Th41;
then Int Cl A /\ Int Cl B = Int Cl Int (A /\ B) by A8,Th1;
hence thesis by A5,A9,A7,A4,A6,XBOOLE_0:def 10;
end;
theorem :: Theorem 11
A is 1st_class & B is 1st_class implies A \/ B is 1st_class & A /\ B
is 1st_class
proof
assume that
A1: A is 1st_class and
A2: B is 1st_class;
A3: Cl Int A = Cl Int Cl A by A1,Th41;
A4: Int Cl B = Int Cl Int B by A2,Th41;
A5: Int Cl A = Int Cl Int A by A1,Th41;
A6: Cl Int B = Cl Int Cl B by A2,Th41;
A7: Cl Int (A \/ B) = Cl Int A \/ Cl Int B by A1,A2,Th43
.= Cl Int Cl (A \/ B) by A3,A6,Th2;
Int Cl (A /\ B) = Int Cl A /\ Int Cl B by A1,A2,Th43
.= Int Cl Int (A /\ B) by A5,A4,Th1;
hence thesis by A7,Th42;
end;
:: 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