isLocalMin_of_anti_mono — Mathlib

English

Let α be a linearly ordered topological space and β a preorder. If a < b < c in α and a function f: α → β is antitone on (a, b] and monotone on [b, c), then f has a local minimum at b; i.e., there exists a neighborhood U of b such that f(b) ≤ f(x) for all x ∈ U.

Русский

Пусть α — линейно упорядоченное топологическое пространство и β — предупорядочение. Пусть a < b < c в α и f: α → β удовлетворяет, что на (a, b] функция antyонна, а на [b, c) монотонна. Тогда в точке b функция достигает локального минимума: существует окрестность U(b), такая что ∀ x ∈ U, f(b) ≤ f(x).

LaTeX

$$$\\forall a,b,c\\in \\alpha\\ (a

Lean4

/-- If `f` is antitone on `(a,b]` and monotone on `[b,c)` then `f` has
a local minimum at `b`. -/
theorem isLocalMin_of_anti_mono {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {β : Type*}
    [Preorder β] {a b c : α} (g₀ : a < b) (g₁ : b < c) {f : α → β} (h₀ : AntitoneOn f (Ioc a b))
    (h₁ : MonotoneOn f (Ico b c)) : IsLocalMin f b :=
  mem_of_superset (Ioo_mem_nhds g₀ g₁) (fun x hx => by rcases le_total x b <;> aesop)

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