isLittleO_iff_forall_isBigOWith — Mathlib

English

IsLittleO l f g is equivalent to the statement that for all c>0, IsBigOWith c l f g holds, which is the normed version of the relation.

Русский

IsLittleO l f g эквивалентно тому, что для всех c>0 выполняется IsBigOWith c l f g (нормализованная версия).

LaTeX

$$IsLittleO_def' ⇔ ∀ c>0, IsBigOWith c l f g$$

Lean4

/-- Definition of `IsLittleO` in terms of `IsBigOWith`. -/
theorem isLittleO_iff_forall_isBigOWith : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g := by rw [IsLittleO_def]

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