isLittleOTVS_congr — Mathlib

English

If f1 = o_{𝕜;l} g and f1(x) = f2(x) for all x, then f2 = o_{𝕜;l} g.

Русский

Если f1 = o_{𝕜;l} g и f1(x) = f2(x) для всех x, тогда f2 = o_{𝕜;l} g.

LaTeX

$$IsLittleOTVS congr_left: $f_1 = o_{𝕜;l} g$ and $\\forall x, f_1(x)=f_2(x)$ imply $f_2 = o_{𝕜;l} g$.$$

Lean4

theorem isLittleOTVS_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂ :=
  by
  simp only [isLittleOTVS_iff_tendsto_div]
  peel with U hU V hV
  exact tendsto_congr' (hf.comp₂ (egauge _ _ · / egauge _ _ ·) hg)

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