tendsto_inv_smul — Mathlib

English

If g = o(g) relative to a function f, then the inverse-smul variant tends to zero along l.

Русский

Если g = o(f), то вариация умножения на обратную величину стремится к нулю вдоль l.

LaTeX

$$$ g =o_{𝕜;l} f \Rightarrow Tendsto (\lambda x. f(x)^{-1} \cdot g(x))\ l (\mathcal{N}_0). $$$

Lean4

theorem tendsto_inv_smul [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} (h : g =o[𝕜; l] f) :
    Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0) :=
  by
  rw [← isLittleOTVS_one (𝕜 := 𝕜), isLittleOTVS_iff]
  intro U hU
  rcases (h.smul_left f⁻¹).1 U hU with ⟨V, hV₀, hV⟩
  refine ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x hx ↦ hx.trans ?_⟩
  by_cases hx₀ : f x = 0 <;> simp [hx₀, egauge_zero_right _ (Filter.nonempty_of_mem hV₀)]

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