tendsto_atTop_atBot_of_antitone — Mathlib

English

If f is antitone and for every b there exists a with f(a) ≤ b, then f tends to atBot as its argument tends to atTop.

Русский

Если f антимонотонна и для каждого b существует a с f(a) ≤ b, тогда f стремится к -∞ по мере стремления аргумента к +∞.

LaTeX

$$$\operatorname{Tendsto} f\; \operatorname{atTop} \operatorname{atBot}$$$

Lean4

theorem tendsto_atTop_atBot_of_antitone [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f)
    (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atTop atBot :=
  @tendsto_atTop_atTop_of_monotone _ βᵒᵈ _ _ _ hf h

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