congr' — Mathlib

English

If f = o_{𝕜;l} g1 and g1(x) = g2(x) for all x, then f = o_{𝕜;l} g2.

Русский

Если f = o_{𝕜;l} g1 и для всех x выполняется g1(x) = g2(x), то f = o_{𝕜;l} g2.

LaTeX

$$$f =o[𝕜; l] g_1 \\Rightarrow (\\forall x, g_1(x)=g_2(x)) \\Rightarrow f =o[𝕜; l] g_2.$$$

Lean4

/-- A stronger version of `IsLittleOTVS.congr` that requires the functions only agree along the
filter. -/
theorem congr' (h : f₁ =o[𝕜; l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =o[𝕜; l] g₂ :=
  (isLittleOTVS_congr hf hg).mp h

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