homeomorphism between a normed space and a ball

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have the following homeomorphism somewhere?

def normed_space.homeomorph_ball (E : Type*) [normed_group E] [normed_space real E] :
  homeomorph E (metric.ball (0 : E) 1)

[Yury G. Kudryashov]

I need any homeomorphism of this type, not some specific one.

[Yury G. Kudryashov]

I came up with

def normed_space.homeomorph_unit_ball : E ≃ₜ ball (0 : E) 1 :=
{ to_fun := λ x,
    begin
      refine ⟨(1 + ∥x∥)⁻¹ • x, mem_ball_zero_iff.2 _⟩,
      have : ∥x∥ < |1 + ∥x∥| := (lt_one_add _).trans_le (le_abs_self _),
      rwa [norm_smul, real.norm_eq_abs, abs_inv, ← div_eq_inv_mul,
        div_lt_one ((norm_nonneg x).trans_lt this)],
    end,
  inv_fun := λ x, (1 - ∥(x : E)∥)⁻¹ • (x : E),
  left_inv := λ x,
    begin
      have : 0 < 1 + ∥x∥ := (norm_nonneg x).trans_lt (lt_one_add _),
      field_simp [this.ne', abs_of_pos this, norm_smul, smul_smul, real.norm_eq_abs, abs_div]
    end,
  right_inv := λ x, subtype.ext
    begin
      have : 0 < 1 - ∥(x : E)∥ := sub_pos.2 (mem_ball_zero_iff.1 x.2),
      field_simp [norm_smul, smul_smul, real.norm_eq_abs, abs_div, abs_of_pos this, this.ne']
    end,
  continuous_to_fun := continuous_subtype_mk _ $
    ((continuous_const.add continuous_norm).inv₀
      (λ x, ((norm_nonneg x).trans_lt (lt_one_add _)).ne')).smul continuous_id,
  continuous_inv_fun := continuous.smul
    ((continuous_const.sub continuous_subtype_coe.norm).inv₀ $
      λ x, (sub_pos.2 $ mem_ball_zero_iff.1 x.2).ne') continuous_subtype_coe }