add_iff_right — Mathlib

English

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

Русский

Если f1 = o_l g и f2 = OWith c1 l g и c1 < c2, то f1+f2 ∈ OWith c2 l g.

LaTeX

$$$ (f_1 =o[l] g) \\land (f_2 =OWith c_1 l g) \\land (c_1 < c_2) \\Rightarrow (f_1 + f_2) =OWith c_2 l g $$$

Lean4

theorem add_iff_right (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 _ ↦ (eq_sub_of_add_eq' rfl).symm) (fun _ ↦ rfl), fun h ↦ h₁.add h⟩

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