isBigOWith_congr — Mathlib

English

If f1 → f2 is l-equivalent and g1 → g2 is l-equivalent, then IsBigOWith c l f1 g1 is equivalent to IsBigOWith c l f2 g2.

Русский

Если f1 ≡ f2 по l и g1 ≡ g2 по l, то IsBigOWith c l f1 g1 эквивалентно IsBigOWith c l f2 g2.

LaTeX

$$$ IsBigOWith\ c\ l\ f1\ g1 \leftrightarrow IsBigOWith\ c\ l\ f2\ g2 $$$

Lean4

theorem isBigOWith_congr (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
    IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂ :=
  by
  simp only [IsBigOWith_def]
  subst c₂
  apply Filter.eventually_congr
  filter_upwards [hf, hg] with _ e₁ e₂
  rw [e₁, e₂]

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