isEquivalent_of_tendsto_one — Mathlib

English

If u - v = o_l v then u ~_l v; equivalently, u/v → 1 along l implies equivalence.

Русский

Если u-v = o_l v, то u ~_l v; эквивалентность эквивалентна тому, что u/v → 1 вдоль l.

LaTeX

$$$ (u - v) = o_{l} v \\Rightarrow u \\sim_{l} v $$$

Lean4

theorem isEquivalent_of_tendsto_one (hz : ∀ᶠ x in l, v x = 0 → u x = 0) (huv : Tendsto (u / v) l (𝓝 1)) : u ~[l] v :=
  by
  rw [isEquivalent_iff_exists_eq_mul]
  exact ⟨u / v, huv, hz.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩

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