add_add — Mathlib

English

If f1 = o_l g1 and f2 = o_l g2, then f1+f2 = o_l (|g1|+|g2|).

Русский

Если f1 = o_l g1 и f2 = o_l g2, то сумма f1+f2 = o_l (|g1|+|g2|).

LaTeX

$$$ (f_1 =o[l] g_1) \\land (f_2 =o[l] g_2) \\Rightarrow (f_1 + f_2) =o[l] (\\lVert g_1 \\rVert + \\lVert g_2 \\rVert) $$$

Lean4

theorem add_add (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) : (fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖ := by
  refine (h₁.trans_le fun x => ?_).add (h₂.trans_le ?_) <;> simp [abs_of_nonneg, add_nonneg]

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