trans_isBigO — Mathlib

English

If f1 ≡ f2 eventually along l and f2 = O[l] g, then f1 = O[l] g.

Русский

Если f1 эквивалентно f2 по l вплоть до концов и f2 = O_l(g), то f1 = O_l(g).

LaTeX

$$$ l.EventuallyEq f_1 f_2 \land f_2 = O[l] g \Rightarrow f_1 = O[l] g $$$

Lean4

@[trans]
theorem _root_.Filter.EventuallyEq.trans_isBigO {f₁ f₂ : α → E} {g : α → F} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =O[l] g) :
    f₁ =O[l] g :=
  h.congr' hf.symm EventuallyEq.rfl

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