isBigOWith_inv — Mathlib

English

f = O[l] g' if and only if for every large enough c, f = IsBigOWith c l f g'.

Русский

f = O[l] g' тогда и только тогда, когда для каждого достаточно большого c выполняется f = IsBigOWith c l f g'.

LaTeX

$$$ f =O[l] g' \iff \forall^\infty c \text{ in } atTop, IsBigOWith c l f g' $$$

Lean4

theorem isBigOWith_inv (hc : 0 < c) : IsBigOWith c⁻¹ l f g ↔ ∀ᶠ x in l, c * ‖f x‖ ≤ ‖g x‖ := by
  simp only [IsBigOWith_def, ← div_eq_inv_mul, le_div_iff₀' hc]
    -- We prove this lemma with strange assumptions to get two lemmas below automatically

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