:: TOPGEN_3 semantic presentation

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
attr a₂ is point-filtered means :Def1: :: TOPGEN_3:def 1
for b₁, b₂, b₃ being set st b₂ in a₂ & b₃ in a₂ & b₁ in b₂ /\ b₃ holds
ex b₄ being Subset of a₁ st
( b₄ in a₂ & b₁ in b₄ & b₄ c= b₂ /\ b₃ );

end;

:: deftheorem Def1 defines point-filtered TOPGEN_3:def 1 :

theorem Th1: :: TOPGEN_3:1

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ is covering iff for b₃ being set st b₃ in b₁ holds
ex b₄ being Subset of b₁ st
( b₄ in b₂ & b₃ in b₄ ) )

proof end;

theorem Th2: :: TOPGEN_3:2

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ is point-filtered & b₂ is covering holds
for b₃ being TopStruct st the carrier of b₃ = b₁ & the topology of b₃ = UniCl b₂ holds
( b₃ is TopSpace & b₂ is Basis of b₃ )

proof end;

theorem Th3: :: TOPGEN_3:3

for b₁ being set
for b₂ being V7 ManySortedSet of b₁ st rng b₂ c= bool (bool b₁) & ( for b₃, b₄ being set st b₃ in b₁ & b₄ in b₂ . b₃ holds
b₃ in b₄ ) & ( for b₃, b₄, b₅ being set st b₃ in b₅ & b₅ in b₂ . b₄ & b₄ in b₁ holds
ex b₆ being set st
( b₆ in b₂ . b₃ & b₆ c= b₅ ) ) & ( for b₃, b₄, b₅ being set st b₃ in b₁ & b₄ in b₂ . b₃ & b₅ in b₂ . b₃ holds
ex b₆ being set st
( b₆ in b₂ . b₃ & b₆ c= b₄ /\ b₅ ) ) holds
ex b₃ being Subset-Family of b₁ st
( b₃ = Union b₂ & ( for b₄ being TopStruct st the carrier of b₄ = b₁ & the topology of b₄ = UniCl b₃ holds
( b₄ is TopSpace & ( for b₅ being non empty TopSpace st b₅ = b₄ holds
b₂ is Neighborhood_System of b₅ ) ) ) )

proof end;

theorem Th4: :: TOPGEN_3:4

for b₁ being set
for b₂ being Subset-Family of b₁ st {} in b₂ & b₁ in b₂ & ( for b₃, b₄ being set st b₃ in b₂ & b₄ in b₂ holds
b₃ \/ b₄ in b₂ ) & ( for b₃ being Subset-Family of b₁ st b₃ c= b₂ holds
Intersect b₃ in b₂ ) holds
for b₃ being TopStruct st the carrier of b₃ = b₁ & the topology of b₃ = COMPLEMENT b₂ holds
( b₃ is TopSpace & ( for b₄ being Subset of b₃ holds
( b₄ is closed iff b₄ in b₂ ) ) )

proof end;

scheme :: TOPGEN_3:sch 1
s1{ F₁() -> set , P₁[ set ] } :

ex b₁ being strict TopSpace st
( the carrier of b₁ = F₁() & ( for b₂ being Subset of b₁ holds
( b₂ is closed iff P₁[b₂] ) ) )

provided

E5: ( P₁[ {} ] & P₁[F₁()] ) and
E6: for b₁, b₂ being set st P₁[b₁] & P₁[b₂] holds
P₁[b₁ \/ b₂] and
E7: for b₁ being Subset-Family of F₁() st ( for b₂ being set st b₂ in b₁ holds
P₁[b₂] ) holds
P₁[ Intersect b₁]

proof end;

Lemma5: for b₁, b₂ being TopSpace st ( for b₃ being set holds
( b₃ is open Subset of b₁ iff b₃ is open Subset of b₂ ) ) holds
( the carrier of b₁ = the carrier of b₂ & the topology of b₁ c= the topology of b₂ )

