isLittleO_completion_right — Mathlib

English

The little-o relation is preserved when passing from f to its image in the completion on the right: f =o[l] ĝ iff f =o[l] g.

Русский

Отношение малого-O сохраняется при переходе от f к его образу в дополнении справа: f =o[l] ĝ эквивалентно f =o[l] g.

LaTeX

$$$ f =o[l]\bigl( (g)̂ \bigr) \iff f =o[l] g, $$$

Lean4

@[simp, norm_cast]
theorem isLittleO_completion_right : f =o[l] (fun x ↦ g x : α → F̂) ↔ f =o[l] g := by
  simp only [isLittleO_iff, norm_coe]

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