isLocalMax

Mathlib.Topology.Order.LocalExtr

URI: https://scilib.ai/kg/mathlib#IsLocalMaxOn.isLocalMax

← MathLib Explorer

English

If IsLocalMaxOn f s a and h : s ∈ 𝓝 a, then IsLocalMax f a.

Русский

Если IsLocalMaxOn f s a и h : s ∈ 𝓝 a, то IsLocalMax f a.

LaTeX

$$$IsLocalMaxOn\ f\ s\ a \rightarrow (s \in 𝓝 a) \rightarrow IsLocalMax f a$$$

Lean4

theorem isLocalMax (hf : IsLocalMaxOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMax f a :=
  have : 𝓝 a ≤ 𝓟 s := le_principal_iff.2 hs
  hf.filter_mono <| le_inf le_rfl this

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

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

Разделы

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

Аффилиация

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