congr_left

Mathlib.Analysis.Asymptotics.TVS

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

English

If f =O_{𝕜;l} g and g =o_{𝕜;l} k, then f =o_{𝕜;l} k.

Русский

Если f =O_{𝕜;l} g и g =o_{𝕜;l} k, тогда f =o_{𝕜;l} k.

LaTeX

$$$f =O_{𝕜;l} g \\to g =o_{𝕜;l} k \\Rightarrow f =o_{𝕜;l} k.$$$

Lean4

theorem congr_left (h : f₁ =o[𝕜; l] g) (hf : ∀ x, f₁ x = f₂ x) : f₂ =o[𝕜; l] g :=
  h.congr hf fun _ ↦ rfl

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

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

Разделы

Аффилиация

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