insert — Mathlib

English

If h and h' are two IsBigOWith bounds, then their max bound on l ⊔ l' holds.

Русский

Если есть две границы IsBigOWith, их максимум на l ⊔ l' образует границу.

LaTeX

$$$\text{If } h: \text IsBigOWith c l f g' \text{ and } h': \text IsBigOWith c' l' f g', \text{ then } \text IsBigOWith (\max(c,c')) (l ⊔ l') f g'$$$

Lean4

protected theorem insert [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F}
    (h1 : IsBigOWith C (𝓝[s] x) g g') (h2 : ‖g x‖ ≤ C * ‖g' x‖) : IsBigOWith C (𝓝[insert x s] x) g g' :=
  (isBigOWith_insert h2).mpr h1

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