congr' — Mathlib

English

If h is IsBigOWith c1 and f1 ≈ f2, g1 ≈ g2, then h is IsBigOWith c2 with c1=c2.

Русский

Если h = IsBigOWith c1 и f1 ≈ f2, g1 ≈ g2, тогда h сохраняет свой вид IsBigOWith c2, где c1=c2.

LaTeX

$$$ IsBigOWith\ c_1\ l\ f_1\ g_1 \rightarrow Eq c_1 c_2 \rightarrow f_1 \approx f_2 \rightarrow g_1 \approx g_2 \rightarrow IsBigOWith\ c\ l\ f_2\ g_2 $$$

Lean4

theorem congr' (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
    IsBigOWith c₂ l f₂ g₂ :=
  (isBigOWith_congr hc hf hg).mp h

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