add_iff_left — Mathlib

English

If f1 = o_l g and f2 = OWith c1 l f2 g with c1 < c2, then f1+f2 is in OWith c2 l (f+f2) g.

Русский

Если f1 = o_l g и f2 = OWith c1 l f2 g, и c1 < c2, тогда сумма f1+f2 принадлежит OWith c2 l (f+f2) g.

LaTeX

$$$ (f_1 =o[l] g) \\land (f_2 =OWith c_1 l f_2 g) \\land (c_1 < c_2) \\Rightarrow (f_1 + f_2) =OWith c_2 l (f + f_2) 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₂⟩

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