:: 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-2011 Association of Mizar Users

begin

registration

let D be non trivial set ;
cluster ADTS D -> non trivial ;
coherence
not ADTS D is trivial

proof end;

end;

registration

cluster non empty non trivial strict TopSpace-like anti-discrete TopStruct ;
existence
ex b₁ being TopSpace st
( b₁ is anti-discrete & not b₁ is trivial & not b₁ is empty & b₁ is strict )

proof end;

end;

theorem Th1: :: ISOMICHI:1

for T being TopSpace
for A, B being Subset of T holds (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B)))

proof end;

theorem Th2: :: ISOMICHI:2

for T being TopSpace
for A, B being Subset of T holds Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B)))

proof end;

begin

definition

let T be TopStruct ;
let A be Subset of T;
attr A is supercondensed means :Def1: :: ISOMICHI:def 1
Int (Cl A) = Int A;
attr A is subcondensed means :Def2: :: ISOMICHI:def 2
Cl (Int A) = Cl A;

end;

:: deftheorem Def1 defines supercondensed ISOMICHI:def 1 :
for T being TopStruct
for A being Subset of T holds
( A is supercondensed iff Int (Cl A) = Int A );

:: deftheorem Def2 defines subcondensed ISOMICHI:def 2 :
for T being TopStruct
for A being Subset of T holds
( A is subcondensed iff Cl (Int A) = Cl A );

registration

let T be TopSpace;
cluster closed -> supercondensed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is closed holds
b₁ is supercondensed

proof end;

end;

theorem :: ISOMICHI:3

for T being TopSpace
for A being Subset of T st A is closed holds
A is supercondensed ;

theorem Th4: :: ISOMICHI:4

for T being TopSpace
for A being Subset of T st A is open holds
A is subcondensed

proof end;

definition

let T be TopSpace;
let A be Subset of T;
redefine attr A is condensed means :Def3: :: ISOMICHI:def 3
( Cl (Int A) = Cl A & Int (Cl A) = Int A );
compatibility
( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) )

proof end;

end;

:: deftheorem Def3 defines condensed ISOMICHI:def 3 :
for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) );

theorem Th5: :: ISOMICHI:5

for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( A is subcondensed & A is supercondensed ) )

proof end;

registration

let T be TopSpace;
cluster condensed -> supercondensed subcondensed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is condensed holds
( b₁ is subcondensed & b₁ is supercondensed ) by Th5;
cluster supercondensed subcondensed -> condensed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is subcondensed & b₁ is supercondensed holds
b₁ is condensed by Th5;

end;

registration

let T be TopSpace;
cluster condensed supercondensed subcondensed Element of K6( the carrier of T);
existence
ex b₁ being Subset of T st
( b₁ is condensed & b₁ is subcondensed & b₁ is supercondensed )

proof end;

end;

theorem :: ISOMICHI:6

for T being TopSpace
for A being Subset of T st A is supercondensed holds
A ` is subcondensed

proof end;

theorem :: ISOMICHI:7

for T being TopSpace
for A being Subset of T st A is subcondensed holds
A ` is supercondensed

proof end;

theorem Th8: :: ISOMICHI:8

for T being TopSpace
for A being Subset of T holds
( A is supercondensed iff Int (Cl A) c= A )

proof end;

theorem Th9: :: ISOMICHI:9

for T being TopSpace
for A being Subset of T holds
( A is subcondensed iff A c= Cl (Int A) )

proof end;

registration

let T be TopSpace;
cluster subcondensed -> semi-open Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is subcondensed holds
b₁ is semi-open

proof end;

cluster semi-open -> subcondensed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is semi-open holds
b₁ is subcondensed

proof end;

end;

theorem Th10: :: ISOMICHI:10

for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )

proof end;

begin

notation

let T be TopStruct ;
let A be Subset of T;
synonym regular_open A for open_condensed ;

end;

notation

let T be TopStruct ;
let A be Subset of T;
synonym regular_closed A for closed_condensed ;

end;

theorem :: ISOMICHI:11

