of_isLocalMax_of_convex_univ — Mathlib

English

IsExtreme is reflexive: IsExtreme 𝕜 A A holds for any A.

Русский

IsExtreme 𝕜 A A выполняется для любого A.

LaTeX

$$$$ IsExtreme\ 𝕜\ A\ A. $$$$

Lean4

/-- A local maximum of a concave function is a global maximum. -/
theorem of_isLocalMax_of_convex_univ {f : E → β} {a : E} (h_local_max : IsLocalMax f a) (h_conc : ConcaveOn ℝ univ f) :
    ∀ x, f x ≤ f a :=
  IsMinOn.of_isLocalMin_of_convex_univ (β := βᵒᵈ) h_local_max h_conc

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