closure — Mathlib

English

If a function has a local minimum on a set at a, and is continuous on closure, then it preserves a local minimum at a in closure.

Русский

Если функция имеет локальный минимум на множестве в точке a и непрерывна на замкнутости, минимум сохраняется в closure.

LaTeX

$$IsLocalMinOn f s a → ContinuousOn f (closure s) → IsLocalMinOn f (closure s) a.$$

Lean4

protected theorem closure (h : IsLocalMinOn f s a) (hc : ContinuousOn f (closure s)) : IsLocalMinOn f (closure s) a :=
  IsLocalMaxOn.closure h.dual hc

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