retract to the unit ball

Stream: Is there code for X?

[Jireh Loreaux]

Do we have in Mathlib the retract of a normed space over ℝ onto the closed unit ball (x ↦ ‖x‖⁻¹ • x for 1 ≤ ‖x‖)?

[Eric Wieser]

Best I can do is

/-- Auxiliary construction; an element of norm 1 such that `a * unitOf a = ‖a‖`. -/
private def unitOf (a : α) : α := by classical exact if a = 0 then 1 else ‖a‖ • a⁻¹

[Eric Wieser]

(which I can't link since it was a local private def)

[Yaël Dillies]

I wrote the existence of the image as a lemma somewhere

[Yury G. Kudryashov]

We have docs#inv_norm_smul_mem_closed_unit_ball

[Yury G. Kudryashov]

Ah, you want a piecewise function, sorry.

[Jireh Loreaux]

I've already written it myself, I just wanted to make sure we didn't already have it.