:: Real Function Differentiability
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
theorem
Th1
:
:: FDIFF_1:1
for
Y
being
Subset
of
REAL
holds
( ( for
r
being
Real
holds
(
r
in
Y
iff
r
in
REAL
) ) iff
Y
=
REAL
)
proof
end;
definition
let
x
be
real
number
;
let
IT
be
Real_Sequence
;
attr
IT
is
x
-convergent
means
:
Def1
:
:: FDIFF_1:def 1
(
IT
is
convergent
&
lim
IT
=
x
);
end;
::
deftheorem
Def1
defines
-convergent
FDIFF_1:def 1 :
for
x
being
real
number
for
IT
being
Real_Sequence
holds
(
IT
is
x
-convergent
iff (
IT
is
convergent
&
lim
IT
=
x
) );
registration
cluster
V1
()
non-zero
V4
(
NAT
)
V5
(
REAL
)
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
0
-convergent
for
Element
of
K19
(
K20
(
NAT
,
REAL
));
existence
ex
b
1
being
Real_Sequence
st
(
b
1
is
0
-convergent
&
b
1
is
non-zero
)
proof
end;
end;
registration
let
f
be
0
-convergent
Real_Sequence
;
cluster
lim
f
->
empty
;
coherence
lim
f
is
empty
proof
end;
end;
registration
cluster
V6
()
quasi_total
0
-convergent
->
convergent
for
Element
of
K19
(
K20
(
NAT
,
REAL
));
coherence
for
b
1
being
Real_Sequence
st
b
1
is
0
-convergent
holds
b
1
is
convergent
proof
end;
end;
reconsider
cs
=
NAT
-->
0
as
Real_Sequence
by
FUNCOP_1:45
;
definition
let
IT
be
PartFunc
of
REAL
,
REAL
;
attr
IT
is
RestFunc-like
means
:
Def2
:
:: FDIFF_1:def 2
(
IT
is
total
& ( for
h
being
non-zero
0
-convergent
Real_Sequence
holds
(
(
h
"
)
(#)
(
IT
/*
h
)
is
convergent
&
lim
(
(
h
"
)
(#)
(
IT
/*
h
)
)
=
0
) ) );
end;
::
deftheorem
Def2
defines
RestFunc-like
FDIFF_1:def 2 :
for
IT
being
PartFunc
of
REAL
,
REAL
holds
(
IT
is
RestFunc-like
iff (
IT
is
total
& ( for
h
being
non-zero
0
-convergent
Real_Sequence
holds
(
(
h
"
)
(#)
(
IT
/*
h
)
is
convergent
&
lim
(
(
h
"
)
(#)
(
IT
/*
h
)
)
=
0
) ) ) );
reconsider
cf
=
REAL
-->
0
as
Function
of
REAL
,
REAL
by
FUNCOP_1:45
;
registration
cluster
V1
()
V4
(
REAL
)
V5
(
REAL
)
V6
()
complex-valued
ext-real-valued
real-valued
RestFunc-like
for
Element
of
K19
(
K20
(
REAL
,
REAL
));
existence
ex
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
RestFunc-like
proof
end;
end;
definition
mode
RestFunc
is
RestFunc-like
PartFunc
of
REAL
,
REAL
;
end;
definition
let
IT
be
PartFunc
of
REAL
,
REAL
;
attr
IT
is
linear
means
:
Def3
:
:: FDIFF_1:def 3
(
IT
is
total
& ex
r
being
Real
st
for
p
being
Real
holds
IT
.
p
=
r
*
p
);
end;
::
deftheorem
Def3
defines
linear
FDIFF_1:def 3 :
for
IT
being
PartFunc
of
REAL
,
REAL
holds
(
IT
is
linear
iff (
IT
is
total
& ex
r
being
Real
st
for
p
being
Real
holds
IT
.
p
=
r
*
p
) );
registration
cluster
V1
()
V4
(
REAL
)
V5
(
REAL
)
V6
()
complex-valued
ext-real-valued
real-valued
linear
for
Element
of
K19
(
K20
(
REAL
,
REAL
));
existence
ex
b
1
being
PartFunc
of
REAL
,
REAL
st
b
1
is
linear
proof
end;
end;
definition
mode
LinearFunc
is
linear
PartFunc
of
REAL
,
REAL
;
end;
theorem
Th2
:
:: FDIFF_1:2
for
L1
,
L2
being
LinearFunc
holds
(
L1
+
L2
is
LinearFunc
&
L1
-
L2
is
LinearFunc
)
proof
end;
theorem
Th3
:
:: FDIFF_1:3
for
r
being
Real
for
L
being
LinearFunc
holds
r
(#)
L
is
LinearFunc
proof
end;
theorem
Th4
:
:: FDIFF_1:4
for
R1
,
R2
being
RestFunc
holds
(
R1
+
R2
is
RestFunc
&
R1
-
R2
is
RestFunc
&
R1
(#)
R2
is
RestFunc
)
proof
end;
theorem
Th5
:
:: FDIFF_1:5
for
r
being
Real
for
R
being
RestFunc
holds
r
(#)
R
is
RestFunc
proof
end;
theorem
Th6
:
:: FDIFF_1:6
for
L1
,
L2
being
LinearFunc
holds
L1
(#)
L2
is
RestFunc-like
proof
end;
theorem
Th7
:
:: FDIFF_1:7
for
R
being
RestFunc
for
L
being
LinearFunc
holds
(
R
(#)
L
is
RestFunc
&
L
(#)
R
is
RestFunc
)
proof
end;
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
let
x0
be
real
number
;
pred
f
is_differentiable_in
x0
means
:
Def4
:
:: FDIFF_1:def 4
ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
ex
R
being
RestFunc
st
for
x
being
Real
st
x
in
N
holds
(
f
.
x
)
-
(
f
.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
.
(
x
-
x0
)
)
);
end;
::
deftheorem
Def4
defines
is_differentiable_in
FDIFF_1:def 4 :
for
f
being
PartFunc
of
REAL
,
REAL
for
x0
being
real
number
holds
(
f
is_differentiable_in
x0
iff ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
ex
R
being
RestFunc
st
for
x
being
Real
st
x
in
N
holds
(
f
.
x
)
-
(
f
.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
.
(
x
-
x0
)
)
) );
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
let
x0
be
real
number
;
assume
A1
:
f
is_differentiable_in
x0
;
func
diff
(
f
,
x0
)
->
Real
means
:
Def5
:
:: FDIFF_1:def 5
ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
ex
R
being
RestFunc
st
(
it
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
.
x
)
-
(
f
.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
.
(
x
-
x0
)
)
) ) );
existence
ex
b
1
being
Real
ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
ex
R
being
RestFunc
st
(
b
1
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
.
x
)
-
(
f
.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
.
(
x
-
x0
)
)
) ) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Real
st ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
ex
R
being
RestFunc
st
(
b
1
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
.
x
)
-
(
f
.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
.
(
x
-
x0
)
)
) ) ) & ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
ex
R
being
RestFunc
st
(
b
2
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
.
x
)
-
(
f
.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
.
(
x
-
x0
)
)
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def5
defines
diff
FDIFF_1:def 5 :
for
f
being
PartFunc
of
REAL
,
REAL
for
x0
being
real
number
st
f
is_differentiable_in
x0
holds
for
b
3
being
Real
holds
(
b
3
=
diff
(
f
,
x0
) iff ex
N
being
Neighbourhood
of
x0
st
(
N
c=
dom
f
& ex
L
being
LinearFunc
ex
R
being
RestFunc
st
(
b
3
=
L
.
1 & ( for
x
being
Real
st
x
in
N
holds
(
f
.
x
)
-
(
f
.
x0
)
=
(
L
.
(
x
-
x0
)
)
+
(
R
.
(
x
-
x0
)
)
) ) ) );
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
let
X
be
set
;
pred
f
is_differentiable_on
X
means
:
Def6
:
:: FDIFF_1:def 6
(
X
c=
dom
f
& ( for
x
being
Real
st
x
in
X
holds
f
|
X
is_differentiable_in
x
) );
end;
::
deftheorem
Def6
defines
is_differentiable_on
FDIFF_1:def 6 :
for
f
being
PartFunc
of
REAL
,
REAL
for
X
being
set
holds
(
f
is_differentiable_on
X
iff (
X
c=
dom
f
& ( for
x
being
Real
st
x
in
X
holds
f
|
X
is_differentiable_in
x
) ) );
theorem
Th8
:
:: FDIFF_1:8
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_differentiable_on
X
holds
X
is
Subset
of
REAL
proof
end;
theorem
Th9
:
:: FDIFF_1:9
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
is_differentiable_on
Z
iff (
Z
c=
dom
f
& ( for
x
being
Real
st
x
in
Z
holds
f
is_differentiable_in
x
) ) )
proof
end;
theorem
:: FDIFF_1:10
for
Y
being
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_differentiable_on
Y
holds
Y
is
open
proof
end;
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
let
X
be
set
;
assume
A1
:
f
is_differentiable_on
X
;
func
f
`|
X
->
PartFunc
of
REAL
,
REAL
means
:
Def7
:
:: FDIFF_1:def 7
(
dom
it
=
X
& ( for
x
being
Real
st
x
in
X
holds
it
.
x
=
diff
(
f
,
x
) ) );
existence
ex
b
1
being
PartFunc
of
REAL
,
REAL
st
(
dom
b
1
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
1
.
x
=
diff
(
f
,
x
) ) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of
REAL
,
REAL
st
dom
b
1
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
1
.
x
=
diff
(
f
,
x
) ) &
dom
b
2
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
2
.
x
=
diff
(
f
,
x
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def7
defines
`|
FDIFF_1:def 7 :
for
f
being
PartFunc
of
REAL
,
REAL
for
X
being
set
st
f
is_differentiable_on
X
holds
for
b
3
being
PartFunc
of
REAL
,
REAL
holds
(
b
3
=
f
`|
X
iff (
dom
b
3
=
X
& ( for
x
being
Real
st
x
in
X
holds
b
3
.
x
=
diff
(
f
,
x
) ) ) );
theorem
:: FDIFF_1:11
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
f
& ex
r
being
Real
st
rng
f
=
{
r
}
holds
(
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
f
`|
Z
)
.
x
=
0
) )
proof
end;
registration
let
h
be
non-zero
0
-convergent
Real_Sequence
;
let
n
be
Element
of
NAT
;
cluster
h
^\
n
->
non-zero
0
-convergent
for
Real_Sequence
;
coherence
for
b
1
being
Real_Sequence
st
b
1
=
h
^\
n
holds
(
b
1
is
non-zero
&
b
1
is
0
-convergent
)
proof
end;
end;
theorem
Th12
:
:: FDIFF_1:12
for
f
being
PartFunc
of
REAL
,
REAL
for
x0
being
real
number
for
N
being
Neighbourhood
of
x0
st
f
is_differentiable_in
x0
&
N
c=
dom
f
holds
for
h
being
non-zero
0
-convergent
Real_Sequence
for
c
being
V8
()
Real_Sequence
st
rng
c
=
{
x0
}
&
rng
(
h
+
c
)
c=
N
holds
(
(
h
"
)
(#)
(
(
f
/*
(
h
+
c
)
)
-
(
f
/*
c
)
)
is
convergent
&
diff
(
f
,
x0
)
=
lim
(
(
h
"
)
(#)
(
(
f
/*
(
h
+
c
)
)
-
(
f
/*
c
)
)
)
)
proof
end;
theorem
Th13
:
:: FDIFF_1:13
for
x0
being
Real
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
is_differentiable_in
x0
&
f2
is_differentiable_in
x0
holds
(
f1
+
f2
is_differentiable_in
x0
&
diff
(
(
f1
+
f2
)
,
x0
)
=
(
diff
(
f1
,
x0
)
)
+
(
diff
(
f2
,
x0
)
)
)
proof
end;
theorem
Th14
:
:: FDIFF_1:14
for
x0
being
Real
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
is_differentiable_in
x0
&
f2
is_differentiable_in
x0
holds
(
f1
-
f2
is_differentiable_in
x0
&
diff
(
(
f1
-
f2
)
,
x0
)
=
(
diff
(
f1
,
x0
)
)
-
(
diff
(
f2
,
x0
)
)
)
proof
end;
theorem
Th15
:
:: FDIFF_1:15
for
x0
,
r
being
Real
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_differentiable_in
x0
holds
(
r
(#)
f
is_differentiable_in
x0
&
diff
(
(
r
(#)
f
)
,
x0
)
=
r
*
(
diff
(
f
,
x0
)
)
)
proof
end;
theorem
Th16
:
:: FDIFF_1:16
for
x0
being
Real
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
f1
is_differentiable_in
x0
&
f2
is_differentiable_in
x0
holds
(
f1
(#)
f2
is_differentiable_in
x0
&
diff
(
(
f1
(#)
f2
)
,
x0
)
=
(
(
f2
.
x0
)
*
(
diff
(
f1
,
x0
)
)
)
+
(
(
f1
.
x0
)
*
(
diff
(
f2
,
x0
)
)
)
)
proof
end;
theorem
Th17
:
:: FDIFF_1:17
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
f
&
f
|
Z
=
id
Z
holds
(
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
f
`|
Z
)
.
x
=
1 ) )
proof
end;
theorem
:: FDIFF_1:18
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
f1
+
f2
)
&
f1
is_differentiable_on
Z
&
f2
is_differentiable_on
Z
holds
(
f1
+
f2
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
+
f2
)
`|
Z
)
.
x
=
(
diff
(
f1
,
x
)
)
+
(
diff
(
f2
,
x
)
)
) )
proof
end;
theorem
:: FDIFF_1:19
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
f1
-
f2
)
&
f1
is_differentiable_on
Z
&
f2
is_differentiable_on
Z
holds
(
f1
-
f2
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
-
f2
)
`|
Z
)
.
x
=
(
diff
(
f1
,
x
)
)
-
(
diff
(
f2
,
x
)
)
) )
proof
end;
theorem
:: FDIFF_1:20
for
r
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
r
(#)
f
)
&
f
is_differentiable_on
Z
holds
(
r
(#)
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
r
(#)
f
)
`|
Z
)
.
x
=
r
*
(
diff
(
f
,
x
)
)
) )
proof
end;
theorem
:: FDIFF_1:21
for
Z
being
open
Subset
of
REAL
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
(
f1
(#)
f2
)
&
f1
is_differentiable_on
Z
&
f2
is_differentiable_on
Z
holds
(
f1
(#)
f2
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
f1
(#)
f2
)
`|
Z
)
.
x
=
(
(
f2
.
x
)
*
(
diff
(
f1
,
x
)
)
)
+
(
(
f1
.
x
)
*
(
diff
(
f2
,
x
)
)
)
) )
proof
end;
theorem
:: FDIFF_1:22
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
f
&
f
|
Z
is
V8
() holds
(
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
f
`|
Z
)
.
x
=
0
) )
proof
end;
theorem
:: FDIFF_1:23
for
r
,
p
being
Real
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
f
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
r
*
x
)
+
p
) holds
(
f
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
f
`|
Z
)
.
x
=
r
) )
proof
end;
theorem
Th24
:
:: FDIFF_1:24
for
f
being
PartFunc
of
REAL
,
REAL
for
x0
being
real
number
st
f
is_differentiable_in
x0
holds
f
is_continuous_in
x0
proof
end;
theorem
:: FDIFF_1:25
for
X
being
set
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_differentiable_on
X
holds
f
|
X
is
continuous
proof
end;
theorem
Th26
:
:: FDIFF_1:26
for
X
being
set
for
Z
being
open
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
st
f
is_differentiable_on
X
&
Z
c=
X
holds
f
is_differentiable_on
Z
proof
end;
theorem
:: FDIFF_1:27
ex
R
being
RestFunc
st
(
R
.
0
=
0
&
R
is_continuous_in
0
)
proof
end;
definition
let
f
be
PartFunc
of
REAL
,
REAL
;
attr
f
is
differentiable
means
:
Def8
:
:: FDIFF_1:def 8
f
is_differentiable_on
dom
f
;
end;
::
deftheorem
Def8
defines
differentiable
FDIFF_1:def 8 :
for
f
being
PartFunc
of
REAL
,
REAL
holds
(
f
is
differentiable
iff
f
is_differentiable_on
dom
f
);
Lm1
:
{}
REAL
is
closed
proof
end;
Lm2
:
[#]
REAL
is
open
proof
end;
registration
cluster
V1
()
V4
(
REAL
)
V5
(
REAL
)
V6
() non
empty
total
quasi_total
complex-valued
ext-real-valued
real-valued
differentiable
for
Element
of
K19
(
K20
(
REAL
,
REAL
));
existence
ex
b
1
being
Function
of
REAL
,
REAL
st
b
1
is
differentiable
proof
end;
end;
theorem
:: FDIFF_1:28
for
Z
being
open
Subset
of
REAL
for
f
being
differentiable
PartFunc
of
REAL
,
REAL
st
Z
c=
dom
f
holds
f
is_differentiable_on
Z
proof
end;