sub_iff_left — Mathlib

English

If f1 = O[l] g, then f1 - f2 = O[l] g is equivalent to f2 = O[l] g.

Русский

Если f1 = O[l] g, тогда f1 - f2 = O[l] g эквивалентно f2 = O[l] g.

LaTeX

$$$ (f_1 =O[l] g) \\Rightarrow (f_1 - f_2) =O[l] g \\Leftrightarrow (f_2 =O[l] g) $$$

Lean4

theorem sub_iff_left (h₂ : f₂ =o[l] g) : (fun x => f₁ x - f₂ x) =o[l] g ↔ (f₁ =o[l] g) :=
  ⟨fun h ↦ h.add h₂ |>.congr (fun _ ↦ sub_add_cancel ..) (fun _ ↦ rfl), fun h ↦ h.sub h₂⟩

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