isEquivalent_iff_tendsto_one — Mathlib

English

If u ~_l v then u^{-1} ~_l v^{-1}.

Русский

Если u эквивалентно v по l, то u^{-1} эквивалентно v^{-1} по l.

LaTeX

$$$ u \\sim_{l} v \\Rightarrow u^{-1} \\sim_{l} v^{-1} $$$

Lean4

theorem isEquivalent_iff_tendsto_one (hz : ∀ᶠ x in l, v x ≠ 0) : u ~[l] v ↔ Tendsto (u / v) l (𝓝 1) :=
  by
  constructor
  · intro hequiv
    have := hequiv.isLittleO.tendsto_div_nhds_zero
    simp only [Pi.sub_apply, sub_div] at this
    have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
      (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
    convert this.add key
    · simp
    · simp
  · exact isEquivalent_of_tendsto_one (hz.mono fun x hnvz hz ↦ (hnvz hz).elim)

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