Commit 2022-03-17 11:06 c9c4f40b

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 for discussion about whether one set of lemmas can be removed.