isBigOWith_const_const — Mathlib

English

Equivalence between IsBigOWith c l f'' 0 and f'' =ᶠ[l] 0; symbolically, (IsBigOWith c l f'' 0) ↔ (f'' =ᶠ[l] 0).

Русский

Эквивалентность: IsBigOWith c l f'' 0 эквивалентно f'' =ᶠ[l] 0.

LaTeX

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

Lean4

theorem isBigOWith_const_const (c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) :
    IsBigOWith (‖c‖ / ‖c'‖) l (fun _x : α => c) fun _x => c' :=
  by
  simp only [IsBigOWith_def]
  apply univ_mem'
  intro x
  rw [mem_setOf, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hc')]

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