:: TEX_1 semantic presentation

theorem Th1: :: TEX_1:1

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Subset of (b₁ modified_with_respect_to b₂) st b₃ = b₄ & b₃ is open holds
b₄ is open

proof end;

theorem Th2: :: TEX_1:2

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being Subset of (b₁ modified_with_respect_to b₂) st b₃ = b₄ & b₃ is closed holds
b₄ is closed

proof end;

theorem Th3: :: TEX_1:3

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ modified_with_respect_to (b₂ ` )) st b₃ = b₂ holds
b₃ is closed

proof end;

theorem Th4: :: TEX_1:4

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ modified_with_respect_to b₂) st b₃ = b₂ & b₂ is dense holds
( b₃ is dense & b₃ is open )

proof end;

theorem Th5: :: TEX_1:5

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ modified_with_respect_to b₂) st b₂ c= b₃ & b₂ is dense holds
b₃ is everywhere_dense

proof end;

theorem Th6: :: TEX_1:6

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ modified_with_respect_to (b₂ ` )) st b₃ = b₂ & b₂ is boundary holds
( b₃ is boundary & b₃ is closed )

proof end;

theorem Th7: :: TEX_1:7

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ modified_with_respect_to (b₂ ` )) st b₃ c= b₂ & b₂ is boundary holds
b₃ is nowhere_dense

proof end;

Lemma7: for b₁, b₂ being set holds
( b₁ c= b₂ iff b₁ is Subset of b₂ )
;

definition

let c₁ be non empty 1-sorted ;
redefine attr a₁ is trivial means :Def1: :: TEX_1:def 1
ex b₁ being Element of a₁ st the carrier of a₁ = {b₁};
compatibility

proof end;

end;

:: deftheorem Def1 defines trivial TEX_1:def 1 :

registration

let c₁ be non empty set ;
cluster 1-sorted(# a₁ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster strict non empty trivial 1-sorted ;
existence

proof end;

cluster strict non empty non trivial 1-sorted ;
existence

proof end;

end;

registration

cluster non empty trivial strict TopStruct ;
existence

proof end;

cluster non empty non trivial strict TopStruct ;
existence

proof end;

end;

theorem Th8: :: TEX_1:8

for b₁ being non empty trivial TopStruct st not the topology of b₁ is empty & b₁ is almost_discrete holds
b₁ is TopSpace-like

proof end;

registration

cluster non empty trivial strict TopStruct ;
existence

proof end;

end;

registration

cluster non empty trivial -> non empty discrete anti-discrete TopStruct ;
coherence

proof end;

cluster non empty discrete anti-discrete -> non empty trivial TopStruct ;
coherence

proof end;

end;

registration

cluster non empty non trivial strict TopStruct ;
existence

proof end;

end;

registration

cluster non empty non discrete -> non empty non trivial TopStruct ;
coherence

proof end;

cluster non empty non anti-discrete -> non empty non trivial TopStruct ;
coherence

proof end;

end;

definition

let c₁ be set ;
func cobool c₁ -> Subset-Family of a₁ equals :: TEX_1:def 2
{{} ,a₁};
coherence

proof end;

end;

:: deftheorem Def2 defines cobool TEX_1:def 2 :

registration

let c₁ be set ;
cluster cobool a₁ -> non empty ;
coherence ;

end;

definition

let c₁ be set ;
func ADTS c₁ -> TopStruct equals :: TEX_1:def 3
TopStruct(# a₁,(cobool a₁) #);
coherence ;

end;

:: deftheorem Def3 defines ADTS TEX_1:def 3 :

registration

let c₁ be set ;
cluster ADTS a₁ -> strict TopSpace-like anti-discrete ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster ADTS a₁ -> non empty strict TopSpace-like anti-discrete ;
coherence ;

end;

theorem Th9: :: TEX_1:9

for b₁ being non empty anti-discrete TopSpace holds TopStruct(# the carrier of b₁,the topology of b₁ #) = ADTS the carrier of b₁ by TDLAT_3:def 2;

theorem Th10: :: TEX_1:10

for b₁ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of (ADTS the carrier of b₁),the topology of (ADTS the carrier of b₁) #) holds
b₁ is anti-discrete by TDLAT_3:def 2;

theorem Th11: :: TEX_1:11

for b₁ being non empty anti-discrete TopSpace
for b₂ being Subset of b₁ holds
( ( b₂ is empty implies Cl b₂ = {} ) & ( not b₂ is empty implies Cl b₂ = the carrier of b₁ ) )

proof end;

theorem Th12: :: TEX_1:12

for b₁ being non empty anti-discrete TopSpace
for b₂ being Subset of b₁ holds
( ( b₂ <> the carrier of b₁ implies Int b₂ = {} ) & ( b₂ = the carrier of b₁ implies Int b₂ = the carrier of b₁ ) )

proof end;

theorem Th13: :: TEX_1:13

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁ st not b₂ is empty holds
Cl b₂ = the carrier of b₁ ) holds
b₁ is anti-discrete

proof end;

theorem Th14: :: TEX_1:14

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁ st b₂ <> the carrier of b₁ holds
Int b₂ = {} ) holds
b₁ is anti-discrete

proof end;

theorem Th15: :: TEX_1:15

for b₁ being non empty anti-discrete TopSpace
for b₂ being Subset of b₁ holds
( ( b₂ <> {} implies b₂ is dense ) & ( b₂ <> the carrier of b₁ implies b₂ is boundary ) )

proof end;

theorem Th16: :: TEX_1:16

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁ st b₂ <> {} holds
b₂ is dense ) holds
b₁ is anti-discrete

proof end;

theorem Th17: :: TEX_1:17

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁ st b₂ <> the carrier of b₁ holds
b₂ is boundary ) holds
b₁ is anti-discrete

proof end;

registration

let c₁ be set ;
cluster 1TopSp a₁ -> discrete ;
coherence

proof end;

end;

theorem Th18: :: TEX_1:18

for b₁ being non empty discrete TopSpace holds TopStruct(# the carrier of b₁,the topology of b₁ #) = 1TopSp the carrier of b₁

proof end;

theorem Th19: :: TEX_1:19

for b₁ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of (1TopSp the carrier of b₁),the topology of (1TopSp the carrier of b₁) #) holds
b₁ is discrete

proof end;

theorem Th20: :: TEX_1:20

for b₁ being non empty discrete TopSpace
for b₂ being Subset of b₁ holds
( Cl b₂ = b₂ & Int b₂ = b₂ )

proof end;

theorem Th21: :: TEX_1:21

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁ holds Cl b₂ = b₂ ) holds
b₁ is discrete

proof end;

theorem Th22: :: TEX_1:22

for b₁ being non empty TopSpace st ( for b₂ being Subset of b₁ holds Int b₂ = b₂ ) holds
b₁ is discrete

proof end;

theorem Th23: :: TEX_1:23

for b₁ being non empty set holds
( ADTS b₁ = 1TopSp b₁ iff ex b₂ being Element of b₁ st b₁ = {b₂} )

proof end;

registration

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

proof end;

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

proof end;

end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
let c₃ be set ;
redefine func \ as c₂ \ c₃ -> Subset-Family of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Element of c₁;
canceled;
func STS c₁,c₂ -> TopStruct equals :: TEX_1:def 5
TopStruct(# a₁,((bool a₁) \ { b₁ where B is Subset of a₁ : ( a₂ in b₁ & b₁ <> a₁ ) } ) #);
coherence ;

end;

:: deftheorem Def4 TEX_1:def 4 :

:: deftheorem Def5 defines STS TEX_1:def 5 :

registration

let c₁ be set ;
let c₂ be Element of c₁;
cluster STS a₁,a₂ -> strict TopSpace-like ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
cluster STS a₁,a₂ -> non empty strict TopSpace-like ;
coherence ;

end;

theorem Th24: :: TEX_1:24

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Subset of (STS b₁,b₂) holds
( ( {b₂} c= b₃ implies b₃ is closed ) & ( not b₃ is empty & b₃ is closed implies {b₂} c= b₃ ) )

proof end;

theorem Th25: :: TEX_1:25

for b₁ being non empty set
for b₂ being Element of b₁ st not b₁ \ {b₂} is empty holds
for b₃ being Subset of (STS b₁,b₂) holds
( ( b₃ = {b₂} implies ( b₃ is closed & b₃ is boundary ) ) & ( not b₃ is empty & b₃ is closed & b₃ is boundary implies b₃ = {b₂} ) )

proof end;

theorem Th26: :: TEX_1:26

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Subset of (STS b₁,b₂) holds
( ( b₃ c= b₁ \ {b₂} implies b₃ is open ) & ( b₃ <> b₁ & b₃ is open implies b₃ c= b₁ \ {b₂} ) )

proof end;

theorem Th27: :: TEX_1:27

for b₁ being non empty set
for b₂ being Element of b₁ st not b₁ \ {b₂} is empty holds
for b₃ being Subset of (STS b₁,b₂) holds
( ( b₃ = b₁ \ {b₂} implies ( b₃ is open & b₃ is dense ) ) & ( b₃ <> b₁ & b₃ is open & b₃ is dense implies b₃ = b₁ \ {b₂} ) )

proof end;

registration

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

proof end;

end;

theorem Th28: :: TEX_1:28

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty TopSpace holds
( TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of (STS b₁,b₂),the topology of (STS b₁,b₂) #) iff ( the carrier of b₃ = b₁ & ( for b₄ being Subset of b₃ holds
( ( {b₂} c= b₄ implies b₄ is closed ) & ( not b₄ is empty & b₄ is closed implies {b₂} c= b₄ ) ) ) ) )

proof end;

theorem Th29: :: TEX_1:29

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty TopSpace holds
( TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of (STS b₁,b₂),the topology of (STS b₁,b₂) #) iff ( the carrier of b₃ = b₁ & ( for b₄ being Subset of b₃ holds
( ( b₄ c= b₁ \ {b₂} implies b₄ is open ) & ( b₄ <> b₁ & b₄ is open implies b₄ c= b₁ \ {b₂} ) ) ) ) )

proof end;

theorem Th30: :: TEX_1:30

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty TopSpace holds
( TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of (STS b₁,b₂),the topology of (STS b₁,b₂) #) iff ( the carrier of b₃ = b₁ & ( for b₄ being non empty Subset of b₃ holds Cl b₄ = b₄ \/ {b₂} ) ) )

proof end;

theorem Th31: :: TEX_1:31

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty TopSpace holds
( TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of (STS b₁,b₂),the topology of (STS b₁,b₂) #) iff ( the carrier of b₃ = b₁ & ( for b₄ being Subset of b₃ st b₄ <> b₁ holds
Int b₄ = b₄ \ {b₂} ) ) )

proof end;

E21: now

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be set ;
assume E22: c₃ = { b₁ where B is Subset of c₁ : ( c₂ in b₁ & b₁ <> c₁ ) } ;
assume E23: c₁ = {c₂} ;
assume E24: c₃ <> {} ;
consider c₄ being Element of c₃;
c₄ in c₃ by E24;
then consider c₅ being Subset of c₁ such that
c₄ = c₅ and
E25: c₂ in c₅ and
E26: c₅ <> c₁ by E22;

E27: now

assume c₁ \ c₅ = {} ;
then c₁ c= c₅ by XBOOLE_1:37;
hence contradiction by E26, XBOOLE_0:def 10;

end;

consider c₆ being Element of c₁ \ c₅;
reconsider c₇ = c₆ as Element of c₁ by E27, XBOOLE_0:def 4;
c₂ <> c₇ by E25, E27, XBOOLE_0:def 4;
hence contradiction by E23, TARSKI:def 1;

end;

theorem Th32: :: TEX_1:32

for b₁ being non empty set
for b₂ being Element of b₁ holds
( STS b₁,b₂ = ADTS b₁ iff b₁ = {b₂} )

proof end;

theorem Th33: :: TEX_1:33

for b₁ being non empty set
for b₂ being Element of b₁ holds
( STS b₁,b₂ = 1TopSp b₁ iff b₁ = {b₂} )

proof end;

theorem Th34: :: TEX_1:34

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Subset of (STS b₁,b₂) st b₃ = {b₂} holds
1TopSp b₁ = (STS b₁,b₂) modified_with_respect_to b₃

proof end;

definition

let c₁ be non empty TopSpace;
redefine attr a₁ is discrete means :Def6: :: TEX_1:def 6
for b₁ being non empty Subset of a₁ holds not b₁ is boundary;
compatibility

proof end;

end;

:: deftheorem Def6 defines discrete TEX_1:def 6 :

theorem Th35: :: TEX_1:35

for b₁ being non empty TopSpace holds
( b₁ is discrete iff for b₂ being Subset of b₁ st b₂ <> the carrier of b₁ holds
not b₂ is dense )

proof end;

registration

cluster non empty non almost_discrete -> non empty non trivial non discrete non anti-discrete TopStruct ;
coherence

proof end;

end;

definition

let c₁ be non empty TopSpace;
redefine attr a₁ is almost_discrete means :Def7: :: TEX_1:def 7
for b₁ being non empty Subset of a₁ holds not b₁ is nowhere_dense;
compatibility

proof end;

end;

:: deftheorem Def7 defines almost_discrete TEX_1:def 7 :

theorem Th36: :: TEX_1:36

for b₁ being non empty TopSpace holds
( b₁ is almost_discrete iff for b₂ being Subset of b₁ st b₂ <> the carrier of b₁ holds
not b₂ is everywhere_dense )

proof end;

theorem Th37: :: TEX_1:37

for b₁ being non empty TopSpace holds
( not b₁ is almost_discrete iff ex b₂ being non empty Subset of b₁ st
( b₂ is boundary & b₂ is closed ) )

proof end;

theorem Th38: :: TEX_1:38

for b₁ being non empty TopSpace holds
( not b₁ is almost_discrete iff ex b₂ being Subset of b₁ st
( b₂ <> the carrier of b₁ & b₂ is dense & b₂ is open ) )

proof end;

registration

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

proof end;

end;

theorem Th39: :: TEX_1:39

for b₁ being non empty set
for b₂ being Element of b₁ holds
( not b₁ \ {b₂} is empty iff not STS b₁,b₂ is almost_discrete )

proof end;

registration

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

proof end;

end;

theorem Th40: :: TEX_1:40

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is boundary holds
not b₁ modified_with_respect_to (b₂ ` ) is almost_discrete

proof end;

theorem Th41: :: TEX_1:41

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ <> the carrier of b₁ & b₂ is dense holds
not b₁ modified_with_respect_to b₂ is almost_discrete

proof end;