exists_within_forall_ge — Mathlib

English

For a nonempty s ⊆ α and a function f: α → β with β linear order, if f tends to cofinitely to atBot, there exists a0 ∈ s with ∀ a ∈ s, f(a) ≤ f(a0).

Русский

Для непустого s и функции f: α → β при линейном порядке β, если f стремится к пределу внизу, то найдётся a0 ∈ s такой, что ∀ a ∈ s, f(a) ≤ f(a0).

LaTeX

$$$\\exists a_0 \\in s, \\forall a \\in s, f(a) \\le f(a_0)$ при $\\operatorname{Tendsto} f \\operatorname{cofinite} \\operatorname{atBot}$$$

Lean4

theorem exists_within_forall_ge [LinearOrder β] {s : Set α} (hs : s.Nonempty) {f : α → β}
    (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) : ∃ a₀ ∈ s, ∀ a ∈ s, f a ≤ f a₀ :=
  @Filter.Tendsto.exists_within_forall_le _ βᵒᵈ _ _ hs _ hf

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