environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, XBOOLE_0, XXREAL_2, ORDINAL2, XXREAL_0, SEQ_4, MESFUNC5, RELAT_1, FUNCT_1, RINFSUP1, VALUED_0, SEQ_1, ARYTM_3, TARSKI, CARD_1, ARYTM_1, SEQ_2, COMPLEX1, NAT_1, REAL_1, MESFUNC1, SUPINF_2, XCMPLX_0, SUPINF_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, XXREAL_3, XCMPLX_0, COMPLEX1, RELAT_1, FUNCT_1, REAL_1, XXREAL_0, RELSET_1, FUNCT_2, NAT_1, XXREAL_2, SUPINF_1, VALUED_0, SUPINF_2, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RINFSUP1, MEASURE6, EXTREAL1, MESFUNC1, MESFUNC5;
definitions TARSKI, VALUED_0;
theorems NAT_1, TARSKI, FUNCT_1, FUNCT_2, SUPINF_2, INT_1, EXTREAL1, SEQ_2, SEQ_4, RINFSUP1, XREAL_0, XBOOLE_0, XREAL_1, XXREAL_0, ORDINAL1, MESFUNC5, XXREAL_2, XXREAL_3;
schemes FUNCT_2;
registrations SUBSET_1, RELSET_1, XREAL_0, MEMBERED, ORDINAL1, INT_1, NUMBERS, XBOOLE_0, VALUED_0, SEQ_2, SEQ_4, XXREAL_3, FUNCT_2, NAT_1, VALUED_1;
constructors HIDDEN, REAL_1, NAT_1, DOMAIN_1, EXTREAL1, COMPLEX1, MEASURE6, MESFUNC1, PARTFUN3, LIMFUNC1, RINFSUP1, MESFUNC5, SUPINF_1, SEQ_4, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities MESFUNC1, RINFSUP1, XXREAL_3, SUPINF_2;
expansions TARSKI, VALUED_0;
Lm1:
for seq being ExtREAL_sequence holds superior_realsequence seq is non-increasing
Lm2:
for seq being ExtREAL_sequence holds inferior_realsequence seq is non-decreasing
Lm3:
for seq being ExtREAL_sequence st seq is bounded & seq is non-increasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )
Lm4:
for seq being ExtREAL_sequence st seq is bounded & seq is non-decreasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )
Lm5:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = +infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
Lm6:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = -infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
Lm7:
for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq in REAL holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )