not_nhds_le_map — Mathlib

English

Let f have a local maximum on s at a, and suppose there exists a nonempty upper-neighborhood of f(a). Then 𝓝(f(a)) is not contained in the image of any nhdsWithin(a,s) under f.

Русский

Пусть f имеет локальный максимум на s в точке a, и существует непустое правое окрестность f(a). Тогда 𝓝(f(a)) не содержится в образе 𝓝[s](a) под функцией f.

LaTeX

$$$\mathrm{IsLocalMaxOn}(f,s,a) \land \mathsf{NeBot}(\mathcal{N}_{>[}](f(a))) \Rightarrow \neg\big(\mathcal{N}(f(a)) \le map\ f\ (\mathcal{N}[s](a))\big)$$$

Lean4

theorem not_nhds_le_map [TopologicalSpace β] (hf : IsLocalMaxOn f s a) [NeBot (𝓝[>] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
  @IsLocalMinOn.not_nhds_le_map α βᵒᵈ _ _ _ _ _ ‹_› hf ‹_›

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