:: TOPGEN_2 semantic presentation

theorem Th1: :: TOPGEN_2:1

for b₁ being non empty TopSpace
for b₂ being Basis of b₁
for b₃ being Element of b₁ holds { b₄ where B is Subset of b₁ : ( b₃ in b₄ & b₄ in b₂ ) } is Basis of b₃

proof end;

theorem Th2: :: TOPGEN_2:2

for b₁ being non empty TopSpace
for b₂ being ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is Basis of b₃ ) holds
Union b₂ is Basis of b₁

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Element of c₁;
func Chi c₂,c₁ -> cardinal number means :Def1: :: TOPGEN_2:def 1
( ex b₁ being Basis of a₂ st a₃ = Card b₁ & ( for b₁ being Basis of a₂ holds a₃ <=` Card b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Chi TOPGEN_2:def 1 :

theorem Th3: :: TOPGEN_2:3

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is cardinal number ) holds
union b₁ is cardinal number

proof end;

E5: now

let c₁ be non empty TopStruct ;
set c₂ = { (Chi b₁,c₁) where B is Point of c₁ : verum } ;

now

let c₃ be set ;
assume c₃ in { (Chi b₁,c₁) where B is Point of c₁ : verum } ;
then ex b₁ being Point of c₁ st c₃ = Chi b₁,c₁ ;
hence c₃ is cardinal number ;

end;

hence union { (Chi b₁,c₁) where B is Point of c₁ : verum } is cardinal number by Th3;
let c₃ be cardinal number ;
assume E6: c₃ = union { (Chi b₁,c₁) where B is Point of c₁ : verum } ;

hereby

let c₄ be Point of c₁;
Chi c₄,c₁ in { (Chi b₁,c₁) where B is Point of c₁ : verum } ;
hence Chi c₄,c₁ <=` c₃ by E6, ZFMISC_1:92;

end;

let c₄ be cardinal number ;
assume E7: for b₁ being Point of c₁ holds Chi b₁,c₁ <=` c₄ ;

now

let c₅ be set ;
assume c₅ in { (Chi b₁,c₁) where B is Point of c₁ : verum } ;
then ex b₁ being Point of c₁ st c₅ = Chi b₁,c₁ ;
hence c₅ c= c₄ by E7;

end;

hence c₃ <=` c₄ by E6, ZFMISC_1:94;

end;

definition

let c₁ be non empty TopStruct ;
func Chi c₁ -> cardinal number means :Def2: :: TOPGEN_2:def 2
( ( for b₁ being Point of a₁ holds Chi b₁,a₁ <=` a₂ ) & ( for b₁ being cardinal number st ( for b₂ being Point of a₁ holds Chi b₂,a₁ <=` b₁ ) holds
a₂ <=` b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Chi TOPGEN_2:def 2 :

theorem Th4: :: TOPGEN_2:4

for b₁ being non empty TopStruct holds Chi b₁ = union { (Chi b₂,b₁) where B is Point of b₁ : verum }

proof end;

theorem Th5: :: TOPGEN_2:5

for b₁ being non empty TopStruct
for b₂ being Point of b₁ holds Chi b₂,b₁ <=` Chi b₁

proof end;

theorem Th6: :: TOPGEN_2:6

for b₁ being non empty TopSpace holds
( b₁ is first-countable iff Chi b₁ <=` alef 0 )

proof end;

definition

let c₁ be non empty TopSpace;
mode Neighborhood_System of c₁ -> ManySortedSet of a₁ means :Def3: :: TOPGEN_2:def 3
for b₁ being Element of a₁ holds a₂ . b₁ is Basis of b₁;
existence

proof end;

end;

:: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def 3 :

definition

let c₁ be non empty TopSpace;
let c₂ be Neighborhood_System of c₁;
redefine func Union as Union c₂ -> Basis of a₁;
coherence

proof end;

let c₃ be Point of c₁;
redefine func . as c₂ . c₃ -> Basis of a₃;
coherence by Def3;

end;

theorem Th7: :: TOPGEN_2:7

canceled;

theorem Th8: :: TOPGEN_2:8

for b₁ being non empty TopSpace
for b₂, b₃ being Point of b₁
for b₄ being Basis of b₂
for b₅ being Basis of b₃
for b₆ being set st b₂ in b₆ & b₆ in b₅ holds
ex b₇ being open Subset of b₁ st
( b₇ in b₄ & b₇ c= b₆ )

proof end;

theorem Th9: :: TOPGEN_2:9

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Basis of b₂
for b₄, b₅ being set st b₄ in b₃ & b₅ in b₃ holds
ex b₆ being open Subset of b₁ st
( b₆ in b₃ & b₆ c= b₄ /\ b₅ )

proof end;

E10: now

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
let c₃ be Element of c₁;
assume E11: c₃ in Cl c₂ ;
let c₄ be Basis of c₃;
let c₅ be set ;
assume c₅ in c₄ ;
then E12: ( c₃ in c₅ & c₅ is open Subset of c₁ ) by YELLOW_8:21;
then c₅ meets Cl c₂ by E11, XBOOLE_0:3;
hence c₅ meets c₂ by E12, TSEP_1:40;

end;

E11: now

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
let c₃ be Element of c₁;
given c₄ being Basis of c₃ such that E12: for b₁ being set st b₁ in c₄ holds
b₁ meets c₂ ;

now

let c₅ be Subset of c₁;
assume ( c₅ is open & c₃ in c₅ ) ;
then consider c₆ being Subset of c₁ such that
E13: ( c₆ in c₄ & c₆ c= c₅ ) by YELLOW_8:def 2;
c₆ meets c₂ by E12, E13;
hence c₂ meets c₅ by E13, XBOOLE_1:63;

end;

hence c₃ in Cl c₂ by PRE_TOPC:def 13;

end;

theorem Th10: :: TOPGEN_2:10

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in Cl b₂ iff for b₄ being Basis of b₃
for b₅ being set st b₅ in b₄ holds
b₅ meets b₂ )

proof end;

theorem Th11: :: TOPGEN_2:11

for b₁ being non empty TopSpace
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in Cl b₂ iff ex b₄ being Basis of b₃ st
for b₅ being set st b₅ in b₄ holds
b₅ meets b₂ )

proof end;

registration

let c₁ be TopSpace;
cluster non empty open Element of K10(K10(the carrier of a₁));
existence

proof end;

end;

theorem Th12: :: TOPGEN_2:12

for b₁ being non empty TopSpace
for b₂ being open Subset-Family of b₁ ex b₃ being open Subset-Family of b₁ st
( b₃ c= b₂ & union b₃ = union b₂ & Card b₃ <=` weight b₁ )

proof end;

definition

let c₁ be TopStruct ;
attr a₁ is finite-weight means :Def4: :: TOPGEN_2:def 4
weight a₁ is finite;

end;

:: deftheorem Def4 defines finite-weight TOPGEN_2:def 4 :

notation

let c₁ be TopStruct ;
antonym infinite-weight c₁ for finite-weight c₁;

end;

registration

cluster finite -> finite-weight TopStruct ;
coherence

proof end;

cluster infinite-weight -> infinite TopStruct ;
coherence

proof end;

end;

registration

cluster non empty finite finite-weight TopStruct ;
existence

proof end;

end;

theorem Th13: :: TOPGEN_2:13

for b₁ being set holds Card (SmallestPartition b₁) = Card b₁

proof end;

theorem Th14: :: TOPGEN_2:14

for b₁ being non empty discrete TopStruct holds
( SmallestPartition the carrier of b₁ is Basis of b₁ & ( for b₂ being Basis of b₁ holds SmallestPartition the carrier of b₁ c= b₂ ) )

proof end;

theorem Th15: :: TOPGEN_2:15

for b₁ being non empty discrete TopStruct holds weight b₁ = Card the carrier of b₁

proof end;

registration

cluster infinite infinite-weight TopStruct ;
existence

proof end;

end;

Lemma17: for b₁ being infinite-weight TopSpace
for b₂ being Basis of b₁ ex b₃ being Basis of b₁ st
( b₃ c= b₂ & Card b₃ = weight b₁ )

proof end;

theorem Th16: :: TOPGEN_2:16

canceled;

theorem Th17: :: TOPGEN_2:17

for b₁ being non empty finite-weight TopSpace ex b₂ being Basis of b₁ex b₃ being Function of the carrier of b₁,the topology of b₁ st
( b₂ = rng b₃ & ( for b₄ being Point of b₁ holds
( b₄ in b₃ . b₄ & ( for b₅ being open Subset of b₁ st b₄ in b₅ holds
b₃ . b₄ c= b₅ ) ) ) )

proof end;

theorem Th18: :: TOPGEN_2:18

for b₁ being TopSpace
for b₂, b₃ being Basis of b₁
for b₄ being Function of the carrier of b₁,the topology of b₁ st b₂ = rng b₄ & ( for b₅ being Point of b₁ holds
( b₅ in b₄ . b₅ & ( for b₆ being open Subset of b₁ st b₅ in b₆ holds
b₄ . b₅ c= b₆ ) ) ) holds
b₂ c= b₃

proof end;

theorem Th19: :: TOPGEN_2:19

for b₁ being TopSpace
for b₂ being Basis of b₁
for b₃ being Function of the carrier of b₁,the topology of b₁ st b₂ = rng b₃ & ( for b₄ being Point of b₁ holds
( b₄ in b₃ . b₄ & ( for b₅ being open Subset of b₁ st b₄ in b₅ holds
b₃ . b₄ c= b₅ ) ) ) holds
weight b₁ = Card b₂

proof end;

Lemma21: for b₁ being non empty finite-weight TopSpace
for b₂ being Basis of b₁ ex b₃ being Basis of b₁ st
( b₃ c= b₂ & Card b₃ = weight b₁ )

proof end;

theorem Th20: :: TOPGEN_2:20

for b₁ being non empty TopSpace
for b₂ being Basis of b₁ ex b₃ being Basis of b₁ st
( b₃ c= b₂ & Card b₃ = weight b₁ )

proof end;

definition

let c₁, c₂ be set ;
func DiscrWithInfin c₁,c₂ -> strict TopStruct means :Def5: :: TOPGEN_2:def 5
( the carrier of a₃ = a₁ & the topology of a₃ = { b₁ where B is Subset of a₁ : not a₂ in b₁ } \/ { (b₁ ` ) where B is Subset of a₁ : b₁ is finite } );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def 5 :

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th21: :: TOPGEN_2:21

for b₁, b₂ being set
for b₃ being Subset of (DiscrWithInfin b₁,b₂) holds
( b₃ is open iff ( not b₂ in b₃ or b₃ ` is finite ) )

proof end;

theorem Th22: :: TOPGEN_2:22

for b₁, b₂ being set
for b₃ being Subset of (DiscrWithInfin b₁,b₂) holds
( b₃ is closed iff not ( b₂ in b₁ & not b₂ in b₃ & not b₃ is finite ) )

proof end;

theorem Th23: :: TOPGEN_2:23

for b₁, b₂, b₃ being set st b₃ in b₁ holds
{b₃} is closed Subset of (DiscrWithInfin b₁,b₂)

proof end;

theorem Th24: :: TOPGEN_2:24

for b₁, b₂, b₃ being set st b₃ in b₁ & b₃ <> b₂ holds
{b₃} is open Subset of (DiscrWithInfin b₁,b₂)

proof end;

theorem Th25: :: TOPGEN_2:25

for b₁, b₂ being set st not b₁ is finite holds
for b₃ being Subset of (DiscrWithInfin b₁,b₂) st b₃ = {b₂} holds
not b₃ is open

proof end;

theorem Th26: :: TOPGEN_2:26

for b₁, b₂ being set
for b₃ being Subset of (DiscrWithInfin b₁,b₂) st b₃ is finite holds
Cl b₃ = b₃

proof end;

theorem Th27: :: TOPGEN_2:27

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st not b₂ is closed holds
for b₃ being Point of b₁ st b₂ \/ {b₃} is closed holds
Cl b₂ = b₂ \/ {b₃}

proof end;

theorem Th28: :: TOPGEN_2:28

for b₁, b₂ being set st b₂ in b₁ holds
for b₃ being Subset of (DiscrWithInfin b₁,b₂) st not b₃ is finite holds
Cl b₃ = b₃ \/ {b₂}

proof end;

theorem Th29: :: TOPGEN_2:29

for b₁, b₂ being set
for b₃ being Subset of (DiscrWithInfin b₁,b₂) st b₃ ` is finite holds
Int b₃ = b₃

proof end;

theorem Th30: :: TOPGEN_2:30

for b₁, b₂ being set st b₂ in b₁ holds
for b₃ being Subset of (DiscrWithInfin b₁,b₂) st not b₃ ` is finite holds
Int b₃ = b₃ \ {b₂}

proof end;

theorem Th31: :: TOPGEN_2:31

for b₁, b₂ being set ex b₃ being Basis of DiscrWithInfin b₁,b₂ st b₃ = ((SmallestPartition b₁) \ {{b₂}}) \/ { (b₄ ` ) where B is Subset of b₁ : b₄ is finite }

proof end;

theorem Th32: :: TOPGEN_2:32

for b₁ being infinite set holds Card (Fin b₁) = Card b₁

proof end;

theorem Th33: :: TOPGEN_2:33

for b₁ being infinite set holds Card { (b₂ ` ) where B is Subset of b₁ : b₂ is finite } = Card b₁

proof end;

theorem Th34: :: TOPGEN_2:34

for b₁ being infinite set
for b₂ being set
for b₃ being Basis of DiscrWithInfin b₁,b₂ st b₃ = ((SmallestPartition b₁) \ {{b₂}}) \/ { (b₄ ` ) where B is Subset of b₁ : b₄ is finite } holds
Card b₃ = Card b₁

proof end;

theorem Th35: :: TOPGEN_2:35

for b₁ being infinite set
for b₂ being set
for b₃ being Basis of DiscrWithInfin b₁,b₂ holds Card b₁ <=` Card b₃

proof end;

theorem Th36: :: TOPGEN_2:36

for b₁ being infinite set
for b₂ being set holds weight (DiscrWithInfin b₁,b₂) = Card b₁

proof end;

theorem Th37: :: TOPGEN_2:37

for b₁ being non empty set
for b₂ being set ex b₃ being prebasis of DiscrWithInfin b₁,b₂ st b₃ = ((SmallestPartition b₁) \ {{b₂}}) \/ { ({b₄} ` ) where B is Element of b₁ : verum }

proof end;

theorem Th38: :: TOPGEN_2:38

for b₁ being TopSpace
for b₂ being Subset-Family of b₁
for b₃ being non empty Subset-Family of b₂ st ( for b₄ being set st b₄ in b₃ holds
b₂ \ b₄ is finite ) holds
Cl (union b₂) = (union (clf b₂)) \/ (meet { (Cl (union b₄)) where B is Subset-Family of b₁ : b₄ in b₃ } )

proof end;

theorem Th39: :: TOPGEN_2:39

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ holds Cl (union b₂) = (union (clf b₂)) \/ (meet { (Cl (union b₃)) where B is Subset-Family of b₁ : ( b₃ c= b₂ & b₂ \ b₃ is finite ) } )

proof end;

theorem Th40: :: TOPGEN_2:40

for b₁ being set
for b₂ being Subset-Family of (bool b₁) st ( for b₃ being Subset-Family of b₁ st b₃ in b₂ holds
TopStruct(# b₁,b₃ #) is TopSpace ) holds
ex b₃ being Subset-Family of b₁ st
( b₃ = Intersect b₂ & TopStruct(# b₁,b₃ #) is TopSpace & ( for b₄ being Subset-Family of b₁ st b₄ in b₂ holds
TopStruct(# b₁,b₄ #) is TopExtension of TopStruct(# b₁,b₃ #) ) & ( for b₄ being TopSpace st the carrier of b₄ = b₁ & ( for b₅ being Subset-Family of b₁ st b₅ in b₂ holds
TopStruct(# b₁,b₅ #) is TopExtension of b₄ ) holds
TopStruct(# b₁,b₃ #) is TopExtension of b₄ ) )

proof end;

theorem Th41: :: TOPGEN_2:41

for b₁ being set
for b₂ being Subset-Family of (bool b₁) ex b₃ being Subset-Family of b₁ st
( b₃ = UniCl (FinMeetCl (union b₂)) & TopStruct(# b₁,b₃ #) is TopSpace & ( for b₄ being Subset-Family of b₁ st b₄ in b₂ holds
TopStruct(# b₁,b₃ #) is TopExtension of TopStruct(# b₁,b₄ #) ) & ( for b₄ being TopSpace st the carrier of b₄ = b₁ & ( for b₅ being Subset-Family of b₁ st b₅ in b₂ holds
b₄ is TopExtension of TopStruct(# b₁,b₅ #) ) holds
b₄ is TopExtension of TopStruct(# b₁,b₃ #) ) )

proof end;