:: Properties of Real Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received June 18, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
::
:: REAL SEQUENCES
::
theorem
Th1
:
:: RFUNCT_2:1
for
seq1
,
seq2
,
seq3
being
Real_Sequence
holds
(
seq1
=
seq2
-
seq3
iff for
n
being
Element
of
NAT
holds
seq1
.
n
=
(
seq2
.
n
)
-
(
seq3
.
n
)
)
proof
end;
theorem
Th2
:
:: RFUNCT_2:2
for
seq1
,
seq2
being
Real_Sequence
for
Ns
being
V37
()
sequence
of
NAT
holds
(
(
seq1
+
seq2
)
*
Ns
=
(
seq1
*
Ns
)
+
(
seq2
*
Ns
)
&
(
seq1
-
seq2
)
*
Ns
=
(
seq1
*
Ns
)
-
(
seq2
*
Ns
)
&
(
seq1
(#)
seq2
)
*
Ns
=
(
seq1
*
Ns
)
(#)
(
seq2
*
Ns
)
)
proof
end;
theorem
Th3
:
:: RFUNCT_2:3
for
p
being
Element
of
REAL
for
seq
being
Real_Sequence
for
Ns
being
V37
()
sequence
of
NAT
holds
(
p
(#)
seq
)
*
Ns
=
p
(#)
(
seq
*
Ns
)
proof
end;
theorem
:: RFUNCT_2:4
for
seq
being
Real_Sequence
for
Ns
being
V37
()
sequence
of
NAT
holds
(
(
-
seq
)
*
Ns
=
-
(
seq
*
Ns
)
&
(
abs
seq
)
*
Ns
=
abs
(
seq
*
Ns
)
)
proof
end;
theorem
Th5
:
:: RFUNCT_2:5
for
seq
being
Real_Sequence
for
Ns
being
V37
()
sequence
of
NAT
holds
(
seq
*
Ns
)
"
=
(
seq
"
)
*
Ns
proof
end;
theorem
:: RFUNCT_2:6
for
seq1
,
seq
being
Real_Sequence
for
Ns
being
V37
()
sequence
of
NAT
holds
(
seq1
/"
seq
)
*
Ns
=
(
seq1
*
Ns
)
/"
(
seq
*
Ns
)
proof
end;
theorem
:: RFUNCT_2:7
for
seq
being
Real_Sequence
st
seq
is
convergent
& ( for
n
being
Element
of
NAT
holds
seq
.
n
<=
0
) holds
lim
seq
<=
0
proof
end;
theorem
Th8
:
:: RFUNCT_2:8
for
W
being non
empty
set
for
h1
,
h2
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
rng
seq
c=
(
dom
h1
)
/\
(
dom
h2
)
holds
(
(
h1
+
h2
)
/*
seq
=
(
h1
/*
seq
)
+
(
h2
/*
seq
)
&
(
h1
-
h2
)
/*
seq
=
(
h1
/*
seq
)
-
(
h2
/*
seq
)
&
(
h1
(#)
h2
)
/*
seq
=
(
h1
/*
seq
)
(#)
(
h2
/*
seq
)
)
proof
end;
theorem
Th9
:
:: RFUNCT_2:9
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
for
r
being
real
number
st
rng
seq
c=
dom
h
holds
(
r
(#)
h
)
/*
seq
=
r
(#)
(
h
/*
seq
)
proof
end;
theorem
:: RFUNCT_2:10
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
rng
seq
c=
dom
h
holds
(
abs
(
h
/*
seq
)
=
(
abs
h
)
/*
seq
&
-
(
h
/*
seq
)
=
(
-
h
)
/*
seq
)
proof
end;
theorem
:: RFUNCT_2:11
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
rng
seq
c=
dom
(
h
^
)
holds
h
/*
seq
is
non-zero
proof
end;
theorem
:: RFUNCT_2:12
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
rng
seq
c=
dom
(
h
^
)
holds
(
h
^
)
/*
seq
=
(
h
/*
seq
)
"
proof
end;
theorem
:: RFUNCT_2:13
for
W
being non
empty
set
for
h1
,
h2
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
h1
is
total
&
h2
is
total
holds
(
(
h1
+
h2
)
/*
seq
=
(
h1
/*
seq
)
+
(
h2
/*
seq
)
&
(
h1
-
h2
)
/*
seq
=
(
h1
/*
seq
)
-
(
h2
/*
seq
)
&
(
h1
(#)
h2
)
/*
seq
=
(
h1
/*
seq
)
(#)
(
h2
/*
seq
)
)
proof
end;
theorem
:: RFUNCT_2:14
for
r
being
Element
of
REAL
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
h
is
total
holds
(
r
(#)
h
)
/*
seq
=
r
(#)
(
h
/*
seq
)
proof
end;
theorem
:: RFUNCT_2:15
for
X
being
set
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
rng
seq
c=
dom
(
h
|
X
)
holds
abs
(
(
h
|
X
)
/*
seq
)
=
(
(
abs
h
)
|
X
)
/*
seq
proof
end;
theorem
:: RFUNCT_2:16
for
X
being
set
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
for
seq
being
sequence
of
W
st
rng
seq
c=
dom
(
h
|
X
)
&
h
"
{
0
}
=
{}
holds
(
(
h
^
)
|
X
)
/*
seq
=
(
(
h
|
X
)
/*
seq
)
"
proof
end;
::
:: MONOTONE FUNCTIONS
::
registration
let
Z
be
set
;
let
f
be
one-to-one
Function
;
cluster
f
|
Z
->
one-to-one
;
coherence
f
|
Z
is
one-to-one
by
FUNCT_1:52
;
end;
theorem
:: RFUNCT_2:17
for
X
being
set
for
h
being
one-to-one
Function
holds
(
h
|
X
)
"
=
(
h
"
)
|
(
h
.:
X
)
proof
end;
theorem
Th18
:
:: RFUNCT_2:18
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
st
rng
h
is
real-bounded
&
upper_bound
(
rng
h
)
=
lower_bound
(
rng
h
)
holds
h
is
V8
()
proof
end;
theorem
:: RFUNCT_2:19
for
Y
being
set
for
W
being non
empty
set
for
h
being
PartFunc
of
W
,
REAL
st
h
.:
Y
is
real-bounded
&
upper_bound
(
h
.:
Y
)
=
lower_bound
(
h
.:
Y
)
holds
h
|
Y
is
V8
()
proof
end;
definition
let
h
be
PartFunc
of
REAL
,
REAL
;
redefine
attr
h
is
increasing
means
:
Def1
:
:: RFUNCT_2:def 1
for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r1
<
h
.
r2
;
compatibility
(
h
is
increasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r1
<
h
.
r2
)
proof
end;
redefine
attr
h
is
decreasing
means
:
Def2
:
:: RFUNCT_2:def 2
for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r2
<
h
.
r1
;
compatibility
(
h
is
decreasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r2
<
h
.
r1
)
proof
end;
redefine
attr
h
is
non-decreasing
means
:
Def3
:
:: RFUNCT_2:def 3
for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r1
<=
h
.
r2
;
compatibility
(
h
is
non-decreasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r1
<=
h
.
r2
)
proof
end;
redefine
attr
h
is
non-increasing
means
:
Def4
:
:: RFUNCT_2:def 4
for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r2
<=
h
.
r1
;
compatibility
(
h
is
non-increasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r2
<=
h
.
r1
)
proof
end;
end;
::
deftheorem
Def1
defines
increasing
RFUNCT_2:def 1 :
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
is
increasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r1
<
h
.
r2
);
::
deftheorem
Def2
defines
decreasing
RFUNCT_2:def 2 :
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
is
decreasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r2
<
h
.
r1
);
::
deftheorem
Def3
defines
non-decreasing
RFUNCT_2:def 3 :
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
is
non-decreasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r1
<=
h
.
r2
);
::
deftheorem
Def4
defines
non-increasing
RFUNCT_2:def 4 :
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
is
non-increasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
dom
h
&
r2
in
dom
h
&
r1
<
r2
holds
h
.
r2
<=
h
.
r1
);
theorem
Th20
:
:: RFUNCT_2:20
for
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
|
Y
is
increasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
Y
/\
(
dom
h
)
&
r2
in
Y
/\
(
dom
h
)
&
r1
<
r2
holds
h
.
r1
<
h
.
r2
)
proof
end;
theorem
Th21
:
:: RFUNCT_2:21
for
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
|
Y
is
decreasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
Y
/\
(
dom
h
)
&
r2
in
Y
/\
(
dom
h
)
&
r1
<
r2
holds
h
.
r2
<
h
.
r1
)
proof
end;
theorem
Th22
:
:: RFUNCT_2:22
for
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
|
Y
is
non-decreasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
Y
/\
(
dom
h
)
&
r2
in
Y
/\
(
dom
h
)
&
r1
<
r2
holds
h
.
r1
<=
h
.
r2
)
proof
end;
theorem
Th23
:
:: RFUNCT_2:23
for
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
|
Y
is
non-increasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
Y
/\
(
dom
h
)
&
r2
in
Y
/\
(
dom
h
)
&
r1
<
r2
holds
h
.
r2
<=
h
.
r1
)
proof
end;
definition
let
h
be
PartFunc
of
REAL
,
REAL
;
attr
h
is
monotone
means
:
Def5
:
:: RFUNCT_2:def 5
(
h
is
non-decreasing
or
h
is
non-increasing
);
end;
::
deftheorem
Def5
defines
monotone
RFUNCT_2:def 5 :
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
is
monotone
iff (
h
is
non-decreasing
or
h
is
non-increasing
) );
registration
cluster
Function-like
non-decreasing
->
monotone
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
non-decreasing
holds
b
1
is
monotone
by
Def5
;
cluster
Function-like
non-increasing
->
monotone
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
non-increasing
holds
b
1
is
monotone
by
Def5
;
cluster
Function-like
non
monotone
->
non
non-decreasing
non
non-increasing
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st not
b
1
is
monotone
holds
( not
b
1
is
non-decreasing
& not
b
1
is
non-increasing
)
;
end;
theorem
Th24
:
:: RFUNCT_2:24
for
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
|
Y
is
non-decreasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
Y
/\
(
dom
h
)
&
r2
in
Y
/\
(
dom
h
)
&
r1
<=
r2
holds
h
.
r1
<=
h
.
r2
)
proof
end;
theorem
Th25
:
:: RFUNCT_2:25
for
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
(
h
|
Y
is
non-increasing
iff for
r1
,
r2
being
Element
of
REAL
st
r1
in
Y
/\
(
dom
h
)
&
r2
in
Y
/\
(
dom
h
)
&
r1
<=
r2
holds
h
.
r2
<=
h
.
r1
)
proof
end;
registration
cluster
Function-like
non-decreasing
non-increasing
->
V8
() for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
non-decreasing
&
b
1
is
non-increasing
holds
b
1
is
V8
()
proof
end;
end;
registration
cluster
Function-like
V8
()
->
non-decreasing
non-increasing
for
Element
of
bool
[:
REAL
,
REAL
:]
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
V8
() holds
(
b
1
is
non-increasing
&
b
1
is
non-decreasing
)
proof
end;
end;
registration
cluster
Relation-like
REAL
-defined
REAL
-valued
Function-like
trivial
complex-valued
ext-real-valued
real-valued
for
Element
of
bool
[:
REAL
,
REAL
:]
;
existence
ex
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
trivial
proof
end;
end;
registration
let
h
be
increasing
PartFunc
of
REAL
,
REAL
;
let
X
be
set
;
cluster
h
|
X
->
increasing
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
h
|
X
holds
b
1
is
increasing
proof
end;
end;
registration
let
h
be
decreasing
PartFunc
of
REAL
,
REAL
;
let
X
be
set
;
cluster
h
|
X
->
decreasing
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
h
|
X
holds
b
1
is
decreasing
proof
end;
end;
registration
let
h
be
non-decreasing
PartFunc
of
REAL
,
REAL
;
let
X
be
set
;
cluster
h
|
X
->
non-decreasing
for
PartFunc
of
REAL
,
REAL
;
coherence
for
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
=
h
|
X
holds
b
1
is
non-decreasing
proof
end;
end;
theorem
:: RFUNCT_2:26
for
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
Y
misses
dom
h
holds
(
h
|
Y
is
increasing
&
h
|
Y
is
decreasing
&
h
|
Y
is
non-decreasing
&
h
|
Y
is
non-increasing
&
h
|
Y
is
monotone
)
proof
end;
theorem
:: RFUNCT_2:27
for
Y
,
X
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
h
|
Y
is
non-decreasing
&
h
|
X
is
non-increasing
holds
h
|
(
Y
/\
X
)
is
V8
()
proof
end;
theorem
:: RFUNCT_2:28
for
X
,
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
X
c=
Y
&
h
|
Y
is
increasing
holds
h
|
X
is
increasing
proof
end;
theorem
:: RFUNCT_2:29
for
X
,
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
X
c=
Y
&
h
|
Y
is
decreasing
holds
h
|
X
is
decreasing
proof
end;
theorem
:: RFUNCT_2:30
for
X
,
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
X
c=
Y
&
h
|
Y
is
non-decreasing
holds
h
|
X
is
non-decreasing
proof
end;
theorem
:: RFUNCT_2:31
for
X
,
Y
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
X
c=
Y
&
h
|
Y
is
non-increasing
holds
h
|
X
is
non-increasing
proof
end;
theorem
Th32
:
:: RFUNCT_2:32
for
Y
being
set
for
r
being
Element
of
REAL
for
h
being
PartFunc
of
REAL
,
REAL
holds
( (
h
|
Y
is
increasing
&
0
<
r
implies
(
r
(#)
h
)
|
Y
is
increasing
) & (
r
=
0
implies
(
r
(#)
h
)
|
Y
is
V8
() ) & (
h
|
Y
is
increasing
&
r
<
0
implies
(
r
(#)
h
)
|
Y
is
decreasing
) )
proof
end;
theorem
:: RFUNCT_2:33
for
Y
being
set
for
r
being
Element
of
REAL
for
h
being
PartFunc
of
REAL
,
REAL
holds
( (
h
|
Y
is
decreasing
&
0
<
r
implies
(
r
(#)
h
)
|
Y
is
decreasing
) & (
h
|
Y
is
decreasing
&
r
<
0
implies
(
r
(#)
h
)
|
Y
is
increasing
) )
proof
end;
theorem
Th34
:
:: RFUNCT_2:34
for
Y
being
set
for
r
being
Element
of
REAL
for
h
being
PartFunc
of
REAL
,
REAL
holds
( (
h
|
Y
is
non-decreasing
&
0
<=
r
implies
(
r
(#)
h
)
|
Y
is
non-decreasing
) & (
h
|
Y
is
non-decreasing
&
r
<=
0
implies
(
r
(#)
h
)
|
Y
is
non-increasing
) )
proof
end;
theorem
:: RFUNCT_2:35
for
Y
being
set
for
r
being
Element
of
REAL
for
h
being
PartFunc
of
REAL
,
REAL
holds
( (
h
|
Y
is
non-increasing
&
0
<=
r
implies
(
r
(#)
h
)
|
Y
is
non-increasing
) & (
h
|
Y
is
non-increasing
&
r
<=
0
implies
(
r
(#)
h
)
|
Y
is
non-decreasing
) )
proof
end;
theorem
Th36
:
:: RFUNCT_2:36
for
X
,
Y
being
set
for
r
being
Element
of
REAL
for
h1
,
h2
being
PartFunc
of
REAL
,
REAL
st
r
in
(
X
/\
Y
)
/\
(
dom
(
h1
+
h2
)
)
holds
(
r
in
X
/\
(
dom
h1
)
&
r
in
Y
/\
(
dom
h2
)
)
proof
end;
theorem
:: RFUNCT_2:37
for
X
,
Y
being
set
for
h1
,
h2
being
PartFunc
of
REAL
,
REAL
holds
( (
h1
|
X
is
increasing
&
h2
|
Y
is
increasing
implies
(
h1
+
h2
)
|
(
X
/\
Y
)
is
increasing
) & (
h1
|
X
is
decreasing
&
h2
|
Y
is
decreasing
implies
(
h1
+
h2
)
|
(
X
/\
Y
)
is
decreasing
) & (
h1
|
X
is
non-decreasing
&
h2
|
Y
is
non-decreasing
implies
(
h1
+
h2
)
|
(
X
/\
Y
)
is
non-decreasing
) & (
h1
|
X
is
non-increasing
&
h2
|
Y
is
non-increasing
implies
(
h1
+
h2
)
|
(
X
/\
Y
)
is
non-increasing
) )
proof
end;
theorem
:: RFUNCT_2:38
for
X
,
Y
being
set
for
h1
,
h2
being
PartFunc
of
REAL
,
REAL
holds
( (
h1
|
X
is
increasing
&
h2
|
Y
is
V8
() implies
(
h1
+
h2
)
|
(
X
/\
Y
)
is
increasing
) & (
h1
|
X
is
decreasing
&
h2
|
Y
is
V8
() implies
(
h1
+
h2
)
|
(
X
/\
Y
)
is
decreasing
) )
proof
end;
theorem
:: RFUNCT_2:39
for
X
,
Y
being
set
for
h1
,
h2
being
PartFunc
of
REAL
,
REAL
st
h1
|
X
is
increasing
&
h2
|
Y
is
non-decreasing
holds
(
h1
+
h2
)
|
(
X
/\
Y
)
is
increasing
proof
end;
theorem
:: RFUNCT_2:40
for
X
,
Y
being
set
for
h1
,
h2
being
PartFunc
of
REAL
,
REAL
st
h1
|
X
is
non-increasing
&
h2
|
Y
is
V8
() holds
(
h1
+
h2
)
|
(
X
/\
Y
)
is
non-increasing
proof
end;
theorem
:: RFUNCT_2:41
for
X
,
Y
being
set
for
h1
,
h2
being
PartFunc
of
REAL
,
REAL
st
h1
|
X
is
decreasing
&
h2
|
Y
is
non-increasing
holds
(
h1
+
h2
)
|
(
X
/\
Y
)
is
decreasing
proof
end;
theorem
:: RFUNCT_2:42
for
X
,
Y
being
set
for
h1
,
h2
being
PartFunc
of
REAL
,
REAL
st
h1
|
X
is
non-decreasing
&
h2
|
Y
is
V8
() holds
(
h1
+
h2
)
|
(
X
/\
Y
)
is
non-decreasing
proof
end;
theorem
:: RFUNCT_2:43
for
x
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
h
|
{
x
}
is
non-increasing
proof
end;
theorem
:: RFUNCT_2:44
for
x
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
h
|
{
x
}
is
decreasing
proof
end;
theorem
:: RFUNCT_2:45
for
x
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
h
|
{
x
}
is
non-decreasing
proof
end;
theorem
:: RFUNCT_2:46
for
x
being
set
for
h
being
PartFunc
of
REAL
,
REAL
holds
h
|
{
x
}
is
non-increasing
proof
end;
theorem
:: RFUNCT_2:47
for
R
being
Subset
of
REAL
holds
(
id
R
)
|
R
is
increasing
proof
end;
theorem
:: RFUNCT_2:48
for
X
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
h
|
X
is
increasing
holds
(
-
h
)
|
X
is
decreasing
proof
end;
theorem
:: RFUNCT_2:49
for
X
being
set
for
h
being
PartFunc
of
REAL
,
REAL
st
h
|
X
is
non-decreasing
holds
(
-
h
)
|
X
is
non-increasing
proof
end;
theorem
:: RFUNCT_2:50
for
p
,
g
being
Element
of
REAL
for
h
being
PartFunc
of
REAL
,
REAL
st (
h
|
[.
p
,
g
.]
is
increasing
or
h
|
[.
p
,
g
.]
is
decreasing
) holds
h
|
[.
p
,
g
.]
is
one-to-one
proof
end;
theorem
:: RFUNCT_2:51
for
p
,
g
being
Element
of
REAL
for
h
being
one-to-one
PartFunc
of
REAL
,
REAL
st
h
|
[.
p
,
g
.]
is
increasing
holds
(
(
h
|
[.
p
,
g
.]
)
"
)
|
(
h
.:
[.
p
,
g
.]
)
is
increasing
proof
end;
theorem
:: RFUNCT_2:52
for
p
,
g
being
Element
of
REAL
for
h
being
one-to-one
PartFunc
of
REAL
,
REAL
st
h
|
[.
p
,
g
.]
is
decreasing
holds
(
(
h
|
[.
p
,
g
.]
)
"
)
|
(
h
.:
[.
p
,
g
.]
)
is
decreasing
proof
end;
:: REAL SEQUENCES
::