:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-2016 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, ARYTM_3, XXREAL_0, CARD_1, RELAT_1, SQUARE_1, FUNCT_1,
TARSKI, XBOOLE_0, FUNCOP_1, ARYTM_1, SUBSET_1, VALUED_0, ORDINAL4,
PARTFUN1, VALUED_1, XCMPLX_0, PRALG_1, COMPLEX1, MEMBERED, PARTFUN3,
REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, COMPLEX1, MEMBERED, SQUARE_1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, MEASURE6, VALUED_0,
VALUED_1, RFUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1,
FUNCOP_1;
constructors REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, RFUNCT_1, MEASURE6,
FUNCOP_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions RELAT_1, VALUED_0;
equalities VALUED_1, ORDINAL1;
expansions RELAT_1;
theorems TARSKI, FUNCT_2, FUNCT_1, XBOOLE_0, FUNCOP_1, RFUNCT_1, SQUARE_1,
XCMPLX_0, XREAL_1, COMPLEX1, VALUED_0, VALUED_1, RELSET_1, XREAL_0,
ORDINAL1;
schemes FUNCT_1;
begin
registration
let r be Real;
cluster r/r -> non negative;
coherence
proof
r <= 0 or 0 <= r;
hence thesis;
end;
end;
registration
let r be Real;
cluster r*r -> non negative;
coherence by XREAL_1:63;
cluster r*(r") -> non negative;
coherence
proof
r*(r") = r/r by XCMPLX_0:def 9;
hence thesis;
end;
end;
registration
let r be non negative Real;
cluster sqrt r -> non negative;
coherence by SQUARE_1:def 2;
end;
registration
let r be positive Real;
cluster sqrt r -> positive;
coherence by SQUARE_1:25;
end;
theorem
for f being Function, A being set st f is one-to-one & A c= dom (f")
holds f.:(f".:A) = A
proof
let f be Function, A be set;
assume that
A1: f is one-to-one and
A2: A c= dom (f");
f"".:(f".:A)=A by A1,A2,FUNCT_1:107;
hence thesis by A1,FUNCT_1:43;
end;
registration
let f be non-empty Function;
cluster f"{0} -> empty;
coherence
proof
assume not thesis;
then consider x being object such that
A1: x in f"{0} by XBOOLE_0:def 1;
x in dom f by A1,FUNCT_1:def 7;
then
A2: f.x in rng f by FUNCT_1:def 3;
f.x in {0} by A1,FUNCT_1:def 7;
then f.x = 0 by TARSKI:def 1;
hence thesis by A2;
end;
end;
definition
let R be Relation;
attr R is positive-yielding means
:Def1:
for r being Real st r in rng R holds 0 < r;
attr R is negative-yielding means
:Def2:
for r being Real st r in rng R holds 0 > r;
attr R is nonpositive-yielding means
:Def3:
for r being Real st r in rng R holds 0 >= r;
attr R is nonnegative-yielding means
:Def4:
for r being Real st r in rng R holds 0 <= r;
end;
registration
let X be set, r be positive Real;
cluster X --> r -> positive-yielding;
coherence
proof
let x be Real;
assume x in rng (X --> r);
hence thesis by TARSKI:def 1;
end;
end;
registration
let X be set, r be negative Real;
cluster X --> r -> negative-yielding;
coherence
proof
let x be Real;
assume x in rng (X --> r);
hence thesis by TARSKI:def 1;
end;
end;
registration
let X be set, r be non positive Real;
cluster X --> r -> nonpositive-yielding;
coherence
proof
let x be Real;
assume x in rng (X --> r);
hence thesis by TARSKI:def 1;
end;
end;
registration
let X be set, r be non negative Real;
cluster X --> r -> nonnegative-yielding;
coherence
proof
let x be Real;
assume x in rng (X --> r);
hence thesis by TARSKI:def 1;
end;
end;
registration
let X be non empty set;
cluster X --> 0 -> non non-empty;
coherence
proof
rng (X --> 0) = {0} by FUNCOP_1:8;
hence {} in rng (X --> 0) by TARSKI:def 1;
end;
end;
registration
cluster positive-yielding -> nonnegative-yielding non-empty for Relation;
coherence;
cluster negative-yielding -> nonpositive-yielding non-empty for Relation;
coherence;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
registration
let X be set;
cluster negative-yielding for Function of X,REAL;
existence
proof
take X --> -jj;
thus thesis;
end;
cluster positive-yielding for Function of X,REAL;
existence
proof
take X --> jj;
thus thesis;
end;
end;
registration
cluster non-empty real-valued for Function;
existence
proof
set f = the non-empty Function of 0,REAL;
take f;
thus thesis;
end;
end;
theorem Th2:
for f being non-empty real-valued Function holds dom(f^) = dom f
proof
let f be non-empty real-valued Function;
thus dom (f^) = dom f \ f"{0} by RFUNCT_1:def 2
.= dom f;
end;
theorem Th3:
for X being non empty set, f being PartFunc of X,REAL, g being
non-empty PartFunc of X,REAL holds dom(f/g) = dom f /\ dom g
proof
let X be non empty set, f be PartFunc of X,REAL, g be non-empty PartFunc of
X,REAL;
thus dom (f/g) = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1
.= dom f /\ dom g;
end;
registration
let X be set;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster f+g -> nonpositive-yielding;
coherence
proof
let r be Real;
set R = f+g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 1;
then x in dom g by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non positive Real by A4,Def3;
a+b is non positive;
hence thesis by A1,A2,VALUED_1:def 1;
end;
end;
registration
let X be set;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster f+g -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f+g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 1;
then x in dom g by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non negative Real by A4,Def4;
a+b is non negative;
hence thesis by A1,A2,VALUED_1:def 1;
end;
end;
registration
let X be set;
let f be positive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster f+g -> positive-yielding;
coherence
proof
let r be Real;
set R = f+g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 1;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non negative Real by Def4;
a+b is positive;
hence thesis by A1,A2,VALUED_1:def 1;
end;
end;
registration
let X be set;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
cluster f+g -> positive-yielding;
coherence;
end;
registration
let X be set;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
cluster f+g -> negative-yielding;
coherence
proof
let r be Real;
set R = f+g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 1;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as negative Real by Def2;
a+b is negative;
hence thesis by A1,A2,VALUED_1:def 1;
end;
end;
registration
let X be set;
let f be negative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster f+g -> negative-yielding;
coherence;
end;
registration
let X be set;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster f-g -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f-g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:12;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non positive Real by Def3;
a-b is non negative;
hence thesis by A1,A2,VALUED_1:13;
end;
end;
registration
let X be set;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster f-g -> nonpositive-yielding;
coherence
proof
let r be Real;
set R = f-g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:12;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non negative Real by Def4;
a-b is non positive;
hence thesis by A1,A2,VALUED_1:13;
end;
end;
registration
let X be set;
let f be positive-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster f-g -> positive-yielding;
coherence
proof
let r be Real;
set R = f-g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:12;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non positive Real by Def3;
a-b is positive;
hence thesis by A1,A2,VALUED_1:13;
end;
end;
registration
let X be set;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
cluster f-g -> negative-yielding;
coherence
proof
let r be Real;
set R = f-g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:12;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as positive Real by Def1;
a-b is negative;
hence thesis by A1,A2,VALUED_1:13;
end;
end;
registration
let X be set;
let f be negative-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster f-g -> negative-yielding;
coherence
proof
let r be Real;
set R = f-g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:12;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as negative Real by Def2;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non negative Real by Def4;
a-b is negative;
hence thesis by A1,A2,VALUED_1:13;
end;
end;
registration
let X be set;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
cluster f-g -> positive-yielding;
coherence
proof
let r be Real;
set R = f-g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:12;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as negative Real by Def2;
a-b is positive;
hence thesis by A1,A2,VALUED_1:13;
end;
end;
registration
let X be set;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster f(#)g -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f(#)g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 4;
then x in dom g by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non positive Real by A4,Def3;
a*b is non negative;
hence thesis by A2,VALUED_1:5;
end;
end;
registration
let X be set;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster f(#)g -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f(#)g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 4;
then x in dom g by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non negative Real by A4,Def4;
a*b is non negative;
hence thesis by A2,VALUED_1:5;
end;
end;
registration
let X be set;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster f(#)g -> nonpositive-yielding;
coherence
proof
let r be Real;
set R = f(#)g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 4;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non negative Real by Def4;
a*b is non positive;
hence thesis by A2,VALUED_1:5;
end;
end;
registration
let X be set;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster f(#)g -> nonpositive-yielding;
coherence;
end;
registration
let X be set;
let f be positive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
cluster f(#)g -> negative-yielding;
coherence
proof
let r be Real;
set R = f(#)g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 4;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
x in dom g by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as negative Real by Def2;
a*b is negative;
hence thesis by A2,VALUED_1:5;
end;
end;
registration
let X be set;
let f be negative-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
cluster f(#)g -> negative-yielding;
coherence;
end;
registration
let X be set;
let f, g be positive-yielding PartFunc of X,REAL;
cluster f(#)g -> positive-yielding;
coherence
proof
let r be Real;
set R = f(#)g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 4;
then x in dom g by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as positive Real by A4,Def1;
a*b is positive;
hence thesis by A2,VALUED_1:5;
end;
end;
registration
let X be set;
let f, g be negative-yielding PartFunc of X,REAL;
cluster f(#)g -> positive-yielding;
coherence
proof
let r be Real;
set R = f(#)g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 4;
then x in dom g by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as negative Real by A4,Def2;
a*b is positive;
hence thesis by A2,VALUED_1:5;
end;
end;
registration
let X be set;
let f, g be non-empty PartFunc of X,REAL;
cluster f(#)g -> non-empty;
coherence
proof
set R = f(#)g;
assume not thesis;
then 0 in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = 0 by FUNCT_1:def 3;
A3: dom R = dom f /\ dom g by VALUED_1:def 4;
then x in dom g by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non zero Real by A4;
a*b is non zero;
hence thesis by A2,VALUED_1:5;
end;
end;
registration
let X be set;
let f be PartFunc of X,REAL;
cluster f(#)f -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f(#)f;
assume r in rng R;
then consider x being object such that
x in dom R and
A1: R.x = r by FUNCT_1:def 3;
f.x * f.x is non negative;
hence thesis by A1,VALUED_1:5;
end;
end;
registration
let X be set;
let r be non positive Real;
let f be nonpositive-yielding PartFunc of X,REAL;
cluster r(#)f -> nonnegative-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
r*a is non negative;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be non negative Real;
let f be nonnegative-yielding PartFunc of X,REAL;
cluster r(#)f -> nonnegative-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
r*a is non negative;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be non positive Real;
let f be nonnegative-yielding PartFunc of X,REAL;
cluster r(#)f -> nonpositive-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
r*a is non positive;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be non negative Real;
let f be nonpositive-yielding PartFunc of X,REAL;
cluster r(#)f -> nonpositive-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
r*a is non positive;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be positive Real;
let f be negative-yielding PartFunc of X,REAL;
cluster r(#)f -> negative-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as negative Real by Def2;
r*a is negative;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be negative Real;
let f be positive-yielding PartFunc of X,REAL;
cluster r(#)f -> negative-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
r*a is negative;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be positive Real;
let f be positive-yielding PartFunc of X,REAL;
cluster r(#)f -> positive-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
r*a is positive;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be negative Real;
let f be negative-yielding PartFunc of X,REAL;
cluster r(#)f -> positive-yielding;
coherence
proof
let z be Real;
set R = r(#)f;
assume z in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = z by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as negative Real by Def2;
r*a is positive;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be set;
let r be non zero Real;
let f be non-empty PartFunc of X,REAL;
cluster r(#)f -> non-empty;
coherence
proof
set R = r(#)f;
assume not thesis;
then 0 in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = 0 by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non zero Real;
r*a is non zero;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
registration
let X be non empty set;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster f/g -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom g \ g"{0} by A1,XBOOLE_0:def 4;
then x in dom g by XBOOLE_0:def 5;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non positive Real by A4,Def3;
a*b" is non negative;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster f/g -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom g \ g"{0} by A1,XBOOLE_0:def 4;
then x in dom g by XBOOLE_0:def 5;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non negative Real by A4,Def4;
a*b" is non negative;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster f/g -> nonpositive-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
x in dom g \ g"{0} by A1,A3,XBOOLE_0:def 4;
then x in dom g by XBOOLE_0:def 5;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non negative Real by Def4;
a*b" is non positive;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster f/g -> nonpositive-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
x in dom g \ g"{0} by A1,A3,XBOOLE_0:def 4;
then x in dom g by XBOOLE_0:def 5;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as non positive Real by Def3;
a*b" is non positive;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f be positive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
cluster f/g -> negative-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
x in dom g \ g"{0} by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as negative Real by Def2;
a*b" is negative;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f be negative-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
cluster f/g -> negative-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom f by A1,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as negative Real by Def2;
x in dom g \ g"{0} by A1,A3,XBOOLE_0:def 4;
then g.x in rng g by FUNCT_1:def 3;
then reconsider b = g.x as positive Real by Def1;
a*b" is negative;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f, g be positive-yielding PartFunc of X,REAL;
cluster f/g -> positive-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom g \ g"{0} by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as positive Real by A4,Def1;
a*b" is positive;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f, g be negative-yielding PartFunc of X,REAL;
cluster f/g -> positive-yielding;
coherence
proof
let r be Real;
set R = f/g;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom g \ g"{0} by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as negative Real by A4,Def2;
a*b" is positive;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f be PartFunc of X,REAL;
cluster f/f -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f/f;
assume r in rng R;
then consider x being object such that
A1: x in dom R & R.x = r by FUNCT_1:def 3;
f.x * (f.x)" is non negative;
hence thesis by A1,RFUNCT_1:def 1;
end;
end;
registration
let X be non empty set;
let f, g be non-empty PartFunc of X,REAL;
cluster f/g -> non-empty;
coherence
proof
set R = f/g;
assume not thesis;
then 0 in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = 0 by FUNCT_1:def 3;
A3: dom R = dom f /\ (dom g \ g"{0}) by RFUNCT_1:def 1;
then x in dom g \ g"{0} by A1,XBOOLE_0:def 4;
then
A4: g.x in rng g by FUNCT_1:def 3;
x in dom f by A1,A3,XBOOLE_0:def 4;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as non zero Real by A4;
a*b" is non zero;
hence thesis by A1,A2,RFUNCT_1:def 1;
end;
end;
registration
let X be set;
let f be nonpositive-yielding Function of X,REAL;
cluster Inv f -> nonpositive-yielding;
coherence
proof
let r be Real;
set R = Inv f;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = X by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
a" is non positive;
hence thesis by A2,VALUED_1:10;
end;
end;
registration
let X be set;
let f be nonnegative-yielding Function of X,REAL;
cluster Inv f -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = Inv f;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = X by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
a" is non negative;
hence thesis by A2,VALUED_1:10;
end;
end;
registration
let X be set;
let f be positive-yielding Function of X,REAL;
cluster Inv f -> positive-yielding;
coherence
proof
let r be Real;
set R = Inv f;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = X by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
a" is positive;
hence thesis by A2,VALUED_1:10;
end;
end;
registration
let X be set;
let f be negative-yielding Function of X,REAL;
cluster Inv f -> negative-yielding;
coherence
proof
let r be Real;
set R = Inv f;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = X by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as negative Real by Def2;
a" is negative;
hence thesis by A2,VALUED_1:10;
end;
end;
registration
let X be set;
let f be non-empty Function of X,REAL;
cluster Inv f -> non-empty;
coherence
proof
set R = Inv f;
assume not thesis;
then 0 in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = 0 by FUNCT_1:def 3;
dom R = X by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
then reconsider a = f.x as non zero Real by A1,ORDINAL1:def 16;
a" is non zero;
hence thesis by A2,VALUED_1:10;
end;
end;
registration
let X be set;
let f be non-empty Function of X,REAL;
cluster -f -> non-empty;
coherence;
end;
registration
let X be set;
let f be nonpositive-yielding Function of X,REAL;
cluster -f -> nonnegative-yielding;
coherence;
end;
registration
let X be set;
let f be nonnegative-yielding Function of X,REAL;
cluster -f -> nonpositive-yielding;
coherence;
end;
registration
let X be set;
let f be positive-yielding Function of X,REAL;
cluster -f -> negative-yielding;
coherence;
end;
registration
let X be set;
let f be negative-yielding Function of X,REAL;
cluster -f -> positive-yielding;
coherence;
end;
registration
let X be set;
let f be Function of X,REAL;
cluster abs f -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = abs f;
assume r in rng R;
then consider x being object such that
x in dom R and
A1: R.x = r by FUNCT_1:def 3;
|.f.x.| is non negative by COMPLEX1:46;
hence thesis by A1,VALUED_1:18;
end;
end;
registration
let X be set;
let f be non-empty Function of X,REAL;
cluster abs f -> positive-yielding;
coherence
proof
let r be Real;
set R = abs f;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = dom f by VALUED_1:def 11;
then reconsider a = f.x as non zero Real by A1,ORDINAL1:def 16;
|.a.| is positive by COMPLEX1:47;
hence thesis by A2,VALUED_1:18;
end;
end;
registration
let X be non empty set;
let f be nonpositive-yielding Function of X,REAL;
cluster f^ -> nonpositive-yielding;
coherence
proof
let r be Real;
set R = f^;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = dom f \ f"{0} by RFUNCT_1:def 2;
then x in dom f by A1,XBOOLE_0:def 5;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non positive Real by Def3;
a" is non positive;
hence thesis by A1,A2,RFUNCT_1:def 2;
end;
end;
registration
let X be non empty set;
let f be nonnegative-yielding Function of X,REAL;
cluster f^ -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = f^;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = dom f \ f"{0} by RFUNCT_1:def 2;
then x in dom f by A1,XBOOLE_0:def 5;
then f.x in rng f by FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
a" is non negative;
hence thesis by A1,A2,RFUNCT_1:def 2;
end;
end;
registration
let X be non empty set;
let f be positive-yielding Function of X,REAL;
cluster f^ -> positive-yielding;
coherence
proof
let r be Real;
set R = f^;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = dom f by Th2;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
a" is positive;
hence thesis by A1,A2,RFUNCT_1:def 2;
end;
end;
registration
let X be non empty set;
let f be negative-yielding Function of X,REAL;
cluster f^ -> negative-yielding;
coherence
proof
let r be Real;
set R = f^;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = dom f by Th2;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as negative Real by Def2;
a" is negative;
hence thesis by A1,A2,RFUNCT_1:def 2;
end;
end;
registration
let X be non empty set;
let f be non-empty Function of X,REAL;
cluster f^ -> non-empty;
coherence
proof
set R = f^;
assume not thesis;
then 0 in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = 0 by FUNCT_1:def 3;
dom R = dom f by Th2;
then reconsider a = f.x as non zero Real by A1,ORDINAL1:def 16;
a" is non zero;
hence thesis by A1,A2,RFUNCT_1:def 2;
end;
end;
definition
let f be real-valued Function;
func sqrt f -> Function means
:Def5:
dom it = dom f & for x being object st x in dom it holds it.x = sqrt(f.x);
existence
proof
deffunc F(object) = sqrt (f.$1);
ex h being Function st dom h = dom f & for x being object st x in dom f
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 and
A2: for c being object st c in dom h holds h.c = sqrt (f.c) and
A3: dom g = dom f and
A4: for c being object st c in dom g holds g.c = sqrt (f.c);
now
let x be object;
assume
A5: x in dom h;
hence h.x = sqrt (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 real-valued Function;
cluster sqrt f -> real-valued;
coherence
proof
let x be object;
set F = sqrt f;
assume x in dom F;
then F.x = sqrt(f.x) by Def5;
hence thesis;
end;
end;
definition
let C be set, D be real-membered set, f be PartFunc of C,D;
redefine func sqrt f -> PartFunc of C,REAL;
coherence
proof
set F = sqrt f;
dom F = dom f & rng F c= REAL by Def5,VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
registration
let X be set;
let f be nonnegative-yielding Function of X,REAL;
cluster sqrt f -> nonnegative-yielding;
coherence
proof
let r be Real;
set R = sqrt f;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = dom f by Def5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as non negative Real by Def4;
sqrt a is non negative;
hence thesis by A1,A2,Def5;
end;
end;
registration
let X be set;
let f be positive-yielding Function of X,REAL;
cluster sqrt f -> positive-yielding;
coherence
proof
let r be Real;
set R = sqrt f;
assume r in rng R;
then consider x being object such that
A1: x in dom R and
A2: R.x = r by FUNCT_1:def 3;
dom R = dom f by Def5;
then f.x in rng f by A1,FUNCT_1:def 3;
then reconsider a = f.x as positive Real by Def1;
sqrt a is positive;
hence thesis by A1,A2,Def5;
end;
end;
definition
let X be set, f be Function of X, REAL;
redefine func sqrt f -> Function of X,REAL;
coherence
proof
dom sqrt f = dom f by Def5
.= X by FUNCT_2:def 1;
hence thesis by FUNCT_2:def 1;
end;
end;
definition
let X be set, f be non-empty Function of X, REAL;
redefine func f^ -> Function of X,REAL;
coherence
proof
dom (f^) = dom f by Th2
.= X by FUNCT_2:def 1;
hence thesis by FUNCT_2:def 1;
end;
end;
definition
let X be non empty set, f be Function of X, REAL, g be non-empty Function of
X, REAL;
redefine func f/g -> Function of X,REAL;
coherence
proof
dom (f/g) = dom f /\ dom g by Th3
.= X /\ dom g by FUNCT_2:def 1
.= X /\ X by FUNCT_2:def 1;
hence thesis by FUNCT_2:def 1;
end;
end;