congr — Mathlib

English

If h is IsBigOWith c l f g and f ≡ f' pointwise, then IsBigOWith c l f' g.

Русский

Если h = IsBigOWith c l f g и f(x) = f'(x) для всех x, то IsBigOWith c l f' g.

LaTeX

$$$ IsBigOWith\ c\ l\ f\ g \rightarrow \forall x, f(x)=f'(x) \Rightarrow IsBigOWith c l f' g $$$

Lean4

theorem congr (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
    IsBigOWith c₂ l f₂ g₂ :=
  h.congr' hc (univ_mem' hf) (univ_mem' hg)

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