exists_mem_basis — Mathlib

English

If f = O[l] g, then there exists c > 0 such that f = OWith c l f g.

Русский

Если f = O[l] g, то существует c > 0 такое, что f = OWith c l f g.

LaTeX

$$$ f =O[l] g \rightarrow \exists c>0, IsBigOWith c l f g $$$

Lean4

theorem exists_mem_basis {ι} {p : ι → Prop} {s : ι → Set α} (h : f =O[l] g') (hb : l.HasBasis p s) :
    ∃ c > 0, ∃ i : ι, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖ :=
  flip Exists.imp h.exists_pos fun c h => by simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h

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