exists_forall_le — Mathlib

English

If f: α → β is a function into a linear ordered β and tends to atTop along cofiniteness, there exists a0 ∈ α such that for all a, f(a0) ≤ f(a).

Русский

Если f: α → β стремится к плюс бесконечности вдоль cofiniteness, то существует a0 ∈ α с f(a0) ≤ f(a) для всех a.

LaTeX

$$$\\exists a_0, \\forall a, f(a_0) \\le f(a)$ given $\\operatorname{Tendsto} f \\operatorname{cofinite} \\operatorname{atTop}$$$

Lean4

theorem exists_forall_le [Nonempty α] [LinearOrder β] {f : α → β} (hf : Tendsto f cofinite atTop) :
    ∃ a₀, ∀ a, f a₀ ≤ f a :=
  let ⟨a₀, _, ha₀⟩ := hf.exists_within_forall_le univ_nonempty
  ⟨a₀, fun a => ha₀ a (mem_univ _)⟩

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