localize — Mathlib

English

If hf : IsMinOn f s a and hs : s ∈ 𝓝 a, then IsLocalMinOn f s a; the local minimum on s follows from a global minimum condition near a.

Русский

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

LaTeX

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

Lean4

theorem localize (hf : IsMinOn f s a) : IsLocalMinOn f s a :=
  hf.filter_mono <| inf_le_right

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