isLittleO_norm_left — Mathlib

English

Let α be a type, E' a normed space, F' a normed space, and l a filter on α. For any f': α → E' and g': α → F', we have (‖f'(x)‖) = o_l(g') if and only if f' = o_l(g').

Русский

Пусть α — тип; E', F'normированы; l — фильтр на α. Тогда x ↦ ‖f'(x)‖ = o_l(g') тогда и только тогда, когда f' = o_l(g').

LaTeX

$$$\\bigl(x \\mapsto \\|f'(x)\\|\\bigr) =o_l\\ g' \\iff f' =o_l\\ g'$$

Lean4

@[simp]
theorem isLittleO_norm_left : (fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g :=
  by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_norm_left

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