environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, INT_1, RAT_1, ARYTM_1, CARD_1, XBOOLE_0, TARSKI, FUNCT_1, FUNCT_2, RELAT_1, NAT_1, ARYTM_3, ZFMISC_1, CARD_3, ORDINAL1, PARTFUN1, XXREAL_0, VALUED_1, SUPINF_2, SUPINF_1, COMPLEX1, PROB_1, VALUED_0, SETFAM_1, MESFUNC1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_3, XCMPLX_0, XREAL_0, MEASURE6, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, INT_1, NAT_1, RAT_1, CARD_3, XXREAL_0, VALUED_0, PROB_1, SUPINF_1, SUPINF_2, MEASURE2, MEASURE3, EXTREAL1, RELSET_2;
definitions TARSKI;
theorems MEASURE1, TARSKI, SUBSET_1, PARTFUN1, FUNCT_1, FUNCT_2, MEASURE5, SETFAM_1, NAT_1, INT_1, CARD_1, CARD_4, WELLORD2, RAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, NUMBERS, XREAL_1, FINSUB_1, PROB_1, XXREAL_0, ORDINAL1, CARD_3, XXREAL_3, RELAT_1, CARD_2;
schemes SUBSET_1, FUNCT_2, SEQ_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, MEASURE1, VALUED_0, XXREAL_3, FUNCT_1;
constructors HIDDEN, WELLORD2, REAL_1, NAT_1, RAT_1, MEASURE3, MEASURE6, EXTREAL1, SUPINF_1, RELSET_2, PARTFUN1, EQREL_1, RELAT_2, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities RELAT_1, SUPINF_2;
expansions TARSKI;
Lm1:
0 = - 0
;
definition
let C be non
empty set ;
let f1,
f2 be
C -defined ExtREAL -valued Function;
deffunc H1(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) + (f2 . $1);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) + (f2 . c) ) holds
b1 = b2
commutativity
for b1 being PartFunc of C,ExtREAL
for f1, f2 being C -defined ExtREAL -valued Function st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) holds
( dom b1 = ((dom f2) /\ (dom f1)) \ (((f2 " {-infty}) /\ (f1 " {+infty})) \/ ((f2 " {+infty}) /\ (f1 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f2 . c) + (f1 . c) ) )
;
deffunc H2(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) - (f2 . $1);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) - (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) - (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) - (f2 . c) ) holds
b1 = b2
deffunc H3(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) * (f2 . $1);
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) * (f2 . c) ) holds
b1 = b2
commutativity
for b1 being PartFunc of C,ExtREAL
for f1, f2 being C -defined ExtREAL -valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f2 . c) * (f1 . c) ) )
;
end;
canceled;
definition
let X be
set ;
let f be
PartFunc of
X,
ExtREAL;
let a be
ExtReal;
less_domredefine func less_dom (
f,
a)
-> Subset of
X;
coherence
less_dom (f,a) is Subset of X
less_eq_domredefine func less_eq_dom (
f,
a)
-> Subset of
X;
coherence
less_eq_dom (f,a) is Subset of X
great_domredefine func great_dom (
f,
a)
-> Subset of
X;
coherence
great_dom (f,a) is Subset of X
great_eq_domredefine func great_eq_dom (
f,
a)
-> Subset of
X;
coherence
great_eq_dom (f,a) is Subset of X
eq_domredefine func eq_dom (
f,
a)
-> Subset of
X;
coherence
eq_dom (f,a) is Subset of X
end;