:: Partial Functions from a Domain to the Set of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received May 27, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, VALUED_0, FUNCT_1, XCMPLX_0,
ARYTM_1, RELAT_1, ARYTM_3, CARD_1, MEMBERED, PARTFUN1, TARSKI, ORDINAL4,
VALUED_1, COMPLEX1, FUNCT_3, XXREAL_2, XXREAL_0, REAL_1, FUNCT_7,
XREAL_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_3, VALUED_0, VALUED_1, COMSEQ_2, SEQ_2, REAL_1;
constructors PARTFUN1, FUNCT_3, XXREAL_0, REAL_1, COMPLEX1, VALUED_1,
PARTFUN2, SEQ_2, RELSET_1, COMSEQ_2, XREAL_0;
registrations FUNCT_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0,
VALUED_1, XCMPLX_0, SEQ_2, XXREAL_0, RELAT_1, ORDINAL1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions TARSKI, PARTFUN1, XBOOLE_0, VALUED_0, SEQ_2;
equalities XBOOLE_0, VALUED_1;
expansions TARSKI, PARTFUN1, XBOOLE_0, SEQ_2;
theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, PARTFUN2, RELSET_1,
RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1,
XXREAL_0, VALUED_0, VALUED_1, SEQ_2, XREAL_0;
schemes FUNCT_1;
begin
reserve x for object, X,Y for set;
reserve C for non empty set;
reserve c for Element of C;
reserve f,f1,f2,f3,g,g1 for complex-valued Function;
reserve r,p for Complex;
Lm1: (-1)"=-1;
::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS
::
definition
let f1,f2 be complex-valued Function;
func f1/f2 -> Function means
:Def1:
dom it = dom f1 /\ (dom f2 \ f2"{0}) &
for c being object st c in dom it holds it.c = f1.c * (f2.c)";
existence
proof
deffunc F(object) = f1.$1 * (f2.$1)";
ex f being Function st dom f = dom f1 /\ (dom f2 \ f2"{0}) &
for x being object st
x in dom f1 /\ (dom f2 \ f2"{0}) holds f.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f, g be Function such that
A1: dom f = dom f1 /\ (dom f2 \ f2"{0}) and
A2: for c being object st c in dom f holds f.c = f1.c * (f2.c)" and
A3: dom g = dom f1 /\ (dom f2 \ f2"{0}) and
A4: for c being object st c in dom g holds g.c = f1.c * (f2.c)";
now
let x be object;
assume
A5: x in dom f;
hence f.x = f1.x * (f2.x)" by A2
.= g.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
end;
registration
let f1, f2 be complex-valued Function;
cluster f1/f2 -> complex-valued;
coherence
proof
let x be object;
set F = f1/f2;
assume x in dom F;
then F.x = f1.x * (f2.x)" by Def1;
hence thesis;
end;
end;
registration
let f1, f2 be real-valued Function;
cluster f1/f2 -> real-valued;
coherence
proof
let x be object;
set F = f1/f2;
assume x in dom F;
then F.x = f1.x * (f2.x)" by Def1;
hence thesis;
end;
end;
definition
let C be set, D be complex-membered set;
let f1, f2 be PartFunc of C,D;
redefine func f1/f2 -> PartFunc of C,COMPLEX; :: redefines / (RFUNCT_1, definition)
coherence
proof
set F = f1/f2;
A1: rng F c= COMPLEX;
dom F = dom f1 /\ (dom f2 \ f2"{0}) by Def1;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let C be set, D be real-membered set;
let f1, f2 be PartFunc of C,D;
redefine func f1/f2 -> PartFunc of C,REAL; :: redefines / (RFUNCT_1, definition)
coherence
proof
set F = f1/f2;
rng F c= REAL by VALUED_0:def 3;
then F is PartFunc of dom F, REAL by RELSET_1:4;
hence thesis by RELSET_1:5;
end;
end;
definition
let f be complex-valued Function;
func f^ -> Function means
:Def2:
dom it = dom f \ f"{0} &
for c being object st c in dom it holds it.c = (f.c)";
existence
proof
deffunc F(object) = (f.$1)";
ex h being Function st dom h = dom f \ f"{0} &
for x being object st x in dom f \ f
"{0} holds h.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let h, g be Function such that
A1: dom h = dom f \ f"{0} and
A2: for c being object st c in dom h holds h.c = (f.c)" and
A3: dom g = dom f \ f"{0} and
A4: for c being object st c in dom g holds g.c = (f.c)";
now
let x be object;
assume
A5: x in dom h;
hence h.x = (f.x)" by A2
.= g.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
end;
registration
let f be complex-valued Function;
cluster f^ -> complex-valued;
coherence
proof
let x be object;
set F = f^;
assume x in dom F;
then F.x = (f.x)" by Def2;
hence thesis;
end;
end;
registration
let f be real-valued Function;
cluster f^ -> real-valued;
coherence
proof
let x be object;
set F = f^;
assume x in dom F;
then F.x = (f.x)" by Def2;
hence thesis;
end;
end;
definition
let C be set, D be complex-membered set, f be PartFunc of C,D;
redefine func f^ -> PartFunc of C,COMPLEX; :: redefines ^ (RFUNCT_1, definition)
coherence
proof
set F = f^;
A1: rng F c= COMPLEX;
dom F = dom f \ f"{0} by Def2;
hence thesis by A1,RELSET_1:4;
end;
end;
definition
let C be set, D be real-membered set, f be PartFunc of C,D;
redefine func f^ -> PartFunc of C,REAL; :: redefines ^ (RFUNCT_1, definition)
coherence
proof
set F = f^;
rng F c= REAL by VALUED_0:def 3;
then F is PartFunc of dom F, REAL by RELSET_1:4;
hence thesis by RELSET_1:5;
end;
end;
theorem Th1:
dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0}
proof
dom (g^) = dom g \ g"{0} by Def2;
hence dom (g^) c= dom g;
thus thesis by XBOOLE_1:28;
end;
theorem Th2:
dom (f1(#)f2) \ (f1(#)f2)"{0} = (dom f1 \ f1"{0}) /\ (dom f2 \ f2"{0})
proof
thus dom (f1(#)f2) \ (f1(#)f2)"{0} c= (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"
{0})
proof
let x be object;
assume
A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0};
then not x in (f1(#)f2)"{0} by XBOOLE_0:def 5;
then not (f1(#)f2).x in {0} by A1,FUNCT_1:def 7;
then (f1(#)f2).x <> 0 by TARSKI:def 1;
then
A2: f1.x * f2.x <> 0 by VALUED_1:5;
then f2.x <> 0;
then not f2.x in {0} by TARSKI:def 1;
then
A3: not x in (f2)"{0} by FUNCT_1:def 7;
x in dom (f1(#)f2) by A1;
then
A4: x in dom f1 /\ dom f2 by VALUED_1:def 4;
then x in dom f2 by XBOOLE_0:def 4;
then
A5: x in dom f2 \ (f2)"{0} by A3,XBOOLE_0:def 5;
f1.x <> 0 by A2;
then not f1.x in {0} by TARSKI:def 1;
then
A6: not x in (f1)"{0} by FUNCT_1:def 7;
x in dom f1 by A4,XBOOLE_0:def 4;
then x in dom f1 \ (f1)"{0} by A6,XBOOLE_0:def 5;
hence thesis by A5,XBOOLE_0:def 4;
end;
thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) c= dom (f1(#)f2) \ (f1(#)f2)
"{0}
proof
let x be object;
assume
A7: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0});
then x in dom f2 \ (f2)"{0} by XBOOLE_0:def 4;
then not x in (f2)"{0} by XBOOLE_0:def 5;
then not f2.x in {0} by A7,FUNCT_1:def 7;
then
A8: f2.x <> 0 by TARSKI:def 1;
A9: x in dom f1 \ (f1)"{0} by A7,XBOOLE_0:def 4;
then not x in (f1)"{0} by XBOOLE_0:def 5;
then not f1.x in {0} by A9,FUNCT_1:def 7;
then f1.x <> 0 by TARSKI:def 1;
then f1.x * f2.x <>0 by A8;
then (f1(#)f2).x <> 0 by VALUED_1:5;
then not (f1(#)f2).x in {0} by TARSKI:def 1;
then
A10: not x in (f1(#)f2)"{0} by FUNCT_1:def 7;
x in dom f1 /\ dom f2 by A7,A9,XBOOLE_0:def 4;
then x in dom (f1(#)f2) by VALUED_1:def 4;
hence thesis by A10,XBOOLE_0:def 5;
end;
end;
theorem Th3:
c in dom (f^) implies f.c <> 0
proof
assume that
A1: c in dom (f^) and
A2: f.c = 0;
A3: c in dom f \ f"{0} by A1,Def2;
then
A4: not c in f"{0} by XBOOLE_0:def 5;
now
per cases by A4,FUNCT_1:def 7;
suppose
not c in dom f;
hence contradiction by A3;
end;
suppose
not f.c in {0};
hence contradiction by A2,TARSKI:def 1;
end;
end;
hence contradiction;
end;
theorem Th4:
(f^)"{0} = {}
proof
set x = the Element of (f^)"{0};
assume
A1: (f^)"{0} <> {};
then
A2: x in dom (f^) by FUNCT_1:def 7;
then
A3: x in dom f \ f"{0} by Def2;
then not x in f"{0} by XBOOLE_0:def 5;
then
A4: not f.x in {0} by A3,FUNCT_1:def 7;
((f^) qua Function).x in {0} by A1,FUNCT_1:def 7;
then (f^).x = 0 by TARSKI:def 1;
then (f.x)" = 0 by A2,Def2;
hence contradiction by A4,TARSKI:def 1,XCMPLX_1:202;
end;
theorem Th5:
(abs(f))"{0} = f"{0} & (-f)"{0} = f"{0}
proof
now
let c be object;
reconsider cc = c as object;
thus c in (abs(f))"{0} implies c in f"{0}
proof
assume
A1: c in (abs(f))"{0};
then (abs(f)).c in {0} by FUNCT_1:def 7;
then (abs(f)).c = 0 by TARSKI:def 1;
then |.f.cc.| = 0 by VALUED_1:18;
then f.c = 0 by COMPLEX1:45;
then
A2: f.c in {0} by TARSKI:def 1;
c in dom (abs(f)) by A1,FUNCT_1:def 7;
then c in dom f by VALUED_1:def 11;
hence thesis by A2,FUNCT_1:def 7;
end;
assume
A3: c in (f)"{0};
then f.c in {0} by FUNCT_1:def 7;
then f.c = 0 by TARSKI:def 1;
then |.f.cc.| = 0 by ABSVALUE:2;
then (abs(f)).c = 0 by VALUED_1:18;
then
A4: (abs(f)).c in {0} by TARSKI:def 1;
c in dom f by A3,FUNCT_1:def 7;
then c in dom (abs(f)) by VALUED_1:def 11;
hence c in (abs(f))"{0} by A4,FUNCT_1:def 7;
end;
hence (abs(f))"{0} = f"{0} by TARSKI:2;
now
let c be object;
reconsider cc = c as object;
thus c in (-f)"{0} implies c in f"{0}
proof
assume
A5: c in (-f)"{0};
then (-f).c in {0} by FUNCT_1:def 7;
then (-f).c = 0 by TARSKI:def 1;
then --(f.cc) = -In(0,REAL) by VALUED_1:8;
then
A6: f.c in {0} by TARSKI:def 1;
c in dom (-f) by A5,FUNCT_1:def 7;
then c in dom f by VALUED_1:8;
hence thesis by A6,FUNCT_1:def 7;
end;
assume
A7: c in (f)"{0};
then f.c in {0} by FUNCT_1:def 7;
then f.c = 0 by TARSKI:def 1;
then (-f).c = -In(0,REAL) by VALUED_1:8;
then
A8: (-f).c in {0} by TARSKI:def 1;
c in dom f by A7,FUNCT_1:def 7;
then c in dom (-f) by VALUED_1:8;
hence c in (-f)"{0} by A8,FUNCT_1:def 7;
end;
hence thesis by TARSKI:2;
end;
theorem Th6:
dom (f^^) = dom (f|(dom (f^)))
proof
A1: dom (f^) = dom f \ f"{0} by Def2;
thus dom (f^^) = dom (f^) \(f^)"{0} by Def2
.= dom (f^) \ {} by Th4
.= dom f /\ dom (f^) by A1,XBOOLE_1:28
.= dom (f|(dom (f^))) by RELAT_1:61;
end;
theorem Th7:
r<>0 implies (r(#)f)"{0} = f"{0}
proof
assume
A1: r<>0;
now
let c be object;
reconsider cc = c as object;
thus c in (r(#)f)"{0} implies c in f"{0}
proof
assume
A2: c in (r(#)f)"{0};
then
A3: c in dom (r(#)f) by FUNCT_1:def 7;
(r(#)f).c in {0} by A2,FUNCT_1:def 7;
then (r(#)f).c = 0 by TARSKI:def 1;
then r*f.cc = 0 by A3,VALUED_1:def 5;
then f.c = 0 by A1;
then
A4: f.c in {0} by TARSKI:def 1;
c in dom f by A3,VALUED_1:def 5;
hence thesis by A4,FUNCT_1:def 7;
end;
assume
A5: c in (f)"{0};
then f.c in {0} by FUNCT_1:def 7;
then f.c = 0 by TARSKI:def 1;
then
A6: r*f.cc = 0;
A7: c in dom f by A5,FUNCT_1:def 7;
then c in dom (r(#)f) by VALUED_1:def 5;
then (r(#)f).c = 0 by A6,VALUED_1:def 5;
then
A8: (r(#)f).c in {0} by TARSKI:def 1;
c in dom (r(#)f) by A7,VALUED_1:def 5;
hence c in (r(#)f)"{0} by A8,FUNCT_1:def 7;
end;
hence thesis by TARSKI:2;
end;
::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem
(f1 + f2) + f3 = f1 + (f2 + f3)
proof
A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 1
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 + f3) by VALUED_1:def 1
.= dom (f1 + (f2 + f3)) by VALUED_1:def 1;
now
let c be object;
assume
A2: c in dom (f1 + f2 + f3);
then c in dom (f1 + f2) /\ dom f3 by VALUED_1:def 1;
then
A3: c in dom (f1 + f2) by XBOOLE_0:def 4;
c in dom f1 /\ dom (f2 + f3) by A1,A2,VALUED_1:def 1;
then
A4: c in dom (f2 + f3) by XBOOLE_0:def 4;
thus (f1 + f2 + f3).c = (f1 + f2).c + f3.c by A2,VALUED_1:def 1
.= f1.c + f2.c + f3.c by A3,VALUED_1:def 1
.= f1.c + (f2.c + f3.c)
.= f1.c + (f2 + f3).c by A4,VALUED_1:def 1
.= (f1 + (f2 + f3)).c by A1,A2,VALUED_1:def 1;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th9:
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
A1: now
let c be object;
assume c in dom (f1(#)f2(#)f3);
thus (f1 (#) f2 (#) f3).c = (f1 (#) f2).c * f3.c by VALUED_1:5
.= f1.c * f2.c * f3.c by VALUED_1:5
.= f1.c * (f2.c * f3.c)
.= f1.c * (f2 (#) f3).c by VALUED_1:5
.= (f1 (#) (f2 (#) f3)).c by VALUED_1:5;
end;
dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by VALUED_1:def 4
.= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 4
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 (#) f3) by VALUED_1:def 4
.= dom (f1 (#) (f2 (#) f3)) by VALUED_1:def 4;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th10:
(f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3
proof
A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by VALUED_1:def 4
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by VALUED_1:def 4
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by VALUED_1:def 4
.= dom (f1 (#) f3 + f2 (#) f3) by VALUED_1:def 1;
now
let c be object;
assume
A2: c in dom ((f1 + f2)(#)f3);
then c in dom (f1 + f2) /\ dom f3 by VALUED_1:def 4;
then
A3: c in dom (f1 + f2) by XBOOLE_0:def 4;
thus ((f1 + f2) (#) f3).c = (f1 + f2).c * f3.c by VALUED_1:5
.= (f1.c + f2.c) * f3.c by A3,VALUED_1:def 1
.= f1.c * f3.c + f2.c * f3.c
.= (f1 (#) f3).c + f2.c* f3.c by VALUED_1:5
.= (f1 (#) f3).c + (f2 (#) f3).c by VALUED_1:5
.=((f1 (#) f3) + (f2 (#) f3)).c by A1,A2,VALUED_1:def 1;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2 by Th10;
theorem Th12:
r(#)(f1(#)f2)=r(#)f1(#)f2
proof
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def 5
.= dom f1 /\ dom f2 by VALUED_1:def 4
.= dom (r(#)f1) /\ dom f2 by VALUED_1:def 5
.= dom (r(#)f1(#)f2) by VALUED_1:def 4;
now
let c be object;
assume
A2: c in dom (r(#)(f1(#)f2));
then c in dom (r(#)f1) /\ dom f2 by A1,VALUED_1:def 4;
then
A3: c in dom (r(#)f1) by XBOOLE_0:def 4;
thus (r(#)(f1(#)f2)).c = r * (f1(#)f2).c by A2,VALUED_1:def 5
.= r*(f1.c * f2.c) by VALUED_1:5
.= (r*f1.c) * f2.c
.= (r(#)f1).c * f2.c by A3,VALUED_1:def 5
.= (r(#)f1 (#) f2).c by VALUED_1:5;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th13:
r(#)(f1(#)f2)=f1(#)(r(#)f2)
proof
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def 5
.= dom f1 /\ dom f2 by VALUED_1:def 4
.= dom f1 /\ dom (r(#)f2) by VALUED_1:def 5
.= dom (f1(#)(r(#)f2)) by VALUED_1:def 4;
now
let c be object;
assume
A2: c in dom (r(#)(f1(#)f2));
then c in dom f1 /\ dom (r(#)f2) by A1,VALUED_1:def 4;
then
A3: c in dom (r(#)f2) by XBOOLE_0:def 4;
thus (r(#)(f1(#)f2)).c = r * (f1(#)f2).c by A2,VALUED_1:def 5
.= r * (f1.c * f2.c) by VALUED_1:5
.= f1.c * (r * f2.c)
.= f1.c * (r(#)f2).c by A3,VALUED_1:def 5
.= (f1(#)(r(#)f2)).c by VALUED_1:5;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th14:
(f1 - f2)(#)f3=f1(#)f3 - f2(#)f3
proof
A1: dom ((f1 - f2) (#) f3) = dom (f1 - f2) /\ dom f3 by VALUED_1:def 4
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:12
.= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by VALUED_1:def 4
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by VALUED_1:def 4
.= dom (f1 (#) f3 - f2 (#) f3) by VALUED_1:12;
now
let c be object;
assume
A2: c in dom ((f1 - f2)(#)f3);
then c in dom (f1 - f2) /\ dom f3 by VALUED_1:def 4;
then
A3: c in dom (f1 - f2) by XBOOLE_0:def 4;
thus ((f1 - f2) (#) f3).c = (f1 - f2).c * f3.c by VALUED_1:5
.= (f1.c - f2.c) * f3.c by A3,VALUED_1:13
.= f1.c * f3.c - f2.c * f3.c
.= (f1 (#) f3).c - f2.c * f3.c by VALUED_1:5
.= (f1 (#) f3).c - (f2 (#) f3).c by VALUED_1:5
.=((f1 (#) f3) - (f2 (#) f3)).c by A1,A2,VALUED_1:13;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2) by Th14;
theorem
r(#)(f1 + f2) = r(#)f1 + r(#)f2
proof
A1: dom (r(#)(f1 + f2)) = dom (f1 + f2) by VALUED_1:def 5
.= dom f1 /\ dom f2 by VALUED_1:def 1
.= dom f1 /\ dom (r(#)f2) by VALUED_1:def 5
.= dom (r(#)f1) /\ dom (r(#)f2) by VALUED_1:def 5
.= dom (r(#)f1 + r(#)f2) by VALUED_1:def 1;
now
let c be object;
assume
A2: c in dom (r(#)(f1 + f2));
then
A3: c in dom (f1 + f2) by VALUED_1:def 5;
A4: c in dom (r(#)f1) /\ dom (r(#)f2) by A1,A2,VALUED_1:def 1;
then
A5: c in dom (r(#)f1) by XBOOLE_0:def 4;
A6: c in dom (r(#)f2) by A4,XBOOLE_0:def 4;
thus (r(#)(f1 + f2)).c = r * (f1 + f2).c by A2,VALUED_1:def 5
.= r * (f1.c + f2.c) by A3,VALUED_1:def 1
.= r * f1.c + r * f2.c
.= (r(#)f1).c + r * f2.c by A5,VALUED_1:def 5
.= (r(#)f1).c + (r(#)f2).c by A6,VALUED_1:def 5
.= (r(#)f1 + r(#)f2).c by A1,A2,VALUED_1:def 1;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
(r*p)(#)f = r(#)(p(#)f)
proof
A1: dom ((r*p) (#) f) = dom f by VALUED_1:def 5
.= dom (p(#)f) by VALUED_1:def 5
.= dom (r(#)(p(#)f)) by VALUED_1:def 5;
now
let c be object;
assume
A2: c in dom ((r*p)(#)f);
then
A3: c in dom (p(#)f) by A1,VALUED_1:def 5;
thus ((r*p)(#)f).c = r*p * f.c by A2,VALUED_1:def 5
.= r*(p * f.c)
.= r * (p(#)f).c by A3,VALUED_1:def 5
.= (r(#)(p(#)f)).c by A1,A2,VALUED_1:def 5;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
r(#)(f1 - f2) = r(#)f1 - r(#)f2
proof
A1: dom (r(#)(f1 - f2)) = dom (f1 - f2) by VALUED_1:def 5
.= dom f1 /\ dom f2 by VALUED_1:12
.= dom f1 /\ dom (r(#)f2) by VALUED_1:def 5
.= dom (r(#)f1) /\ dom (r(#)f2) by VALUED_1:def 5
.= dom (r(#)f1 - r(#)f2) by VALUED_1:12;
now
let c be object;
assume
A2: c in dom (r(#)(f1 - f2));
then
A3: c in dom (f1 - f2) by VALUED_1:def 5;
A4: c in dom (r(#)f1) /\ dom (r(#)f2) by A1,A2,VALUED_1:12;
then
A5: c in dom (r(#)f1) by XBOOLE_0:def 4;
A6: c in dom (r(#)f2) by A4,XBOOLE_0:def 4;
thus (r(#)(f1 - f2)).c = r * (f1 - f2).c by A2,VALUED_1:def 5
.= r * (f1.c - f2.c) by A3,VALUED_1:13
.= r * f1.c - r * f2.c
.= (r(#)f1).c - r * f2.c by A5,VALUED_1:def 5
.= (r(#)f1).c - (r(#)f2).c by A6,VALUED_1:def 5
.= (r(#)f1 - r(#)f2).c by A1,A2,VALUED_1:13;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
f1-f2 = (-1)(#)(f2-f1)
proof
A1: dom (f1 - f2) = dom f2 /\ dom f1 by VALUED_1:12
.= dom (f2 - f1) by VALUED_1:12
.= dom ((-1)(#)(f2 - f1)) by VALUED_1:def 5;
now
A2: dom (f1 - f2) = dom f2 /\ dom f1 by VALUED_1:12
.= dom (f2 - f1) by VALUED_1:12;
let c be object such that
A3: c in dom (f1-f2);
thus (f1 - f2).c = f1.c - f2.c by A3,VALUED_1:13
.= (-1)*(f2.c - f1.c)
.= (-1)*((f2 - f1).c) by A3,A2,VALUED_1:13
.= ((-1)(#)(f2 - f1)).c by A1,A3,VALUED_1:def 5;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
f1 - (f2 + f3) = f1 - f2 - f3
proof
A1: dom (f1 - (f2 + f3)) = dom f1 /\ dom (f2 + f3) by VALUED_1:12
.= dom f1 /\ (dom f2 /\ dom f3) by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by VALUED_1:12
.= dom (f1 - f2 - f3) by VALUED_1:12;
now
let c be object;
assume
A2: c in dom (f1 - (f2 + f3));
then c in dom f1 /\ dom (f2 + f3) by VALUED_1:12;
then
A3: c in dom (f2 + f3) by XBOOLE_0:def 4;
c in dom (f1 - f2) /\ dom f3 by A1,A2,VALUED_1:12;
then
A4: c in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 + f3)).c = f1.c - (f2 + f3).c by A2,VALUED_1:13
.= f1.c - (f2.c + f3.c) by A3,VALUED_1:def 1
.= f1.c - f2.c - f3.c
.= (f1 - f2).c - f3.c by A4,VALUED_1:13
.= (f1 - f2 - f3).c by A1,A2,VALUED_1:13;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
1(#)f = f
proof
A1: now
let c be object;
assume c in dom (1(#)f);
hence (1(#)f).c = 1 * f.c by VALUED_1:def 5
.= f.c;
end;
dom (1(#)f) = dom f by VALUED_1:def 5;
hence thesis by A1,FUNCT_1:2;
end;
theorem
f1 - (f2 - f3) = f1 - f2 + f3
proof
A1: dom (f1 - (f2 - f3)) = dom f1 /\ dom (f2 - f3) by VALUED_1:12
.= dom f1 /\ (dom f2 /\ dom f3) by VALUED_1:12
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by VALUED_1:12
.= dom (f1 - f2 + f3) by VALUED_1:def 1;
now
let c be object;
assume
A2: c in dom (f1 - (f2 - f3));
then c in dom f1 /\ dom (f2 - f3) by VALUED_1:12;
then
A3: c in dom (f2 - f3) by XBOOLE_0:def 4;
c in dom (f1 - f2) /\ dom f3 by A1,A2,VALUED_1:def 1;
then
A4: c in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 - f3)).c = f1.c - (f2 - f3).c by A2,VALUED_1:13
.= f1.c - (f2.c - f3.c) by A3,VALUED_1:13
.= f1.c - f2.c + f3.c
.= (f1 - f2).c + f3.c by A4,VALUED_1:13
.= (f1 - f2 + f3).c by A1,A2,VALUED_1:def 1;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
f1 + (f2 - f3) = f1 + f2 - f3
proof
A1: dom (f1 + (f2 - f3)) = dom f1 /\ dom (f2 - f3) by VALUED_1:def 1
.= dom f1 /\ (dom f2 /\ dom f3) by VALUED_1:12
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 + f2) /\ dom f3 by VALUED_1:def 1
.= dom (f1 + f2 - f3) by VALUED_1:12;
now
let c be object;
assume
A2: c in dom (f1 + (f2 - f3));
then c in dom f1 /\ dom (f2 - f3) by VALUED_1:def 1;
then
A3: c in dom (f2 - f3) by XBOOLE_0:def 4;
c in dom (f1 + f2) /\ dom f3 by A1,A2,VALUED_1:12;
then
A4: c in dom (f1 + f2) by XBOOLE_0:def 4;
thus (f1 + (f2 - f3)).c = f1.c + (f2 - f3).c by A2,VALUED_1:def 1
.= f1.c + (f2.c - f3.c) by A3,VALUED_1:13
.= f1.c + f2.c - f3.c
.= (f1 + f2).c - f3.c by A4,VALUED_1:def 1
.= (f1 + f2 - f3).c by A1,A2,VALUED_1:13;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th24:
abs(f1(#)f2) = abs(f1)(#)abs(f2)
proof
A1: now
let c be object;
assume c in dom (abs(f1 (#) f2));
thus (abs(f1(#)f2)).c = |.(f1(#)f2).c.| by VALUED_1:18
.= |.f1.c * f2.c.| by VALUED_1:5
.= |.f1.c.| * |.f2.c.| by COMPLEX1:65
.= ((abs(f1)).c) * |.f2.c.| by VALUED_1:18
.= ((abs(f1)).c) * (abs(f2)).c by VALUED_1:18
.= (abs(f1)(#)abs(f2)).c by VALUED_1:5;
end;
dom (abs(f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def 11
.= dom f1 /\ dom f2 by VALUED_1:def 4
.= dom f1 /\ dom (abs(f2)) by VALUED_1:def 11
.= dom (abs(f1)) /\ dom (abs(f2)) by VALUED_1:def 11
.= dom (abs(f1)(#)abs(f2)) by VALUED_1:def 4;
hence thesis by A1,FUNCT_1:2;
end;
theorem
abs(r(#)f) = |.r.|(#)abs(f)
proof
A1: dom (abs(r(#)f)) = dom (r(#)f) by VALUED_1:def 11
.= dom f by VALUED_1:def 5
.= dom (abs(f)) by VALUED_1:def 11
.= dom (|.r.|(#)abs(f)) by VALUED_1:def 5;
now
let c be object;
assume
A2: c in dom (abs(r(#)f));
then
A3: c in dom (r(#)f) by VALUED_1:def 11;
thus (abs(r(#)f)).c = |.(r(#)f).c.| by VALUED_1:18
.=|.r*(f.c).| by A3,VALUED_1:def 5
.=|.r.|*|.f.c.| by COMPLEX1:65
.=|.r.|*(abs(f)).c by VALUED_1:18
.=(|.r.|(#)abs(f)).c by A1,A2,VALUED_1:def 5;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th26:
f^^ = f|(dom (f^))
proof
A1: dom (f^^) = dom (f|(dom (f^))) by Th6;
now
let c be object;
assume
A2: c in dom (f^^);
then c in dom f /\ dom (f^) by A1,RELAT_1:61;
then
A3: c in dom (f^) by XBOOLE_0:def 4;
thus (f^^).c = ((f^).c)" by A2,Def2
.= ((f.c)")" by A3,Def2
.= (f|(dom (f^))).c by A1,A2,FUNCT_1:47;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th27:
(f1(#)f2)^ = (f1^)(#)(f2^)
proof
A1: dom ((f1(#)f2)^) = dom (f1(#)f2) \ (f1(#)f2)"{0} by Def2
.= (dom f1 \ f1"{0}) /\ (dom f2 \ (f2)"{0}) by Th2
.= dom (f1^) /\ (dom f2 \ (f2)"{0}) by Def2
.= dom (f1^) /\ dom (f2^) by Def2
.= dom ((f1^) (#) (f2^)) by VALUED_1:def 4;
now
let c be object;
assume
A2: c in dom ((f1(#)f2)^);
then
A3: c in dom (f1^) /\ dom (f2^) by A1,VALUED_1:def 4;
then
A4: c in dom (f1^) by XBOOLE_0:def 4;
A5: c in dom (f2^) by A3,XBOOLE_0:def 4;
thus ((f1(#)f2)^).c = ((f1(#)f2).c)" by A2,Def2
.= (f1.c * f2.c)" by VALUED_1:5
.= (f1.c)"* (f2.c)" by XCMPLX_1:204
.= ((f1^).c)*(f2.c)" by A4,Def2
.= ((f1^).c) *((f2^).c) by A5,Def2
.= ((f1^) (#) (f2^)).c by VALUED_1:5;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th28:
r<>0 implies (r(#)f)^ = r" (#) (f^)
proof
assume
A1: r<>0;
A2: dom ((r(#)f)^) = dom (r(#)f) \ (r(#)f)"{0} by Def2
.= dom (r(#)f) \ f"{0} by A1,Th7
.= dom f \ f"{0} by VALUED_1:def 5
.= dom (f^) by Def2
.= dom (r"(#)(f^)) by VALUED_1:def 5;
now
let c be object;
assume
A3: c in dom ((r(#)f)^);
then
A4: c in dom (r(#)f) \ (r(#)f)"{0} by Def2;
A5: c in dom (f^) by A2,A3,VALUED_1:def 5;
thus ((r(#)f)^).c = ((r(#)f).c)" by A3,Def2
.= (r*(f.c))" by A4,VALUED_1:def 5
.= r"* (f.c)" by XCMPLX_1:204
.= r"* ((f^).c) by A5,Def2
.= (r" (#) (f^)).c by A2,A3,VALUED_1:def 5;
end;
hence thesis by A2,FUNCT_1:2;
end;
theorem
(-f)^ = (-1)(#)(f^) by Lm1,Th28;
theorem Th30:
(abs(f))^ = abs(f^)
proof
A1: dom ((abs(f))^) = dom (abs(f)) \ (abs(f))"{0} by Def2
.= dom f \ (abs(f))"{0} by VALUED_1:def 11
.= dom f \ f"{0} by Th5
.= dom (f^) by Def2
.= dom (abs((f^))) by VALUED_1:def 11;
now
let c be object;
assume
A2: c in dom ((abs(f))^);
then
A3: c in dom (f^) by A1,VALUED_1:def 11;
thus ((abs(f))^).c = ((abs(f)).c)" by A2,Def2
.= (|.f.c.|)" by VALUED_1:18
.= 1/|.f.c.| by XCMPLX_1:215
.= |.1/f.c.| by COMPLEX1:80
.= |.(f.c)".| by XCMPLX_1:215
.= |.f^.c.| by A3,Def2
.= (abs(f^)).c by VALUED_1:18;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th31:
f/g = f(#) (g^)
proof
A1: now
let c be object;
assume
A2: c in dom (f/g);
then c in dom f /\ (dom g \ g"{0}) by Def1;
then c in dom f /\ dom (g^) by Def2;
then
A3: c in dom (g^) by XBOOLE_0:def 4;
thus (f/g).c = f.c * (g.c)" by A2,Def1
.= f.c * (g^).c by A3,Def2
.= (f (#) (g^)).c by VALUED_1:5;
end;
dom (f/g) = dom f /\ (dom g \ g"{0}) by Def1
.= dom f /\ dom (g^) by Def2
.= dom (f(#)(g^)) by VALUED_1:def 4;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th32:
r(#)(g/f) = (r(#)g)/f
proof
thus r(#)(g/f) = r(#)(g(#)(f^)) by Th31
.= (r(#)g)(#)(f^) by Th12
.= (r(#)g)/f by Th31;
end;
theorem
(f/g)(#)g = (f|dom(g^))
proof
A1: dom ((f/g)(#)g) = dom (f/g) /\ dom g by VALUED_1:def 4
.= dom f /\ (dom g \ g"{0}) /\ dom g by Def1
.= dom f /\ ((dom g \ g"{0}) /\ dom g) by XBOOLE_1:16
.= dom f /\ (dom (g^) /\ dom g) by Def2
.= dom f /\ dom (g^) by Th1,XBOOLE_1:28
.= dom (f|(dom (g^))) by RELAT_1:61;
now
let c be object;
assume
A2: c in dom ((f/g)(#)g);
then c in dom f /\ dom (g^) by A1,RELAT_1:61;
then
A3: c in dom (g^) by XBOOLE_0:def 4;
then
A4: g.c <> 0 by Th3;
thus ((f/g)(#)g).c = ((f/g).c) * g.c by VALUED_1:5
.= (f(#)(g^)).c * g.c by Th31
.= (f.c) *((g^).c) * g.c by VALUED_1:5
.= (f.c)*(g.c)"*g.c by A3,Def2
.= (f.c)*((g.c)" * (g.c))
.= (f.c)*1 by A4,XCMPLX_0:def 7
.= (f|(dom (g^))).c by A1,A2,FUNCT_1:47;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th34:
(f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1)
proof
A1: now
let c be object;
assume c in dom ((f/g)(#)(f1/g1));
thus ((f/g)(#)(f1/g1)).c = ((f/g).c)* (f1/g1).c by VALUED_1:5
.= ((f(#)(g^)).c) * (f1/g1).c by Th31
.= ((f(#)(g^)).c) * (f1(#)(g1^)).c by Th31
.= (f.c) * ((g^).c) * (f1(#)(g1^)).c by VALUED_1:5
.= (f.c) * ((g^).c) * ((f1.c)* (g1^).c) by VALUED_1:5
.= (f.c) * ((f1.c) * (((g^).c) * (g1^).c))
.= (f.c) * ((f1.c) * ((g^)(#)(g1^)).c) by VALUED_1:5
.= (f.c) * (f1.c) * ((g^)(#)(g1^)).c
.= (f.c) * (f1.c) * ((g(#)g1)^).c by Th27
.= ((f(#)f1).c) * ((g(#)g1)^).c by VALUED_1:5
.= ((f(#)f1)(#)((g(#)g1)^)).c by VALUED_1:5
.= ((f(#)f1)/(g(#)g1)).c by Th31;
end;
dom ((f/g)(#)(f1/g1)) = dom (f/g) /\ dom (f1/g1) by VALUED_1:def 4
.= dom f /\ (dom g \ g"{0}) /\ dom (f1/g1) by Def1
.= dom f /\ (dom g \ g"{0}) /\ (dom f1 /\ (dom g1 \ g1"{0})) by Def1
.= dom f /\ ((dom g \ g"{0}) /\ (dom f1 /\ (dom g1 \ g1"{0}))) by
XBOOLE_1:16
.= dom f /\ (dom f1 /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0}))) by
XBOOLE_1:16
.= dom f /\ dom f1 /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0})) by XBOOLE_1:16
.= dom (f(#)f1) /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0})) by VALUED_1:def 4
.= dom (f(#)f1) /\ (dom (g(#)g1) \ (g(#)g1)"{0}) by Th2
.= dom ((f(#)f1)/(g(#)g1)) by Def1;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th35:
(f1/f2)^ = (f2|dom(f2^))/f1
proof
thus (f1/f2)^ = (f1(#)(f2^))^ by Th31
.= (f1^)(#)(f2^^) by Th27
.= (f2|dom(f2^))(#)(f1^) by Th26
.= (f2|dom(f2^))/f1 by Th31;
end;
theorem Th36:
g (#) (f1/f2) = (g (#) f1)/f2
proof
thus g (#) (f1/f2) = g (#) (f1 (#) (f2^)) by Th31
.= g (#) f1 (#) (f2^) by Th9
.= (g (#) f1)/f2 by Th31;
end;
theorem
g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1
proof
thus g/(f1/f2) = g (#) ((f1/f2)^) by Th31
.= g (#) ((f2|dom(f2^))/f1) by Th35
.= (g (#) (f2|dom(f2^)))/f1 by Th36;
end;
theorem
-f/g = (-f)/g & f/(-g) = -f/g
proof
thus -f/g = (-f)/g by Th32;
thus f/(-g) = f (#) ((-g)^) by Th31
.= f (#) ((-1) (#) (g^)) by Lm1,Th28
.= -(f (#) (g^)) by Th13
.= -(f/g) by Th31;
end;
theorem
f1/f + f2/f = (f1 + f2)/f & f1/f - f2/f = (f1 - f2)/f
proof
thus f1/f + f2/f = f1(#)(f^) +f2/f by Th31
.= f1(#)(f^) + f2(#)(f^) by Th31
.= (f1+f2) (#) (f^) by Th10
.= (f1+f2)/f by Th31;
thus f1/f - f2/f = f1(#)(f^) - f2/f by Th31
.= f1(#)(f^) -f2(#)(f^) by Th31
.= (f1-f2)(#)(f^) by Th14
.= (f1-f2)/f by Th31;
end;
theorem Th40:
f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g)
proof
A1: now
let c be object;
A2: dom (g^) c= dom g by Th1;
assume
A3: c in dom ((f1/f) + (g1/g));
then
A4: c in dom (f1/f) /\ dom (g1/g) by VALUED_1:def 1;
then
A5: c in dom (f1/f) by XBOOLE_0:def 4;
A6: c in dom (g1/g) by A4,XBOOLE_0:def 4;
A7: dom (f^) c= dom f by Th1;
A8: c in dom (f1 (#)(f^)) /\ dom (g1/g) by A4,Th31;
then c in dom (f1 (#)(f^)) by XBOOLE_0:def 4;
then
A9: c in dom f1 /\ dom(f^) by VALUED_1:def 4;
then
A10: c in dom(f^) by XBOOLE_0:def 4;
then
A11: f.c <> 0 by Th3;
c in dom (f1 (#)(f^)) /\ dom (g1(#)(g^)) by A8,Th31;
then c in dom (g1(#)(g^)) by XBOOLE_0:def 4;
then
A12: c in dom g1 /\ dom(g^) by VALUED_1:def 4;
then
A13: c in dom(g^) by XBOOLE_0:def 4;
then
A14: g.c <> 0 by Th3;
c in dom g1 by A12,XBOOLE_0:def 4;
then c in dom g1 /\ dom f by A10,A7,XBOOLE_0:def 4;
then
A15: c in dom (g1(#)f) by VALUED_1:def 4;
c in dom f1 by A9,XBOOLE_0:def 4;
then c in dom f1 /\ dom g by A13,A2,XBOOLE_0:def 4;
then c in dom (f1(#)g) by VALUED_1:def 4;
then c in dom (f1(#)g) /\ dom (g1(#)f) by A15,XBOOLE_0:def 4;
then
A16: c in dom (f1(#)g + g1(#)f) by VALUED_1:def 1;
c in dom (f^) /\ dom (g^) by A10,A13,XBOOLE_0:def 4;
then c in dom ((f^)(#)(g^)) by VALUED_1:def 4;
then c in dom ((f(#)g)^) by Th27;
then c in dom (f1(#)g + g1(#)f) /\ dom ((f(#)g)^) by A16,XBOOLE_0:def 4;
then c in dom ((f1(#)g + g1(#)f)(#)((f(#)g)^)) by VALUED_1:def 4;
then
A17: c in dom ((f1(#)g + g1(#)f)/(f(#)g)) by Th31;
thus (f1/f + g1/g).c = (f1/f).c + (g1/g).c by A3,VALUED_1:def 1
.= (f1.c) * (f.c)" + (g1/g).c by A5,Def1
.= (f1.c) *(1*(f.c)") + (g1.c) * 1 * (g.c)" by A6,Def1
.= (f1.c) *((g.c) *(g.c)"* (f.c)") + (g1.c) * (1 * (g.c)") by A14,
XCMPLX_0:def 7
.= (f1.c) *(g.c *((g.c)"* (f.c)")) + (g1.c) * ((f.c) *(f.c)" * (g.c)")
by A11,XCMPLX_0:def 7
.= (f1.c) *((g.c) *((g.c * f.c)")) + (g1.c) * ((f.c) *((f.c)" * (g.c)"
)) by XCMPLX_1:204
.= (f1.c) *((g.c) *((f.c* g.c)")) + (g1.c) * ((f.c) *((f.c * g.c)"))
by XCMPLX_1:204
.= (f1.c) *((g.c) * ((f(#)g).c)") + (g1.c) * ((f.c) *((f.c * g.c)"))
by VALUED_1:5
.= (f1.c) *(g.c) * ((f(#)g).c)" + (g1.c) * ((f.c) * ((f(#) g).c)") by
VALUED_1:5
.= (f1(#)g).c * ((f(#)g).c)" + (g1.c) *f.c *((f(#)g).c)" by VALUED_1:5
.= (f1(#)g).c * ((f(#)g).c)" + (g1(#)f).c *((f(#)g).c)" by VALUED_1:5
.= ((f1(#)g).c + (g1(#)f).c) *((f(#)g).c)"
.= (f1(#)g + g1(#)f).c *((f(#)g).c)" by A16,VALUED_1:def 1
.= ((f1(#)g + g1(#)f)/(f(#)g)).c by A17,Def1;
end;
dom ((f1/f) + (g1/g)) = dom (f1/f) /\ dom (g1/g) by VALUED_1:def 1
.= dom f1 /\ (dom f \ f"{0}) /\ dom (g1/g) by Def1
.= dom f1 /\ (dom f \ f"{0}) /\ (dom g1 /\ (dom g \ g"{0})) by Def1
.= dom f1 /\ (dom f /\ (dom f \ f"{0})) /\ (dom g1 /\ (dom g \ g"{0}))
by Th1
.= dom f /\ (dom f \ f"{0}) /\ dom f1 /\ (dom g /\ (dom g \ g"{0}) /\
dom g1) by Th1
.= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0}) /\
dom g1)) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0})) /\
dom g1) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\ dom g /\ (dom g \ g"{0}) /\
dom g1) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0}) /\ (dom (f1(#)g) /\ (dom g \ g"{0}) /\ dom
g1) by VALUED_1:def 4
.= dom f /\ (dom f \ f"{0}) /\ (dom (f1(#)g) /\ (dom g1 /\ (dom g \ g"{0
}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ dom f /\ (dom g1 /\ (dom g \ g"{0
}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom f /\ (dom g1 /\ (dom g \ g"{
0})))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom g1 /\ dom f /\ (dom g \ g"{0
}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom (g1(#)f) /\ (dom g \ g"{0}))
) by VALUED_1:def 4
.= dom (f1(#)g) /\ (dom (g1(#)f) /\ ((dom f \ f"{0}) /\ (dom g \ g"{0}))
) by XBOOLE_1:16
.= dom (f1(#)g) /\ dom (g1(#) f) /\ ((dom f \ f"{0}) /\ (dom g \ g"{0}))
by XBOOLE_1:16
.= dom (f1(#)g + g1(#)f) /\ ((dom f \ f"{0}) /\ (dom g \ g"{0})) by
VALUED_1:def 1
.= dom (f1(#)g + g1(#)f) /\ (dom (f(#)g) \ (f(#)g)"{0}) by Th2
.= dom ((f1(#)g + g1(#)f)/(f(#)g)) by Def1;
hence thesis by A1,FUNCT_1:2;
end;
theorem
(f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1)
proof
thus (f/g)/(f1/g1) = (f/g)(#)((f1/g1)^) by Th31
.= (f/g)(#)(((g1|dom(g1^)))/f1) by Th35
.= (f(#)(g1|dom(g1^)))/(g(#)f1) by Th34;
end;
theorem
f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g)
proof
thus f1/f - g1/g = f1/f + ((-1)(#) g1)/g by Th32
.= (f1(#)g + (-1)(#) g1(#)f)/(f(#)g) by Th40
.= (f1(#)g - (g1(#)f))/(f(#)g) by Th12;
end;
theorem
abs(f1/f2) = abs(f1)/abs(f2)
proof
thus abs(f1/f2) = abs(f1(#)(f2^)) by Th31
.= abs(f1)(#)abs((f2^)) by Th24
.= abs(f1)(#)((abs(f2))^) by Th30
.= abs(f1)/abs(f2) by Th31;
end;
theorem Th44:
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X
proof
A1: now
let c be object;
assume
A2: c in dom ((f1+f2)|X);
then
A3: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (f1+f2) by A3,XBOOLE_0:def 4;
then
A6: c in dom f1 /\ dom f2 by VALUED_1:def 1;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
then
A7: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A6,XBOOLE_0:def 4;
then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
then
A8: c in dom (f1|X) by RELAT_1:61;
then c in dom (f1|X) /\ dom (f2|X) by A7,XBOOLE_0:def 4;
then
A9: c in dom ((f1|X) + (f2|X)) by VALUED_1:def 1;
thus ((f1+f2)|X).c = (f1+f2).c by A2,FUNCT_1:47
.= (f1.c) + (f2.c) by A5,VALUED_1:def 1
.= ((f1|X).c) + (f2.c) by A8,FUNCT_1:47
.= ((f1|X).c) + ((f2|X).c) by A7,FUNCT_1:47
.= ((f1|X)+(f2|X)).c by A9,VALUED_1:def 1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by VALUED_1:def 1
.= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16
.= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16
.= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:61
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
.= dom ((f1|X)+(f2|X)) by VALUED_1:def 1;
hence (f1+f2)|X = f1|X + f2|X by A1,FUNCT_1:2;
A10: now
let c be object;
assume
A11: c in dom ((f1+f2)|X);
then
A12: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A13: c in X by XBOOLE_0:def 4;
A14: c in dom (f1+f2) by A12,XBOOLE_0:def 4;
then
A15: c in dom f1 /\ dom f2 by VALUED_1:def 1;
then c in dom f1 by XBOOLE_0:def 4;
then c in dom f1 /\ X by A13,XBOOLE_0:def 4;
then
A16: c in dom (f1|X) by RELAT_1:61;
c in dom f2 by A15,XBOOLE_0:def 4;
then c in dom (f1|X) /\ dom f2 by A16,XBOOLE_0:def 4;
then
A17: c in dom ((f1|X) + f2) by VALUED_1:def 1;
thus ((f1+f2)|X).c = (f1+f2).c by A11,FUNCT_1:47
.= (f1.c) +(f2.c) by A14,VALUED_1:def 1
.= ((f1|X).c) +(f2.c) by A16,FUNCT_1:47
.= ((f1|X)+f2).c by A17,VALUED_1:def 1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VALUED_1:def 1
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:61
.= dom ((f1|X)+ f2) by VALUED_1:def 1;
hence (f1+f2)|X = f1|X + f2 by A10,FUNCT_1:2;
A18: now
let c be object;
assume
A19: c in dom ((f1+f2)|X);
then
A20: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A21: c in X by XBOOLE_0:def 4;
A22: c in dom (f1+f2) by A20,XBOOLE_0:def 4;
then
A23: c in dom f1 /\ dom f2 by VALUED_1:def 1;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A21,XBOOLE_0:def 4;
then
A24: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A23,XBOOLE_0:def 4;
then c in dom f1 /\ dom (f2|X) by A24,XBOOLE_0:def 4;
then
A25: c in dom (f1 + (f2|X)) by VALUED_1:def 1;
thus ((f1+f2)|X).c = (f1+f2).c by A19,FUNCT_1:47
.= (f1.c) +(f2.c) by A22,VALUED_1:def 1
.= (f1.c) +((f2|X).c) by A24,FUNCT_1:47
.= (f1+(f2|X)).c by A25,VALUED_1:def 1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VALUED_1:def 1
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:61
.= dom (f1 + (f2|X)) by VALUED_1:def 1;
hence thesis by A18,FUNCT_1:2;
end;
theorem Th45:
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)
f2)|X = f1 (#) f2|X
proof
A1: now
let c be object;
assume
A2: c in dom ((f1(#)f2)|X);
then
A3: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
c in dom (f1(#)f2) by A3,XBOOLE_0:def 4;
then
A5: c in dom f1 /\ dom f2 by VALUED_1:def 4;
then c in dom f1 by XBOOLE_0:def 4;
then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
then
A6: c in dom (f1|X) by RELAT_1:61;
c in dom f2 by A5,XBOOLE_0:def 4;
then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
then
A7: c in dom (f2|X) by RELAT_1:61;
thus ((f1(#)f2)|X).c = (f1(#)f2).c by A2,FUNCT_1:47
.= (f1.c) *(f2.c) by VALUED_1:5
.= ((f1|X).c) *(f2.c) by A6,FUNCT_1:47
.= ((f1|X).c) *((f2|X).c) by A7,FUNCT_1:47
.= ((f1|X)(#)(f2|X)).c by VALUED_1:5;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by VALUED_1:def 4
.= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16
.= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16
.= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:61
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
.= dom ((f1|X)(#)(f2|X)) by VALUED_1:def 4;
hence (f1(#)f2)|X = f1|X (#) f2|X by A1,FUNCT_1:2;
A8: now
let c be object;
assume
A9: c in dom ((f1(#)f2)|X);
then
A10: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then c in dom (f1(#)f2) by XBOOLE_0:def 4;
then c in dom f1 /\ dom f2 by VALUED_1:def 4;
then
A11: c in dom f1 by XBOOLE_0:def 4;
c in X by A10,XBOOLE_0:def 4;
then c in dom f1 /\ X by A11,XBOOLE_0:def 4;
then
A12: c in dom (f1|X) by RELAT_1:61;
thus ((f1(#)f2)|X).c = (f1(#)f2).c by A9,FUNCT_1:47
.= (f1.c) *(f2.c) by VALUED_1:5
.= ((f1|X).c) *(f2.c) by A12,FUNCT_1:47
.= ((f1|X)(#)f2).c by VALUED_1:5;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VALUED_1:def 4
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:61
.= dom ((f1|X)(#) f2) by VALUED_1:def 4;
hence (f1(#)f2)|X = f1|X (#) f2 by A8,FUNCT_1:2;
A13: now
let c be object;
assume
A14: c in dom ((f1(#)f2)|X);
then
A15: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then c in dom (f1(#)f2) by XBOOLE_0:def 4;
then c in dom f1 /\ dom f2 by VALUED_1:def 4;
then
A16: c in dom f2 by XBOOLE_0:def 4;
c in X by A15,XBOOLE_0:def 4;
then c in dom f2 /\ X by A16,XBOOLE_0:def 4;
then
A17: c in dom (f2|X) by RELAT_1:61;
thus ((f1(#)f2)|X).c = (f1(#)f2).c by A14,FUNCT_1:47
.= (f1.c) *(f2.c) by VALUED_1:5
.= (f1.c) *((f2|X).c) by A17,FUNCT_1:47
.= (f1(#)(f2|X)).c by VALUED_1:5;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VALUED_1:def 4
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:61
.= dom (f1 (#) (f2|X)) by VALUED_1:def 4;
hence thesis by A13,FUNCT_1:2;
end;
theorem Th46:
(-f)|X = -(f|X) & (f^)|X = (f|X)^ & (abs(f))|X = abs((f|X))
proof
A1: now
let c be object;
assume
A2: c in dom ((-f)|X);
then
A3: c in dom (-f) /\ X by RELAT_1:61;
then c in dom (-f) by XBOOLE_0:def 4;
then
A4: c in dom f by VALUED_1:8;
c in X by A3,XBOOLE_0:def 4;
then c in dom f /\ X by A4,XBOOLE_0:def 4;
then
A5: c in dom (f|X) by RELAT_1:61;
thus ((-f)|X).c = (-f).c by A2,FUNCT_1:47
.= -(f.c) by VALUED_1:8
.= -((f|X).c) by A5,FUNCT_1:47
.= (-(f|X)).c by VALUED_1:8;
end;
dom ((-f)|X) = dom (-f) /\ X by RELAT_1:61
.= dom f /\ X by VALUED_1:8
.= dom (f|X) by RELAT_1:61
.= dom (-(f|X)) by VALUED_1:8;
hence (-f)|X = -(f|X) by A1,FUNCT_1:2;
A6: dom ((f^)|X) = dom (f^) /\ X by RELAT_1:61
.= (dom f \ f"{0}) /\ X by Def2
.= dom f /\ X \ f"{0} /\ X by XBOOLE_1:50
.= dom (f|X) \ X /\ f"{0} by RELAT_1:61
.= dom (f|X) \ (f|X)"{0} by FUNCT_1:70
.= dom ((f|X)^) by Def2;
A7: dom ((f|X)^) c= dom (f|X) by Th1;
now
let c be object;
assume
A8: c in dom ((f^)|X);
then c in dom (f^) /\ X by RELAT_1:61;
then
A9: c in dom (f^) by XBOOLE_0:def 4;
thus ((f^)|X).c = (f^).c by A8,FUNCT_1:47
.= (f.c)" by A9,Def2
.= ((f|X).c)" by A7,A6,A8,FUNCT_1:47
.= ((f|X)^).c by A6,A8,Def2;
end;
hence (f^)|X = (f|X)^ by A6,FUNCT_1:2;
A10: dom ((abs(f))|X) = dom (abs(f)) /\ X by RELAT_1:61
.= dom f /\ X by VALUED_1:def 11
.= dom (f|X) by RELAT_1:61
.= dom (abs((f|X))) by VALUED_1:def 11;
now
let c be object;
assume
A11: c in dom ((abs(f))|X);
then
A12: c in dom (f|X) by A10,VALUED_1:def 11;
thus ((abs(f))|X).c = (abs(f)).c by A11,FUNCT_1:47
.= |.f.c.| by VALUED_1:18
.= |.(f|X).c.| by A12,FUNCT_1:47
.= (abs((f|X))).c by VALUED_1:18;
end;
hence thesis by A10,FUNCT_1:2;
end;
theorem
(f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 & (f1-f2)|X = f1 - f2| X
proof
thus (f1-f2)|X = (f1|X)+ (-f2)|X by Th44
.= (f1|X) - (f2|X) by Th46;
thus (f1-f2)|X = (f1|X) - f2 by Th44;
thus (f1-f2)|X = f1+ (-f2)|X by Th44
.= f1 - (f2|X) by Th46;
end;
theorem
(f1/f2)|X = f1|X / f2|X & (f1/f2)|X = f1|X / f2 &(f1/f2)|X = f1 / f2|X
proof
thus (f1/f2)|X = (f1(#)(f2^))|X by Th31
.= (f1|X) (#) (f2^|X) by Th45
.= (f1|X) (#) ((f2|X)^) by Th46
.= (f1|X)/(f2|X) by Th31;
thus (f1/f2)|X = (f1(#)(f2^))|X by Th31
.= (f1|X) (#) (f2^) by Th45
.= (f1|X)/f2 by Th31;
thus (f1/f2)|X = (f1(#)(f2^))|X by Th31
.= f1 (#) (f2^)|X by Th45
.= f1 (#) ((f2|X)^) by Th46
.= f1/(f2|X) by Th31;
end;
theorem Th49:
(r(#)f)|X = r(#)(f|X)
proof
A1: now
let c be object;
assume
A2: c in dom ((r(#)f)|X);
then
A3: c in dom (r(#)f) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (r(#)f) by A3,XBOOLE_0:def 4;
then c in dom f by VALUED_1:def 5;
then c in dom f /\ X by A4,XBOOLE_0:def 4;
then
A6: c in dom (f|X) by RELAT_1:61;
then
A7: c in dom (r(#)(f|X)) by VALUED_1:def 5;
thus ((r(#)f)|X).c = (r(#)f).c by A2,FUNCT_1:47
.= r*(f.c) by A5,VALUED_1:def 5
.= r*(f|X).c by A6,FUNCT_1:47
.= (r(#)(f|X)).c by A7,VALUED_1:def 5;
end;
dom ((r(#)f)|X) = dom (r(#)f) /\ X by RELAT_1:61
.= dom f /\ X by VALUED_1:def 5
.= dom (f|X) by RELAT_1:61
.= dom (r(#)(f|X)) by VALUED_1:def 5;
hence thesis by A1,FUNCT_1:2;
end;
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::
reserve r,r1,r2,p for Real;
reserve f,f1,f2 for PartFunc of C,REAL;
theorem Th50:
(f1 is total & f2 is total iff f1+f2 is total) & (f1 is total &
f2 is total iff f1-f2 is total) & (f1 is total & f2 is total iff f1(#)f2 is
total)
proof
thus f1 is total & f2 is total iff f1+f2 is total
proof
thus f1 is total & f2 is total implies f1+f2 is total;
assume f1+f2 is total;
then dom (f1+f2) = C;
then
A1: dom f1 /\ dom f2 = C by VALUED_1:def 1;
then
A2: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A1,XBOOLE_1:17;
hence dom f1 = C & dom f2 = C by A2;
end;
thus f1 is total & f2 is total iff f1-f2 is total
proof
thus f1 is total & f2 is total implies f1-f2 is total;
assume f1-f2 is total;
then dom (f1-f2) = C;
then
A3: dom f1 /\ dom f2 = C by VALUED_1:12;
then
A4: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A3,XBOOLE_1:17;
hence dom f1 = C & dom f2 = C by A4;
end;
thus f1 is total & f2 is total implies f1(#)f2 is total;
assume f1(#)f2 is total;
then dom (f1(#)f2) = C;
then
A5: dom f1 /\ dom f2 = C by VALUED_1:def 4;
then
A6: C c= dom f2 by XBOOLE_1:17;
C c= dom f1 by A5,XBOOLE_1:17;
hence dom f1 = C & dom f2 = C by A6;
end;
theorem Th51:
f is total iff r(#)f is total
by VALUED_1:def 5;
theorem
f is total iff -f is total by Th51;
theorem
f is total iff abs(f) is total
by VALUED_1:def 11;
theorem Th54:
f^ is total iff f"{0} = {} & f is total
proof
thus f^ is total implies f"{0} = {} & f is total
proof
assume f^ is total;
then
A1: dom (f^) = C;
f"{0} c= C;
then f"{0} c= dom f \ f"{0} by A1,Def2;
hence f"{0} = {} by XBOOLE_1:38;
then C = dom f \ {} by A1,Def2;
hence dom f = C;
end;
assume that
A2: f"{0} = {} and
A3: f is total;
thus dom (f^) = dom f \ f"{0} by Def2
.= C by A2,A3;
end;
theorem Th55:
f1 is total & f2"{0} = {} & f2 is total iff f1/f2 is total
proof
thus f1 is total & f2"{0} = {} & f2 is total implies f1/f2 is total
proof
assume that
A1: f1 is total and
A2: f2"{0} = {} and
A3: f2 is total;
f2^ is total by A2,A3,Th54;
then f1(#)(f2^) is total by A1;
hence thesis by Th31;
end;
assume f1/f2 is total;
then
A4: f1(#)(f2^) is total by Th31;
hence f1 is total by Th50;
f2^ is total by A4,Th50;
hence thesis by Th54;
end;
theorem
f1 is total & f2 is total implies (f1+f2).c = f1.c + f2.c & (f1-f2).c
= f1.c - f2.c & (f1(#)f2).c = f1.c * f2.c
proof
assume that
A1: f1 is total and
A2: f2 is total;
f1+f2 is total by A1,A2;
then dom (f1+f2) = C;
hence (f1+f2).c = f1.c + f2.c by VALUED_1:def 1;
f1-f2 is total by A1,A2;
then dom (f1-f2) = C;
hence (f1-f2).c = f1.c - f2.c by VALUED_1:13;
thus thesis by VALUED_1:5;
end;
theorem
f is total implies (r(#)f).c = r * (f.c)
proof
assume f is total;
then r(#)f is total;
then dom (r(#)f) = C;
hence thesis by VALUED_1:def 5;
end;
theorem
f is total implies (-f).c = - f.c & (abs(f)).c = |.f.c.| by VALUED_1:8,18;
theorem
f^ is total implies (f^).c = (f.c)"
by Def2;
theorem
f1 is total & f2^ is total implies (f1/f2).c = f1.c *(f2.c)"
proof
assume that
A1: f1 is total and
A2: f2^ is total;
A3: f2 is total by A2,Th54;
f2"{0} = {} by A2,Th54;
then f1/f2 is total by A1,A3,Th55;
then dom (f1/f2) = C;
hence thesis by Def1;
end;
::
:: CHARCTERISTIC FUNCTION OF A SUBSET OF A DOMAIN
::
definition
let X,C be set;
redefine func chi(X,C) -> PartFunc of C,REAL; :: redefines chi (FUNCT_3, definition)
coherence
proof
for x being object st x in rng chi(X,C) holds x in REAL
by XREAL_0:def 1;
then
A1: rng chi(X,C) c= REAL;
dom chi(X,C) =C by FUNCT_3:def 3;
hence thesis by A1,RELSET_1:4;
end;
end;
registration
let X,C be set;
cluster chi(X,C) -> total for PartFunc of C,REAL;
coherence
by FUNCT_3:def 3;
end;
theorem Th61:
f= chi(X,C) iff ( dom f = C & for c holds (c in X implies f.c =
1) & (not c in X implies f.c = 0))
proof
thus f= chi(X,C) implies (dom f = C & for c holds (c in X implies f.c = 1) &
(not c in X implies f.c = 0)) by FUNCT_3:def 3;
assume that
A1: dom f = C and
A2: for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0);
for x st x in C holds (x in X implies (f qua Function).x = 1) & (not x
in X implies (f qua Function).x = 0) by A2;
hence thesis by A1,FUNCT_3:def 3;
end;
theorem
chi(X,C) is total;
theorem
c in X iff chi(X,C).c = 1 by Th61;
theorem
not c in X iff chi(X,C).c = 0 by Th61;
theorem
c in C \ X iff chi(X,C).c = 0
proof
thus c in C \ X implies chi(X,C).c = 0
proof
assume c in C \ X;
then not c in X by XBOOLE_0:def 5;
hence thesis by Th61;
end;
assume chi(X,C).c = 0;
then not c in X by Th61;
hence thesis by XBOOLE_0:def 5;
end;
theorem
chi(C,C).c = 1 by Th61;
theorem Th67:
chi(X,C).c <> 1 iff chi(X,C).c = 0
by Th61;
theorem
X misses Y implies chi(X,C) + chi(Y,C) = chi(X \/ Y,C)
proof
assume
A1: X /\ Y = {};
A2: now
let c such that
A3: c in dom (chi(X,C) + chi(Y,C));
now
per cases;
suppose
A4: c in X;
then not c in Y by A1,XBOOLE_0:def 4;
then
A5: chi(Y,C).c = 0 by Th61;
A6: c in X \/ Y by A4,XBOOLE_0:def 3;
chi(X,C).c = 1 by A4,Th61;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A5,A6,Th61;
end;
suppose
A7: not c in X;
then
A8: chi(X,C).c = 0 by Th61;
now
per cases;
suppose
A9: c in Y;
then
A10: c in X \/ Y by XBOOLE_0:def 3;
chi(Y,C).c = 1 by A9,Th61;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A8,A10,Th61;
end;
suppose
A11: not c in Y;
then
A12: not c in X \/ Y by A7,XBOOLE_0:def 3;
chi(Y,C).c = 0 by A11,Th61;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A8,A12,Th61;
end;
end;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c;
end;
end;
hence (chi(X,C) + chi(Y,C)).c = chi(X \/ Y,C).c by A3,VALUED_1:def 1;
end;
dom (chi(X,C) + chi(Y,C)) = dom chi(X,C) /\ dom chi(Y,C) by VALUED_1:def 1
.= C /\ dom chi(Y,C) by Th61
.= C /\ C by Th61
.= dom chi(X \/ Y,C) by Th61;
hence thesis by A2,PARTFUN1:5;
end;
theorem
chi(X,C) (#) chi(Y,C) = chi(X /\ Y,C)
proof
A1: now
let c such that
c in dom (chi(X,C) (#) chi(Y,C));
now
per cases;
suppose
A2: chi(X,C).c * chi(Y,C).c = 0;
now
per cases by A2;
suppose
chi(X,C).c = 0;
then not c in X by Th61;
then not c in X /\ Y by XBOOLE_0:def 4;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A2,Th61;
end;
suppose
chi(Y,C).c = 0;
then not c in Y by Th61;
then not c in X /\ Y by XBOOLE_0:def 4;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A2,Th61;
end;
end;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c;
end;
suppose
A3: chi(X,C).c * chi(Y,C).c <> 0;
then
A4: chi(Y,C).c <> 0;
then
A5: chi(Y,C).c = 1 by Th67;
A6: c in Y by A4,Th61;
A7: chi(X,C).c <> 0 by A3;
then c in X by Th61;
then
A8: c in X /\ Y by A6,XBOOLE_0:def 4;
chi(X,C).c = 1 by A7,Th67;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A5,A8,Th61;
end;
end;
hence (chi(X,C)(#)chi(Y,C)).c = chi(X /\ Y,C).c by VALUED_1:5;
end;
dom (chi(X,C) (#) chi(Y,C)) = dom chi(X,C) /\ dom chi(Y,C) by VALUED_1:def 4
.= C /\ dom chi(Y,C) by Th61
.= C /\ C by Th61
.= dom chi(X /\ Y,C) by Th61;
hence thesis by A1,PARTFUN1:5;
end;
::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::
reserve f for real-valued Function;
theorem Th70:
f|Y is bounded_above iff ex r st for c being object st c in Y /\
dom f holds f.c <= r
proof
thus f|Y is bounded_above implies ex r st
for c being object st c in Y /\ dom f
holds f.c <= r
proof
given r being Real such that
A1: for p being object st p in dom(f|Y) holds (f|Y).p<r;
take r;
let c be object;
assume c in Y /\ dom f;
then
A2: c in dom(f|Y) by RELAT_1:61;
then (f|Y).c < r by A1;
hence thesis by A2,FUNCT_1:47;
end;
given r such that
A3: for c being object st c in Y /\ dom f holds f.c <= r;
reconsider r1 = r+1 as Real;
take r1;
let p be object;
assume
A4: p in dom(f|Y);
then p in Y /\ dom f by RELAT_1:61;
then f.p <= r by A3;
then
A5: (f|Y).p <= r by A4,FUNCT_1:47;
r < r1 by XREAL_1:29;
hence thesis by A5,XXREAL_0:2;
end;
theorem Th71:
f|Y is bounded_below iff ex r st for c being object st c in Y /\
dom f holds r <= f.c
proof
thus f|Y is bounded_below implies
ex r st for c being object st c in Y /\ dom f
holds r <= f.c
proof
given r being Real such that
A1: for p being object st p in dom(f|Y) holds r < (f|Y).p;
take r;
let c be object;
assume c in Y /\ dom f;
then
A2: c in dom(f|Y) by RELAT_1:61;
then r < (f|Y).c by A1;
hence thesis by A2,FUNCT_1:47;
end;
given r such that
A3: for c being object st c in Y /\ dom f holds r <= f.c;
reconsider r1 = r-1 as Real;
take r1;
let p be object;
assume
A4: p in dom(f|Y);
then p in Y /\ dom f by RELAT_1:61;
then r <= f.p by A3;
then
A5: r <= (f|Y).p by A4,FUNCT_1:47;
r1 < r by XREAL_1:44;
hence thesis by A5,XXREAL_0:2;
end;
theorem Th72:
f is bounded iff ex r st for c being object st c in dom f holds |.f.c.|<=r
proof
thus f is bounded implies ex r st for c being object st c in dom f
holds |.f.c.|<=r
proof
assume
A1: f is bounded;
then consider r1 such that
A2: for c being object st c in dom f holds f.c < r1 by SEQ_2:def 1;
consider r2 such that
A3: for c being object st c in dom f holds r2 < f.c by A1,SEQ_2:def 2;
take g=|.r1.|+|.r2.|;
let c be object such that
A4: c in dom f;
A5: 0 <= |.r2.| by COMPLEX1:46;
r1 <= |.r1.| by ABSVALUE:4;
then f.c <= |.r1.| by A2,A4,XXREAL_0:2;
then
A6: f.c + (0 qua Real)<= |.r1.|+|.r2.| by A5,XREAL_1:7;
A7: 0 <= |.r1.| by COMPLEX1:46;
-|.r2.| <= r2 by ABSVALUE:4;
then -|.r2.| <= f.c by A3,A4,XXREAL_0:2;
then
A8: -|.r1.|+-|.r2.| <= ((0 qua Real) + f.c)
by A7,XREAL_1:7;
-|.r1.|+-|.r2.| = -g;
hence thesis by A6,A8,ABSVALUE:5;
end;
given r such that
A9: for c being object st c in dom f holds |.f.c.| <= r;
thus f is bounded_above
proof
take r+1;
let c be object;
assume c in dom f;
then
A10: |.f.c.| < r+1 by A9,XREAL_1:39;
f.c <= |.f.c.| by ABSVALUE:4;
hence thesis by A10,XXREAL_0:2;
end;
take -(r+1);
let c be object;
assume c in dom f;
then |.f.c.| < r+1 by A9,XREAL_1:39;
then
A11: -(r+1) < -|.f.c.| by XREAL_1:24;
-|.f.c.| <= f.c by ABSVALUE:4;
hence thesis by A11,XXREAL_0:2;
end;
theorem
f|Y is bounded iff ex r st for c being object st c in Y /\ dom f holds
|.f.c.|<=r
proof
thus f|Y is bounded implies
ex r st for c being object st c in Y /\ dom f holds
|.f.c.|<=r
proof
assume
A1: f|Y is bounded;
then consider r1 such that
A2: for c being object st c in Y /\ dom f holds f.c <= r1 by Th70;
consider r2 such that
A3: for c being object st c in Y /\ dom f holds r2 <= f.c by A1,Th71;
take g=|.r1.|+|.r2.|;
A4: r1 <= |.r1.| by ABSVALUE:4;
let c be object such that
A5: c in Y /\ dom f;
f.c <= r1 by A2,A5;
then
A6: f.c <= |.r1.| by A4,XXREAL_0:2;
A7: -|.r2.| <= r2 by ABSVALUE:4;
r2 <= f.c by A3,A5;
then
A8: -|.r2.| <= f.c by A7,XXREAL_0:2;
0 <= |.r1.| by COMPLEX1:46;
then
A9: -|.r1.|+-|.r2.| <= (0 qua Real) + f.c by A8,XREAL_1:7;
0 <= |.r2.| by COMPLEX1:46;
then
A10: f.c + (0 qua Real) <= |.r1.|+|.r2.| by A6,XREAL_1:7;
-|.r1.|+-|.r2.| = -g;
hence thesis by A10,A9,ABSVALUE:5;
end;
given r such that
A11: for c being object st c in Y /\ dom f holds |.f.c.| <= r;
now
let c be object;
assume c in Y /\ dom f;
then |.f.c.| <= r by A11;
then
A12: -r <= -|.f.c.| by XREAL_1:24;
-|.f.c.| <= f.c by ABSVALUE:4;
hence -r <= f.c by A12,XXREAL_0:2;
end;
then
A13: f|Y is bounded_below by Th71;
now
let c be object;
assume c in Y /\ dom f;
then
A14: |.f.c.| <= r by A11;
f.c <= |.f.c.| by ABSVALUE:4;
hence f.c <= r by A14,XXREAL_0:2;
end;
then f|Y is bounded_above by Th70;
hence thesis by A13;
end;
theorem
(Y c= X & f|X is bounded_above implies f|Y is bounded_above) & (Y c= X
& f|X is bounded_below implies f|Y is bounded_below) & (Y c= X & f|X is bounded
implies f|Y is bounded)
proof
thus
A1: Y c= X & f|X is bounded_above implies f|Y is bounded_above
proof
assume that
A2: Y c= X and
A3: f|X is bounded_above;
consider r such that
A4: for c being object st c in X /\ dom f holds f.c <= r by A3,Th70;
now
take r;
let c be object;
assume
A5: c in Y /\ dom f;
then
A6: c in dom f by XBOOLE_0:def 4;
c in Y by A5,XBOOLE_0:def 4;
then c in X /\ dom f by A2,A6,XBOOLE_0:def 4;
hence f.c <= r by A4;
end;
hence thesis by Th70;
end;
thus
A7: Y c= X & f|X is bounded_below implies f|Y is bounded_below
proof
assume that
A8: Y c= X and
A9: f|X is bounded_below;
consider r such that
A10: for c being object st c in X /\ dom f holds r <= f.c by A9,Th71;
now
take r;
let c be object;
assume
A11: c in Y /\ dom f;
then
A12: c in dom f by XBOOLE_0:def 4;
c in Y by A11,XBOOLE_0:def 4;
then c in X /\ dom f by A8,A12,XBOOLE_0:def 4;
hence r <= f.c by A10;
end;
hence thesis by Th71;
end;
assume that
A13: Y c= X and
A14: f|X is bounded;
thus thesis by A1,A7,A13,A14;
end;
theorem
f|X is bounded_above & f|Y is bounded_below implies f|(X /\ Y) is bounded
proof
assume that
A1: f|X is bounded_above and
A2: f|Y is bounded_below;
consider r1 such that
A3: for c being object st c in X /\ dom f holds f.c <= r1 by A1,Th70;
now
let c be object;
assume
A4: c in X /\ Y /\ dom f;
then c in X /\ Y by XBOOLE_0:def 4;
then
A5: c in X by XBOOLE_0:def 4;
c in dom f by A4,XBOOLE_0:def 4;
then c in X /\ dom f by A5,XBOOLE_0:def 4;
hence f.c <= r1 by A3;
end;
hence f|(X /\ Y) is bounded_above by Th70;
consider r2 such that
A6: for c being object st c in Y /\ dom f holds r2 <= f.c by A2,Th71;
now
let c be object;
assume
A7: c in X /\ Y /\ dom f;
then c in X /\ Y by XBOOLE_0:def 4;
then
A8: c in Y by XBOOLE_0:def 4;
c in dom f by A7,XBOOLE_0:def 4;
then c in Y /\ dom f by A8,XBOOLE_0:def 4;
hence r2 <= f.c by A6;
end;
hence thesis by Th71;
end;
registration
cluster constant -> bounded for real-valued Function;
coherence
proof
let f be real-valued Function;
per cases;
suppose
A1: f is empty;
reconsider z=0 as Real;
assume f is constant;
thus f is bounded_above
proof
take z;
let x be object;
thus thesis by A1;
end;
take z;
let x be object;
thus thesis by A1;
end;
suppose
A2: f is not empty;
assume f is constant;
then consider r such that
A3: for c being object st c in dom f holds f.c = r by A2,VALUED_0:15;
thus f is bounded_above
proof
take r+1;
let y be object;
assume y in dom f;
then f.y = r by A3;
hence thesis by XREAL_1:39;
end;
take r-1;
let y be object;
assume y in dom f;
then f.y = r by A3;
hence thesis by XREAL_1:231;
end;
end;
end;
theorem
X misses dom f implies f|X is bounded
proof
assume X /\ dom f = {};
then dom(f|X) = {} by RELAT_1:61;
then f|X = {};
hence thesis;
end;
theorem
(0(#)f)|Y is bounded
proof
reconsider p1 = 0 as Real;
set r = 0;
now
take p=p1;
let c be object;
assume c in Y /\ dom (r(#)f);
then
A1: c in dom (r(#)f) by XBOOLE_0:def 4;
r*f.c <= 0;
hence (r(#)f).c <= p by A1,VALUED_1:def 5;
end;
hence (r(#)f)|Y is bounded_above by Th70;
now
take p=p1;
let c be object;
assume c in Y /\ dom (r(#)f);
then
A2: c in dom (r(#)f) by XBOOLE_0:def 4;
0 <= r*f.c;
hence p <= (r(#)f).c by A2,VALUED_1:def 5;
end;
hence thesis by Th71;
end;
registration
let f be bounded_above real-valued Function, X be set;
cluster f|X -> bounded_above for real-valued Function;
coherence
proof
consider r such that
A1: for y being object st y in dom f holds f.y<r by SEQ_2:def 1;
f|X is bounded_above
proof
take r;
let y be object;
assume
A2: y in dom(f|X);
then y in dom f by RELAT_1:57;
then f.y < r by A1;
hence thesis by A2,FUNCT_1:47;
end;
hence thesis;
end;
end;
registration
let f be bounded_below real-valued Function, X be set;
cluster f|X -> bounded_below for real-valued Function;
coherence
proof
consider r such that
A1: for y being object st y in dom f holds r < f.y by SEQ_2:def 2;
f|X is bounded_below
proof
take r;
let y be object;
assume
A2: y in dom(f|X);
then y in dom f by RELAT_1:57;
then r < f.y by A1;
hence thesis by A2,FUNCT_1:47;
end;
hence thesis;
end;
end;
registration
let f be bounded_above real-valued Function;
let r be non negative Real;
cluster r(#)f -> bounded_above for real-valued Function;
coherence
proof
consider r1 such that
A1: for c being object st c in dom f holds f.c < r1 by SEQ_2:def 1;
now
take p = r*|.r1.|+1;
let c be object;
A2: r1 <= |.r1.| by ABSVALUE:4;
assume
A3: c in dom (r(#)f);
then c in dom f by VALUED_1:def 5;
then f.c < |.r1.| by A1,A2,XXREAL_0:2;
then r * (f.c) <= |.r1.|*r by XREAL_1:64;
then (r(#)f).c <= |.r1.|*r by A3,VALUED_1:def 5;
hence (r(#)f).c < p by XREAL_1:39;
end;
hence thesis;
end;
end;
registration
let f be bounded_below real-valued Function;
let r be non negative Real;
cluster r(#)f -> bounded_below for real-valued Function;
coherence
proof
consider r1 such that
A1: for c being object st c in dom f holds r1 < f.c by SEQ_2:def 2;
now
take p = r*(-|.r1.|)-1;
let c be object;
A2: -|.r1.| <= r1 by ABSVALUE:4;
assume
A3: c in dom (r(#)f);
then c in dom f by VALUED_1:def 5;
then f.c >= -|.r1.| by A1,A2,XXREAL_0:2;
then r * (f.c) >= (-|.r1.|)*r by XREAL_1:64;
then (r(#)f).c >= (-|.r1.|)*r by A3,VALUED_1:def 5;
hence (r(#)f).c > p by XREAL_1:231;
end;
hence thesis;
end;
end;
registration
let f be bounded_above real-valued Function;
let r be non positive Real;
cluster r(#)f -> bounded_below for real-valued Function;
coherence
proof
consider r1 such that
A1: for c being object st c in dom f holds f.c < r1 by SEQ_2:def 1;
now
take p=r*|.r1.|-1;
let c be object;
A2: r1<=|.r1.| by ABSVALUE:4;
assume
A3: c in dom (r(#)f);
then c in dom f by VALUED_1:def 5;
then f.c <= |.r1.| by A1,A2,XXREAL_0:2;
then r*|.r1.| <= r * f.c by XREAL_1:65;
then r*|.r1.| <= (r(#)f).c by A3,VALUED_1:def 5;
hence p < (r(#)f).c by XREAL_1:231;
end;
hence thesis;
end;
end;
registration
let f be bounded_below real-valued Function;
let r be non positive Real;
cluster r(#)f -> bounded_above for real-valued Function;
coherence
proof
consider r1 such that
A1: for c being object st c in dom f holds r1 < f.c by SEQ_2:def 2;
now
take p=r*(-|.r1.|)+1;
let c be object;
A2: -|.r1.| <= r1 by ABSVALUE:4;
assume
A3: c in dom (r(#)f);
then c in dom f by VALUED_1:def 5;
then -|.r1.| <= f.c by A1,A2,XXREAL_0:2;
then r * f.c <= r*(-|.r1.|) by XREAL_1:65;
then (r(#)f).c <= r*(-|.r1.|) by A3,VALUED_1:def 5;
hence (r(#)f).c < p by XREAL_1:39;
end;
hence thesis;
end;
end;
theorem Th78:
(f|Y is bounded_above & 0<=r implies (r(#)f)|Y is bounded_above)
& (f|Y is bounded_above & r<=0 implies (r(#)f)|Y is bounded_below)
proof
(r(#)f)|Y = r(#)(f|Y) by Th49;
hence thesis;
end;
theorem Th79:
(f|Y is bounded_below & 0<=r implies (r(#)f)|Y is bounded_below)
& (f|Y is bounded_below & r<=0 implies (r(#)f)|Y is bounded_above)
proof
(r(#)f)|Y = r(#)(f|Y) by Th49;
hence thesis;
end;
theorem Th80:
f|Y is bounded implies (r(#)f)|Y is bounded
proof
assume
A1: f|Y is bounded;
per cases;
suppose
A2: 0 <= r;
hence (r(#)f)|Y is bounded_above by A1,Th78;
thus thesis by A1,A2,Th79;
end;
suppose
A3: r <= 0;
hence (r(#)f)|Y is bounded_above by A1,Th79;
thus thesis by A1,A3,Th78;
end;
end;
registration
let f;
cluster abs f -> bounded_below;
coherence
proof
now
reconsider p = -1 as Real;
take p;
let c be object;
assume c in dom (abs(f));
0 <= |.f.c.| by COMPLEX1:46;
hence p < (abs(f)).c by VALUED_1:18;
end;
hence thesis;
end;
end;
theorem
(abs f)|X is bounded_below;
registration
let f be bounded real-valued Function;
cluster abs f -> bounded for real-valued Function;
coherence
proof
consider r1 such that
A1: for c being object st c in dom f holds |.f.c.| <= r1 by Th72;
now
take r1;
let c be object;
assume c in dom abs f;
then c in dom f by VALUED_1:def 11;
then |.|.f.c.|.| <= r1 by A1;
hence |.(abs f).c.| <= r1 by VALUED_1:18;
end;
hence thesis by Th72;
end;
end;
registration
let f be bounded_above real-valued Function;
cluster -f -> bounded_below for real-valued Function;
coherence;
end;
theorem Th82:
f|Y is bounded implies (abs f)|Y is bounded & (-f)|Y is bounded
proof
assume
A1: f|Y is bounded;
(abs f)|Y = abs(f|Y) by Th46;
hence (abs f)|Y is bounded by A1;
thus thesis by A1,Th80;
end;
reserve f1,f2 for real-valued Function;
registration
let f1,f2 be bounded_above real-valued Function;
cluster f1+f2 -> bounded_above for real-valued Function;
coherence
proof
consider r2 such that
A1: for c being object st c in dom f2 holds f2.c < r2 by SEQ_2:def 1;
consider r1 such that
A2: for c being object st c in dom f1 holds f1.c < r1 by SEQ_2:def 1;
now
take r=r1+r2;
let c be object;
assume
A3: c in dom (f1+f2);
then
A4: c in dom f1 /\ dom f2 by VALUED_1:def 1;
then c in dom f1 by XBOOLE_0:def 4;
then
A5: f1.c < r1 by A2;
c in dom f2 by A4,XBOOLE_0:def 4;
then f1.c + f2.c < r by A1,A5,XREAL_1:8;
hence (f1+f2).c < r by A3,VALUED_1:def 1;
end;
hence thesis;
end;
end;
registration
let f1,f2 be bounded_below real-valued Function;
cluster f1+f2 -> bounded_below for real-valued Function;
coherence
proof
consider r2 such that
A1: for c being object st c in dom f2 holds f2.c > r2 by SEQ_2:def 2;
consider r1 such that
A2: for c being object st c in dom f1 holds f1.c > r1 by SEQ_2:def 2;
now
take r=r1+r2;
let c be object;
assume
A3: c in dom (f1+f2);
then
A4: c in dom f1 /\ dom f2 by VALUED_1:def 1;
then c in dom f1 by XBOOLE_0:def 4;
then
A5: f1.c > r1 by A2;
c in dom f2 by A4,XBOOLE_0:def 4;
then f1.c + f2.c > r by A1,A5,XREAL_1:8;
hence (f1+f2).c > r by A3,VALUED_1:def 1;
end;
hence thesis;
end;
end;
theorem Th83:
(f1|X is bounded_above & f2|Y is bounded_above implies (f1+f2)|
(X /\ Y) is bounded_above) & (f1|X is bounded_below & f2|Y is bounded_below
implies (f1+f2)|(X /\ Y) is bounded_below) & (f1|X is bounded & f2|Y is bounded
implies (f1+f2)|(X /\ Y) is bounded)
proof
(f1+f2)|(X /\ Y) = f1|(X /\ Y)+f2|(X /\ Y) by Th44
.= f1|(X /\ Y)+f2|Y|X by RELAT_1:71
.= f1|X|Y+f2|Y|X by RELAT_1:71;
hence thesis;
end;
registration
let f1,f2 be bounded real-valued Function;
cluster f1(#)f2 -> bounded for real-valued Function;
coherence
proof
consider r2 such that
A1: for c being object st c in dom f2 holds |.f2.c.| <= r2 by Th72;
consider r1 such that
A2: for c being object st c in dom f1 holds |.f1.c.| <= r1 by Th72;
now
take r=r1*r2;
let c be object;
A3: 0<=|.f2.c.| by COMPLEX1:46;
assume c in dom (f1(#)f2);
then
A4: c in dom f1 /\ dom f2 by VALUED_1:def 4;
then c in dom f1 by XBOOLE_0:def 4;
then
A5: |.f1.c.| <= r1 by A2;
c in dom f2 by A4,XBOOLE_0:def 4;
then
A6: |.f2.c.| <= r2 by A1;
0<=|.f1.c.| by COMPLEX1:46;
then |.f1.c.|*|.f2.c.| <= r by A5,A6,A3,XREAL_1:66;
then |.f1.c * f2.c.| <= r by COMPLEX1:65;
hence |.(f1(#)f2).c.| <= r by VALUED_1:5;
end;
hence thesis by Th72;
end;
end;
theorem Th84:
f1|X is bounded & f2|Y is bounded implies (f1(#)f2)|(X /\ Y) is
bounded & (f1-f2)|(X /\ Y) is bounded
proof
assume that
A1: f1|X is bounded and
A2: f2|Y is bounded;
(f1(#)f2)|(X /\ Y) = f1|(X /\ Y)(#)f2|(X /\ Y) by Th45
.= f1|(X /\ Y)(#)f2|Y|X by RELAT_1:71
.= f1|X|Y(#)f2|Y|X by RELAT_1:71;
hence (f1(#)f2)|(X /\ Y) is bounded by A1,A2;
(-f2)|Y is bounded by A2,Th82;
hence thesis by A1,Th83;
end;
theorem Th85:
f|X is bounded_above & f|Y is bounded_above implies f|(X \/ Y)
is bounded_above
proof
assume that
A1: f|X is bounded_above and
A2: f|Y is bounded_above;
consider r1 such that
A3: for c being object st c in X /\ dom f holds f.c <= r1 by A1,Th70;
consider r2 such that
A4: for c being object st c in Y /\ dom f holds f.c <= r2 by A2,Th70;
now
take r = |.r1.| + |.r2.|;
let c be object;
assume
A5: c in (X \/ Y) /\ dom f;
then
A6: c in dom f by XBOOLE_0:def 4;
A7: c in X \/ Y by A5,XBOOLE_0:def 4;
now
per cases by A7,XBOOLE_0:def 3;
suppose
c in X;
then c in X /\ dom f by A6,XBOOLE_0:def 4;
then
A8: f.c <= r1 by A3;
A9: 0 <= |.r2.| by COMPLEX1:46;
r1 <= |.r1.| by ABSVALUE:4;
then f.c <= |.r1.| by A8,XXREAL_0:2;
then f.c + (0 qua Real) <= r by A9,XREAL_1:7;
hence f.c <= r;
end;
suppose
c in Y;
then c in Y /\ dom f by A6,XBOOLE_0:def 4;
then
A10: f.c <= r2 by A4;
A11: 0 <= |.r1.| by COMPLEX1:46;
r2 <= |.r2.| by ABSVALUE:4;
then f.c <= |.r2.| by A10,XXREAL_0:2;
then (0 qua Real) + f.c <= r by A11,XREAL_1:7;
hence f.c <= r;
end;
end;
hence f.c <= r;
end;
hence thesis by Th70;
end;
theorem Th86:
f|X is bounded_below & f|Y is bounded_below implies f|(X \/ Y)
is bounded_below
proof
assume that
A1: f|X is bounded_below and
A2: f|Y is bounded_below;
consider r1 such that
A3: for c being object st c in X /\ dom f holds r1 <= f.c by A1,Th71;
consider r2 such that
A4: for c being object st c in Y /\ dom f holds r2 <= f.c by A2,Th71;
now
take r = -|.r1.| - |.r2.|;
let c be object;
assume
A5: c in (X \/ Y) /\ dom f;
then
A6: c in dom f by XBOOLE_0:def 4;
A7: c in X \/ Y by A5,XBOOLE_0:def 4;
now
per cases by A7,XBOOLE_0:def 3;
suppose
c in X;
then c in X /\ dom f by A6,XBOOLE_0:def 4;
then
A8: r1 <= f.c by A3;
A9: 0 <= |.r2.| by COMPLEX1:46;
-|.r1.| <= r1 by ABSVALUE:4;
then -|.r1.| <= f.c by A8,XXREAL_0:2;
then r <= f.c - 0 by A9,XREAL_1:13;
hence r <= f.c;
end;
suppose
c in Y;
then c in Y /\ dom f by A6,XBOOLE_0:def 4;
then
A10: r2 <= f.c by A4;
A11: 0 <= |.r1.| by COMPLEX1:46;
-|.r2.| <= r2 by ABSVALUE:4;
then -|.r2.| <= f.c by A10,XXREAL_0:2;
then -|.r2.| - |.r1.| <= f.c - 0 by A11,XREAL_1:13;
hence r <= f.c;
end;
end;
hence r <= f.c;
end;
hence thesis by Th71;
end;
theorem
f|X is bounded & f|Y is bounded implies f|(X \/ Y) is bounded
by Th85,Th86;
reserve f,f1,f2 for PartFunc of C,REAL;
registration
let C;
let f1,f2 be constant PartFunc of C,REAL;
cluster f1+f2 -> constant;
coherence
proof
consider r2 being Element of REAL such that
A1: for c st c in dom f2 holds f2.c = r2 by PARTFUN2:def 1;
consider r1 being Element of REAL such that
A2: for c st c in dom f1 holds f1.c = r1 by PARTFUN2:def 1;
now
let c;
assume
A3: c in dom(f1+f2);
then
A4: c in dom f1 /\ dom f2 by VALUED_1:def 1;
then
A5: c in dom f1 by XBOOLE_0:def 4;
A6: c in dom f2 by A4,XBOOLE_0:def 4;
thus (f1+f2).c = f1.c + f2.c by A3,VALUED_1:def 1
.= f1.c + r2 by A1,A6
.= r1+r2 by A2,A5;
end;
hence thesis by PARTFUN2:def 1;
end;
cluster f1-f2 -> constant;
coherence
proof
consider r2 being Element of REAL such that
A7: for c st c in dom f2 holds f2.c = r2 by PARTFUN2:def 1;
consider r1 being Element of REAL such that
A8: for c st c in dom f1 holds f1.c = r1 by PARTFUN2:def 1;
now
let c;
assume
A9: c in dom(f1-f2);
then
A10: c in dom f1 /\ dom f2 by VALUED_1:12;
then
A11: c in dom f1 by XBOOLE_0:def 4;
A12: c in dom f2 by A10,XBOOLE_0:def 4;
thus (f1-f2).c = f1.c - f2.c by A9,VALUED_1:13
.= f1.c - r2 by A7,A12
.= r1-r2 by A8,A11;
end;
hence thesis by PARTFUN2:def 1;
end;
cluster f1(#)f2 -> constant;
coherence
proof
consider r2 being Element of REAL such that
A13: for c st c in dom f2 holds f2.c = r2 by PARTFUN2:def 1;
consider r1 being Element of REAL such that
A14: for c st c in dom f1 holds f1.c = r1 by PARTFUN2:def 1;
now
let c;
assume
A15: c in dom(f1(#)f2);
then
A16: c in dom f1 /\ dom f2 by VALUED_1:def 4;
then
A17: c in dom f1 by XBOOLE_0:def 4;
A18: c in dom f2 by A16,XBOOLE_0:def 4;
thus (f1(#)f2).c = f1.c * f2.c by A15,VALUED_1:def 4
.= f1.c * r2 by A13,A18
.= r1*r2 by A14,A17;
end;
hence thesis by PARTFUN2:def 1;
end;
end;
theorem
f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is
constant & (f1-f2)|(X /\ Y) is constant & (f1(#)f2)|(X /\ Y) is constant
proof
assume that
A1: f1|X is constant and
A2: f2|Y is constant;
consider r1 be Element of REAL such that
A3: for c st c in X /\ dom f1 holds f1.c = r1 by A1,PARTFUN2:57;
consider r2 be Element of REAL such that
A4: for c st c in Y /\ dom f2 holds f2.c = r2 by A2,PARTFUN2:57;
now
let c;
assume
A5: c in X /\ Y /\ dom (f1+f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1+f2) by A5,XBOOLE_0:def 4;
then
A9: c in (dom f1 /\ dom f2) by VALUED_1:def 1;
then c in dom f1 by XBOOLE_0:def 4;
then
A10: c in X /\ dom f1 by A7,XBOOLE_0:def 4;
A11: c in Y by A6,XBOOLE_0:def 4;
c in dom f2 by A9,XBOOLE_0:def 4;
then
A12: c in Y /\ dom f2 by A11,XBOOLE_0:def 4;
thus (f1+f2).c =f1.c + f2.c by A8,VALUED_1:def 1
.= r1 + f2.c by A3,A10
.= r1 + r2 by A4,A12;
end;
hence (f1+f2)|(X /\ Y) is constant by PARTFUN2:57;
now
let c;
assume
A13: c in X /\ Y /\ dom (f1-f2);
then
A14: c in X /\ Y by XBOOLE_0:def 4;
then
A15: c in X by XBOOLE_0:def 4;
A16: c in dom (f1-f2) by A13,XBOOLE_0:def 4;
then
A17: c in (dom f1 /\ dom f2) by VALUED_1:12;
then c in dom f1 by XBOOLE_0:def 4;
then
A18: c in X /\ dom f1 by A15,XBOOLE_0:def 4;
A19: c in Y by A14,XBOOLE_0:def 4;
c in dom f2 by A17,XBOOLE_0:def 4;
then
A20: c in Y /\ dom f2 by A19,XBOOLE_0:def 4;
thus (f1-f2).c = f1.c - f2.c by A16,VALUED_1:13
.= r1 - f2.c by A3,A18
.= r1 - r2 by A4,A20;
end;
hence (f1-f2)|(X /\ Y) is constant by PARTFUN2:57;
now
let c;
assume
A21: c in X /\ Y /\ dom (f1(#)f2);
then
A22: c in X /\ Y by XBOOLE_0:def 4;
c in dom (f1(#)f2) by A21,XBOOLE_0:def 4;
then
A23: c in (dom f1 /\ dom f2) by VALUED_1:def 4;
then
A24: c in dom f1 by XBOOLE_0:def 4;
A25: c in dom f2 by A23,XBOOLE_0:def 4;
c in Y by A22,XBOOLE_0:def 4;
then
A26: c in Y /\ dom f2 by A25,XBOOLE_0:def 4;
c in X by A22,XBOOLE_0:def 4;
then
A27: c in X /\ dom f1 by A24,XBOOLE_0:def 4;
thus (f1(#)f2).c =f1.c * f2.c by VALUED_1:5
.= r1 * f2.c by A3,A27
.= r1 * r2 by A4,A26;
end;
hence thesis by PARTFUN2:57;
end;
registration
let C;
let f be constant PartFunc of C,REAL;
cluster -f -> constant;
coherence
proof
consider r be Element of REAL such that
A1: for c be Element of C st c in dom f holds f.c = r by PARTFUN2:def 1;
now
take p=-r;
let c be Element of C;
assume c in dom (-f);
then c in dom f by VALUED_1:8;
then -f.c = p by A1;
hence (-f).c = p by VALUED_1:8;
end;
hence thesis by PARTFUN2:def 1;
end;
cluster abs f -> constant;
coherence
proof
consider r be Element of REAL such that
A2: for c be Element of C st c in dom f holds f.c = r by PARTFUN2:def 1;
now
reconsider p= |.r.| as Element of REAL by XREAL_0:def 1;
take p;
let c be Element of C;
assume c in dom (abs f);
then c in dom f by VALUED_1:def 11;
then |.f.c.| = p by A2;
hence (abs f).c = p by VALUED_1:18;
end;
hence thesis by PARTFUN2:def 1;
end;
let p;
cluster p(#)f -> constant;
coherence
proof
consider r be Element of REAL such that
A3: for c be Element of C st c in dom f holds f.c = r by PARTFUN2:def 1;
now
reconsider r1= p*r as Element of REAL by XREAL_0:def 1;
take r1;
let c be Element of C;
assume c in dom (p(#)f);
then c in dom f by VALUED_1:def 5;
then p*(f.c) = r1 by A3;
hence (p(#)f).c = r1 by VALUED_1:6;
end;
hence thesis by PARTFUN2:def 1;
end;
end;
theorem Th89:
f|Y is constant implies (p(#)f)|Y is constant
proof
(p(#)f)|Y = p(#)(f|Y) by Th49;
hence thesis;
end;
theorem Th90:
f|Y is constant implies (-f)|Y is constant
proof
(-f)|Y = -(f|Y) by Th46;
hence thesis;
end;
theorem Th91:
f|Y is constant implies (abs f)|Y is constant
proof
(abs f)|Y = abs(f|Y) by Th46;
hence thesis;
end;
theorem
f|Y is constant implies (for r holds (r(#)f)|Y is bounded) & (-f)|Y is
bounded & (abs f)|Y is bounded
proof
assume
A1: f|Y is constant;
hereby
let r;
(r(#)f)|Y is constant by A1,Th89;
hence (r(#)f)|Y is bounded;
end;
(-f)|Y is constant by A1,Th90;
hence (-f)|Y is bounded;
(abs f)|Y is constant by A1,Th91;
hence thesis;
end;
theorem
(f1|X is bounded_above & f2|Y is constant implies (f1+f2)|(X /\ Y) is
bounded_above) & (f1|X is bounded_below & f2|Y is constant implies (f1+f2)|(X
/\ Y) is bounded_below) & (f1|X is bounded & f2|Y is constant implies (f1+f2)|(
X /\ Y) is bounded) by Th83;
theorem
(f1|X is bounded_above & f2|Y is constant implies (f1-f2)|(X /\ Y) is
bounded_above) & (f1|X is bounded_below & f2|Y is constant implies (f1-f2)|(X
/\ Y) is bounded_below) & (f1|X is bounded & f2|Y is constant implies (f1-f2)|(
X /\ Y) is bounded & (f2-f1)|(X /\ Y) is bounded& (f1(#)f2)|(X /\ Y) is bounded
)
proof
thus f1|X is bounded_above & f2|Y is constant implies (f1-f2)|(X /\ Y) is
bounded_above
proof
assume that
A1: f1|X is bounded_above and
A2: f2|Y is constant;
(-f2)|Y is constant by A2,Th90;
hence thesis by A1,Th83;
end;
thus f1|X is bounded_below & f2|Y is constant implies (f1-f2)|(X /\ Y) is
bounded_below
proof
assume that
A3: f1|X is bounded_below and
A4: f2|Y is constant;
(-f2)|Y is constant by A4,Th90;
hence thesis by A3,Th83;
end;
assume that
A5: f1|X is bounded and
A6: f2|Y is constant;
(-f2)|Y is constant by A6,Th90;
hence (f1-f2)|(X /\ Y) is bounded by A5,Th83;
thus (f2-f1)|(X /\ Y) is bounded by A5,A6,Th84;
thus thesis by A5,A6,Th84;
end;