How to show a function is a retraction

Stream: new members

[Joseph Cooper]

import Mathlib

open Set
open Function

def complex_nth_hawaiian_circle (n : ℕ): Set ℂ :=
  Metric.sphere (1/((n:ℕ)+1)) (1/((n:ℕ)+1))

def hawaiian_earring_complex: Set ℂ:=
  ⋃ (n:ℕ), complex_nth_hawaiian_circle n

open Classical in
noncomputable
def my_function (n: ℕ): ℂ → ℂ:=
  Set.piecewise ((complex_nth_hawaiian_circle n)) (id) (fun z ↦ 0)


-- want to show f is a retraction
example (n:ℕ): CategoryTheory.retraction (my_function n):= by
  sorry

I wish to show that my function, when restricted to the Hawaiian earring, is a retraction from the Hawaiian earring to the nth circle. How would one usually write this, using definitions from Mathlib?