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.

src/analysis/ODE/picard_lindelof.lean

@@ -184,7 +184,7 @@ begin
   refine (complete_space_iff_is_complete_range
     uniform_inducing_to_continuous_map).2 (is_closed.is_complete _),
   rw [range_to_continuous_map, set_of_and],
-  refine (is_closed_eq (continuous_map.continuous_evalx _) continuous_const).inter _,
+  refine (is_closed_eq (continuous_map.continuous_eval_const _) continuous_const).inter _,
   have : is_closed {f : Icc v.t_min v.t_max → E | lipschitz_with v.C f} :=
     is_closed_set_of_lipschitz_with v.C,
   exact this.preimage continuous_map.continuous_coe

src/topology/compact_open.lean

@@ -18,8 +18,7 @@ topological spaces.
 ## Main definitions
 
 * `compact_open` is the compact-open topology on `C(α, β)`. It is declared as an instance.
-* `ev` is the evaluation map `C(α, β) × α → β`. It is continuous as long as `α` is locally compact.
-* `coev` is the coevaluation map `β → C(α, β × α)`. It is always continuous.
+* `continuous_map.coev` is the coevaluation map `β → C(α, β × α)`. It is always continuous.
 * `continuous_map.curry` is the currying map `C(α × β, γ) → C(α, C(β, γ))`. This map always exists
   and it is continuous as long as `α × β` is locally compact.
 * `continuous_map.uncurry` is the uncurrying map `C(α, C(β, γ)) → C(α × β, γ)`. For this map to
@@ -90,34 +89,36 @@ end functorial
 
 section ev
 
-variables (α β)
-
-/-- The evaluation map `map C(α, β) × α → β` -/
-def ev (p : C(α, β) × α) : β := p.1 p.2
-
 variables {α β}
 
