isLocalMin — Mathlib

English

If IsLocalMinOn f s a and hs : s ∈ 𝓝 a then IsLocalMin f a; the local minimum on a set implies a local minimum at the point.

Русский

Если IsLocalMinOn f s a и hs : s ∈ 𝓝 a, то IsLocalMin f a; локальный минимум на множестве порождает локальный минимум в точке.

LaTeX

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

Lean4

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

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