isBigOWith_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

$$$\text{IsBigO}(l,f,g') \land \text{IsBigO}(l',f,g') \Rightarrow \text{IsBigO}(l ⊔ l',f,g')$$$

Lean4

theorem isBigOWith_insert [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F}
    (h : ‖g x‖ ≤ C * ‖g' x‖) : IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g' := by
  simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]

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