proof end;

theorem Th5: :: TOPGEN_3:5

for b₁, b₂ being TopSpace st ( for b₃ being set holds
( b₃ is open Subset of b₁ iff b₃ is open Subset of b₂ ) ) holds
TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #)

proof end;

Lemma6: for b₁, b₂ being TopSpace st ( for b₃ being set holds
( b₃ is closed Subset of b₁ iff b₃ is closed Subset of b₂ ) ) holds
( the carrier of b₁ = the carrier of b₂ & the topology of b₁ c= the topology of b₂ )

proof end;

theorem Th6: :: TOPGEN_3:6

for b₁, b₂ being TopSpace st ( for b₃ being set holds
( b₃ is closed Subset of b₁ iff b₃ is closed Subset of b₂ ) ) holds
TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #)

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Subset of [:c₁,(bool c₂):];
redefine func rng as rng c₃ -> Subset-Family of a₂;
coherence

proof end;

end;

theorem Th7: :: TOPGEN_3:7

for b₁ being set
for b₂ being Function of bool b₁, bool b₁ st b₂ . {} = {} & ( for b₃ being Subset of b₁ holds b₃ c= b₂ . b₃ ) & ( for b₃, b₄ being Subset of b₁ holds b₂ . (b₃ \/ b₄) = (b₂ . b₃) \/ (b₂ . b₄) ) & ( for b₃ being Subset of b₁ holds b₂ . (b₂ . b₃) = b₂ . b₃ ) holds
for b₃ being TopStruct st the carrier of b₃ = b₁ & the topology of b₃ = COMPLEMENT (rng b₂) holds
( b₃ is TopSpace & ( for b₄ being Subset of b₃ holds Cl b₄ = b₂ . b₄ ) )

proof end;

scheme :: TOPGEN_3:sch 2
s2{ F₁() -> set , F₂( set ) -> set } :

ex b₁ being strict TopSpace st
( the carrier of b₁ = F₁() & ( for b₂ being Subset of b₁ holds Cl b₂ = F₂(b₂) ) )

provided

E9: F₂({} ) = {} and
E10: for b₁ being Subset of F₁() holds
( b₁ c= F₂(b₁) & F₂(b₁) c= F₁() ) and
E11: for b₁, b₂ being Subset of F₁() holds F₂((b₁ \/ b₂)) = F₂(b₁) \/ F₂(b₂) and
E12: for b₁ being Subset of F₁() holds F₂(F₂(b₁)) = F₂(b₁)

proof end;

theorem Th8: :: TOPGEN_3:8

for b₁, b₂ being TopSpace st the carrier of b₁ = the carrier of b₂ & ( for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
Cl b₃ = Cl b₄ ) holds
the topology of b₁ = the topology of b₂

proof end;

theorem Th9: :: TOPGEN_3:9

for b₁ being set
for b₂ being Function of bool b₁, bool b₁ st b₂ . b₁ = b₁ & ( for b₃ being Subset of b₁ holds b₂ . b₃ c= b₃ ) & ( for b₃, b₄ being Subset of b₁ holds b₂ . (b₃ /\ b₄) = (b₂ . b₃) /\ (b₂ . b₄) ) & ( for b₃ being Subset of b₁ holds b₂ . (b₂ . b₃) = b₂ . b₃ ) holds
for b₃ being TopStruct st the carrier of b₃ = b₁ & the topology of b₃ = rng b₂ holds
( b₃ is TopSpace & ( for b₄ being Subset of b₃ holds Int b₄ = b₂ . b₄ ) )

proof end;

scheme :: TOPGEN_3:sch 3
s3{ F₁() -> set , F₂( set ) -> set } :

ex b₁ being strict TopSpace st
( the carrier of b₁ = F₁() & ( for b₂ being Subset of b₁ holds Int b₂ = F₂(b₂) ) )

provided

