isBigOWith_zero_right_iff — Mathlib

English

For any c, f'', l, the relation IsBigOWith c l f'' (0) is equivalent to f'' being eventually zero: f'' =ᶠ[l] 0.

Русский

Для любого c, f'', l равносильно: IsBigOWith c l f'' (0) тогда и только тогда, когда f'' =ᶠ[l] 0.

LaTeX

$$$\\mathrm{IsBigOWith\\;}(c\\,l)\\;f''\\;0 \\iff f''=^l 0$$$

Lean4

@[simp]
theorem isBigOWith_zero_right_iff : (IsBigOWith c l f'' fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0 := by
  simp only [IsBigOWith_def, norm_zero, mul_zero, norm_le_zero_iff, EventuallyEq, Pi.zero_apply]

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