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