isLittleO_congr — Mathlib

English

If f1 =ᶠ[l] f2 and g1 =ᶠ[l] g2, then f1 = o[l] g1 iff f2 = o[l] g2.

Русский

Если f1 эквивалентно f2 по l и g1 эквивалентно g2 по l, то f1 = o_l(g1) тогда и только тогда f2 = o_l(g2).

LaTeX

$$$ (f_1 =^\!{l}^{} f_2) \land (g_1 =^\!{l}^{} g_2) \Rightarrow \bigl(f_1 = o[l]\, g_1 \iff f_2 = o[l]\, g_2\bigr) $$$

Lean4

theorem isLittleO_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =o[l] g₁ ↔ f₂ =o[l] g₂ :=
  by
  simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => isBigOWith_congr (Eq.refl c) hf hg

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