:: ISOMICHI semantic presentation

registration

let c₁ be non trivial set ;
cluster ADTS a₁ -> 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 b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Int (Cl (Int b₂))) /\ (Int (Cl (Int b₃))) = Int (Cl (Int (b₂ /\ b₃)))

proof end;

theorem Th2: :: ISOMICHI:2

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds Cl (Int (Cl (b₂ \/ b₃))) = (Cl (Int (Cl b₂))) \/ (Cl (Int (Cl b₃)))

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
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 b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is closed holds
b₂ is supercondensed

proof end;

theorem Th4: :: ISOMICHI:4

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is open holds
b₂ is subcondensed

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset of c₁;
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 b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is condensed iff ( b₂ is subcondensed & b₂ is supercondensed ) )

proof end;

registration

let c₁ be TopSpace;
cluster condensed -> supercondensed subcondensed Element of K10(the carrier of a₁);
coherence by Th5;
cluster supercondensed subcondensed -> condensed Element of K10(the carrier of a₁);
coherence by Th5;

end;

registration

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

proof end;

end;

theorem Th6: :: ISOMICHI:6

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is supercondensed holds
b₂ ` is subcondensed

proof end;

theorem Th7: :: ISOMICHI:7

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is subcondensed holds
b₂ ` is supercondensed

proof end;

theorem Th8: :: ISOMICHI:8

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is supercondensed iff Int (Cl b₂) c= b₂ )

proof end;

theorem Th9: :: ISOMICHI:9

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is subcondensed iff b₂ c= Cl (Int b₂) )

proof end;

registration

let c₁ be TopSpace;
cluster subcondensed -> semi-open Element of K10(the carrier of a₁);
coherence

proof end;

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

proof end;

end;

theorem Th10: :: ISOMICHI:10

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is condensed iff ( Int (Cl b₂) c= b₂ & b₂ c= Cl (Int b₂) ) )

proof end;

notation

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
synonym regular_open c₂ for open_condensed c₂;

end;

notation

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
synonym regular_closed c₂ for closed_condensed c₂;

end;

theorem Th11: :: ISOMICHI:11

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

proof end;

registration

let c₁ be TopSpace;
cluster [#] a₁ -> regular_closed regular_open ;
coherence by Th11;

end;

theorem Th12: :: ISOMICHI:12

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

proof end;

registration

let c₁ be TopSpace;
cluster {} a₁ -> regular_closed regular_open ;
coherence by Th12;

end;

theorem Th13: :: ISOMICHI:13

canceled;

theorem Th14: :: ISOMICHI:14

for b₁ being TopSpace holds Int (Cl ({} b₁)) = {} b₁

proof end;

theorem Th15: :: ISOMICHI:15

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is regular_open holds
b₂ ` is regular_closed

proof end;

registration

let c₁ be TopSpace;
cluster regular_closed regular_open Element of K10(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be TopSpace;
let c₂ be regular_open Subset of c₁;
cluster a₂ ` -> regular_closed ;
coherence by Th15;

end;

theorem Th16: :: ISOMICHI:16

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is regular_closed holds
b₂ ` is regular_open

proof end;

registration

let c₁ be TopSpace;
let c₂ be regular_closed Subset of c₁;
cluster a₂ ` -> regular_open ;
coherence by Th16;

end;

registration

let c₁ be TopSpace;
cluster regular_open -> open Element of K10(the carrier of a₁);
coherence by TOPS_1:107;
cluster regular_closed -> closed Element of K10(the carrier of a₁);
coherence by TOPS_1:106;

end;

theorem Th17: :: ISOMICHI:17

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( Int (Cl b₂) is regular_open & Cl (Int b₂) is regular_closed )

proof end;

registration

let c₁ be TopSpace;
let c₂ be Subset of c₁;
cluster Int (Cl a₂) -> regular_open ;
coherence by Th17;
cluster Cl (Int a₂) -> regular_closed ;
coherence by Th17;

end;

theorem Th18: :: ISOMICHI:18

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is regular_open iff ( b₂ is supercondensed & b₂ is open ) )

proof end;

theorem Th19: :: ISOMICHI:19

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is regular_closed iff ( b₂ is subcondensed & b₂ is closed ) )

proof end;

registration

let c₁ be TopSpace;
cluster regular_open -> open condensed semi-open supercondensed subcondensed Element of K10(the carrier of a₁);
coherence by TOPS_1:107;
cluster open condensed -> open regular_open Element of K10(the carrier of a₁);
coherence by TOPS_1:107;
cluster regular_closed -> closed condensed semi-open supercondensed subcondensed Element of K10(the carrier of a₁);
coherence by TOPS_1:106;
cluster closed condensed -> closed regular_closed Element of K10(the carrier of a₁);
coherence by TOPS_1:106;

end;

theorem Th20: :: ISOMICHI:20

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is condensed iff ex b₃ being Subset of b₁ st
( b₃ is regular_open & b₃ c= b₂ & b₂ c= Cl b₃ ) )

