congr_left

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigOWith.congr_left

English

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

Русский

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

LaTeX

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

Lean4

theorem congr_left (h : IsBigOWith c l f₁ g) (hf : ∀ x, f₁ x = f₂ x) : IsBigOWith c l f₂ g :=
  h.congr rfl hf fun _ => rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru