isLittleO_ofReal_left — Mathlib

English

For f: α → ℝ and g: α → E, (f · : α → ℂ) = o_l g if and only if f = o_l g.

Русский

Для f: α → ℝ и g: α → E выполняется (f · : α → ℂ) = o_l g тогда и только тогда, когда f = o_l g.

LaTeX

$$$$ (f · : α \to \mathbb{C}) =o[l] g \iff f =o[l] g.$$$$

Lean4

@[simp, norm_cast]
theorem isLittleO_ofReal_left {f : α → ℝ} {g : α → E} : (f · : α → ℂ) =o[l] g ↔ f =o[l] g :=
  (isTheta_ofReal f l).isLittleO_congr_left

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