environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, ZFMISC_1, RELAT_1, SUPINF_2, XXREAL_0, CARD_1, SUPINF_1, SUBSET_1, NAT_1, ARYTM_3, ORDINAL1, XXREAL_2, ORDINAL2, XBOOLE_0, REAL_1, ARYTM_1, MEASURE5, XXREAL_1, MEMBERED, MEMBER_1, TARSKI, XCMPLX_0, FREEALG, QUANTAL1, SETFAM_1, FINSET_1, COMPLEX1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, PSCOMP_1, RCOMP_1, PRALG_1, PRE_TOPC, PARTFUN1, INT_1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, FINSET_1, NUMBERS, MEMBERED, ABSVALUE, COMPLEX1, VALUED_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, MEMBER_1, FUNCT_3, XXREAL_0, XXREAL_1, XXREAL_2, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, SUPINF_1, SUPINF_2, MEASURE5, VALUED_1;
definitions SEQ_2, TARSKI, XBOOLE_0, XXREAL_2, FINSET_1, RCOMP_1;
theorems SUPINF_2, FUNCT_1, MEASURE5, FUNCT_2, NAT_1, CARD_4, WELLORD2, XREAL_0, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, SETFAM_1, TARSKI, COMPLEX1, ABSVALUE, VALUED_1, SEQ_1, XCMPLX_1, SEQ_4, SEQ_2, RCOMP_1, RELSET_1, INT_1, SUBSET_1, MEMBER_1;
schemes RECDEF_1, NAT_1, FINSET_1, FUNCT_2, BINOP_2, DOMAIN_1, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, VALUED_0, VALUED_1, NAT_1, INT_1, FINSET_1, MEMBER_1, RCOMP_1, SEQ_2, SEQ_4, FCONT_3, FUNCT_2, MEASURE5, RELSET_1, XCMPLX_0, SEQ_1;
constructors HIDDEN, WELLORD2, DOMAIN_1, REAL_1, NAT_1, CARD_1, SUPINF_2, MEASURE5, SUPINF_1, RCOMP_1, RELSET_1, COMPLEX1, SEQ_2, SEQM_3, VALUED_0, VALUED_1, FUNCOP_1, SEQ_4, BINOP_2, LIMFUNC1, MEMBER_1, FUNCT_3, COMSEQ_2, SEQ_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities SUPINF_2, SUBSET_1, XXREAL_3, RCOMP_1, VALUED_1, XCMPLX_0, MEMBER_1;
expansions SEQ_2, TARSKI, XBOOLE_0, XXREAL_2, RCOMP_1;
Lm1:
for A being real-membered set
for x, y being Real holds
( y in x ++ A iff ex z being Real st
( z in A & y = x + z ) )
Lm2:
for X being Subset of REAL st X is bounded_above holds
-- X is bounded_below
Lm3:
for X being Subset of REAL st X is bounded_below holds
-- X is bounded_above
Lm4:
for X being Subset of REAL st X is closed holds
-- X is closed
Lm5:
for X being Subset of REAL
for p being Real holds p ++ X = { (p + r3) where r3 is Real : r3 in X }
Lm6:
for X being Subset of REAL
for s being Real st X is bounded_above holds
s ++ X is bounded_above
Lm7:
for X being Subset of REAL
for p being Real st X is bounded_below holds
p ++ X is bounded_below
Lm8:
for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed
Lm9:
for X being non empty set
for f being Function of X,REAL st f is with_max holds
- f is with_min
Lm10:
for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max