environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PRE_TOPC, METRIC_1, REAL_1, XXREAL_0, CARD_1, ARYTM_3, COMPLEX1, ARYTM_1, SETFAM_1, NATTRA_1, RCOMP_1, SUBSET_1, STRUCT_0, TARSKI, ZFMISC_1, PCOMPS_1, FINSET_1, FUNCT_1, CARD_3, FUNCOP_1, COMPTS_1, RELAT_1, ORDINAL1, RLVECT_3, CARD_5, NEWTON, FINSEQ_1, PSCOMP_1, ORDINAL2, TOPMETR, TMAP_1, BINOP_1, FUNCT_2, SETWISEO, COH_SP, FINSOP_1, NAT_1, RELAT_2, NAGATA_1, FUNCT_7;
notations HIDDEN, BINOP_1, SETWISEO, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, COMPLEX1, RELSET_1, FUNCT_2, FINSEQ_1, ZFMISC_1, PCOMPS_1, PRE_TOPC, FINSET_1, CARD_1, XCMPLX_0, NUMBERS, XXREAL_0, XREAL_0, REAL_1, NAT_1, FINSOP_1, VALUED_1, STRUCT_0, TOPS_2, COMPTS_1, METRIC_1, NEWTON, CARD_3, PROB_1, FUNCOP_1, CANTOR_1, DOMAIN_1, TOPMETR, PSCOMP_1, BORSUK_1, TMAP_1;
definitions PCOMPS_1, TARSKI, BINOP_1;
theorems FUNCT_1, FUNCT_2, METRIC_1, XREAL_0, XCMPLX_1, ABSVALUE, TOPMETR, TMAP_1, CARD_1, PCOMPS_1, PCOMPS_2, BORSUK_1, XBOOLE_1, TARSKI, SETFAM_1, XBOOLE_0, SUBSET_1, TOPS_1, TOPS_2, PRE_TOPC, CARD_3, URYSOHN1, NAT_1, YELLOW_9, FINSEQ_1, FINSOP_1, SETWISEO, NEWTON, ZFMISC_1, BINOP_1, SEQ_2, PROB_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, PREPOWER, ORDINAL1, VALUED_1, JORDAN5A;
schemes FUNCT_1, FRAENKEL, FUNCT_2, NAT_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_LAR, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, BORSUK_1, TOPMETR, PSCOMP_1, VALUED_0, VALUED_1, FUNCT_2, CARD_3, FUNCT_1, PRE_TOPC, ZFMISC_1, BINOP_2, NEWTON, ORDINAL1;
constructors HIDDEN, SETWISEO, REAL_1, PROB_1, FUNCOP_1, FINSOP_1, NEWTON, CARD_5, TOPS_2, COMPTS_1, TMAP_1, CANTOR_1, PCOMPS_1, PSCOMP_1, URYSOHN3, BINOP_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities PCOMPS_1, BINOP_1, SUBSET_1, COMPTS_1, STRUCT_0;
expansions PCOMPS_1, TARSKI, COMPTS_1;
Lm1:
for r, s, t being Real st r >= 0 & s >= 0 & r + s < t holds
( r < t & s < t )
Lm2:
for r1, r2, r3, r4 being Real holds |.(r1 - r4).| <= (|.(r1 - r2).| + |.(r2 - r3).|) + |.(r3 - r4).|
Lm3:
for T being non empty TopSpace
for O being open Subset of T
for A being Subset of T st O meets Cl A holds
O meets A
Lm4:
for T being non empty TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
Cl A c= Cl (union F)
Lm5:
for T being non empty TopSpace ex Un being FamilySequence of T st Un is sigma_discrete
Lm6:
for T being non empty TopSpace
for U being open Subset of T
for A being Subset of T st A is closed holds
U \ A is open
Lm7:
for r being Real
for A being Point of RealSpace st r > 0 holds
A in Ball (A,r)
Lm8:
for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) )
by METRIC_1:def 2, METRIC_1:def 4, METRIC_1:def 5;
Lm9:
for r being Real
for X being non empty set
for f being Function of [:X,X:],REAL
for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y)))