mul_limZero_right — Mathlib

English

If f ≈ g, then for every ε>0 there exists i such that for all j≥i and k≥j, abv(f_k - g_j) < ε.

Русский

Если f ≈ g, тогда для каждого ε>0 существует i такой, что для всех j≥i и k≥j выполняется abv(f_k - g_j) < ε.

LaTeX

$$$f \approx g \Rightarrow \forall \varepsilon>0, \exists i, \forall j\ge i, \forall k\ge j, abv(f_k - g_j) < \varepsilon$$$

Lean4

theorem mul_limZero_right (f : CauSeq β abv) {g} (hg : LimZero g) : LimZero (f * g)
  | ε, ε0 =>
    let ⟨F, F0, hF⟩ := f.bounded' 0
    (hg _ <| div_pos ε0 F0).imp fun _ H j ij =>
      by
      have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0
      rwa [mul_comm F, div_mul_cancel₀ _ (ne_of_gt F0), ← abv_mul] at this

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