⊢ Continuous fun z => (exp (-z * I) - exp (z * I)) * I / 2
⊢ Continuous sin
change Continuous fun z => (exp (-z * I) - exp (z * I)) * I / 2
no goals
⊢ Continuous fun z => (exp (-z * I) - exp (z * I)) * I / 2
continuity