isLocalExtr — Mathlib

English

Let f: α → β, s ⊆ α, and a ∈ α. If a is a local extremum of f on s and s is a neighborhood of a, then f has a local extremum at a.

Русский

Пусть f: α → β, s ⊆ α и a ∈ α. Если a является локальным экстремумом f на s и s содержит окрестность a, то у f есть локальный экстремум в точке a.

LaTeX

$$$\mathrm{IsLocalExtrOn}(f,s,a) \land s \in \mathcal{N}(a) \Rightarrow \mathrm{IsLocalExtr}(f,a)$$$

Lean4

theorem isLocalExtr (hf : IsExtrOn f s a) (hs : s ∈ 𝓝 a) : IsLocalExtr f a :=
  hf.localize.isLocalExtr hs

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