tendsto_inv₀_cobounded

Stream: Is there code for X?

[Jireh Loreaux]

I'm pretty sure we don't have this. Am I wrong? Feel free to golf.

import Mathlib.Analysis.Normed.Field.Basic

namespace Filter

open Bornology Topology

theorem tendsto_inv₀_cobounded (𝕜 : Type*) [NormedField 𝕜] :
    Tendsto (Inv.inv : 𝕜 → 𝕜) (cobounded 𝕜) (𝓝 0) := by
  rw [←comap_norm_atTop, @NormedAddCommGroup.tendsto_nhds_zero]
  intro ε hε
  filter_upwards [(atTop_basis.comap (‖·‖)).mem_of_mem (i := (ε / 2)⁻¹) (by trivial)] with x hx
  simp only [Set.mem_preimage, Set.mem_Ici] at hx
  rw [norm_inv, inv_lt (lt_of_lt_of_le (by positivity) hx) hε]
  exact ((inv_lt_inv hε (half_pos hε)).mpr <| half_lt_self hε).trans_le hx

end Filter

[Yury G. Kudryashov]

We should add comap Inv.inv (𝓝[≠] 0) = cobounded k

[Jireh Loreaux]

Yes, I have that in my draft.

[Jireh Loreaux]

I'll PR shortly.

[Jireh Loreaux]

#8234

[Yury G. Kudryashov]

I added more lemmas, revived my old branch with (nhds a)⁻¹ = nhds a⁻¹, and made your PR depend on mine. If you prefer to merge the old version, then review my modifications, then feel free to revert your branch and merge the PR.

[Yury G. Kudryashov]

BTW, once this PR is merged (one way or another), I'm going to get rid of comap norm atTop.

[Jireh Loreaux]

Yeah, I was planning on that too, but if you want to that's fine.

[Yury G. Kudryashov]

I started in branch#YK-comap-norm-atTop