Подстраница "Користувач:Галактион/Теорема Коші про середнє значення" создана для того, чтобы перенести информацию из раздела "Обговорення" статьи "Теорема Коші про середнє значення ". Галактион 04:40, 5 березня 2010 (UTC)
t
⊢
X
f
×
Y
f
⊆
R
2
∧
X
g
×
Y
g
⊆
R
2
∧
{
a
,
b
}
⊆
R
∧
a
<
b
∧
[
a
,
b
]
⊆
X
f
∩
X
g
∧
f
:
X
f
↦
Y
f
∧
g
:
X
g
↦
Y
g
∧
{
f
,
g
}
⊆
C
o
n
t
(
[
a
,
b
]
)
∧
{
f
,
g
}
⊆
C
o
n
t
1
(
(
a
,
b
)
)
→
(
∀
x
∈
(
a
,
b
)
(
g
′
(
x
)
≠
0
)
→
∃
c
∈
(
a
,
b
)
(
f
(
b
)
−
f
(
a
)
g
(
b
)
−
g
(
a
)
=
f
′
(
c
)
g
′
(
c
)
)
)
{\displaystyle {\begin{aligned}t\vdash \quad \mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }\subseteq \mathbb {R} ^{2}\ \land \ \mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }\subseteq \mathbb {R} ^{2}\ \land \ \{a,\ b\}\subseteq \mathbb {R} \ \land \ a<b\ \land \ [a,\ b]\subseteq \mathbb {X} _{\mathrm {f} }\cap \mathbb {X} _{\mathrm {g} }\ \ \land \\\ \mathrm {f} :\mathbb {X} _{\mathrm {f} }\mapsto \mathbb {Y} _{\mathrm {f} }\ \land \ \mathrm {g} :\mathbb {X} _{\mathrm {g} }\mapsto \mathbb {Y} _{\mathrm {g} }\ \land \ \{\mathrm {f} ,\ \mathrm {g} \}\subseteq \mathrm {C_{ont}} ([a,\ b])\ \land \ \{\mathrm {f} ,\ \mathrm {g} \}\subseteq \mathrm {C_{ont}^{1}} ((a,\ b))\\\ \to \ \ (\forall _{x\ \in \ (a,b)}\ (g'(x)\neq 0)\ \ \to \ \ \exists _{c\ \in \ (a,b)}\ ({\frac {f(b)-f(a)}{g(b)-g(a)}}={\frac {f'(c)}{g'(c)}})\ )\end{aligned}}}
t
⊢
{
d
o
m
(
f
)
×
c
o
d
(
f
)
,
d
o
m
(
g
)
×
c
o
d
(
g
)
}
⊆
P
(
R
2
)
∧
{
a
,
b
}
⊆
R
∧
a
<
b
∧
[
a
,
b
]
⊆
d
o
m
(
f
)
∩
d
o
m
(
g
)
∧
{
f
,
g
}
⊆
C
o
n
t
(
[
a
,
b
]
)
∧
{
f
,
g
}
⊆
C
o
n
t
1
(
(
a
,
b
)
)
→
(
∀
x
(
x
∈
(
a
,
b
)
→
g
′
(
x
)
≠
0
)
→
∃
c
(
c
∈
(
a
,
b
)
∧
f
(
b
)
−
f
(
a
)
g
(
b
)
−
g
(
a
)
=
f
′
(
c
)
g
′
(
c
)
)
)
{\displaystyle {\begin{aligned}t\vdash \quad \{\mathrm {dom(f)} \times \mathrm {cod(f)} ,\ \mathrm {dom(g)} \times \mathrm {cod(g)} \}\subseteq {\mathcal {P}}(\mathbb {R} ^{2})\ \land \ \{a,b\}\subseteq \mathbb {R} \ \land \ a<b\ \ \land \\\ [a,b]\subseteq \mathrm {dom(f)} \cap \mathrm {dom(g)} \ \land \ \{\mathrm {f} ,\mathrm {g} \}\subseteq \mathrm {C_{ont}} ([a,b])\ \land \ \{\mathrm {f} ,\mathrm {g} \}\subseteq \mathrm {C_{ont}^{1}} ((a,b))\to \\\ (\forall x\ (x\in (a,b)\to g'(x)\neq 0)\ \to \ \exists c\ (c\in (a,b)\ \land \ {\frac {f(b)-f(a)}{g(b)-g(a)}}={\frac {f'(c)}{g'(c)}})\ )\end{aligned}}}
Примечание
Г.М. Фихтенгольц излагает теорему Коши так:
Пусть 1) функции
f
(
x
)
{\displaystyle ~f(x)}
g
(
x
)
{\displaystyle ~g(x)}
[
a
,
b
]
{\displaystyle ~[a,\ b]}
f
′
(
x
)
{\displaystyle ~f'(x)}
g
′
(
x
)
{\displaystyle ~g'(x)}
(
a
,
b
)
{\displaystyle ~(a,\ b)}
g
′
(
x
)
≠
0
{\displaystyle ~g'(x)\neq 0}
(
a
,
b
)
{\displaystyle ~(a,b)}
Тогда между
a
{\displaystyle ~a}
b
{\displaystyle ~b}
c
(
a
<
c
<
b
)
{\displaystyle ~c\ (a<c<b)}
f
(
b
)
−
f
(
a
)
g
(
b
)
−
g
(
a
)
=
f
′
(
c
)
g
′
(
c
)
{\displaystyle ~{\frac {f(b)-f(a)}{g(b)-g(a)}}={\frac {f'(c)}{g'(c)}}}
g
:
X
2
↦
Y
2
{\displaystyle ~\mathrm {g} :X_{2}\mapsto Y_{2}}
g
=
{
⟨
x
,
y
⟩
|
⟨
x
,
y
⟩
∈
R
2
∧
y
=
x
}
{\displaystyle ~\mathrm {g} =\{\langle x,y\rangle |\ \ \langle x,y\rangle \in \mathbb {R} ^{2}\ \land \ y=x\}}
тогда получим следующее:
0.
g
(
x
)
=
x
∧
g
′
(
x
)
=
1
∧
∀
x
(
x
∈
(
a
,
b
)
→
g
′
(
x
)
≠
0
)
{\displaystyle ~0.\ g(x)=x\ \land \ g'(x)=1\ \land \ \forall x\ (x\in (a,b)\to g'(x)\neq 0)}
1.
g
′
=
{
⟨
x
,
y
⟩
|
⟨
x
,
y
⟩
∈
R
2
∧
y
=
1
}
{\displaystyle ~1.\ \mathrm {g'} =\{\langle x,y\rangle |\ \ \langle x,y\rangle \in \mathbb {R} ^{2}\ \land \ y=1\}}
2.
g
(
b
)
=
b
∧
g
(
a
)
=
a
∧
g
(
b
)
−
g
(
a
)
=
b
−
a
∧
g
′
(
c
)
=
1
{\displaystyle ~2.\ g(b)=b\ \land \ g(a)=a\ \land \ g(b)-g(a)=b-a\ \land \ g'(c)=1}
3.
t
⊢
X
×
Y
⊆
R
2
∧
{
a
,
b
}
⊆
R
∧
a
<
b
∧
[
a
,
b
]
⊆
X
∧
f
:
X
↦
Y
∧
f
∈
C
o
n
t
(
[
a
,
b
]
)
∧
f
∈
C
o
n
t
1
(
(
a
,
b
)
)
→
∃
c
∈
(
a
,
b
)
(
f
(
b
)
−
f
(
a
)
b
−
a
=
f
′
(
c
)
)
{\displaystyle {\begin{aligned}3.\ t\vdash \quad X\times Y\subseteq \mathbb {R} ^{2}\ \land \ \{a,b\}\subseteq \mathbb {R} \ \land \ a<b\ \land \ [a,b]\subseteq X\ \land \ \mathrm {f} :X\mapsto Y\ \land \\\ \mathrm {f} \in \mathrm {C_{ont}} ([a,b])\ \land \ \mathrm {f} \in \mathrm {C_{ont}^{1}} ((a,b))\ \to \ \exists _{c\ \in \ (a,b)}({\frac {f(b)-f(a)}{b-a}}=f'(c)\ )\end{aligned}}}
Теорема об остаточном члене
ред.
Руководствуясь теоремой Коши можно доказать следующую теорему
t
⊢
T
1
×
Y
1
⊆
R
2
∧
T
2
×
Y
2
⊆
R
2
∧
{
x
0
,
x
}
⊆
R
∧
x
0
<
x
∧
[
x
0
,
x
]
⊆
T
1
∩
T
2
∧
{\displaystyle ~t\vdash \quad T_{1}\times Y_{1}\subseteq \mathbb {R} ^{2}\ \land \ T_{2}\times Y_{2}\subseteq \mathbb {R} ^{2}\ \land \ \{x_{0},x\}\subseteq \mathbb {R} \ \land \ x_{0}<x\ \land \ [x_{0},x]\subseteq T_{1}\cap T_{2}\ \land }
f
:
T
1
↦
Y
1
∧
g
:
T
2
↦
Y
2
∧
∀
i
∈
N
∧
i
<
n
+
1
(
f
∈
C
o
n
t
i
(
[
x
0
,
x
]
)
)
∧
g
∈
C
o
n
t
0
(
[
x
0
,
x
]
)
∧
f
∈
C
o
n
t
n
+
1
(
(
x
0
,
x
)
)
∧
g
∈
C
o
n
t
1
(
(
x
0
,
x
)
)
∧
∀
t
(
t
∈
(
x
0
,
x
)
→
g
′
(
t
)
≠
0
)
∧
r
n
(
x
0
,
x
)
=
f
(
x
)
−
∑
k
=
0
n
f
(
k
)
(
x
0
)
k
!
(
x
−
x
0
)
k
→
∃
c
(
c
∈
(
x
0
,
x
)
∧
r
n
(
x
0
,
x
)
=
g
(
x
)
−
g
(
x
0
)
g
′
(
c
)
⋅
n
!
⋅
f
(
n
+
1
)
(
c
)
⋅
(
x
−
c
)
n
)
{\displaystyle {\begin{aligned}\mathrm {f} :T_{1}\mapsto Y_{1}\ \land \ \mathrm {g} :T_{2}\mapsto Y_{2}\ \land \ \forall _{i\ \in \ \mathbb {N} \ \land \ i\ <\ n+1}\ (\mathrm {f} \in \mathrm {C_{ont}^{i}} ([x_{0},x]))\ \land \ \mathrm {g} \in \mathrm {C_{ont}^{0}} ([x_{0},x])\ \land \\\ \mathrm {f} \in \mathrm {C_{ont}^{n+1}} ((x_{0},x))\ \land \ \mathrm {g} \in \mathrm {C_{ont}^{1}} ((x_{0},x))\ \land \ \forall t\ (t\in (x_{0},x)\to g'(t)\neq 0)\ \land \\\ r_{n}(x_{0},x)=f(x)-\sum _{k=0}^{n}{\frac {f^{(k)}(x_{0})}{k!}}(x-x_{0})^{k}\ \to \\\ \exists c\ (c\in (x_{0},x)\ \land \ r_{n}(x_{0},x)={\frac {g(x)-g(x_{0})}{g'(c)\cdot n!}}\cdot f^{(n+1)}(c)\cdot (x-c)^{n}\ )\end{aligned}}}
Если конкретизировать функцию
g
:
T
2
↦
Y
2
{\displaystyle ~\mathrm {g} :T_{2}\mapsto Y_{2}}
g
=
{
⟨
t
,
y
⟩
|
⟨
t
,
y
⟩
∈
R
2
∧
y
=
x
−
t
}
{\displaystyle ~\mathrm {g} =\{\langle t,y\rangle |\ \ \langle t,y\rangle \in \mathbb {R} ^{2}\ \land \ y=x-t\}}
тогда получим следующее:
0.
g
(
t
)
=
x
−
t
∧
g
′
(
t
)
=
−
1
∧
∀
t
(
t
∈
(
x
0
,
x
)
→
g
′
(
t
)
≠
0
)
{\displaystyle ~0.\ g(t)=x-t\ \land \ g'(t)=-1\ \land \ \forall t\ (t\in (x_{0},x)\to g'(t)\neq 0)}
1.
g
′
=
{
⟨
t
,
y
⟩
|
⟨
t
,
y
⟩
∈
R
2
∧
y
=
−
1
}
{\displaystyle ~1.\ \mathrm {g'} =\{\langle t,y\rangle |\ \ \langle t,y\rangle \in \mathbb {R} ^{2}\ \land y=-1\}}
2.
g
(
x
)
=
x
−
x
=
0
∧
g
(
x
0
)
=
x
−
x
0
∧
g
(
x
)
−
g
(
x
0
)
=
−
(
x
−
x
0
)
∧
g
′
(
c
)
=
−
1
{\displaystyle ~2.\ g(x)=x-x=0\ \land \ g(x_{0})=x-x_{0}\ \land \ g(x)-g(x_{0})=-(x-x_{0})\ \land \ g'(c)=-1}
3.
t
⊢
T
×
Y
⊆
R
2
∧
{
x
0
,
x
}
⊆
R
∧
x
0
<
x
∧
[
x
0
,
x
]
⊆
T
∧
f
:
T
↦
Y
∧
∀
i
(
i
∈
N
∧
i
<
n
+
1
→
f
∈
C
o
n
t
i
(
[
x
0
,
x
]
)
)
∧
f
∈
C
o
n
t
n
+
1
(
(
a
,
b
)
)
∧
r
n
(
x
0
,
x
)
=
f
(
x
)
−
∑
k
=
0
n
f
k
(
x
0
)
k
!
(
x
−
x
0
)
k
→
∃
c
(
c
∈
(
x
0
,
x
)
∧
r
n
(
x
0
,
x
)
=
f
(
n
+
1
)
(
c
)
n
!
⋅
(
x
−
x
0
)
⋅
(
x
−
c
)
n
)
{\displaystyle {\begin{aligned}3.\ t\vdash \quad T\times Y\subseteq \mathbb {R} ^{2}\ \land \ \{x_{0},x\}\subseteq \mathbb {R} \ \land \ x_{0}<x\ \land \ [x_{0},x]\subseteq T\ \land \ \mathrm {f} :T\mapsto Y\ \land \\\ \forall i\ (i\in \mathbb {N} \ \land \ i<n+1\to \mathrm {f} \in \mathrm {C_{ont}^{i}} ([x_{0},x])\ )\ \land \ \mathrm {f} \in \mathrm {C_{ont}^{n+1}} ((a,b))\ \land \\\ r_{n}(x_{0},x)=f(x)-\sum _{k=0}^{n}{\frac {f^{k}(x_{0})}{k!}}(x-x_{0})^{k}\ \to \\\ \exists c\ (c\in (x_{0},x)\ \land \ r_{n}(x_{0},x)={\frac {f^{(n+1)}(c)}{n!}}\cdot (x-x_{0})\cdot (x-c)^{n}\ )\end{aligned}}}
g
:
T
2
↦
Y
2
{\displaystyle ~\mathrm {g} :T_{2}\mapsto Y_{2}}
g
=
{
⟨
t
,
y
⟩
|
⟨
t
,
y
⟩
∈
R
2
∧
y
=
(
x
−
t
)
n
+
1
}
{\displaystyle ~\mathrm {g} =\{\langle t,y\rangle |\ \ \langle t,y\rangle \in \mathbb {R} ^{2}\ \land \ y=(x-t)^{n+1}\}}
тогда получим следующее:
0.
g
(
t
)
=
(
x
−
t
)
n
+
1
∧
g
′
(
t
)
=
−
(
n
+
1
)
⋅
(
x
−
t
)
n
∧
∀
t
(
t
∈
(
x
0
,
x
)
→
g
′
(
t
)
≠
0
)
{\displaystyle ~0.\ g(t)=(x-t)^{n+1}\ \land \ g'(t)=-(n+1)\cdot (x-t)^{n}\ \land \ \forall t\ (t\in (x_{0},x)\to g'(t)\neq 0)}
1.
g
′
=
{
⟨
t
,
y
⟩
|
⟨
t
,
y
⟩
∈
R
2
∧
y
=
−
(
n
+
1
)
⋅
(
x
−
t
)
n
}
{\displaystyle ~1.\ \mathrm {g'} =\{\langle t,y\rangle |\ \ \langle t,y\rangle \in \mathbb {R} ^{2}\ \land \ y=-(n+1)\cdot (x-t)^{n}\}}
2.
g
(
x
)
=
(
x
−
x
)
n
+
1
=
0
∧
g
(
x
0
)
=
(
x
−
x
0
)
n
+
1
∧
g
(
x
)
−
g
(
x
0
)
=
−
(
x
−
x
0
)
n
+
1
∧
g
′
(
c
)
=
−
(
n
+
1
)
⋅
(
x
−
c
)
n
{\displaystyle {\begin{aligned}2.\ g(x)=(x-x)^{n+1}=0\ \land \ g(x_{0})=(x-x_{0})^{n+1}\ \land \ g(x)-g(x_{0})=-(x-x_{0})^{n+1}\ \land \\\ g'(c)=-(n+1)\cdot (x-c)^{n}\end{aligned}}}
3.
t
⊢
T
×
Y
⊆
R
2
∧
{
x
0
,
x
}
⊆
R
∧
x
0
<
x
∧
[
x
0
,
x
]
⊆
T
∧
f
:
T
↦
Y
∧
∀
i
(
i
∈
N
∧
i
<
n
+
1
→
f
∈
C
o
n
t
i
(
[
x
0
,
x
]
)
)
∧
f
∈
C
o
n
t
n
+
1
(
(
x
0
,
x
)
)
∧
r
n
(
x
0
,
x
)
=
f
(
x
)
−
∑
k
=
0
n
f
k
(
x
0
)
k
!
(
x
−
x
0
)
k
→
∃
c
(
c
∈
(
x
0
,
x
)
∧
r
n
(
x
0
,
x
)
=
f
(
n
+
1
)
(
c
)
(
n
+
1
)
!
⋅
(
x
−
x
0
)
n
+
1
)
{\displaystyle {\begin{aligned}3.\ t\vdash \quad T\times Y\subseteq \mathbb {R} ^{2}\ \land \ \{x_{0},x\}\subseteq \mathbb {R} \ \land \ x_{0}<x\ \land \ [x_{0},x]\subseteq T\ \land \ \mathrm {f} :T\mapsto Y\ \ \land \\\ \forall i\ (i\in \mathbb {N} \ \land i<n+1\to \mathrm {f} \in \mathrm {C_{ont}^{i}} ([x_{0},x])\ )\ \land \ \mathrm {f} \in \mathrm {C_{ont}^{n+1}} ((x_{0},x))\ \land \\\ r_{n}(x_{0},x)=f(x)-\sum _{k=0}^{n}{\frac {f^{k}(x_{0})}{k!}}(x-x_{0})^{k}\ \to \\\ \exists c\ (c\in (x_{0},x)\ \land \ r_{n}(x_{0},x)={\frac {f^{(n+1)}(c)}{(n+1)!}}\cdot (x-x_{0})^{n+1}\ )\end{aligned}}}
![{\displaystyle {\begin{aligned}t\vdash \quad \mathbb {X} _{\mathrm {f} }\times \mathbb {Y} _{\mathrm {f} }\subseteq \mathbb {R} ^{2}\ \land \ \mathbb {X} _{\mathrm {g} }\times \mathbb {Y} _{\mathrm {g} }\subseteq \mathbb {R} ^{2}\ \land \ \{a,\ b\}\subseteq \mathbb {R} \ \land \ a<b\ \land \ [a,\ b]\subseteq \mathbb {X} _{\mathrm {f} }\cap \mathbb {X} _{\mathrm {g} }\ \ \land \\\ \mathrm {f} :\mathbb {X} _{\mathrm {f} }\mapsto \mathbb {Y} _{\mathrm {f} }\ \land \ \mathrm {g} :\mathbb {X} _{\mathrm {g} }\mapsto \mathbb {Y} _{\mathrm {g} }\ \land \ \{\mathrm {f} ,\ \mathrm {g} \}\subseteq \mathrm {C_{ont}} ([a,\ b])\ \land \ \{\mathrm {f} ,\ \mathrm {g} \}\subseteq \mathrm {C_{ont}^{1}} ((a,\ b))\\\ \to \ \ (\forall _{x\ \in \ (a,b)}\ (g'(x)\neq 0)\ \ \to \ \ \exists _{c\ \in \ (a,b)}\ ({\frac {f(b)-f(a)}{g(b)-g(a)}}={\frac {f'(c)}{g'(c)}})\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/addd5e3d54e84b5be717c6a0dafd1e2d32867086)
![{\displaystyle {\begin{aligned}t\vdash \quad \{\mathrm {dom(f)} \times \mathrm {cod(f)} ,\ \mathrm {dom(g)} \times \mathrm {cod(g)} \}\subseteq {\mathcal {P}}(\mathbb {R} ^{2})\ \land \ \{a,b\}\subseteq \mathbb {R} \ \land \ a<b\ \ \land \\\ [a,b]\subseteq \mathrm {dom(f)} \cap \mathrm {dom(g)} \ \land \ \{\mathrm {f} ,\mathrm {g} \}\subseteq \mathrm {C_{ont}} ([a,b])\ \land \ \{\mathrm {f} ,\mathrm {g} \}\subseteq \mathrm {C_{ont}^{1}} ((a,b))\to \\\ (\forall x\ (x\in (a,b)\to g'(x)\neq 0)\ \to \ \exists c\ (c\in (a,b)\ \land \ {\frac {f(b)-f(a)}{g(b)-g(a)}}={\frac {f'(c)}{g'(c)}})\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78c26720fe33e6c511b30537635048018576a179)
![{\displaystyle ~[a,\ b]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ab2cebebc3eb1af54b73f63a1382b3888f7fe86c)
![{\displaystyle {\begin{aligned}3.\ t\vdash \quad X\times Y\subseteq \mathbb {R} ^{2}\ \land \ \{a,b\}\subseteq \mathbb {R} \ \land \ a<b\ \land \ [a,b]\subseteq X\ \land \ \mathrm {f} :X\mapsto Y\ \land \\\ \mathrm {f} \in \mathrm {C_{ont}} ([a,b])\ \land \ \mathrm {f} \in \mathrm {C_{ont}^{1}} ((a,b))\ \to \ \exists _{c\ \in \ (a,b)}({\frac {f(b)-f(a)}{b-a}}=f'(c)\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de7a8ec009f196a9b4395f90aee0ebffa9c7bf30)
![{\displaystyle ~t\vdash \quad T_{1}\times Y_{1}\subseteq \mathbb {R} ^{2}\ \land \ T_{2}\times Y_{2}\subseteq \mathbb {R} ^{2}\ \land \ \{x_{0},x\}\subseteq \mathbb {R} \ \land \ x_{0}<x\ \land \ [x_{0},x]\subseteq T_{1}\cap T_{2}\ \land }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ba2a05a2d8f6e9bc229d3d5f13a306837e03e6ee)
![{\displaystyle {\begin{aligned}\mathrm {f} :T_{1}\mapsto Y_{1}\ \land \ \mathrm {g} :T_{2}\mapsto Y_{2}\ \land \ \forall _{i\ \in \ \mathbb {N} \ \land \ i\ <\ n+1}\ (\mathrm {f} \in \mathrm {C_{ont}^{i}} ([x_{0},x]))\ \land \ \mathrm {g} \in \mathrm {C_{ont}^{0}} ([x_{0},x])\ \land \\\ \mathrm {f} \in \mathrm {C_{ont}^{n+1}} ((x_{0},x))\ \land \ \mathrm {g} \in \mathrm {C_{ont}^{1}} ((x_{0},x))\ \land \ \forall t\ (t\in (x_{0},x)\to g'(t)\neq 0)\ \land \\\ r_{n}(x_{0},x)=f(x)-\sum _{k=0}^{n}{\frac {f^{(k)}(x_{0})}{k!}}(x-x_{0})^{k}\ \to \\\ \exists c\ (c\in (x_{0},x)\ \land \ r_{n}(x_{0},x)={\frac {g(x)-g(x_{0})}{g'(c)\cdot n!}}\cdot f^{(n+1)}(c)\cdot (x-c)^{n}\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/825b0ab73ec97312402859ecaf31a5bb0d042520)
![{\displaystyle {\begin{aligned}3.\ t\vdash \quad T\times Y\subseteq \mathbb {R} ^{2}\ \land \ \{x_{0},x\}\subseteq \mathbb {R} \ \land \ x_{0}<x\ \land \ [x_{0},x]\subseteq T\ \land \ \mathrm {f} :T\mapsto Y\ \land \\\ \forall i\ (i\in \mathbb {N} \ \land \ i<n+1\to \mathrm {f} \in \mathrm {C_{ont}^{i}} ([x_{0},x])\ )\ \land \ \mathrm {f} \in \mathrm {C_{ont}^{n+1}} ((a,b))\ \land \\\ r_{n}(x_{0},x)=f(x)-\sum _{k=0}^{n}{\frac {f^{k}(x_{0})}{k!}}(x-x_{0})^{k}\ \to \\\ \exists c\ (c\in (x_{0},x)\ \land \ r_{n}(x_{0},x)={\frac {f^{(n+1)}(c)}{n!}}\cdot (x-x_{0})\cdot (x-c)^{n}\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4c9485a89c0605c7fb7c8a0c59f6847f80e4042)
![{\displaystyle {\begin{aligned}3.\ t\vdash \quad T\times Y\subseteq \mathbb {R} ^{2}\ \land \ \{x_{0},x\}\subseteq \mathbb {R} \ \land \ x_{0}<x\ \land \ [x_{0},x]\subseteq T\ \land \ \mathrm {f} :T\mapsto Y\ \ \land \\\ \forall i\ (i\in \mathbb {N} \ \land i<n+1\to \mathrm {f} \in \mathrm {C_{ont}^{i}} ([x_{0},x])\ )\ \land \ \mathrm {f} \in \mathrm {C_{ont}^{n+1}} ((x_{0},x))\ \land \\\ r_{n}(x_{0},x)=f(x)-\sum _{k=0}^{n}{\frac {f^{k}(x_{0})}{k!}}(x-x_{0})^{k}\ \to \\\ \exists c\ (c\in (x_{0},x)\ \land \ r_{n}(x_{0},x)={\frac {f^{(n+1)}(c)}{(n+1)!}}\cdot (x-x_{0})^{n+1}\ )\end{aligned}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4a0b04abc87d11a71dc6e268578629d3672d7ea0)