:: 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 b1 being TopSpace st
( b1 is anti-discrete & not b1 is trivial & b1 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 b1 being Subset of T st b1 is closed holds
b1 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 b1 being Subset of T st b1 is condensed holds
( b1 is subcondensed & b1 is supercondensed ) ;
cluster supercondensed subcondensed -> condensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is subcondensed & b1 is supercondensed holds
b1 is condensed ;
end;

registration
let T be TopSpace;
cluster condensed supercondensed subcondensed for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is condensed & b1 is subcondensed & b1 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 b1 being Subset of T st b1 is subcondensed holds
b1 is semi-open by Th9, DECOMP_1:def 2;
cluster semi-open -> subcondensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is semi-open holds
b1 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 b1 being Subset of T st b1 is empty holds
( b1 is regular_open & b1 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 b1 being Subset of T st
( b1 is regular_open & b1 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 b1 being Subset of T st b1 is regular_open holds
b1 is open by TOPS_1:67;
cluster regular_closed -> closed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is regular_closed holds
b1 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 b1 being Subset of T st b1 is regular_open holds
( b1 is condensed & b1 is open ) by TOPS_1:67;
cluster open condensed -> regular_open for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is condensed & b1 is open holds
b1 is regular_open by TOPS_1:67;
cluster regular_closed -> closed condensed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is regular_closed holds
( b1 is condensed & b1 is closed ) by TOPS_1:66;
cluster closed condensed -> regular_closed for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is condensed & b1 is closed holds
b1 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 b1 being Element of bool the carrier of T holds
( b1 = Fr A iff b1 = (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 b1 being Subset of T st b1 is 1st_class holds
( not b1 is 2nd_class & not b1 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 b1 being Subset of T st b1 is 2nd_class holds
( not b1 is 1st_class & not b1 is 3rd_class )
proof end;
cluster 3rd_class -> non 1st_class non 2nd_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is 3rd_class holds
( not b1 is 1st_class & not b1 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 b1 being Subset of T st b1 is supercondensed holds
b1 is 1st_class
proof end;
cluster subcondensed -> 1st_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is subcondensed holds
b1 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 b1 being Subset of T st b1 is proper & not b1 is empty holds
b1 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 b1 being Subset of T st b1 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 b1 being TopSpace st
( b1 is with_1st_class_subsets & b1 is with_2nd_class_subsets & b1 is strict & not b1 is trivial )
proof end;
cluster non empty strict TopSpace-like with_3rd_class_subsets for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is with_3rd_class_subsets & not b1 is empty & b1 is strict )
proof end;
end;

registration
let T be TopSpace;
cluster 1st_class for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 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 b1 being Subset of T st b1 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 b1 being Subset of T st b1 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;