E11: F₂(F₁()) = F₁() and
E12: for b₁ being Subset of F₁() holds F₂(b₁) c= b₁ and
E13: for b₁, b₂ being Subset of F₁() holds F₂((b₁ /\ b₂)) = F₂(b₁) /\ F₂(b₂) and
E14: for b₁ being Subset of F₁() holds F₂(F₂(b₁)) = F₂(b₁)

proof end;

theorem Th10: :: TOPGEN_3:10

for b₁, b₂ being TopSpace st the carrier of b₁ = the carrier of b₂ & ( for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
Int b₃ = Int b₄ ) holds
the topology of b₁ = the topology of b₂

proof end;

definition

func Sorgenfrey-line -> non empty strict TopSpace means :Def2: :: TOPGEN_3:def 2
( the carrier of a₁ = REAL & ex b₁ being Subset-Family of REAL st
( the topology of a₁ = UniCl b₁ & b₁ = { [.b₂,b₃.[ where B is Element of REAL , B is Element of REAL : ( b₂ < b₃ & b₃ is rational ) } ) );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def2 defines Sorgenfrey-line TOPGEN_3:def 2 :

Lemma13: the carrier of Sorgenfrey-line = REAL
by Def2;

consider c₁ being Subset-Family of REAL such that
Lemma14: the topology of Sorgenfrey-line = UniCl c₁ and
Lemma15: c₁ = { [.b₁,b₂.[ where B is Element of REAL , B is Element of REAL : ( b₁ < b₂ & b₂ is rational ) } by Def2;

c₁ c= the topology of Sorgenfrey-line
by Lemma14, CANTOR_1:1;

then Lemma16: c₁ is Basis of Sorgenfrey-line
by Lemma13, Lemma14, CANTOR_1:def 2;

theorem Th11: :: TOPGEN_3:11

for b₁, b₂ being real number holds [.b₁,b₂.[ is open Subset of Sorgenfrey-line

proof end;

theorem Th12: :: TOPGEN_3:12

for b₁, b₂ being real number holds ].b₁,b₂.[ is open Subset of Sorgenfrey-line

proof end;

theorem Th13: :: TOPGEN_3:13

for b₁ being real number holds left_open_halfline b₁ is open Subset of Sorgenfrey-line

proof end;

theorem Th14: :: TOPGEN_3:14

for b₁ being real number holds right_open_halfline b₁ is open Subset of Sorgenfrey-line

proof end;

theorem Th15: :: TOPGEN_3:15

for b₁ being real number holds right_closed_halfline b₁ is open Subset of Sorgenfrey-line

proof end;

theorem Th16: :: TOPGEN_3:16

Card INT = alef 0

proof end;

theorem Th17: :: TOPGEN_3:17

Card RAT = alef 0

proof end;

theorem Th18: :: TOPGEN_3:18

for b₁ being set st b₁ is mutually-disjoint & ( for b₂ being set st b₂ in b₁ holds
ex b₃, b₄ being real number st
( b₃ < b₄ & ].b₃,b₄.[ c= b₂ ) ) holds
b₁ is countable

proof end;

definition

let c₂ be set ;
let c₃ be real number ;
pred c₂ is_local_minimum_of c₁ means :Def3: :: TOPGEN_3:def 3
( a₂ in a₁ & ex b₁ being real number st
( b₁ < a₂ & ].b₁,a₂.[ misses a₁ ) );

end;

:: deftheorem Def3 defines is_local_minimum_of TOPGEN_3:def 3 :

theorem Th19: :: TOPGEN_3:19

for b₁ being Subset of REAL holds { b₂ where B is Element of REAL : b₂ is_local_minimum_of b₁ } is countable

proof end;

registration

cluster INT -> infinite ;
coherence by NUMBERS:17, FINSET_1:13;
cluster RAT -> infinite ;
coherence by NUMBERS:18, FINSET_1:13;
cluster REAL -> infinite ;
coherence

proof end;

let c₂ be infinite set ;
cluster bool a₁ -> infinite ;
coherence by FINSET_1:24;

end;

registration

let c₂ be Aleph;
cluster exp 2,a₁ -> infinite ;
coherence

proof end;

end;

definition

func continuum -> infinite cardinal number equals :: TOPGEN_3:def 4
Card REAL ;
coherence ;

end;

:: deftheorem Def4 defines continuum TOPGEN_3:def 4 :

theorem Th20: :: TOPGEN_3:20

Card { [.b₁,b₂.[ where B is Element of REAL , B is Element of REAL : ( b₁ < b₂ & b₂ is rational ) } = continuum

proof end;

registration

let c₂ be infinite set ;
cluster infinite Element of bool a₁;
existence

proof end;

end;

definition

let c₂ be set ;
let c₃ be real number ;
func c₁ -powers c₂ -> Function of NAT , REAL means :Def5: :: TOPGEN_3:def 5
for b₁ being natural number holds
( ( b₁ in a₁ & a₃ . b₁ = a₂ |^ b₁ ) or ( not b₁ in a₁ & a₃ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :

theorem Th21: :: TOPGEN_3:21

for b₁ being set
for b₂ being real number st 0 < b₂ & b₂ < 1 holds
b₁ -powers b₂ is summable

proof end;

theorem Th22: :: TOPGEN_3:22

for b₁ being real number
for b₂ being Element of NAT st 0 < b₁ & b₁ < 1 holds
Sum ((b₁ GeoSeq ) ^\ b₂) = (b₁ |^ b₂) / (1 - b₁)

proof end;

theorem Th23: :: TOPGEN_3:23

for b₁ being Element of NAT holds Sum (((1 / 2) GeoSeq ) ^\ (b₁ + 1)) = (1 / 2) |^ b₁

proof end;

theorem Th24: :: TOPGEN_3:24

for b₁ being real number
for b₂ being set st 0 < b₁ & b₁ < 1 holds
Sum (b₂ -powers b₁) <= Sum (b₁ GeoSeq )

proof end;

theorem Th25: :: TOPGEN_3:25

for b₁ being set
for b₂ being Element of NAT holds Sum ((b₁ -powers (1 / 2)) ^\ (b₂ + 1)) <= (1 / 2) |^ b₂

proof end;

theorem Th26: :: TOPGEN_3:26

for b₁ being infinite Subset of NAT
for b₂ being natural number holds (Partial_Sums (b₁ -powers (1 / 2))) . b₂ < Sum (b₁ -powers (1 / 2))

proof end;

theorem Th27: :: TOPGEN_3:27

for b₁, b₂ being infinite Subset of NAT st Sum (b₁ -powers (1 / 2)) = Sum (b₂ -powers (1 / 2)) holds
b₁ = b₂

proof end;

theorem Th28: :: TOPGEN_3:28

for b₁ being set st b₁ is countable holds
Fin b₁ is countable

proof end;

theorem Th29: :: TOPGEN_3:29

continuum = exp 2,(alef 0)

proof end;

theorem Th30: :: TOPGEN_3:30

alef 0 <` continuum

proof end;

theorem Th31: :: TOPGEN_3:31

for b₁ being Subset-Family of REAL st Card b₁ <` continuum holds
Card { b₂ where B is Element of REAL : ex b₁ being set st
( b₃ in UniCl b₁ & b₂ is_local_minimum_of b₃ ) } <` continuum

proof end;

theorem Th32: :: TOPGEN_3:32

for b₁ being Subset-Family of REAL st Card b₁ <` continuum holds
ex b₂ being real number ex b₃ being rational number st
( b₂ < b₃ & not [.b₂,b₃.[ in UniCl b₁ )

proof end;

theorem Th33: :: TOPGEN_3:33

weight Sorgenfrey-line = continuum

proof end;

definition

let c₂ be set ;
func ClFinTop c₁ -> strict TopSpace means :Def6: :: TOPGEN_3:def 6
( the carrier of a₂ = a₁ & ( for b₁ being Subset of a₂ holds
( b₁ is closed iff ( b₁ is finite or b₁ = a₁ ) ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def6 defines ClFinTop TOPGEN_3:def 6 :

theorem Th34: :: TOPGEN_3:34

for b₁ being set
for b₂ being Subset of (ClFinTop b₁) holds
( b₂ is open iff ( b₂ = {} or b₂ ` is finite ) )

proof end;

theorem Th35: :: TOPGEN_3:35

for b₁ being infinite set
for b₂ being Subset of b₁ st b₂ is finite holds
not b₂ ` is finite

proof end;

registration

let c₂ be non empty set ;
cluster ClFinTop a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th36: :: TOPGEN_3:36

for b₁ being infinite set
for b₂, b₃ being non empty open Subset of (ClFinTop b₁) holds b₂ meets b₃

proof end;

definition

let c₂, c₃ be set ;
func c₂ -PointClTop c₁ -> strict TopSpace means :Def7: :: TOPGEN_3:def 7
( the carrier of a₃ = a₁ & ( for b₁ being Subset of a₃ holds Cl b₁ = IFEQ b₁,{} ,b₁,(b₁ \/ ({a₂} /\ a₁)) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def7 defines -PointClTop TOPGEN_3:def 7 :

registration

let c₂ be non empty set ;
let c₃ be set ;
cluster a₂ -PointClTop a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th37: :: TOPGEN_3:37

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty Subset of (b₂ -PointClTop b₁) holds Cl b₃ = b₃ \/ {b₂}

proof end;

theorem Th38: :: TOPGEN_3:38

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty Subset of (b₂ -PointClTop b₁) holds
( b₃ is closed iff b₂ in b₃ )

proof end;

registration

let c₂ be non empty set ;
let c₃ be proper Subset of c₂;
cluster a₂ ` -> non empty ;
coherence

proof end;

end;

theorem Th39: :: TOPGEN_3:39

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being proper Subset of (b₂ -PointClTop b₁) holds
( b₃ is open iff not b₂ in b₃ )

proof end;

theorem Th40: :: TOPGEN_3:40

for b₁, b₂, b₃ being set st b₂ in b₁ holds
( {b₃} is closed Subset of (b₂ -PointClTop b₁) iff b₃ = b₂ )

proof end;

theorem Th41: :: TOPGEN_3:41

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

proof end;

definition

let c₂, c₃ be set ;
func c₂ -DiscreteTop c₁ -> strict TopSpace means :Def8: :: TOPGEN_3:def 8
( the carrier of a₃ = a₁ & ( for b₁ being Subset of a₃ holds Int b₁ = IFEQ b₁,a₁,b₁,(b₁ /\ a₂) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def 8 :

registration

let c₂ be non empty set ;
let c₃ be set ;
cluster a₂ -DiscreteTop a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th42: :: TOPGEN_3:42

for b₁ being non empty set
for b₂ being set
for b₃ being proper Subset of (b₂ -DiscreteTop b₁) holds Int b₃ = b₃ /\ b₂

proof end;

theorem Th43: :: TOPGEN_3:43

for b₁ being non empty set
for b₂ being set
for b₃ being proper Subset of (b₂ -DiscreteTop b₁) holds
( b₃ is open iff b₃ c= b₂ )

proof end;

Lemma46: for b₁ being set
for b₂ being Subset of b₁ st b₂ is proper holds
not b₁ is empty

proof end;

theorem Th44: :: TOPGEN_3:44

for b₁ being set
for b₂ being Subset of b₁ holds the topology of (b₂ -DiscreteTop b₁) = {b₁} \/ (bool b₂)

proof end;

theorem Th45: :: TOPGEN_3:45

for b₁ being set holds ADTS b₁ = {} -DiscreteTop b₁

proof end;

theorem Th46: :: TOPGEN_3:46

for b₁ being set holds 1TopSp b₁ = b₁ -DiscreteTop b₁

proof end;