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

registration

let D be non trivial set ;

cluster ADTS D -> non trivial ;

coherence
not ADTS D is trivial

proof end;

end;

registration

cluster non trivial strict TopSpace-like anti-discrete for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is anti-discrete & not b₁ is trivial & 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;

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 for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is closed holds
b₁ is supercondensed by PRE_TOPC:22;

end;

theorem :: ISOMICHI:3

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

theorem :: ISOMICHI:4

for T being TopSpace
for A being Subset of T st A is open holds
A is subcondensed by TOPS_1:23;

definition

let T be TopSpace;
let A be Subset of T;

redefine attr A is condensed means :: 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 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 :: ISOMICHI:5

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

registration

let T be TopSpace;

cluster condensed -> supercondensed subcondensed for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is condensed holds
( b₁ is subcondensed & b₁ is supercondensed ) ;

cluster supercondensed subcondensed -> condensed for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is subcondensed & b₁ is supercondensed holds
b₁ is condensed ;

end;

registration

let T be TopSpace;

cluster condensed supercondensed subcondensed for Element of bool 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;

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

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 for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is subcondensed holds
b₁ is semi-open by Th9, DECOMP_1:def 2;

cluster semi-open -> subcondensed for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is semi-open holds
b₁ is subcondensed by DECOMP_1:def 2, Th9;

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;

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 for Element of bool 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

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

proof end;

theorem Th13: :: ISOMICHI:13

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 for Element of bool 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 Th13;

end;

theorem Th14: :: ISOMICHI:14

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 Th14;

end;

registration

let T be TopSpace;

cluster regular_open -> open for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is regular_open holds
b₁ is open by TOPS_1:67;

cluster regular_closed -> closed for Element of bool the carrier of T;

coherence
for b₁ being Subset of T st b₁ is regular_closed holds
b₁ is closed 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: :: ISOMICHI:15

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 Th15;

cluster Cl (Int A) -> regular_closed ;

coherence
Cl (Int A) is regular_closed by Th15;

end;

theorem :: ISOMICHI:16

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

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 for Element of bool 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:67;

cluster open condensed -> regular_open for Element of bool 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:67;

cluster regular_closed -> closed condensed for Element of bool 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:66;

cluster closed condensed -> regular_closed for Element of bool 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:66;

end;

theorem :: ISOMICHI:18

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

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;

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 bool the carrier of T holds
( b₁ = Fr A iff b₁ = (Cl A) \ (Int A) ) by TOPGEN_1:8;

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

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 Th21: :: ISOMICHI:21

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 Th21;

end;

theorem Th22: :: ISOMICHI:22

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 Th23: :: ISOMICHI:23

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

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;

theorem :: ISOMICHI:25

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

proof end;

theorem :: ISOMICHI:26

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

proof end;

theorem Th27: :: ISOMICHI:27

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

proof end;

theorem :: ISOMICHI:28

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

proof end;

theorem :: ISOMICHI:29

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

proof end;

theorem :: ISOMICHI:30

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

proof end;

theorem Th31: :: ISOMICHI:31

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

proof end;

theorem Th32: :: ISOMICHI:32

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

proof end;

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

proof end;

theorem :: ISOMICHI:33

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

proof end;

theorem Th34: :: ISOMICHI:34

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

proof end;

notation

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

end;

theorem Th35: :: ISOMICHI:35

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

:: deftheorem 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 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 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:36

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 ) by Th35;

registration

let T be TopSpace;

cluster 1st_class -> non 2nd_class non 3rd_class for Element of bool 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 ) by XBOOLE_0:def 9, XBOOLE_1:60;

cluster 2nd_class -> non 1st_class non 3rd_class for Element of bool 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 for Element of bool 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 Th37: :: ISOMICHI:37

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 for Element of bool 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 for Element of bool 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 :: 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 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 for Element of bool 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 trivial strict anti-discrete TopSpace;

cluster 2nd_class for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st b₁ is 2nd_class

proof end;

end;

registration

cluster non trivial strict TopSpace-like with_1st_class_subsets with_2nd_class_subsets for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is with_1st_class_subsets & b₁ is with_2nd_class_subsets & b₁ is strict & not b₁ is trivial )

proof end;

cluster non empty strict TopSpace-like with_3rd_class_subsets for 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 for Element of bool 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 for Element of bool 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 for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st b₁ is 3rd_class by Def11;

end;

theorem Th38: :: ISOMICHI:38

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

proof end;

theorem Th39: :: ISOMICHI:39

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

proof end;

theorem Th40: :: ISOMICHI:40

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 Th38;

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 Th39;

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 Th40;

end;

theorem Th41: :: ISOMICHI:41

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 Th42: :: ISOMICHI:42

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 Th43: :: ISOMICHI:43

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

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;