proof end;

theorem Th21: :: ISOMICHI:21

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is condensed iff ex b₃ being Subset of b₁ st
( b₃ is regular_closed & Int b₃ c= b₂ & b₂ c= b₃ ) )

proof end;

notation

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
synonym Bound c₂ for Fr c₂;

end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
redefine func Fr c₂ -> Element of K10(the carrier of a₁) equals :: ISOMICHI:def 4
(Cl a₂) \ (Int a₂);
compatibility by TOPGEN_1:10;

end;

:: deftheorem Def4 defines Bound ISOMICHI:def 4 :

theorem Th22: :: ISOMICHI:22

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Fr b₂ is closed

proof end;

registration

let c₁ be TopSpace;
let c₂ be Subset of c₁;
cluster Bound a₂ -> closed ;
coherence by Th22;

end;

theorem Th23: :: ISOMICHI:23

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is condensed iff ( Fr b₂ = (Cl (Int b₂)) \ (Int (Cl b₂)) & Fr b₂ = (Cl (Int b₂)) /\ (Cl (Int (b₂ ` ))) ) )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
func Border c₂ -> Subset of a₁ equals :: ISOMICHI:def 5
Int (Fr a₂);
coherence ;

end;

:: deftheorem Def5 defines Border ISOMICHI:def 5 :

theorem Th24: :: ISOMICHI:24

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( Border b₂ is regular_open & Border b₂ = (Int (Cl b₂)) \ (Cl (Int b₂)) & Border b₂ = (Int (Cl b₂)) /\ (Int (Cl (b₂ ` ))) )

proof end;

registration

let c₁ be TopSpace;
let c₂ be Subset of c₁;
cluster Border a₂ -> open condensed regular_open semi-open supercondensed subcondensed ;
coherence by Th24;

end;

theorem Th25: :: ISOMICHI:25

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is supercondensed iff ( Int b₂ is regular_open & Border b₂ is empty ) )

proof end;

theorem Th26: :: ISOMICHI:26

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is subcondensed iff ( Cl b₂ is regular_closed & Border b₂ is empty ) )

proof end;

registration

let c₁ be TopSpace;
let c₂ be Subset of c₁;
cluster Border (Border a₂) -> empty open condensed regular_closed regular_open semi-open supercondensed subcondensed ;
coherence ;

end;

theorem Th27: :: ISOMICHI:27

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is condensed iff ( Int b₂ is regular_open & Cl b₂ is regular_closed & Border b₂ is empty ) )

proof end;

theorem Th28: :: ISOMICHI:28

for b₁ being Subset of R^1
for b₂ being real number st b₁ = ].-infty, b₂ holds
Int b₁ = ].-infty, b₂

proof end;

theorem Th29: :: ISOMICHI:29

for b₁ being Subset of R^1
for b₂ being real number st b₁ = [. b₂ holds
Int b₁ = ]. b₂

proof end;

theorem Th30: :: ISOMICHI:30

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

proof end;

theorem Th31: :: ISOMICHI:31

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₁ = RAT b₂,b₃ holds
Int b₁ = {}

proof end;

theorem Th32: :: ISOMICHI:32

for b₁ being Subset of R^1
for b₂, b₃ being real number st b₁ = IRRAT b₂,b₃ holds
Int b₁ = {}

proof end;

theorem Th33: :: ISOMICHI:33

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

proof end;

theorem Th34: :: ISOMICHI:34

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

proof end;

theorem Th35: :: ISOMICHI:35

for b₁, b₂ being real number st b₁ >= b₂ holds
IRRAT b₁,b₂ = {}

proof end;

theorem Th36: :: ISOMICHI:36

for b₁, b₂ being real number holds IRRAT b₁,b₂ c= [. b₁

proof end;

theorem Th37: :: ISOMICHI:37

for b₁ being Subset of R^1
for b₂, b₃, b₄ being real number st b₁ = (].-infty, b₂) \/ (RAT b₃,b₄) & b₂ < b₃ & b₃ < b₄ holds
Int b₁ = ].-infty, b₂

proof end;

theorem Th38: :: ISOMICHI:38

for b₁, b₂ being real number holds [.b₁,b₂.] misses ]. b₂

proof end;

Lemma28: for b₁, b₂ being real number st b₁ < b₂ holds
[.b₁,b₂.] \ (]. b₂) = [.b₁,b₂.]

proof end;

Lemma29: for b₁, b₂ being real number st b₁ < b₂ holds
[.b₁,b₂.] \/ {b₂} = [.b₁,b₂.]

proof end;

theorem Th39: :: ISOMICHI:39

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

proof end;

theorem Th40: :: ISOMICHI:40

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

proof end;

theorem Th41: :: ISOMICHI:41

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

proof end;

theorem Th42: :: ISOMICHI:42

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

proof end;

