isLittleO_prod_left — Mathlib

English

If IsBigOWith c l f'' g'' holds, then almost surely g''(x) = 0 implies f''(x) = 0.

Русский

Если выполняется IsBigOWith c l f'' g'', то почти наверняка g''(x) = 0 влечет f''(x) = 0.

LaTeX

$$eq_zero_imp : IsBigOWith c l f'' g'' → ∀ᶠ x in l, g'' x = 0 → f'' x = 0$$

Lean4

@[simp]
theorem isLittleO_prod_left : (fun x => (f' x, g' x)) =o[l] k' ↔ f' =o[l] k' ∧ g' =o[l] k' :=
  ⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left h.2⟩

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