isLocalMin — Mathlib

English

If hf : IsMinOn f s a and hs : s ∈ 𝓝 a, then IsLocalMin f a; a local minimum transfers from a global minimum to a local environment.

Русский

Если hf : IsMinOn f s a и hs : s ∈ 𝓝 a, тогда IsLocalMin f a; локальный минимум переносится из глобального минимума в локальную окрестность.

LaTeX

$$$IsMinOn\ f\ s\ a \rightarrow (s \in 𝓝 a) \rightarrow IsLocalMin f a$$$

Lean4

theorem isLocalMin (hf : IsMinOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMin f a :=
  hf.localize.isLocalMin hs

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