mul_limZero_left — Mathlib

English

If g has LimZero, then f*g has LimZero (provided f is a CauSeq): LimZero(g) → LimZero(f*g).

Русский

Если g имеет LimZero, то f*g имеет LimZero (при условии, что f — CauSeq): LimZero(g) → LimZero(f*g).

LaTeX

$$$\text{LimZero}(g) \Rightarrow \text{LimZero}(f \cdot g)$$$

Lean4

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

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