environ
vocabularies HIDDEN, RLVECT_1, RVSUM_1, ALGSTR_0, METRIC_1, SQUARE_1, VALUED_0, PRE_TOPC, EQREL_1, PROB_1, MEASURE5, SUPINF_1, XREAL_0, MCART_1, XBOOLE_0, ORDINAL1, FINSEQ_2, EUCLID_9, ARYTM_3, XCMPLX_0, EUCLID, RCOMP_1, PCOMPS_1, SUBSET_1, TARSKI, NAT_1, NUMBERS, CARD_1, CARD_3, TOPS_1, REAL_1, TOPMETR, RELAT_1, FUNCT_1, FINSEQ_1, XXREAL_0, ARYTM_1, XXREAL_1, QC_LANG1, FUNCT_2, FINSET_1, CANTOR_1, RLVECT_3, SETFAM_1, ZFMISC_1, STRUCT_0, FUNCOP_1, SRINGS_3, SRINGS_4, SRINGS_1, FINSUB_1, SIMPLEX0, PARTFUN1, COMPLEX1, TIETZE_2, ORDINAL2, XXREAL_2, FUNCT_7, MEMBERED, RLTOPSP1, FUNCSDOM, SRINGS_5;
notations HIDDEN, SQUARE_1, ALGSTR_0, RLVECT_1, XXREAL_3, EXTREAL1, VALUED_1, RVSUM_1, EQREL_1, MEASURE5, SUPINF_1, ZFMISC_1, FINSUB_1, SIMPLEX0, SUBSET_1, NUMBERS, XXREAL_0, SETFAM_1, XREAL_0, RCOMP_1, TARSKI, ORDINAL1, XCMPLX_0, PCOMPS_1, EUCLID_9, PRE_TOPC, FINSEQ_2, CARD_1, XBOOLE_0, CARD_3, TOPS_1, TOPMETR, FUNCT_1, FINSEQ_1, TOPS_2, CANTOR_1, RELAT_1, FINSET_1, FUNCT_2, FUNCOP_1, RELSET_1, NAT_1, STRUCT_0, TIETZE_2, SRINGS_1, SRINGS_3, SRINGS_4, PARTFUN1, XTUPLE_0, PROB_1, COMPLEX1, VALUED_0, XXREAL_2, MEMBERED, BINOP_1, METRIC_1, EUCLID, RLTOPSP1, FUNCSDOM;
definitions TARSKI, XBOOLE_0, TOPS_2;
theorems TBSP_1, JORDAN2B, EXTREAL1, XXREAL_3, VALUED_0, MEASURE5, FINSUB_1, SETFAM_1, SRINGS_1, EUCLID_9, EUCLID, CARD_4, TOPS_1, NUMBERS, XBOOLE_0, XBOOLE_1, MARGREL1, FINSEQ_1, FINSEQ_2, FUNCT_1, TOPGEN_1, XXREAL_0, XREAL_1, XXREAL_1, ORDINAL1, CARD_3, CARD_1, BORSUK_5, CANTOR_1, TIETZE_2, TOPGEN_4, NAT_1, XCMPLX_1, ZFMISC_1, TARSKI, FUNCT_2, WAYBEL12, CARD_2, FUNCOP_1, PRE_TOPC, SCMYCIEL, SRINGS_3, SRINGS_4, CARD_5, SRINGS_2, XREAL_0, PARTFUN1, REAL_NS1, ABSVALUE, RELSET_1, MESFUNC1, FUNCT_5, FUNCT_6, RVSUM_1, XXREAL_2, SUBSET_1, BINOP_1, PCOMPS_1, MEMBERED, VALUED_1, COMPLEX1, SQUARE_1, EUCLID_3, METRIC_1;
schemes FINSEQ_4, FUNCT_1, CARD_4, FINSEQ_1, XBOOLE_0, BINOP_1;
registrations METRIC_1, XXREAL_1, FINSEQ_1, SUBSET_1, XREAL_0, NAT_1, ORDINAL1, NUMBERS, FINSEQ_2, TOPGEN_4, CARD_1, EUCLID_9, TOPS_1, XXREAL_0, EUCLID, VALUED_0, MONOID_0, RCOMP_1, CARD_3, FINSET_1, RELSET_1, SRINGS_1, SRINGS_3, SRINGS_4, XCMPLX_0, XTUPLE_0, FUNCT_1, FUNCT_2, SETFAM_1, MEMBERED, STRUCT_0, XXREAL_2, SQUARE_1, RLTOPSP1, XBOOLE_0, MFOLD_1;
constructors HIDDEN, SQUARE_1, SUPINF_2, EXTREAL1, EUCLID_9, TOPS_1, FUNCSDOM, MONOID_0, TOPGEN_2, TIETZE_2, SRINGS_1, SRINGS_3, SRINGS_4, TOPGEN_3, COMPLEX1, INTEGRA1, WAYBEL23;
requirements HIDDEN, SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
equalities XCMPLX_0, METRIC_1, PCOMPS_1, TOPMETR, EUCLID, CARD_3, EUCLID_9, FINSEQ_1, FUNCSDOM;
expansions XBOOLE_0, STRUCT_0, TARSKI, TOPS_2, PRE_TOPC;
Th16:
for n being Nat holds OpenHypercubesRAT n is countable
Th17:
for n being Nat holds union (OpenHypercubesRAT n) is countable
Th18:
for n being Nat holds union (OpenHypercubesRAT n) is Subset-Family of (TOP-REAL n)
Th22:
for n being Nat holds not union (OpenHypercubesRAT n) is empty
Lm1:
for n being Nat
for X being non empty set
for S being non empty Subset-Family of X
for x being Element of Product (n,S) ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )
Lm2:
for n being Nat
for X being non empty set
for S being non empty Subset-Family of X
for x being Subset of (Funcs ((Seg n),X))
for s being Tuple of n,S st ( for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ) holds
x is Element of Product (n,S)
definition
let n be non
zero Nat;
existence
ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = sup (rng (abs (x - y)))
uniqueness
for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = sup (rng (abs (x - y))) ) & ( for x, y being Element of REAL n holds b2 . (x,y) = sup (rng (abs (x - y))) ) holds
b1 = b2
end;
definition
let n be non
zero Nat;
existence
ex b1 being strict RLTopStruct st
( TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) )
uniqueness
for b1, b2 being strict RLTopStruct st TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) holds
b1 = b2
;
end;