isEquivalent_of_tendsto_one' — Mathlib

English

If hz holds for all x that v(x) ≠ 0 implies u(x) ≠ 0 and huv is Tendsto(u/v)→1, then u ~_l v.

Русский

Если hz выполняется для всех x при v(x) ≠ 0, u(x) ≠ 0 и huv: Tendsto(u/v)→1, тогда u ~_l v.

LaTeX

$$$ (hz) \\Rightarrow (huv) \\Rightarrow u \\sim_{l} v $$$

Lean4

theorem isEquivalent_of_tendsto_one' (hz : ∀ x, v x = 0 → u x = 0) (huv : Tendsto (u / v) l (𝓝 1)) : u ~[l] v :=
  isEquivalent_of_tendsto_one (Eventually.of_forall hz) huv

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