add_iff_left — Mathlib

English

If f2 = O[l] g, then (f1+f2) = O[l] g iff f1 = O[l] g.

Русский

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

LaTeX

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

Lean4

theorem add_iff_left (h₂ : f₂ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g ↔ (f₁ =O[l] g) :=
  ⟨fun h ↦ h.sub h₂ |>.congr (fun _ ↦ add_sub_cancel_right _ _) (fun _ ↦ rfl), fun h ↦ h.add h₂⟩

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