inv — Mathlib

English

If f has a local minimum at a and f is eventually positive near a, then the inverse function f^{-1} has a local maximum at f(a).

Русский

Если f имеет локальный минимум в точке a, и близко к a функция положительна, то наоборот f^{-1} имеет локальный максимум в точке f(a).

LaTeX

$$IsLocalMin\,f\,a \wedge (\forall^\infty z \in \mathcal{N}(a), 0 < f(z)) \Rightarrow IsLocalMax\,f^{-1}\, (f(a))$$

Lean4

theorem inv {f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ z in 𝓝 a, 0 < f z) : IsLocalMax f⁻¹ a := by
  filter_upwards [h1, h2] with z h3 h4 using (inv_le_inv₀ h4 h2.self_of_nhds).mpr h3

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