isLittleO_const_id_atBot — Mathlib

English

If c is a constant, then (c) =o (Bornology.cobounded) of the norm of id in a cobounded setting; equivalently, a bounded constant is little-o of the identity in cobounded Bornology.

Русский

Если константа ограничена, то она есть little-o по отношению к тождественному отображению в области COBOUNDED Bornology.

LaTeX

$$$ (f := const\\; c) =o[Bornology.cobounded E'']\\; id $$$

Lean4

theorem isLittleO_const_id_atBot (c : E'') : (fun _x : ℝ => c) =o[atBot] id :=
  isLittleO_const_left.2 <| Or.inr tendsto_abs_atBot_atTop

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