isLittleO_insert — Mathlib

English

If f =O_l g' and f =O_{l'} g', then f =O_{l ⊔ l'} g'.

Русский

Если f =O_l g' и f =O_{l'} g', то f =O_{l ⊔ l'} g'.

LaTeX

$$$(f =O[l] g') \land (f =O[l'] g') \Rightarrow f =O[l ⊔ l'] g'$$$

Lean4

theorem isLittleO_insert [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'} (h : g x = 0) :
    g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g' :=
  by
  simp_rw [IsLittleO_def]
  refine forall_congr' fun c => forall_congr' fun hc => ?_
  rw [isBigOWith_insert]
  rw [h, norm_zero]
  exact mul_nonneg hc.le (norm_nonneg _)

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