tendsto.units

Stream: Is there code for X?

[Jireh Loreaux]

Do we have this? I couldn't find it anywhere. Ignore the import that is too strong.

import analysis.normed_space.units

variables {ι R : Type*} [monoid R] [topological_space R] [has_continuous_mul R] [t2_space R]
open filter
open_locale topological_space

@[simps]
def tendsto.units {f : ι → Rˣ} {r₁ r₂ : R} {l : filter ι} [l.ne_bot]
  (h₁ : tendsto (coe ∘ f) l (𝓝 r₁)) (h₂ : tendsto (units.inv ∘ f) l (𝓝 r₂)) : Rˣ :=
{ val := r₁,
  inv := r₂,
  val_inv := tendsto_nhds_unique (by simpa using h₁.mul h₂) tendsto_const_nhds,
  inv_val := tendsto_nhds_unique (by simpa using h₂.mul h₁) tendsto_const_nhds }

[Eric Wieser]

It probably shouldn't be stated with units.inv, which isn't simp-normal form

[Eric Wieser]

Instead as (λ u, ↑(u⁻¹)) would likely be better