exists_forall_ge — Mathlib

English

If f: α → β with β linear order and α nonempty, and f tends to cofinitely to atBot, then there exists a0 with ∀ a, f(a) ≤ f(a0).

Русский

Если для некоторого f: α → β, где β упорядовано, справедливо, что f стремится к нижнему пределу, то существует a0 с ∀ a, f(a) ≤ f(a0).

LaTeX

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

Lean4

theorem exists_forall_ge [Nonempty α] [LinearOrder β] {f : α → β} (hf : Tendsto f cofinite atBot) :
    ∃ a₀, ∀ a, f a ≤ f a₀ :=
  @Filter.Tendsto.exists_forall_le _ βᵒᵈ _ _ _ hf

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