environ
vocabularies HIDDEN, NUMBERS, SETFAM_1, XBOOLE_0, SUBSET_1, TARSKI, ABIAN, PRE_TOPC, STRUCT_0, CANTOR_1, RLVECT_3, ZFMISC_1, RELAT_1, PBOOLE, FUNCT_1, CARD_3, TOPGEN_2, RCOMP_1, YELLOW_8, TOPS_1, XXREAL_1, ARYTM_3, RAT_1, XXREAL_0, CARD_1, ORDINAL1, LIMFUNC1, CARD_2, INT_1, ARYTM_1, TAXONOM2, CARD_5, ORDINAL2, FINSET_1, MCART_1, NEWTON, FUNCT_7, SERIES_1, PREPOWER, COMPLEX1, NAT_1, VALUED_1, FINSUB_1, FINSEQ_1, ARYTM_2, WAYBEL23, FUNCOP_1, TEX_1, COMPTS_1, TOPGEN_3, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FINSET_1, DOMAIN_1, FINSUB_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FINSEQ_1, ORDINAL1, CARD_1, CARD_3, FUNCOP_1, TAXONOM2, CARD_2, CARD_5, ARYTM_3, ARYTM_2, XCMPLX_0, COMPLEX1, XXREAL_0, XREAL_0, NEWTON, INT_1, NAT_1, RAT_1, NUMBERS, ABIAN, FUNCT_7, VALUED_1, PREPOWER, SERIES_1, RCOMP_1, PBOOLE, LIMFUNC1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, TEX_1, CANTOR_1, YELLOW_8, WAYBEL23, TOPGEN_2;
definitions TARSKI, XBOOLE_0, FUNCT_1, CARD_3, PRE_TOPC, TAXONOM2, YELLOW_8, TOPGEN_2;
theorems TARSKI, XBOOLE_0, XBOOLE_1, SETFAM_1, PRE_TOPC, CANTOR_1, ABIAN, YELLOW_9, SUBSET_1, ZFMISC_1, CARD_3, CARD_5, FUNCT_1, YELLOW_8, TOPS_1, FUNCT_2, MSSUBFAM, RAT_1, XREAL_0, CARD_1, NUMBERS, CARD_4, CARD_2, INT_1, XCMPLX_1, FINSET_1, ORDINAL3, ARYTM_2, ARYTM_3, SERIES_1, ABSVALUE, PREPOWER, NEWTON, NAT_1, IRRAT_1, ORDINAL1, FINSUB_1, FUNCT_7, FINSEQ_1, TDLAT_3, FUNCOP_1, TEX_1, XREAL_1, XXREAL_0, WAYBEL23, VALUED_1, XXREAL_1, RELAT_1, PARTFUN1, TOPS_2, XTUPLE_0;
schemes FUNCT_1, FUNCT_2, NAT_1, CLASSES1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, INT_1, RAT_1, CARD_1, MEMBERED, NEWTON, PBOOLE, CARD_5, STRUCT_0, PRE_TOPC, TOPS_1, TEX_2, VALUED_0, VALUED_1, FUNCT_2, NAT_1, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, ARYTM_2, FINSUB_1, REAL_1, SQUARE_1, CARD_2, PROB_1, RCOMP_1, LIMFUNC1, NEWTON, PREPOWER, SERIES_1, ABIAN, TOPS_1, COMPTS_1, TEX_1, TAXONOM2, WAYBEL23, TOPGEN_2, RELSET_1, FINSEQ_2;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities CARD_3, STRUCT_0, SUBSET_1, COMPTS_1, LIMFUNC1, PROB_1, ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0, CARD_3, PRE_TOPC, SUBSET_1;
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 )
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 )
scheme
TopDefByClosureOp{
F1()
-> set ,
F2(
object )
-> 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)
scheme
TopDefByInteriorOp{
F1()
-> set ,
F2(
object )
-> 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)
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 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:64;
definition
let X,
x0 be
set ;
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;
definition
let X,
X0 be
set ;
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;