isBigOWith_norm_left — Mathlib

English

If a bound holds for f under g' with a neighborhood restricted by insert, and g(x) = 0, then the bound holds with the insert in the neighborhood.

Русский

Если граница для f относительно g' удерживается при вставке x в окрестность, и g(x)=0, тогда граница сохраняется при вставке x.

LaTeX

$$$[\text{TopologicalSpace } \alpha] \; f,g,x,s,C:\; (\|g x\| \le C \|g' x\|) \Rightarrow ( IsBigOWith C (nhdsWithin x (insert x s)) g f' )$$

Lean4

@[simp]
theorem isBigOWith_norm_left : IsBigOWith c l (fun x => ‖f' x‖) g ↔ IsBigOWith c l f' g := by
  simp only [IsBigOWith_def, norm_norm]

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