begin
:: deftheorem Def1 defines point-filtered TOPGEN_3:def 1 :
theorem Th1:
theorem Th2:
theorem
theorem Th4:
scheme
TopDefByClosedPred{
F1()
-> set ,
P1[
set ] } :
provided
A1:
(
P1[
{} ] &
P1[
F1()] )
and A2:
for
A,
B being
set st
P1[
A] &
P1[
B] holds
P1[
A \/ B]
and A3:
for
G being
Subset-Family of
F1() st ( for
A being
set st
A in G holds
P1[
A] ) holds
P1[
Intersect G]
Lm1:
for T1, T2 being TopSpace st ( for A being set holds
( A is open Subset of T1 iff A is open Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )
theorem
Lm2:
for T1, T2 being TopSpace st ( for A being set holds
( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds
( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )
theorem Th6:
theorem Th7:
scheme
TopDefByClosureOp{
F1()
-> set ,
F2(
set )
-> set } :
provided
A1:
F2(
{} )
= {}
and A2:
for
A being
Subset of
F1() holds
(
A c= F2(
A) &
F2(
A)
c= F1() )
and A3:
for
A,
B being
Subset of
F1() holds
F2(
(A \/ B))
= F2(
A)
\/ F2(
B)
and A4:
for
A being
Subset of
F1() holds
F2(
F2(
A))
= F2(
A)
theorem Th8:
theorem Th9:
scheme
TopDefByInteriorOp{
F1()
-> set ,
F2(
set )
-> set } :
provided
A1:
F2(
F1())
= F1()
and A2:
for
A being
Subset of
F1() holds
F2(
A)
c= A
and A3:
for
A,
B being
Subset of
F1() holds
F2(
(A /\ B))
= F2(
A)
/\ F2(
B)
and A4:
for
A being
Subset of
F1() holds
F2(
F2(
A))
= F2(
A)
theorem Th10:
begin
:: deftheorem Def2 defines Sorgenfrey-line TOPGEN_3:def 2 :
Lm3:
the carrier of Sorgenfrey-line = REAL
by Def2;
consider BB being Subset-Family of REAL such that
Lm4:
the topology of Sorgenfrey-line = UniCl BB
and
Lm5:
BB = { [.x,q.[ where x, q is Element of REAL : ( x < q & q is rational ) }
by Def2;
BB c= the topology of Sorgenfrey-line
by Lm4, CANTOR_1:1;
then Lm6:
BB is Basis of Sorgenfrey-line
by Lm3, Lm4, CANTOR_1:def 2, TOPS_2:78;
theorem Th11:
theorem
theorem
theorem
theorem
theorem Th16:
theorem Th17:
theorem Th18:
:: deftheorem Def3 defines is_local_minimum_of TOPGEN_3:def 3 :
theorem Th19:
:: deftheorem defines continuum TOPGEN_3:def 4 :
theorem Th20:
:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
begin
:: deftheorem Def6 defines ClFinTop TOPGEN_3:def 6 :
theorem Th34:
theorem Th35:
theorem
begin
definition
let X,
x0 be
set ;
func x0 -PointClTop X -> strict TopSpace means :
Def7:
( the
carrier of
it = X & ( for
A being
Subset of
it holds
Cl A = IFEQ A,
{} ,
A,
(A \/ ({x0} /\ X)) ) );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = X & ( for A being Subset of b1 holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) )
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for A being Subset of b1 holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) & the carrier of b2 = X & ( for A being Subset of b2 holds Cl A = IFEQ A,{} ,A,(A \/ ({x0} /\ X)) ) holds
b1 = b2;
end;
:: deftheorem Def7 defines -PointClTop TOPGEN_3:def 7 :
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
begin
definition
let X,
X0 be
set ;
func X0 -DiscreteTop X -> strict TopSpace means :
Def8:
( the
carrier of
it = X & ( for
A being
Subset of
it holds
Int A = IFEQ A,
X,
A,
(A /\ X0) ) );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = X & ( for A being Subset of b1 holds Int A = IFEQ A,X,A,(A /\ X0) ) )
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = X & ( for A being Subset of b1 holds Int A = IFEQ A,X,A,(A /\ X0) ) & the carrier of b2 = X & ( for A being Subset of b2 holds Int A = IFEQ A,X,A,(A /\ X0) ) holds
b1 = b2;
end;
:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def 8 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem