mathlib

c9c4f40b - chore(topology/compact_open): remove `continuous_map.ev`, and rename related lemmas to `eval'` (#12738)

chore(topology/compact_open): remove `continuous_map.ev`, and rename related lemmas to `eval'` (#12738) This: * Eliminates `continuous_map.ev α β` in favor of `(λ p : C(α, β) × α, p.1 p.2)`, as this unifies better and does not require lean to unfold `ev` at the right time. * Renames `continuous_map.continuous_evalx` to `continuous_map.continuous_eval_const` to match the `smul_const`-style names. * Renames `continuous_map.continuous_ev` to `continuous_map.continuous_eval'` to match `continuous_map.continuous_eval`. * Renames `continuous_map.continuous_ev₁` to `continuous_map.continuous_eval_const'`. * Adds `continuous_map.continuous_coe'` to match `continuous_map.continuous_coe`. * Golfs some nearby lemmas. The unprimed lemma names have the same statement but different typeclasses, so the `ev` lemmas have taken the primed name. See [this zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Evaluation.20of.20continuous.20functions.20is.20continuous/near/275502201) for discussion about whether one set of lemmas can be removed.