isBigO_rev_principal — Mathlib

English

If f is continuous on a compact set s and f(i) ≠ 0 for all i ∈ s, then f is BigO with respect to the principal filter on s, i.e., there is a bound relating f to a constant function on s.

Русский

Если f непрерывна на компактном множестве s и f(i) ≠ 0 для всех i ∈ s, то f ∈ BigO относительно главного фильтра на s.

LaTeX

$$$ \\text{ContinuousOn } f s \\Rightarrow \\text{IsCompact } s \\Rightarrow (\\forall i\\in s, f(i) \\neq 0) \\Rightarrow \\text{IsBigO}( \\text{principal } s) f (\\text{constant}) $$$

Lean4

protected theorem isBigO_rev_principal (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) :
    (fun _ => c) =O[𝓟 s] f :=
  (hf.isBigOWith_rev_principal hs hC c).isBigO

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