isLittleO_completion_left — Mathlib

English

Passing from g to its completion on the left does not change the little-o relation with f: (ĝ) =o[l] f iff g =o[l] f.

Русский

Перемещение g в дополнение слева не меняет отношение мало‑меньше нуля: ĝ =o[l] f эквивалентно g =o[l] f.

LaTeX

$$$ (\hat{g}) =o[l] f \iff g =o[l] f, $$$

Lean4

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

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