isBigOWith_map — Mathlib

English

There exists a transitive relation between IsBigO and EventuallyEq implemented via a composition rule.

Русский

Существует переходное отношение между IsBigO и EventuallyEq, реализованное через правило композиции.

LaTeX

$$$ @Trans\ (f,g) : IsBigOWith c l f g \to\ l.EventuallyEq f f' \to\ l.EventuallyEq g g' \to IsBigOWith c l f' g' $$$

Lean4

@[simp]
theorem isBigOWith_map {k : β → α} {l : Filter β} : IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k) :=
  by
  simp only [IsBigOWith_def]
  exact eventually_map

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