-/-- The evaluation map `C(α, β) × α → β` is continuous if `α` is locally compact. -/
-lemma continuous_ev [locally_compact_space α] : continuous (ev α β) :=
+/-- The evaluation map `C(α, β) × α → β` is continuous if `α` is locally compact.
+
+See also `continuous_map.continuous_eval` -/
+lemma continuous_eval' [locally_compact_space α] : continuous (λ p : C(α, β) × α, p.1 p.2) :=
 continuous_iff_continuous_at.mpr $ assume ⟨f, x⟩ n hn,
   let ⟨v, vn, vo, fxv⟩ := mem_nhds_iff.mp hn in
   have v ∈ 𝓝 (f x), from is_open.mem_nhds vo fxv,
   let ⟨s, hs, sv, sc⟩ :=
     locally_compact_space.local_compact_nhds x (f ⁻¹' v)
       (f.continuous.tendsto x this) in
   let ⟨u, us, uo, xu⟩ := mem_nhds_iff.mp hs in
-  show (ev α β) ⁻¹' n ∈ 𝓝 (f, x), from
+  show (λ p : C(α, β) × α, p.1 p.2) ⁻¹' n ∈ 𝓝 (f, x), from
   let w := compact_open.gen s v ×ˢ u in
-  have w ⊆ ev α β ⁻¹' n, from assume ⟨f', x'⟩ ⟨hf', hx'⟩, calc
+  have w ⊆ (λ p : C(α, β) × α, p.1 p.2) ⁻¹' n, from assume ⟨f', x'⟩ ⟨hf', hx'⟩, calc
     f' x' ∈ f' '' s  : mem_image_of_mem f' (us hx')
     ...       ⊆ v            : hf'
     ...       ⊆ n            : vn,
   have is_open w, from (continuous_map.is_open_gen sc vo).prod uo,
   have (f, x) ∈ w, from ⟨image_subset_iff.mpr sv, xu⟩,
   mem_nhds_iff.mpr ⟨w, by assumption, by assumption, by assumption⟩
 
-lemma continuous_ev₁ [locally_compact_space α] (a : α) : continuous (λ f : C(α, β), f a) :=
-continuous_ev.comp (continuous_id.prod_mk continuous_const)
+/-- See also `continuous_map.continuous_eval_const` -/
+lemma continuous_eval_const' [locally_compact_space α] (a : α) : continuous (λ f : C(α, β), f a) :=
+continuous_eval'.comp (continuous_id.prod_mk continuous_const)
+
+/-- See also `continuous_map.continuous_coe` -/
+lemma continuous_coe' [locally_compact_space α] : @continuous (C(α, β)) (α → β) _ _ coe_fn :=
+continuous_pi continuous_eval_const'
 
 instance [t2_space β] : t2_space C(α, β) :=
 ⟨ begin
@@ -211,8 +212,8 @@ begin
     { rintros s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂,
       haveI := is_compact_iff_compact_space.mp hs₁,
       haveI := is_compact_iff_compact_space.mp hs₂,
-      have h₁ := (continuous_ev₁ (⟨x, hxs₁⟩ : s₁)).continuous_at.tendsto.comp (hf s₁ hs₁),
-      have h₂ := (continuous_ev₁ (⟨x, hxs₂⟩ : s₂)).continuous_at.tendsto.comp (hf s₂ hs₂),
+      have h₁ := (continuous_eval_const' (⟨x, hxs₁⟩ : s₁)).continuous_at.tendsto.comp (hf s₁ hs₁),
+      have h₂ := (continuous_eval_const' (⟨x, hxs₂⟩ : s₂)).continuous_at.tendsto.comp (hf s₂ hs₂),
       exact tendsto_nhds_unique h₁ h₂ },
     -- So glue the `f s hs` together and prove that this glued function `f₀` is a limit on each
     -- compact set `s`
@@ -235,7 +236,7 @@ variables (α β)
 
 /-- The coevaluation map `β → C(α, β × α)` sending a point `x : β` to the continuous function
 on `α` sending `y` to `(x, y)`. -/
-def coev (b : β) : C(α, β × α) := ⟨λ a, (b, a), continuous.prod_mk continuous_const continuous_id⟩
+def coev (b : β) : C(α, β × α) := ⟨prod.mk b, continuous_const.prod_mk continuous_id⟩
 
 variables {α β}
 lemma image_coev {y : β} (s : set α) : (coev α β y) '' s = ({y} : set β) ×ˢ s := by tidy
@@ -288,7 +289,7 @@ begin
   apply continuous_of_continuous_uncurry,
   apply continuous_of_continuous_uncurry,
   rw ←homeomorph.comp_continuous_iff' (homeomorph.prod_assoc _ _ _).symm,
-  convert continuous_ev;
+  convert continuous_eval';
   tidy
 end
 
@@ -298,8 +299,7 @@ lemma curry_apply (f : C(α × β, γ)) (a : α) (b : β) : f.curry a b = f (a,
 /-- The uncurried form of a continuous map `α → C(β, γ)` is a continuous map `α × β → γ`. -/
 lemma continuous_uncurry_of_continuous [locally_compact_space β] (f : C(α, C(β, γ))) :
   continuous (function.uncurry (λ x y, f x y)) :=
-have hf : function.uncurry (λ x y, f x y) = ev β γ ∘ prod.map f id, by { ext, refl },
-hf ▸ continuous.comp continuous_ev $ continuous.prod_map f.2 continuous_id
+continuous_eval'.comp $ f.continuous.prod_map continuous_id
 
 /-- The uncurried form of a continuous map `α → C(β, γ)` as a continuous map `α × β → γ` (if `β` is
     locally compact). If `α` is also locally compact, then this is a homeomorphism between the two
@@ -313,7 +313,7 @@ lemma continuous_uncurry [locally_compact_space α] [locally_compact_space β] :
 begin
   apply continuous_of_continuous_uncurry,
   rw ←homeomorph.comp_continuous_iff' (homeomorph.prod_assoc _ _ _),
-  apply continuous.comp continuous_ev (continuous.prod_map continuous_ev continuous_id);
+  apply continuous.comp continuous_eval' (continuous.prod_map continuous_eval' continuous_id);
   apply_instance
 end
 
@@ -342,13 +342,12 @@ def curry [locally_compact_space α] [locally_compact_space β] : C(α × β, γ
 
 /-- If `α` has a single element, then `β` is homeomorphic to `C(α, β)`. -/
 def continuous_map_of_unique [unique α] : β ≃ₜ C(α, β) :=
-{ to_fun := continuous_map.comp ⟨_, continuous_fst⟩ ∘ coev α β,
-  inv_fun := ev α β ∘ (λ f, (f, default)),
+{ to_fun := const α,
+  inv_fun := λ f, f default,
   left_inv := λ a, rfl,
   right_inv := λ f, by { ext, rw unique.eq_default a, refl },
-  continuous_to_fun := continuous.comp (continuous_comp _) continuous_coev,
-  continuous_inv_fun :=
-    continuous.comp continuous_ev (continuous.prod_mk continuous_id continuous_const) }
+  continuous_to_fun := continuous_const',
+  continuous_inv_fun := continuous_eval'.comp (continuous_id.prod_mk continuous_const) }
 
 @[simp] lemma continuous_map_of_unique_apply [unique α] (b : β) (a : α) :
   continuous_map_of_unique b a = b :=

src/topology/continuous_function/bounded.lean

@@ -214,7 +214,7 @@ lemma continuous_coe : continuous (λ (f : α →ᵇ β) x, f x) :=
 uniform_continuous.continuous uniform_continuous_coe
 
 /-- When `x` is fixed, `(f : α →ᵇ β) ↦ f x` is continuous -/
-@[continuity] theorem continuous_evalx {x : α} : continuous (λ f : α →ᵇ β, f x) :=
+@[continuity] theorem continuous_eval_const {x : α} : continuous (λ f : α →ᵇ β, f x) :=
 (continuous_apply x).comp continuous_coe
 
 /-- The evaluation map is continuous, as a joint function of `u` and `x` -/

src/topology/continuous_function/compact.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import topology.continuous_function.bounded
 import topology.uniform_space.compact_separated
+import topology.compact_open
 
 /-!
 # Continuous functions on a compact space
@@ -124,14 +125,17 @@ end
 instance [complete_space β] : complete_space (C(α, β)) :=
 (isometric_bounded_of_compact α β).complete_space
 
+/-- See also `continuous_map.continuous_eval'` -/
 @[continuity] lemma continuous_eval : continuous (λ p : C(α, β) × α, p.1 p.2) :=
 continuous_eval.comp ((isometric_bounded_of_compact α β).continuous.prod_map continuous_id)
 
-@[continuity] lemma continuous_evalx (x : α) : continuous (λ f : C(α, β), f x) :=
+/-- See also `continuous_map.continuous_eval_const` -/
+@[continuity] lemma continuous_eval_const (x : α) : continuous (λ f : C(α, β), f x) :=
 continuous_eval.comp (continuous_id.prod_mk continuous_const)
 
+/-- See also `continuous_map.continuous_coe'` -/
 lemma continuous_coe : @continuous (C(α, β)) (α → β) _ _ coe_fn :=
-continuous_pi continuous_evalx
+continuous_pi continuous_eval_const
 
 -- TODO at some point we will need lemmas characterising this norm!
 -- At the moment the only way to reason about it is to transfer `f : C(α,E)` back to `α →ᵇ E`.

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -227,17 +227,17 @@ equicontinuous. Equicontinuity follows from the Lipschitz control, we check clos
 private lemma closed_candidates_b : is_closed (candidates_b X Y) :=
 begin
   have I1 : ∀ x y, is_closed {f : Cb X Y | f (inl x, inl y) = dist x y} :=
-    λx y, is_closed_eq continuous_evalx continuous_const,
+    λx y, is_closed_eq continuous_eval_const continuous_const,
   have I2 : ∀ x y, is_closed {f : Cb X Y | f (inr x, inr y) = dist x y } :=
-    λx y, is_closed_eq continuous_evalx continuous_const,
+    λx y, is_closed_eq continuous_eval_const continuous_const,
   have I3 : ∀ x y, is_closed {f : Cb X Y | f (x, y) = f (y, x)} :=
-    λx y, is_closed_eq continuous_evalx continuous_evalx,
+    λx y, is_closed_eq continuous_eval_const continuous_eval_const,
   have I4 : ∀ x y z, is_closed {f : Cb X Y | f (x, z) ≤ f (x, y) + f (y, z)} :=
-    λx y z, is_closed_le continuous_evalx (continuous_evalx.add continuous_evalx),
+    λx y z, is_closed_le continuous_eval_const (continuous_eval_const.add continuous_eval_const),
   have I5 : ∀ x, is_closed {f : Cb X Y | f (x, x) = 0} :=
-    λx, is_closed_eq continuous_evalx continuous_const,
+    λx, is_closed_eq continuous_eval_const continuous_const,
   have I6 : ∀ x y, is_closed {f : Cb X Y | f (x, y) ≤ max_var X Y} :=
-    λx y, is_closed_le continuous_evalx continuous_const,
+    λx y, is_closed_le continuous_eval_const continuous_const,
   have : candidates_b X Y = (⋂x y, {f : Cb X Y | f ((@inl X Y x), (@inl X Y y)) = dist x y})
                ∩ (⋂x y, {f : Cb X Y | f ((@inr X Y x), (@inr X Y y)) = dist x y})
                ∩ (⋂x y, {f : Cb X Y | f (x, y) = f (y, x)})