:: ISOMICHI semantic presentation

registration

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

proof end;

end;

registration

cluster non empty strict anti-discrete non trivial TopStruct ;
existence

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 :

:: deftheorem Def2 defines subcondensed ISOMICHI:def 2 :

theorem Th3: :: ISOMICHI:3

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

proof end;

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

proof end;

end;

:: deftheorem Def3 defines condensed ISOMICHI:def 3 :

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 K10(the carrier of T);
coherence by Th5;
cluster supercondensed subcondensed -> condensed Element of K10(the carrier of T);
coherence by Th5;

end;

registration

let T be TopSpace;
cluster condensed supercondensed subcondensed Element of K10(the carrier of T);
existence

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 K10(the carrier of T);
coherence

proof end;

cluster semi-open -> subcondensed Element of K10(the carrier of T);
coherence

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;

notation

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

end;

notation

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

end;

theorem Th11: :: 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 by Th11;

end;

theorem Th12: :: ISOMICHI:12

for X being TopSpace holds
( {} X is regular_open & {} X is regular_closed )

proof end;

registration

let T be TopSpace;
cluster {} T -> regular_closed regular_open ;
coherence by Th12;

end;

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 K10(the carrier of T);
existence

proof end;

end;

registration

let T be TopSpace;
let A be regular_open Subset of T;
cluster A ` -> regular_closed ;
coherence 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 by Th16;

end;

registration

let T be TopSpace;
cluster regular_open -> open Element of K10(the carrier of T);
coherence by TOPS_1:107;
cluster regular_closed -> closed Element of K10(the carrier of T);
coherence 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 by Th17;
cluster Cl (Int A) -> regular_closed ;
coherence 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 semi-open supercondensed subcondensed Element of K10(the carrier of T);
coherence by TOPS_1:107;
cluster open condensed -> open regular_open Element of K10(the carrier of T);
coherence by TOPS_1:107;
cluster regular_closed -> closed condensed semi-open supercondensed subcondensed Element of K10(the carrier of T);
coherence by TOPS_1:106;
cluster closed condensed -> closed regular_closed Element of K10(the carrier of T);
coherence 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;

notation

let T be TopStruct ;
let A be Subset of T;
synonym Bound A for Fr A;

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 by TOPGEN_1:10;

end;

:: deftheorem defines Bound ISOMICHI:def 4 :

theorem Th22: :: ISOMICHI:22

for T being TopSpace
for A being Subset of T holds Fr A is closed

proof end;

registration

let T be TopSpace;
let A be Subset of T;
cluster Bound A -> closed ;
coherence by Th22;

end;

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 ;

end;

:: deftheorem defines Border ISOMICHI:def 5 :

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 -> open condensed regular_open semi-open supercondensed subcondensed ;
coherence 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 open condensed regular_closed regular_open semi-open supercondensed subcondensed ;
coherence ;

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;

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 holds
Int A = ]. a

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) 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 Th33: :: ISOMICHI:33

for a, b being real number holds (].-infty, a) \ (].-infty, b) = [.b,a.]

proof end;

theorem Th34: :: ISOMICHI:34

for a, b being real number st a < b holds
[. b misses ].-infty, a

proof end;

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

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;

theorem Th38: :: ISOMICHI:38

for a, b being real number holds [.a,b.] misses ]. b

proof end;

Lm1: for a, b being real number st a < b holds
[.a,b.] \ (]. b) = [.a,b.]

proof end;

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

proof end;

theorem Th39: :: ISOMICHI:39

for b being real number holds ([. b) \ (]. b) = {b}

proof end;

theorem Th40: :: ISOMICHI:40

for a, b being real number st a < b holds
[.a,b.] = ([. a) \ (]. b)

proof end;

theorem :: ISOMICHI:41

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

proof end;

theorem Th42: :: ISOMICHI:42

for a, b being real number holds ].a,b.[ = (]. a) \ ([. b)

proof end;

theorem Th43: :: ISOMICHI:43

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

proof end;

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;

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 :

:: deftheorem Def7 defines 2nd_class ISOMICHI:def 7 :

:: deftheorem Def8 defines 3rd_class ISOMICHI:def 8 :

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 K10(the carrier of T);
coherence

proof end;

cluster 2nd_class -> non 1st_class non 3rd_class Element of K10(the carrier of T);
coherence

proof end;

cluster 3rd_class -> non 1st_class non 2nd_class Element of K10(the carrier of T);
coherence

proof end;

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 non 2nd_class non 3rd_class Element of K10(the carrier of T);
coherence

proof end;

cluster subcondensed -> 1st_class non 2nd_class non 3rd_class Element of K10(the carrier of T);
coherence

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 :

:: deftheorem Def10 defines with_2nd_class_subsets ISOMICHI:def 10 :

:: deftheorem Def11 defines with_3rd_class_subsets ISOMICHI:def 11 :

registration

let T be non empty anti-discrete TopSpace;
cluster non empty proper -> non 1st_class 2nd_class non 3rd_class Element of K10(the carrier of T);
coherence

proof end;

end;

registration

let T be non empty strict anti-discrete non trivial TopSpace;
cluster non 1st_class 2nd_class non 3rd_class Element of K10(the carrier of T);
existence

proof end;

end;

registration

cluster non empty strict non trivial with_1st_class_subsets with_2nd_class_subsets TopStruct ;
existence

proof end;

cluster non empty strict with_3rd_class_subsets TopStruct ;
existence

proof end;

end;

registration

let T be TopSpace;
cluster 1st_class non 2nd_class non 3rd_class Element of K10(the carrier of T);
existence

proof end;

end;

registration

let T be with_2nd_class_subsets TopSpace;
cluster non 1st_class 2nd_class non 3rd_class Element of K10(the carrier of T);
existence by Def10;

end;

registration

let T be with_3rd_class_subsets TopSpace;
cluster non 1st_class non 2nd_class 3rd_class Element of K10(the carrier of T);
existence 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 non 2nd_class non 3rd_class ;
coherence by Th48;

end;

registration

let T be with_2nd_class_subsets TopSpace;
let A be 2nd_class Subset of T;
cluster A ` -> non 1st_class 2nd_class non 3rd_class ;
coherence by Th49;

end;

registration

let T be with_3rd_class_subsets TopSpace;
let A be 3rd_class Subset of T;
cluster A ` -> non 1st_class non 2nd_class 3rd_class ;
coherence 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;