tendsto_atTop_iInf — Mathlib

English

For an antitone f: ι → α with InfConvergenceClass, Tendsto f atTop to inf_i f(i).

Русский

Для антимонотонной f: ι → α при условии InfConvergenceClass: Tendsto f к inf_i f(i) при atTop.

LaTeX

$$$ \operatorname{Tendsto} f \operatorname{atTop} \left( \nhds\left( \inf_{i} f(i) \right)\right)$$$

Lean4

theorem tendsto_atTop_iInf (h_anti : Antitone f) : Tendsto f atTop (𝓝 (⨅ i, f i)) :=
  tendsto_atTop_ciInf h_anti (OrderBot.bddBelow _)

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