d
⊢
X
×
Y
⊆
R
2
∧
f
:
X
↦
Y
∧
v
∈
X
∧
∃
{
u
,
w
}
⊆
X
∧
u
<
w
(
u
<
v
<
w
)
→
{\displaystyle ~d\vdash \ \mathbb {X} \times \mathbb {Y} \subseteq \mathbb {R} ^{2}\ \ \land \ \ \mathrm {f} :\mathbb {X} \mapsto \mathbb {Y} \quad \land \quad v\in \mathbb {X} \ \ \land \ \ \exists _{\{u,w\}\ \subseteq \ \mathbb {X} \ \land \ u\ <\ w}\ (u<v<w)\quad \to }
(
f
h
a
s
a
l
o
c
a
l
m
a
x
i
m
u
m
a
t
v
.
↔
∃
δ
∈
(
0
,
∞
)
(
(
v
−
δ
,
v
+
δ
)
⊆
X
∧
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
x
)
≤
f
(
v
)
)
)
)
{\displaystyle ~(\mathrm {f\ has\ a\ local\ maximum\ at} \ v.\leftrightarrow \exists _{\delta \ \in \ (0,\infty )}\ (\ (v-\delta ,v+\delta )\subseteq \mathbb {X} \ \land \ \forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(x)\leq f(v))\ ))}
∧
{\displaystyle ~\land }
(
f
h
a
s
a
l
o
c
a
l
m
i
n
i
m
u
n
a
t
v
.
↔
∃
δ
∈
(
0
,
∞
)
(
(
v
−
δ
,
v
+
δ
)
⊆
X
∧
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
v
)
≤
f
(
x
)
)
)
)
{\displaystyle ~(\mathrm {f\ has\ a\ local\ minimun\ at} \ v.\leftrightarrow \exists _{\delta \ \in \ (0,\infty )}\ (\ (v-\delta ,v+\delta )\subseteq \mathbb {X} \ \land \ \forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(v)\leq f(x))\ ))}
∧
{\displaystyle ~\land }
(
f
h
a
s
a
l
o
c
a
l
e
x
t
r
e
m
u
m
a
t
v
.
↔
∃
δ
∈
(
0
,
∞
)
(
(
v
−
δ
,
v
+
δ
)
⊆
X
∧
{\displaystyle ~(\mathrm {f\ has\ a\ local\ extremum\ at} \ v.\ \leftrightarrow \ \exists _{\delta \ \in \ (0,\infty )}\ (\ (v-\delta ,v+\delta )\subseteq \mathbb {X} \ \land }
(
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
x
)
≤
f
(
v
)
)
∨
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
v
)
≤
f
(
x
)
)
)
)
)
{\displaystyle ~(\forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(x)\leq f(v))\quad \lor \quad \forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(v)\leq f(x))\ )\ ))}
∧
{\displaystyle ~\land }
(
f
h
a
s
a
s
t
r
i
c
t
l
o
c
a
l
m
a
x
i
m
u
m
a
t
v
.
↔
∃
δ
∈
(
0
,
∞
)
(
(
v
−
δ
,
v
+
δ
)
⊆
X
∧
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
x
)
<
f
(
v
)
)
)
)
{\displaystyle {\begin{aligned}(\mathrm {f\ has\ a\ strict\ local\ maximum\ at} \ v.\ \leftrightarrow \ \exists _{\delta \ \in \ (0,\infty )}\ (\ (v-\delta ,v+\delta )\subseteq \mathbb {X} \quad \land \\\ \forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(x)<f(v))\ ))\end{aligned}}}
∧
{\displaystyle ~\land }
(
f
h
a
s
a
s
t
r
i
c
t
l
o
c
a
l
m
i
n
i
m
u
n
a
t
v
.
↔
∃
δ
∈
(
0
,
∞
)
(
(
v
−
δ
,
v
+
δ
)
⊆
X
∧
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
v
)
<
f
(
x
)
)
)
)
{\displaystyle {\begin{aligned}(\mathrm {f\ has\ a\ strict\ local\ minimun\ at} \ v.\ \leftrightarrow \ \exists _{\delta \ \in \ (0,\infty )}\ (\ (v-\delta ,v+\delta )\subseteq \mathbb {X} \quad \land \\\ \forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(v)<f(x))\ ))\end{aligned}}}
∧
{\displaystyle ~\land }
(
f
h
a
s
a
s
t
r
i
c
t
l
o
c
a
l
e
x
t
r
e
m
u
m
a
t
v
.
↔
∃
δ
∈
(
0
,
∞
)
(
(
v
−
δ
,
v
+
δ
)
⊆
X
∧
{\displaystyle ~(\mathrm {f\ has\ a\ strict\ local\ extremum\ at} \ v.\ \leftrightarrow \ \exists _{\delta \ \in \ (0,\infty )}\ (\ (v-\delta ,v+\delta )\subseteq \mathbb {X} \quad \land }
(
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
x
)
<
f
(
v
)
)
∨
∀
x
∈
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
(
f
(
v
)
<
f
(
x
)
)
)
)
)
{\displaystyle ~(\forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(x)<f(v))\quad \lor \quad \forall _{x\ \in \ (v-\delta ,\ v+\delta )\setminus \{v\}}\ (f(v)<f(x))\ )))}
Примечание
1.
(
v
−
δ
,
v
+
δ
)
=
{
x
|
x
∈
R
∧
v
−
δ
<
x
<
v
+
δ
}
=
{
x
|
x
∈
R
∧
|
v
−
x
|
<
δ
}
{\displaystyle ~(v-\delta ,v+\delta )=\{x|\ \ x\in \mathbb {R} \ \land \ v-\delta <x<v+\delta \}=\{x|\ \ x\in \mathbb {R} \ \land \ |v-x|<\delta \}}
2.
(
v
−
δ
,
v
+
δ
)
∖
{
v
}
=
(
v
−
δ
,
v
)
∪
(
v
,
v
+
δ
)
=
{
x
|
x
∈
R
∧
0
<
|
v
−
x
|
<
δ
}
{\displaystyle ~(v-\delta ,v+\delta )\setminus \{v\}=(v-\delta ,v)\cup (v,v+\delta )=\{x|\ \ x\in \mathbb {R} \ \land \ 0<|v-x|<\delta \}}
Галактион 20:20, 14 серпня 2009 (UTC)