tendsto_atTop_atBot_iff_of_antitone

English

If f is antitone, Tendsto f atTop to atBot is equivalent to: for every b there exists a with f(a) ≤ b.

Русский

Если f антимонотонна, тогда сходимость f от atTop к atBot эквивалентна существованию a такой, что f(a) ≤ b для данного b.

LaTeX

$$$\text{Tendsto } f\ atTop\ atBot \leftrightarrow \forall b, \exists a, f(a) \le b$$$

Lean4

theorem tendsto_atTop_atBot_iff_of_antitone (hf : Antitone f) : Tendsto f atTop atBot ↔ ∀ b : β, ∃ a, f a ≤ b :=
  tendsto_atTop_atTop_iff_of_monotone (β := βᵒᵈ) hf

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