:: by Magdalena Jastrz\c{e}bska and Adam Grabowski

::

:: Received March 31, 2005

:: Copyright (c) 2005-2021 Association of Mizar Users

registration

existence

ex b_{1} being TopSpace st

( b_{1} is anti-discrete & not b_{1} is trivial & b_{1} is strict )

end;
ex b

( b

proof 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)))

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

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

proof 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 );

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

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;

coherence

for b_{1} being Subset of T st b_{1} is closed holds

b_{1} is supercondensed
by PRE_TOPC:22;

end;
coherence

for b

b

theorem :: ISOMICHI:3

theorem :: ISOMICHI:4

definition

let T be TopSpace;

let A be Subset of T;

compatibility

( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) )

end;
let A be Subset of T;

compatibility

( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) )

proof 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 ) );

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

for A being Subset of T holds

( A is condensed iff ( A is subcondensed & A is supercondensed ) ) ;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is condensed holds

( b_{1} is subcondensed & b_{1} is supercondensed )
;

coherence

for b_{1} being Subset of T st b_{1} is subcondensed & b_{1} is supercondensed holds

b_{1} is condensed
;

end;
coherence

for b

( b

coherence

for b

b

registration

let T be TopSpace;

existence

ex b_{1} being Subset of T st

( b_{1} is condensed & b_{1} is subcondensed & b_{1} is supercondensed )

end;
existence

ex b

( b

proof end;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is subcondensed holds

b_{1} is semi-open
by Th9, DECOMP_1:def 2;

coherence

for b_{1} being Subset of T st b_{1} is semi-open holds

b_{1} is subcondensed
by DECOMP_1:def 2, Th9;

end;
coherence

for b

b

coherence

for b

b

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

for A being Subset of T holds

( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) )

proof end;

notation
end;

registration
end;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is empty holds

( b_{1} is regular_open & b_{1} is regular_closed )

end;
coherence

for b

( b

proof end;

registration

let T be TopSpace;

existence

ex b_{1} being Subset of T st

( b_{1} is regular_open & b_{1} is regular_closed )

end;
existence

ex b

( b

proof end;

registration
end;

registration
end;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is regular_open holds

b_{1} is open
by TOPS_1:67;

coherence

for b_{1} being Subset of T st b_{1} is regular_closed holds

b_{1} is closed
by TOPS_1:66;

end;
coherence

for b

b

coherence

for b

b

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

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

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;

coherence

Int (Cl A) is regular_open by Th15;

coherence

Cl (Int A) is regular_closed by Th15;

end;
let A be Subset of T;

coherence

Int (Cl A) is regular_open by Th15;

coherence

Cl (Int A) is regular_closed by Th15;

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

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

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;

coherence

for b_{1} being Subset of T st b_{1} is regular_open holds

( b_{1} is condensed & b_{1} is open )
by TOPS_1:67;

coherence

for b_{1} being Subset of T st b_{1} is condensed & b_{1} is open holds

b_{1} is regular_open
by TOPS_1:67;

coherence

for b_{1} being Subset of T st b_{1} is regular_closed holds

( b_{1} is condensed & b_{1} is closed )
by TOPS_1:66;

coherence

for b_{1} being Subset of T st b_{1} is condensed & b_{1} is closed holds

b_{1} is regular_closed
by TOPS_1:66;

end;
coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

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

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

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;

compatibility

for b_{1} being Element of bool the carrier of T holds

( b_{1} = Fr A iff b_{1} = (Cl A) \ (Int A) )
by TOPGEN_1:8;

end;
let A be Subset of T;

compatibility

for b

( b

:: deftheorem defines Fr ISOMICHI:def 4 :

for T being TopStruct

for A being Subset of T holds Fr A = (Cl A) \ (Int A);

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 `))) ) )

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;

:: deftheorem defines Border ISOMICHI:def 5 :

for T being TopStruct

for A being Subset of T holds Border A = Int (Fr A);

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 `))) )

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

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

for A being Subset of T holds

( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) )

proof 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 ) )

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

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 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.[

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 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.[

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;

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

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

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

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

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is 1st_class holds

( not b_{1} is 2nd_class & not b_{1} is 3rd_class )
by XBOOLE_0:def 9, XBOOLE_1:60;

coherence

for b_{1} being Subset of T st b_{1} is 2nd_class holds

( not b_{1} is 1st_class & not b_{1} is 3rd_class )

for b_{1} being Subset of T st b_{1} is 3rd_class holds

( not b_{1} is 1st_class & not b_{1} is 2nd_class )
;

end;
coherence

for b

( not b

coherence

for b

( not b

proof end;

coherence for b

( not b

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is supercondensed holds

b_{1} is 1st_class

for b_{1} being Subset of T st b_{1} is subcondensed holds

b_{1} is 1st_class

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

definition

let T be TopSpace;

end;
attr T is with_2nd_class_subsets means :Def10: :: ISOMICHI:def 10

ex A being Subset of T st A is 2nd_class ;

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 ;

ex A being Subset of T st A is 3rd_class ;

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

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

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

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;

coherence

for b_{1} being Subset of T st b_{1} is proper & not b_{1} is empty holds

b_{1} is 2nd_class

end;
coherence

for b

b

proof end;

registration

let T be non trivial strict anti-discrete TopSpace;

existence

ex b_{1} being Subset of T st b_{1} is 2nd_class

end;
existence

ex b

proof end;

registration

ex b_{1} being TopSpace st

( b_{1} is with_1st_class_subsets & b_{1} is with_2nd_class_subsets & b_{1} is strict & not b_{1} is trivial )

ex b_{1} being TopSpace st

( b_{1} is with_3rd_class_subsets & not b_{1} is empty & b_{1} is strict )
end;

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

existence ex b

( b

proof end;

existence ex b

( b

proof end;

registration
end;

registration

let T be with_2nd_class_subsets TopSpace;

existence

ex b_{1} being Subset of T st b_{1} is 2nd_class
by Def10;

end;
existence

ex b

registration

let T be with_3rd_class_subsets TopSpace;

existence

ex b_{1} being Subset of T st b_{1} is 3rd_class
by Def11;

end;
existence

ex b

registration
end;

registration

let T be with_2nd_class_subsets TopSpace;

let A be 2nd_class Subset of T;

coherence

A ` is 2nd_class by Th39;

end;
let A be 2nd_class Subset of T;

coherence

A ` is 2nd_class by Th39;

registration

let T be with_3rd_class_subsets TopSpace;

let A be 3rd_class Subset of T;

coherence

A ` is 3rd_class by Th40;

end;
let A be 3rd_class Subset of T;

coherence

A ` is 3rd_class by Th40;

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

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

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

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 )

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;

:: A is condensed implies A` is condensed = TDLAT_1:16;