:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
begin
registration
let
r
be
real
number
;
cluster
r
/
r
->
non
negative
;
coherence
not
r
/
r
is
negative
proof
end;
end;
registration
let
r
be
real
number
;
cluster
r
*
r
->
non
negative
;
coherence
not
r
*
r
is
negative
by
XREAL_1:63
;
cluster
r
*
(
r
"
)
->
non
negative
;
coherence
not
r
*
(
r
"
)
is
negative
proof
end;
end;
registration
let
r
be
real
non
negative
number
;
cluster
sqrt
r
->
non
negative
;
coherence
not
sqrt
r
is
negative
by
SQUARE_1:def 2
;
end;
registration
let
r
be
real
positive
number
;
cluster
sqrt
r
->
positive
;
coherence
sqrt
r
is
positive
by
SQUARE_1:25
;
end;
theorem
:: PARTFUN3:1
for
f
being
Function
for
A
being
set
st
f
is
one-to-one
&
A
c=
dom
(
f
"
)
holds
f
.:
(
(
f
"
)
.:
A
)
=
A
proof
end;
registration
let
f
be
non-empty
Function
;
cluster
f
"
{
0
}
->
empty
;
coherence
f
"
{
0
}
is
empty
proof
end;
end;
definition
let
R
be
Relation
;
attr
R
is
positive-yielding
means
:
Def1
:
:: PARTFUN3:def 1
for
r
being
real
number
st
r
in
rng
R
holds
0
<
r
;
attr
R
is
negative-yielding
means
:
Def2
:
:: PARTFUN3:def 2
for
r
being
real
number
st
r
in
rng
R
holds
0
>
r
;
attr
R
is
nonpositive-yielding
means
:
Def3
:
:: PARTFUN3:def 3
for
r
being
real
number
st
r
in
rng
R
holds
0
>=
r
;
attr
R
is
nonnegative-yielding
means
:
Def4
:
:: PARTFUN3:def 4
for
r
being
real
number
st
r
in
rng
R
holds
0
<=
r
;
end;
::
deftheorem
Def1
defines
positive-yielding
PARTFUN3:def 1 :
for
R
being
Relation
holds
(
R
is
positive-yielding
iff for
r
being
real
number
st
r
in
rng
R
holds
0
<
r
);
::
deftheorem
Def2
defines
negative-yielding
PARTFUN3:def 2 :
for
R
being
Relation
holds
(
R
is
negative-yielding
iff for
r
being
real
number
st
r
in
rng
R
holds
0
>
r
);
::
deftheorem
Def3
defines
nonpositive-yielding
PARTFUN3:def 3 :
for
R
being
Relation
holds
(
R
is
nonpositive-yielding
iff for
r
being
real
number
st
r
in
rng
R
holds
0
>=
r
);
::
deftheorem
Def4
defines
nonnegative-yielding
PARTFUN3:def 4 :
for
R
being
Relation
holds
(
R
is
nonnegative-yielding
iff for
r
being
real
number
st
r
in
rng
R
holds
0
<=
r
);
registration
let
X
be
set
;
let
r
be
real
positive
number
;
cluster
X
-->
r
->
positive-yielding
;
coherence
X
-->
r
is
positive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
negative
number
;
cluster
X
-->
r
->
negative-yielding
;
coherence
X
-->
r
is
negative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
non
positive
number
;
cluster
X
-->
r
->
nonpositive-yielding
;
coherence
X
-->
r
is
nonpositive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
non
negative
number
;
cluster
X
-->
r
->
nonnegative-yielding
;
coherence
X
-->
r
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be non
empty
set
;
cluster
X
-->
0
->
non
non-empty
;
coherence
not
X
-->
0
is
non-empty
proof
end;
end;
registration
cluster
Relation-like
positive-yielding
->
non-empty
nonnegative-yielding
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
positive-yielding
holds
(
b
1
is
nonnegative-yielding
&
b
1
is
non-empty
)
proof
end;
cluster
Relation-like
negative-yielding
->
non-empty
nonpositive-yielding
for
set
;
coherence
for
b
1
being
Relation
st
b
1
is
negative-yielding
holds
(
b
1
is
nonpositive-yielding
&
b
1
is
non-empty
)
proof
end;
end;
registration
let
X
be
set
;
cluster
Relation-like
X
-defined
REAL
-valued
Function-like
total
V33
(
X
,
REAL
)
complex-valued
ext-real-valued
real-valued
negative-yielding
for
Element
of
K6
(
K7
(
X
,
REAL
));
existence
ex
b
1
being
Function
of
X
,
REAL
st
b
1
is
negative-yielding
proof
end;
cluster
Relation-like
X
-defined
REAL
-valued
Function-like
total
V33
(
X
,
REAL
)
complex-valued
ext-real-valued
real-valued
positive-yielding
for
Element
of
K6
(
K7
(
X
,
REAL
));
existence
ex
b
1
being
Function
of
X
,
REAL
st
b
1
is
positive-yielding
proof
end;
end;
registration
cluster
Relation-like
non-empty
Function-like
real-valued
for
set
;
existence
ex
b
1
being
Function
st
(
b
1
is
non-empty
&
b
1
is
real-valued
)
proof
end;
end;
theorem
Th2
:
:: PARTFUN3:2
for
f
being
non-empty
real-valued
Function
holds
dom
(
f
^
)
=
dom
f
proof
end;
theorem
Th3
:
:: PARTFUN3:3
for
X
being non
empty
set
for
f
being
PartFunc
of
X
,
REAL
for
g
being
non-empty
PartFunc
of
X
,
REAL
holds
dom
(
f
/
g
)
=
(
dom
f
)
/\
(
dom
g
)
proof
end;
registration
let
X
be
set
;
let
f
,
g
be
nonpositive-yielding
PartFunc
of
X
,
REAL
;
cluster
f
+
g
->
nonpositive-yielding
;
coherence
f
+
g
is
nonpositive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
,
g
be
nonnegative-yielding
PartFunc
of
X
,
REAL
;
cluster
f
+
g
->
nonnegative-yielding
;
coherence
f
+
g
is
nonnegative-yielding
proof
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
f
+
g
is
positive-yielding
proof
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
f
+
g
is
positive-yielding
;
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
f
+
g
is
negative-yielding
proof
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
f
+
g
is
negative-yielding
;
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
f
-
g
is
nonnegative-yielding
proof
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
f
-
g
is
nonpositive-yielding
proof
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
f
-
g
is
positive-yielding
proof
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
f
-
g
is
negative-yielding
proof
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
f
-
g
is
negative-yielding
proof
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
f
-
g
is
positive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
,
g
be
nonpositive-yielding
PartFunc
of
X
,
REAL
;
cluster
f
(#)
g
->
nonnegative-yielding
;
coherence
f
(#)
g
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
,
g
be
nonnegative-yielding
PartFunc
of
X
,
REAL
;
cluster
f
(#)
g
->
nonnegative-yielding
;
coherence
f
(#)
g
is
nonnegative-yielding
proof
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
f
(#)
g
is
nonpositive-yielding
proof
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
f
(#)
g
is
nonpositive-yielding
;
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
f
(#)
g
is
negative-yielding
proof
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
f
(#)
g
is
negative-yielding
;
end;
registration
let
X
be
set
;
let
f
,
g
be
positive-yielding
PartFunc
of
X
,
REAL
;
cluster
f
(#)
g
->
positive-yielding
;
coherence
f
(#)
g
is
positive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
,
g
be
negative-yielding
PartFunc
of
X
,
REAL
;
cluster
f
(#)
g
->
positive-yielding
;
coherence
f
(#)
g
is
positive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
,
g
be
non-empty
PartFunc
of
X
,
REAL
;
cluster
f
(#)
g
->
non-empty
;
coherence
f
(#)
g
is
non-empty
proof
end;
end;
registration
let
X
be
set
;
let
f
be
PartFunc
of
X
,
REAL
;
cluster
f
(#)
f
->
nonnegative-yielding
;
coherence
f
(#)
f
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
non
positive
number
;
let
f
be
nonpositive-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
nonnegative-yielding
;
coherence
r
(#)
f
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
non
negative
number
;
let
f
be
nonnegative-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
nonnegative-yielding
;
coherence
r
(#)
f
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
non
positive
number
;
let
f
be
nonnegative-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
nonpositive-yielding
;
coherence
r
(#)
f
is
nonpositive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
non
negative
number
;
let
f
be
nonpositive-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
nonpositive-yielding
;
coherence
r
(#)
f
is
nonpositive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
positive
number
;
let
f
be
negative-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
negative-yielding
;
coherence
r
(#)
f
is
negative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
negative
number
;
let
f
be
positive-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
negative-yielding
;
coherence
r
(#)
f
is
negative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
positive
number
;
let
f
be
positive-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
positive-yielding
;
coherence
r
(#)
f
is
positive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be
real
negative
number
;
let
f
be
negative-yielding
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
positive-yielding
;
coherence
r
(#)
f
is
positive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
r
be non
zero
real
number
;
let
f
be
non-empty
PartFunc
of
X
,
REAL
;
cluster
r
(#)
f
->
non-empty
;
coherence
r
(#)
f
is
non-empty
proof
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
f
/
g
is
nonnegative-yielding
proof
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
f
/
g
is
nonnegative-yielding
proof
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
f
/
g
is
nonpositive-yielding
proof
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
f
/
g
is
nonpositive-yielding
proof
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
f
/
g
is
negative-yielding
proof
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
f
/
g
is
negative-yielding
proof
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
f
/
g
is
positive-yielding
proof
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
f
/
g
is
positive-yielding
proof
end;
end;
registration
let
X
be non
empty
set
;
let
f
be
PartFunc
of
X
,
REAL
;
cluster
f
/
f
->
nonnegative-yielding
;
coherence
f
/
f
is
nonnegative-yielding
proof
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
f
/
g
is
non-empty
proof
end;
end;
registration
let
X
be
set
;
let
f
be
nonpositive-yielding
Function
of
X
,
REAL
;
cluster
Inv
f
->
nonpositive-yielding
;
coherence
Inv
f
is
nonpositive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
be
nonnegative-yielding
Function
of
X
,
REAL
;
cluster
Inv
f
->
nonnegative-yielding
;
coherence
Inv
f
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
be
positive-yielding
Function
of
X
,
REAL
;
cluster
Inv
f
->
positive-yielding
;
coherence
Inv
f
is
positive-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
be
negative-yielding
Function
of
X
,
REAL
;
cluster
Inv
f
->
negative-yielding
;
coherence
Inv
f
is
negative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
be
non-empty
Function
of
X
,
REAL
;
cluster
Inv
f
->
non-empty
;
coherence
Inv
f
is
non-empty
proof
end;
end;
registration
let
X
be
set
;
let
f
be
non-empty
Function
of
X
,
REAL
;
cluster
-
f
->
non-empty
;
coherence
-
f
is
non-empty
;
end;
registration
let
X
be
set
;
let
f
be
nonpositive-yielding
Function
of
X
,
REAL
;
cluster
-
f
->
nonnegative-yielding
;
coherence
-
f
is
nonnegative-yielding
;
end;
registration
let
X
be
set
;
let
f
be
nonnegative-yielding
Function
of
X
,
REAL
;
cluster
-
f
->
nonpositive-yielding
;
coherence
-
f
is
nonpositive-yielding
;
end;
registration
let
X
be
set
;
let
f
be
positive-yielding
Function
of
X
,
REAL
;
cluster
-
f
->
negative-yielding
;
coherence
-
f
is
negative-yielding
;
end;
registration
let
X
be
set
;
let
f
be
negative-yielding
Function
of
X
,
REAL
;
cluster
-
f
->
positive-yielding
;
coherence
-
f
is
positive-yielding
;
end;
registration
let
X
be
set
;
let
f
be
Function
of
X
,
REAL
;
cluster
|.
f
.|
->
nonnegative-yielding
;
coherence
abs
f
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
be
non-empty
Function
of
X
,
REAL
;
cluster
|.
f
.|
->
positive-yielding
;
coherence
abs
f
is
positive-yielding
proof
end;
end;
registration
let
X
be non
empty
set
;
let
f
be
nonpositive-yielding
Function
of
X
,
REAL
;
cluster
f
^
->
nonpositive-yielding
;
coherence
f
^
is
nonpositive-yielding
proof
end;
end;
registration
let
X
be non
empty
set
;
let
f
be
nonnegative-yielding
Function
of
X
,
REAL
;
cluster
f
^
->
nonnegative-yielding
;
coherence
f
^
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be non
empty
set
;
let
f
be
positive-yielding
Function
of
X
,
REAL
;
cluster
f
^
->
positive-yielding
;
coherence
f
^
is
positive-yielding
proof
end;
end;
registration
let
X
be non
empty
set
;
let
f
be
negative-yielding
Function
of
X
,
REAL
;
cluster
f
^
->
negative-yielding
;
coherence
f
^
is
negative-yielding
proof
end;
end;
registration
let
X
be non
empty
set
;
let
f
be
non-empty
Function
of
X
,
REAL
;
cluster
f
^
->
non-empty
;
coherence
f
^
is
non-empty
proof
end;
end;
definition
let
f
be
real-valued
Function
;
func
sqrt
f
->
Function
means
:
Def5
:
:: PARTFUN3:def 5
(
dom
it
=
dom
f
& ( for
x
being
set
st
x
in
dom
it
holds
it
.
x
=
sqrt
(
f
.
x
)
) );
existence
ex
b
1
being
Function
st
(
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
sqrt
(
f
.
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Function
st
dom
b
1
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
1
holds
b
1
.
x
=
sqrt
(
f
.
x
)
) &
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
sqrt
(
f
.
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def5
defines
sqrt
PARTFUN3:def 5 :
for
f
being
real-valued
Function
for
b
2
being
Function
holds
(
b
2
=
sqrt
f
iff (
dom
b
2
=
dom
f
& ( for
x
being
set
st
x
in
dom
b
2
holds
b
2
.
x
=
sqrt
(
f
.
x
)
) ) );
registration
let
f
be
real-valued
Function
;
cluster
sqrt
f
->
real-valued
;
coherence
sqrt
f
is
real-valued
proof
end;
end;
definition
let
C
be
set
;
let
D
be
real-membered
set
;
let
f
be
PartFunc
of
C
,
D
;
:: original:
sqrt
redefine
func
sqrt
f
->
PartFunc
of
C
,
REAL
;
coherence
sqrt
f
is
PartFunc
of
C
,
REAL
proof
end;
end;
registration
let
X
be
set
;
let
f
be
nonnegative-yielding
Function
of
X
,
REAL
;
cluster
sqrt
f
->
nonnegative-yielding
;
coherence
sqrt
f
is
nonnegative-yielding
proof
end;
end;
registration
let
X
be
set
;
let
f
be
positive-yielding
Function
of
X
,
REAL
;
cluster
sqrt
f
->
positive-yielding
;
coherence
sqrt
f
is
positive-yielding
proof
end;
end;
definition
let
X
be
set
;
let
f
be
Function
of
X
,
REAL
;
:: original:
sqrt
redefine
func
sqrt
f
->
Function
of
X
,
REAL
;
coherence
sqrt
f
is
Function
of
X
,
REAL
proof
end;
end;
definition
let
X
be
set
;
let
f
be
non-empty
Function
of
X
,
REAL
;
:: original:
^
redefine
func
f
^
->
Function
of
X
,
REAL
;
coherence
f
^
is
Function
of
X
,
REAL
proof
end;
end;
definition
let
X
be non
empty
set
;
let
f
be
Function
of
X
,
REAL
;
let
g
be
non-empty
Function
of
X
,
REAL
;
:: original:
/
redefine
func
f
/
g
->
Function
of
X
,
REAL
;
coherence
f
/
g
is
Function
of
X
,
REAL
proof
end;
end;