theorem Th43: :: ISOMICHI:43

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

proof end;

theorem Th44: :: ISOMICHI:44

for b₁ being Subset of R^1
for b₂, b₃, b₄ being real number st b₁ = (].-infty, b₂) \/ [.b₃,b₄.] & b₂ < b₃ & b₃ < b₄ holds
Int b₁ = (].-infty, b₂) \/ ].b₃,b₄.[

proof end;

notation

let c₁, c₂ be set ;
antonym c₁,c₂ are_c=-incomparable for c₁,c₂ are_c=-comparable ;

end;

theorem Th45: :: ISOMICHI:45

for b₁, b₂ being set holds
( b₁,b₂ are_c=-incomparable or b₁ c= b₂ or b₂ c< b₁ )

proof end;

definition

let c₁ be TopSpace;
let c₂ be Subset of c₁;
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 Th46: :: ISOMICHI:46

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is 1st_class or b₂ is 2nd_class or b₂ is 3rd_class )

proof end;

registration

let c₁ be TopSpace;
cluster 1st_class -> non 2nd_class non 3rd_class Element of K10(the carrier of a₁);
coherence

proof end;

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

proof end;

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

proof end;

end;

theorem Th47: :: ISOMICHI:47

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is 1st_class iff Border b₂ is empty )

proof end;

registration

let c₁ be TopSpace;
cluster supercondensed -> 1st_class non 2nd_class non 3rd_class Element of K10(the carrier of a₁);
coherence

proof end;

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

proof end;

end;

definition

let c₁ be TopSpace;
attr a₁ is with_1st_class_subsets means :Def9: :: ISOMICHI:def 9
ex b₁ being Subset of a₁ st b₁ is 1st_class;
attr a₁ is with_2nd_class_subsets means :Def10: :: ISOMICHI:def 10
ex b₁ being Subset of a₁ st b₁ is 2nd_class;
attr a₁ is with_3rd_class_subsets means :Def11: :: ISOMICHI:def 11
ex b₁ being Subset of a₁ st b₁ 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 c₁ be non empty anti-discrete TopSpace;
cluster non empty proper -> non 1st_class 2nd_class non 3rd_class Element of K10(the carrier of a₁);
coherence

proof end;

end;

registration

let c₁ be non empty strict anti-discrete non trivial TopSpace;
cluster non 1st_class 2nd_class non 3rd_class Element of K10(the carrier of a₁);
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 c₁ be TopSpace;
cluster 1st_class non 2nd_class non 3rd_class Element of K10(the carrier of a₁);
existence

proof end;

end;

registration

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

end;

registration

let c₁ be with_3rd_class_subsets TopSpace;
cluster non 1st_class non 2nd_class 3rd_class Element of K10(the carrier of a₁);
existence by Def11;

end;

theorem Th48: :: ISOMICHI:48

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is 1st_class iff b₂ ` is 1st_class )

proof end;

theorem Th49: :: ISOMICHI:49

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is 2nd_class iff b₂ ` is 2nd_class )

proof end;

theorem Th50: :: ISOMICHI:50

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( b₂ is 3rd_class iff b₂ ` is 3rd_class )

proof end;

registration

let c₁ be TopSpace;
let c₂ be 1st_class Subset of c₁;
cluster a₂ ` -> 1st_class non 2nd_class non 3rd_class ;
coherence by Th48;

end;

registration

let c₁ be with_2nd_class_subsets TopSpace;
let c₂ be 2nd_class Subset of c₁;
cluster a₂ ` -> non 1st_class 2nd_class non 3rd_class ;
coherence by Th49;

end;

registration

let c₁ be with_3rd_class_subsets TopSpace;
let c₂ be 3rd_class Subset of c₁;
cluster a₂ ` -> non 1st_class non 2nd_class 3rd_class ;
coherence by Th50;

end;

theorem Th51: :: ISOMICHI:51

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is 1st_class holds
( Int (Cl b₂) = Int (Cl (Int b₂)) & Cl (Int b₂) = Cl (Int (Cl b₂)) )

proof end;

theorem Th52: :: ISOMICHI:52

for b₁ being TopSpace
for b₂ being Subset of b₁ st ( Int (Cl b₂) = Int (Cl (Int b₂)) or Cl (Int b₂) = Cl (Int (Cl b₂)) ) holds
b₂ is 1st_class

proof end;

theorem Th53: :: ISOMICHI:53

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is 1st_class & b₃ is 1st_class holds
( (Int (Cl b₂)) /\ (Int (Cl b₃)) = Int (Cl (b₂ /\ b₃)) & (Cl (Int b₂)) \/ (Cl (Int b₃)) = Cl (Int (b₂ \/ b₃)) )

proof end;

theorem Th54: :: ISOMICHI:54

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is 1st_class & b₃ is 1st_class holds
( b₂ \/ b₃ is 1st_class & b₂ /\ b₃ is 1st_class )

proof end;