isBigO_principal — Mathlib

English

If f is continuous on a compact set s, then f is BigO with respect to the principal filter on s with a finite bound; i.e., there exists a constant C with ∥f(x)∥ ≤ C for x ∈ s.

Русский

Если f непрерывна на компактном множестве s, то существует константа C such that ∥f(x)∥ ≤ C для всех x ∈ s.

LaTeX

$$$ \\text{ContinuousOn } f s \\Rightarrow \\text{IsCompact } s \\Rightarrow f =O[\\mathcal{P} s] (\\lambda _ => c) $$$

Lean4

protected theorem isBigO_principal (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) : f =O[𝓟 s] fun _ => c :=
  (hf.isBigOWith_principal hs hc).isBigO

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