isLocalExtr

Mathlib.Topology.Order.LocalExtr

URI: https://scilib.ai/kg/mathlib#IsLocalExtrOn.isLocalExtr

← MathLib Explorer

English

If IsLocalExtrOn f s a holds and hs : s ∈ 𝓝 a, then IsLocalExtr f a.

Русский

Если IsLocalExtrOn f s a выполняется и hs : s ∈ 𝓝 a, тогда IsLocalExtr f a.

LaTeX

$$$IsLocalExtrOn\ f\ s\ a \rightarrow (s \in 𝓝 a) \rightarrow IsLocalExtr f a$$$

Lean4

theorem isLocalExtr (hf : IsLocalExtrOn f s a) (hs : s ∈ 𝓝 a) : IsLocalExtr f a :=
  hf.elim (fun hf => (hf.isLocalMin hs).isExtr) fun hf => (hf.isLocalMax hs).isExtr

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru