right_le_add_of_lt_one — Mathlib

English

If f1 = o_l f2, then f2 = O_l (f1 + f2).

Русский

Если f1 = o_l f2, то f2 = O_l (f1 + f2).

LaTeX

$$$\\displaystyle \\text{If } f_1 = o_l f_2, \\; f_2 = O_l (f_1 + f_2).$$$

Lean4

theorem right_le_add_of_lt_one {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) :
    IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x :=
  (h.neg_right.right_le_sub_of_lt_one hc).neg_right.of_neg_left.congr rfl (fun _ ↦ rfl) fun x ↦ by
    rw [neg_sub, sub_neg_eq_add]

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