for T being TopSpace holds
( [#] T is regular_open & [#] T is regular_closed )

proof end;

registration

let T be TopSpace;
cluster [#] T -> regular_closed regular_open ;
coherence
( [#] T is regular_open & [#] T is regular_closed )

proof end;

end;

registration

let T be TopSpace;
cluster empty -> regular_closed regular_open Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is empty holds
( b₁ is regular_open & b₁ is regular_closed )

proof end;

end;

theorem :: ISOMICHI:12

canceled;

theorem :: ISOMICHI:13

canceled;

theorem :: ISOMICHI:14

for T being TopSpace holds Int (Cl ({} T)) = {} T

proof end;

theorem Th15: :: ISOMICHI:15

for T being TopSpace
for A being Subset of T st A is regular_open holds
A ` is regular_closed

proof end;

registration

let T be TopSpace;
cluster regular_closed regular_open Element of K6( the carrier of T);
existence
ex b₁ being Subset of T st
( b₁ is regular_open & b₁ is regular_closed )

proof end;

end;

registration

let T be TopSpace;
let A be regular_open Subset of T;
cluster A ` -> regular_closed ;
coherence
A ` is regular_closed by Th15;

end;

theorem Th16: :: ISOMICHI:16

for T being TopSpace
for A being Subset of T st A is regular_closed holds
A ` is regular_open

proof end;

registration

let T be TopSpace;
let A be regular_closed Subset of T;
cluster A ` -> regular_open ;
coherence
A ` is regular_open by Th16;

end;

registration

let T be TopSpace;
cluster regular_open -> open Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is regular_open holds
b₁ is open by TOPS_1:107;
cluster regular_closed -> closed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is regular_closed holds
b₁ is closed by TOPS_1:106;

end;

theorem Th17: :: ISOMICHI:17

for T being TopSpace
for A being Subset of T holds
( Int (Cl A) is regular_open & Cl (Int A) is regular_closed )

proof end;

registration

let T be TopSpace;
let A be Subset of T;
cluster Int (Cl A) -> regular_open ;
coherence
Int (Cl A) is regular_open by Th17;
cluster Cl (Int A) -> regular_closed ;
coherence
Cl (Int A) is regular_closed by Th17;

end;

theorem :: ISOMICHI:18

for T being TopSpace
for A being Subset of T holds
( A is regular_open iff ( A is supercondensed & A is open ) )

proof end;

theorem :: ISOMICHI:19

for T being TopSpace
for A being Subset of T holds
( A is regular_closed iff ( A is subcondensed & A is closed ) )

proof end;

registration

let T be TopSpace;
cluster regular_open -> open condensed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is regular_open holds
( b₁ is condensed & b₁ is open ) by TOPS_1:107;
cluster open condensed -> regular_open Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is condensed & b₁ is open holds
b₁ is regular_open by TOPS_1:107;
cluster regular_closed -> closed condensed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is regular_closed holds
( b₁ is condensed & b₁ is closed ) by TOPS_1:106;
cluster closed condensed -> regular_closed Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is condensed & b₁ is closed holds
b₁ is regular_closed by TOPS_1:106;

end;

theorem :: ISOMICHI:20

for T being TopSpace
for A being Subset of T holds
( A is condensed iff ex B being Subset of T st
( B is regular_open & B c= A & A c= Cl B ) )

proof end;

theorem :: ISOMICHI:21

for T being TopSpace
for A being Subset of T holds
( A is condensed iff ex B being Subset of T st
( B is regular_closed & Int B c= A & A c= B ) )

proof end;

begin

definition

let T be TopStruct ;
let A be Subset of T;
redefine func Fr A equals :: ISOMICHI:def 4
(Cl A) \ (Int A);
compatibility
for b₁ being Element of K6( the carrier of T) holds
( b₁ = Fr A iff b₁ = (Cl A) \ (Int A) ) by TOPGEN_1:10;

end;

:: deftheorem defines Fr ISOMICHI:def 4 :
for T being TopStruct
for A being Subset of T holds Fr A = (Cl A) \ (Int A);

theorem :: ISOMICHI:22

canceled;

theorem :: ISOMICHI:23

for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )

proof end;

definition

let T be TopStruct ;
let A be Subset of T;
func Border A -> Subset of T equals :: ISOMICHI:def 5
Int (Fr A);
coherence
Int (Fr A) is Subset of T ;

end;

:: deftheorem defines Border ISOMICHI:def 5 :
for T being TopStruct
for A being Subset of T holds Border A = Int (Fr A);

theorem Th24: :: ISOMICHI:24

for T being TopSpace
for A being Subset of T holds
( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )

proof end;

registration

let T be TopSpace;
let A be Subset of T;
cluster Border A -> regular_open ;
coherence
Border A is regular_open by Th24;

end;

theorem Th25: :: ISOMICHI:25

for T being TopSpace
for A being Subset of T holds
( A is supercondensed iff ( Int A is regular_open & Border A is empty ) )

proof end;

theorem Th26: :: ISOMICHI:26

for T being TopSpace
for A being Subset of T holds
( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )

proof end;

registration

let T be TopSpace;
let A be Subset of T;
cluster Border (Border A) -> empty ;
coherence
Border (Border A) is empty ;

end;

theorem :: ISOMICHI:27

for T being TopSpace
for A being Subset of T holds
( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) )

proof end;

begin

theorem :: ISOMICHI:28

for A being Subset of R^1
for a being real number st A = ].-infty,a.] holds
Int A = ].-infty,a.[

proof end;

theorem :: ISOMICHI:29

for A being Subset of R^1
for a being real number st A = [.a,+infty.[ holds
Int A = ].a,+infty.[

proof end;

theorem Th30: :: ISOMICHI:30

for A being Subset of R^1
for a, b being real number st A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ holds
Cl A = the carrier of R^1

proof end;

theorem :: ISOMICHI:31

for A being Subset of R^1
for a, b being real number st A = RAT (a,b) holds
Int A = {}

proof end;

theorem :: ISOMICHI:32

for A being Subset of R^1
for a, b being real number st A = IRRAT (a,b) holds
Int A = {}

proof end;

theorem :: ISOMICHI:33

canceled;

theorem :: ISOMICHI:34

canceled;

theorem :: ISOMICHI:35

for a, b being real number st a >= b holds
IRRAT (a,b) = {}

proof end;

theorem Th36: :: ISOMICHI:36

for a, b being real number holds IRRAT (a,b) c= [.a,+infty.[

proof end;

theorem Th37: :: ISOMICHI:37

for A being Subset of R^1
for a, b, c being real number st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds
Int A = ].-infty,a.[

proof end;

Lm1: for a, b being real number st a < b holds
[.a,b.] \/ {b} = [.a,b.]

proof end;

theorem :: ISOMICHI:38

canceled;

theorem :: ISOMICHI:39

canceled;

theorem :: ISOMICHI:40

canceled;

theorem :: ISOMICHI:41

for a, b being real number st a < b holds
REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[

proof end;

theorem :: ISOMICHI:42

canceled;

theorem :: ISOMICHI:43

canceled;

theorem Th44: :: ISOMICHI:44

for A being Subset of R^1
for a, b, c being real number st A = ].-infty,a.] \/ [.b,c.] & a < b & b < c holds
Int A = ].-infty,a.[ \/ ].b,c.[

proof end;

begin

notation

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

end;

theorem Th45: :: ISOMICHI:45

for A, B being set holds
( A,B are_c=-incomparable or A c= B or B c< A )

proof end;

definition

let T be TopSpace;
let A be Subset of T;
attr A is 1st_class means :Def6: :: ISOMICHI:def 6
Int (Cl A) c= Cl (Int A);
attr A is 2nd_class means :Def7: :: ISOMICHI:def 7
Cl (Int A) c< Int (Cl A);
attr A is 3rd_class means :Def8: :: ISOMICHI:def 8
Cl (Int A), Int (Cl A) are_c=-incomparable ;

end;

:: deftheorem Def6 defines 1st_class ISOMICHI:def 6 :
for T being TopSpace
for A being Subset of T holds
( A is 1st_class iff Int (Cl A) c= Cl (Int A) );

:: deftheorem Def7 defines 2nd_class ISOMICHI:def 7 :
for T being TopSpace
for A being Subset of T holds
( A is 2nd_class iff Cl (Int A) c< Int (Cl A) );

:: deftheorem Def8 defines 3rd_class ISOMICHI:def 8 :
for T being TopSpace
for A being Subset of T holds
( A is 3rd_class iff Cl (Int A), Int (Cl A) are_c=-incomparable );

theorem :: ISOMICHI:46

for T being TopSpace
for A being Subset of T holds
( A is 1st_class or A is 2nd_class or A is 3rd_class )

proof end;

registration

let T be TopSpace;
cluster 1st_class -> non 2nd_class non 3rd_class Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is 1st_class holds
( not b₁ is 2nd_class & not b₁ is 3rd_class )

proof end;

cluster 2nd_class -> non 1st_class non 3rd_class Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is 2nd_class holds
( not b₁ is 1st_class & not b₁ is 3rd_class )

proof end;

cluster 3rd_class -> non 1st_class non 2nd_class Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is 3rd_class holds
( not b₁ is 1st_class & not b₁ is 2nd_class ) ;

end;

theorem Th47: :: ISOMICHI:47

for T being TopSpace
for A being Subset of T holds
( A is 1st_class iff Border A is empty )

proof end;

registration

let T be TopSpace;
cluster supercondensed -> 1st_class Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is supercondensed holds
b₁ is 1st_class

proof end;

cluster subcondensed -> 1st_class Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is subcondensed holds
b₁ is 1st_class

proof end;

end;

definition

let T be TopSpace;
attr T is with_1st_class_subsets means :Def9: :: ISOMICHI:def 9
ex A being Subset of T st A is 1st_class ;
attr T is with_2nd_class_subsets means :Def10: :: ISOMICHI:def 10
ex A being Subset of T st A is 2nd_class ;
attr T is with_3rd_class_subsets means :Def11: :: ISOMICHI:def 11
ex A being Subset of T st A is 3rd_class ;

end;

:: deftheorem Def9 defines with_1st_class_subsets ISOMICHI:def 9 :
for T being TopSpace holds
( T is with_1st_class_subsets iff ex A being Subset of T st A is 1st_class );

:: deftheorem Def10 defines with_2nd_class_subsets ISOMICHI:def 10 :
for T being TopSpace holds
( T is with_2nd_class_subsets iff ex A being Subset of T st A is 2nd_class );

:: deftheorem Def11 defines with_3rd_class_subsets ISOMICHI:def 11 :
for T being TopSpace holds
( T is with_3rd_class_subsets iff ex A being Subset of T st A is 3rd_class );

registration

let T be non empty anti-discrete TopSpace;
cluster non empty proper -> 2nd_class Element of K6( the carrier of T);
coherence
for b₁ being Subset of T st b₁ is proper & not b₁ is empty holds
b₁ is 2nd_class

proof end;

end;

registration

let T be non empty non trivial strict anti-discrete TopSpace;
cluster 2nd_class Element of K6( the carrier of T);
existence
ex b₁ being Subset of T st b₁ is 2nd_class

proof end;

end;

registration

cluster non empty non trivial strict TopSpace-like with_1st_class_subsets with_2nd_class_subsets TopStruct ;
existence
ex b₁ being TopSpace st
( b₁ is with_1st_class_subsets & b₁ is with_2nd_class_subsets & not b₁ is empty & b₁ is strict & not b₁ is trivial )

proof end;

cluster non empty strict TopSpace-like with_3rd_class_subsets TopStruct ;
existence
ex b₁ being TopSpace st
( b₁ is with_3rd_class_subsets & not b₁ is empty & b₁ is strict )

proof end;

end;

registration

let T be TopSpace;
cluster 1st_class Element of K6( the carrier of T);
existence
ex b₁ being Subset of T st b₁ is 1st_class

proof end;

end;

registration

let T be with_2nd_class_subsets TopSpace;
cluster 2nd_class Element of K6( the carrier of T);
existence
ex b₁ being Subset of T st b₁ is 2nd_class by Def10;

end;

registration

let T be with_3rd_class_subsets TopSpace;
cluster 3rd_class Element of K6( the carrier of T);
existence
ex b₁ being Subset of T st b₁ is 3rd_class by Def11;

end;

theorem Th48: :: ISOMICHI:48

for T being TopSpace
for A being Subset of T holds
( A is 1st_class iff A ` is 1st_class )

proof end;

theorem Th49: :: ISOMICHI:49

for T being TopSpace
for A being Subset of T holds
( A is 2nd_class iff A ` is 2nd_class )

proof end;

theorem Th50: :: ISOMICHI:50

for T being TopSpace
for A being Subset of T holds
( A is 3rd_class iff A ` is 3rd_class )

proof end;

registration

let T be TopSpace;
let A be 1st_class Subset of T;
cluster A ` -> 1st_class ;
coherence
A ` is 1st_class by Th48;

end;

registration

let T be with_2nd_class_subsets TopSpace;
let A be 2nd_class Subset of T;
cluster A ` -> 2nd_class ;
coherence
A ` is 2nd_class by Th49;

end;

registration

let T be with_3rd_class_subsets TopSpace;
let A be 3rd_class Subset of T;
cluster A ` -> 3rd_class ;
coherence
A ` is 3rd_class by Th50;

end;

theorem Th51: :: ISOMICHI:51

for T being TopSpace
for A being Subset of T st A is 1st_class holds
( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )

proof end;

theorem Th52: :: ISOMICHI:52

for T being TopSpace
for A being Subset of T st ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) holds
A is 1st_class

proof end;

theorem Th53: :: ISOMICHI:53

for T being TopSpace
for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) )

proof end;

theorem :: ISOMICHI:54

for T being TopSpace
for A, B being Subset of T st A is 1st_class & B is 1st_class holds
( A \/ B is 1st_class & A /\ B is 1st_class )

proof end;