environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PRE_TOPC, RCOMP_1, SUBSET_1, FUNCT_1, URYSOHN1, CARD_1, ZFMISC_1, STRUCT_0, TARSKI, ARYTM_3, PARTFUN1, SEQFUNC, RELAT_1, NEWTON, XXREAL_0, NAT_1, ARYTM_1, REAL_1, CARD_3, PROB_1, LIMFUNC1, SUPINF_1, TOPMETR, ORDINAL2, XXREAL_1, SUPINF_2, XXREAL_2, TMAP_1, METRIC_1, PCOMPS_1, COMPLEX1, URYSOHN3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_1, XXREAL_2, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, NEWTON, SUPINF_2, TOPMETR, STRUCT_0, PRE_TOPC, COMPTS_1, TMAP_1, METRIC_1, PCOMPS_1, SEQFUNC, PROB_1, LIMFUNC1, SUPINF_1, URYSOHN1;
definitions PRE_TOPC, TARSKI;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, PCOMPS_1, PRE_TOPC, TOPS_1, TOPMETR, ABSVALUE, PARTFUN1, URYSOHN1, XREAL_0, RELSET_1, URYSOHN2, TMAP_1, METRIC_1, XBOOLE_0, XBOOLE_1, PREPOWER, XCMPLX_1, XREAL_1, PEPIN, NEWTON, XXREAL_0, SUBSET_1, NUMBERS, XXREAL_1, XXREAL_2, RELAT_1;
schemes NAT_1, FUNCT_2, RECDEF_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, URYSOHN1, TOPMETR, WAYBEL_3, VALUED_0, XREAL_0, FUNCT_1, NEWTON;
constructors HIDDEN, REAL_1, PROB_1, LIMFUNC1, NEWTON, SUPINF_2, MEASURE5, URYSOHN1, TMAP_1, WAYBEL_3, PCOMPS_1, BORSUK_6, COMPTS_1, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities STRUCT_0, LIMFUNC1, PROB_1;
expansions PRE_TOPC, TARSKI;
Lm1:
for T being non empty normal TopSpace
for A, B being closed Subset of T st A <> {} & A misses B holds
ex G being Function of (dyadic 0),(bool the carrier of T) st
( A c= G . 0 & B = ([#] T) \ (G . 1) & ( for r1, r2 being Element of dyadic 0 st r1 < r2 holds
( G . r1 is open & G . r2 is open & Cl (G . r1) c= G . r2 ) ) )
definition
let T be non
empty TopSpace;
let A,
B be
Subset of
T;
let R be
Rain of
A,
B;
existence
ex b1 being Function of T,R^1 st
for p being Point of T holds
( ( Rainbow (p,R) = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b1 . p = sup S ) )
uniqueness
for b1, b2 being Function of T,R^1 st ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies b1 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b1 . p = sup S ) ) ) & ( for p being Point of T holds
( ( Rainbow (p,R) = {} implies b2 . p = 0 ) & ( for S being non empty Subset of ExtREAL st S = Rainbow (p,R) holds
b2 . p = sup S ) ) ) holds
b1 = b2
end;