tendsto_atBot_atTop_of_antitone — Mathlib

English

If f is antitone and for every b there exists a with f(a) ≤ b, then Tendsto f atBot atTop.

Русский

Если f антимонотонна и для каждого b существует a с f(a) ≤ b, то Tendsto f atBot atTop.

LaTeX

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

Lean4

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

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