feat(Topology): define ContinuousEval{,Const} classes

Mathlib.lean

@@ -4662,6 +4662,8 @@ import Mathlib.Topology.Filter
 import Mathlib.Topology.GDelta
 import Mathlib.Topology.Germ
 import Mathlib.Topology.Gluing
+import Mathlib.Topology.Hom.ContinuousEval
+import Mathlib.Topology.Hom.ContinuousEvalConst
 import Mathlib.Topology.Hom.Open
 import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.Homotopy.Basic

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -80,25 +80,28 @@ variable {𝕜 ι : Type*} {E : ι → Type*} {F : Type*}
     [NormedField 𝕜] [Finite ι] [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
     [TopologicalSpace F] [AddCommGroup F] [TopologicalAddGroup F] [Module 𝕜 F]
 
-/-- Applying a multilinear map to a vector is continuous in both coordinates. -/
-theorem ContinuousMultilinearMap.continuous_eval :
-    Continuous fun p : ContinuousMultilinearMap 𝕜 E F × ∀ i, E i => p.1 p.2 := by
-  cases nonempty_fintype ι
-  let _ := TopologicalAddGroup.toUniformSpace F
-  have := comm_topologicalAddGroup_is_uniform (G := F)
-  refine (UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous
-    (embedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt
-  exact ⟨ball m 1, NormedSpace.isVonNBounded_of_isBounded _ isBounded_ball,
-    ball_mem_nhds _ one_pos⟩
+instance ContinuousMultilinearMap.instContinuousEval :
+    ContinuousEval (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F where
+  continuous_eval := by
+    cases nonempty_fintype ι
+    let _ := TopologicalAddGroup.toUniformSpace F
+    have := comm_topologicalAddGroup_is_uniform (G := F)
+    refine (UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous
+      (embedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt
+    exact ⟨ball m 1, NormedSpace.isVonNBounded_of_isBounded _ isBounded_ball,
+      ball_mem_nhds _ one_pos⟩
+
+@[deprecated (since := "2024-10-05")]
+protected alias ContinuousMultilinearMap.continuous_eval := continuous_eval
 
 namespace ContinuousLinearMap
 
 variable {G : Type*} [AddCommGroup G] [TopologicalSpace G] [Module 𝕜 G] [ContinuousConstSMul 𝕜 F]
   (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F)
 
 lemma continuous_uncurry_of_multilinear :
-    Continuous (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) :=
-  ContinuousMultilinearMap.continuous_eval.comp <| .prodMap (map_continuous f) continuous_id
+    Continuous (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) := by
+  fun_prop
 
 lemma continuousOn_uncurry_of_multilinear {s} :
     ContinuousOn (fun (p : G × (Π i, E i)) ↦ f p.1 p.2) s :=

Mathlib/Analysis/ODE/PicardLindelof.lean

@@ -223,10 +223,10 @@ instance [CompleteSpace E] : CompleteSpace v.FunSpace := by
   refine (completeSpace_iff_isComplete_range isUniformInducing_toContinuousMap).2
       (IsClosed.isComplete ?_)
   rw [range_toContinuousMap, setOf_and]
-  refine (isClosed_eq (ContinuousMap.continuous_eval_const _) continuous_const).inter ?_
+  refine (isClosed_eq (continuous_eval_const _) continuous_const).inter ?_
   have : IsClosed {f : Icc v.tMin v.tMax → E | LipschitzWith v.C f} :=
     isClosed_setOf_lipschitzWith v.C
-  exact this.preimage ContinuousMap.continuous_coe
+  exact this.preimage continuous_coeFun
 
 theorem intervalIntegrable_vComp (t₁ t₂ : ℝ) : IntervalIntegrable f.vComp volume t₁ t₂ :=
   f.continuous_vComp.intervalIntegrable _ _

Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

@@ -240,6 +240,15 @@ theorem embedding_toContinuousMap :
     Embedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) :=
   ⟨inducing_toContinuousMap A B, toContinuousMap_injective⟩
 
+@[to_additive]
+instance instContinuousEvalConst : ContinuousEvalConst (ContinuousMonoidHom A B) A B :=
+  .of_continuous_forget (inducing_toContinuousMap A B).continuous
+
+@[to_additive]
+instance instContinuousEval [LocallyCompactPair A B] :
+    ContinuousEval (ContinuousMonoidHom A B) A B :=
+  .of_continuous_forget (inducing_toContinuousMap A B).continuous
+
 @[to_additive]
 lemma range_toContinuousMap :
     Set.range (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) =
@@ -254,10 +263,10 @@ theorem closedEmbedding_toContinuousMap [ContinuousMul B] [T2Space B] :
   toEmbedding := embedding_toContinuousMap A B
   isClosed_range := by
     simp only [range_toContinuousMap, Set.setOf_and, Set.setOf_forall]
-    refine .inter (isClosed_singleton.preimage (ContinuousMap.continuous_eval_const 1)) <|
+    refine .inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
       isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_
-    exact isClosed_eq (ContinuousMap.continuous_eval_const (x * y)) <|
-      .mul (ContinuousMap.continuous_eval_const x) (ContinuousMap.continuous_eval_const y)
+    exact isClosed_eq (continuous_eval_const (x * y)) <|
+      .mul (continuous_eval_const x) (continuous_eval_const y)
 
 variable {A B C D E}
 

Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

@@ -36,7 +36,7 @@ lemma isClosed_range_toContinuousMultilinearMap [ContinuousSMul 𝕜 E] [T2Space
       ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F)) := by
   simp only [range_toContinuousMultilinearMap, setOf_forall]
   repeat refine isClosed_iInter fun _ ↦ ?_
-  exact isClosed_singleton.preimage (ContinuousMultilinearMap.continuous_eval_const _)
+  exact isClosed_singleton.preimage (continuous_eval_const _)
 
 end IsClosedRange
 
@@ -125,6 +125,10 @@ lemma embedding_toContinuousMultilinearMap :
   haveI := comm_topologicalAddGroup_is_uniform (G := F)
   isUniformEmbedding_toContinuousMultilinearMap.embedding
 
+instance instTopologicalAddGroup : TopologicalAddGroup (E [⋀^ι]→L[𝕜] F) :=
+  embedding_toContinuousMultilinearMap.topologicalAddGroup
+    (toContinuousMultilinearMapLinear (R := ℕ))
+
 @[continuity, fun_prop]
 lemma continuous_toContinuousMultilinearMap :
     Continuous (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F → _)) :=
@@ -159,21 +163,19 @@ lemma closedEmbedding_toContinuousMultilinearMap [T2Space F] :
       (E [⋀^ι]→L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F) :=
   ⟨embedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap⟩
 
-@[continuity, fun_prop]
-theorem continuous_eval_const (x : ι → E) :
-    Continuous fun p : E [⋀^ι]→L[𝕜] F ↦ p x :=
-  (ContinuousMultilinearMap.continuous_eval_const x).comp continuous_toContinuousMultilinearMap
+instance instContinuousEvalConst : ContinuousEvalConst (E [⋀^ι]→L[𝕜] F) (ι → E) F :=
+  .of_continuous_forget continuous_toContinuousMultilinearMap
 
-theorem continuous_coe_fun :
-    Continuous (DFunLike.coe : E [⋀^ι]→L[𝕜] F → (ι → E) → F) :=
-  continuous_pi continuous_eval_const
+@[deprecated (since := "2024-10-05")]
+protected alias continuous_eval_const := continuous_eval_const
+
+@[deprecated (since := "2024-10-05")]
+protected alias continuous_coe_fun := continuous_coeFun
 
 instance instT2Space [T2Space F] : T2Space (E [⋀^ι]→L[𝕜] F) :=
-  .of_injective_continuous DFunLike.coe_injective continuous_coe_fun
+  .of_injective_continuous DFunLike.coe_injective continuous_coeFun
 
-instance instT3Space [T2Space F] : T2Space (E [⋀^ι]→L[𝕜] F) :=
-  letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
-  haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+instance instT3Space [T2Space F] : T3Space (E [⋀^ι]→L[𝕜] F) :=
   inferInstance
 
 section RestrictScalars

Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Topology.Algebra.Module.Multilinear.Bounded
 import Mathlib.Topology.Algebra.Module.UniformConvergence
+import Mathlib.Topology.Hom.ContinuousEvalConst
 
 /-!
 # Topology on continuous multilinear maps
@@ -152,6 +153,11 @@ end UniformAddGroup
 
 variable [TopologicalSpace F] [TopologicalAddGroup F]
 
+instance instTopologicalAddGroup : TopologicalAddGroup (ContinuousMultilinearMap 𝕜 E F) :=
+  letI := TopologicalAddGroup.toUniformSpace F
+  haveI := comm_topologicalAddGroup_is_uniform (G := F)
+  inferInstance
+
 instance instContinuousConstSMul
     {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
     ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F) := by
@@ -188,20 +194,21 @@ theorem hasBasis_nhds_zero :
 
 variable [∀ i, ContinuousSMul 𝕜 (E i)]
 
-theorem continuous_eval_const (x : Π i, E i) :
-    Continuous fun p : ContinuousMultilinearMap 𝕜 E F ↦ p x := by
-  letI := TopologicalAddGroup.toUniformSpace F
-  haveI := comm_topologicalAddGroup_is_uniform (G := F)
-  exact (uniformContinuous_eval_const x).continuous
+instance : ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F where
+  continuous_eval_const x :=
+    let _ := TopologicalAddGroup.toUniformSpace F
+    have _ := comm_topologicalAddGroup_is_uniform (G := F)
+    (uniformContinuous_eval_const x).continuous
 
+@[deprecated (since := "2024-10-05")] protected alias continuous_eval_const := continuous_eval_const
 @[deprecated (since := "2024-04-10")] alias continuous_eval_left := continuous_eval_const
-
-theorem continuous_coe_fun :
-    Continuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F) :=
-  continuous_pi continuous_eval_const
+@[deprecated (since := "2024-10-05")] protected alias continuous_coe_fun := continuous_coeFun
 
 instance instT2Space [T2Space F] : T2Space (ContinuousMultilinearMap 𝕜 E F) :=
-  .of_injective_continuous DFunLike.coe_injective continuous_coe_fun
+  .of_injective_continuous DFunLike.coe_injective continuous_coeFun
+
+instance instT3Space [T2Space F] : T3Space (ContinuousMultilinearMap 𝕜 E F) :=
+  inferInstance
 
 section RestrictScalars
 

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
 import Mathlib.Topology.Algebra.Module.UniformConvergence
+import Mathlib.Topology.Hom.ContinuousEvalConst
 
 /-!
 # Strong topologies on the space of continuous linear maps
@@ -151,12 +152,19 @@ instance instTopologicalAddGroup [TopologicalSpace F] [TopologicalAddGroup F]
   haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
   infer_instance
 
+theorem continuousEvalConst [TopologicalSpace F] [TopologicalAddGroup F]
+    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) :
+    ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F where
+  continuous_eval_const x := by
+    letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
+    haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
+    exact (UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp
+      (embedding_coeFn σ F 𝔖).continuous
+
 theorem t2Space [TopologicalSpace F] [TopologicalAddGroup F] [T2Space F]
-    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) : T2Space (UniformConvergenceCLM σ F 𝔖) := by
-  letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
-  haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
-  haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
-  exact (embedding_coeFn σ F 𝔖).t2Space
+    (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) : T2Space (UniformConvergenceCLM σ F 𝔖) :=
+  have := continuousEvalConst σ F 𝔖 h𝔖
+  .of_injective_continuous DFunLike.coe_injective continuous_coeFun
 
 instance instDistribMulAction (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
     [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) :
@@ -321,11 +329,13 @@ instance uniformSpace [UniformSpace F] [UniformAddGroup F] : UniformSpace (E →
 instance uniformAddGroup [UniformSpace F] [UniformAddGroup F] : UniformAddGroup (E →SL[σ] F) :=
   UniformConvergenceCLM.instUniformAddGroup σ F _
 
-instance [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [T2Space F] :
-    T2Space (E →SL[σ] F) :=
-  UniformConvergenceCLM.t2Space σ F _
-    (Set.eq_univ_of_forall fun x =>
-      Set.mem_sUnion_of_mem (Set.mem_singleton x) (isVonNBounded_singleton x))
+instance instContinuousEvalConst [TopologicalSpace F] [TopologicalAddGroup F]
+    [ContinuousSMul 𝕜₁ E] : ContinuousEvalConst (E →SL[σ] F) E F :=
+  UniformConvergenceCLM.continuousEvalConst σ F _ Bornology.isVonNBounded_covers
+
+instance instT2Space [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜₁ E]
+    [T2Space F] : T2Space (E →SL[σ] F) :=
+  UniformConvergenceCLM.t2Space σ F _ Bornology.isVonNBounded_covers
 
 protected theorem hasBasis_nhds_zero_of_basis [TopologicalSpace F] [TopologicalAddGroup F]
     {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :

Mathlib/Topology/CompactOpen.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton
 -/
+import Mathlib.Topology.Hom.ContinuousEval
 import Mathlib.Topology.ContinuousMap.Basic
 
 /-!
@@ -160,27 +161,24 @@ section Ev
 
 /-- The evaluation map `C(X, Y) × X → Y` is continuous
 if `X, Y` is a locally compact pair of spaces. -/
-@[continuity]
-theorem continuous_eval [LocallyCompactPair X Y] : Continuous fun p : C(X, Y) × X => p.1 p.2 := by
-  simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]
-  rintro ⟨f, x⟩ U ⟨hx : f x ∈ U, hU : IsOpen U⟩
-  rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩
-  filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2
+instance [LocallyCompactPair X Y] : ContinuousEval C(X, Y) X Y where
+  continuous_eval := by
+    simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]
+    rintro ⟨f, x⟩ U ⟨hx : f x ∈ U, hU : IsOpen U⟩
+    rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩
+    filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2
 
-/-- Evaluation of a continuous map `f` at a point `x` is continuous in `f`.
+@[deprecated (since := "2024-10-01")] protected alias continuous_eval := continuous_eval
 
-Porting note: merged `continuous_eval_const` with `continuous_eval_const'` removing unneeded
-assumptions. -/
-@[continuity]
-theorem continuous_eval_const (a : X) : Continuous fun f : C(X, Y) => f a :=
-  continuous_def.2 fun U hU ↦ by simpa using isOpen_setOf_mapsTo (isCompact_singleton (x := a)) hU
+instance : ContinuousEvalConst C(X, Y) X Y where
+  continuous_eval_const x :=
+    continuous_def.2 fun U hU ↦ by simpa using isOpen_setOf_mapsTo isCompact_singleton hU
 
-/-- Coercion from `C(X, Y)` with compact-open topology to `X → Y` with pointwise convergence
-topology is a continuous map.
+@[deprecated (since := "2024-10-01")] protected alias continuous_eval_const := continuous_eval_const
 
-Porting note: merged `continuous_coe` with `continuous_coe'` removing unneeded assumptions. -/
+@[deprecated continuous_coeFun (since := "2024-10-01")]
 theorem continuous_coe : Continuous ((⇑) : C(X, Y) → (X → Y)) :=
-  continuous_pi continuous_eval_const
+  continuous_coeFun
 
 lemma isClosed_setOf_mapsTo {t : Set Y} (ht : IsClosed t) (s : Set X) :
     IsClosed {f : C(X, Y) | MapsTo f s t} :=
@@ -192,7 +190,7 @@ lemma isClopen_setOf_mapsTo (hK : IsCompact K) (hU : IsClopen U) :
 
 @[norm_cast]
 lemma specializes_coe {f g : C(X, Y)} : ⇑f ⤳ ⇑g ↔ f ⤳ g := by
-  refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coe⟩
+  refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩
   suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
     simpa [specializes_iff_pure, nhds_compactOpen]
   exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)
@@ -202,18 +200,18 @@ lemma inseparable_coe {f g : C(X, Y)} : Inseparable (f : X → Y) g ↔ Insepara
   simp only [inseparable_iff_specializes_and, specializes_coe]
 
 instance [T0Space Y] : T0Space C(X, Y) :=
-  t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe
+  t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun
 
 instance [R0Space Y] : R0Space C(X, Y) where
   specializes_symmetric f g h := by
     rw [← specializes_coe] at h ⊢
     exact h.symm
 
 instance [T1Space Y] : T1Space C(X, Y) :=
-  t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coe
+  t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun
 
 instance [R1Space Y] : R1Space C(X, Y) :=
-  .of_continuous_specializes_imp continuous_coe fun _ _ ↦ specializes_coe.1
+  .of_continuous_specializes_imp continuous_coeFun fun _ _ ↦ specializes_coe.1
 
 instance [T2Space Y] : T2Space C(X, Y) := inferInstance
 
@@ -388,7 +386,8 @@ theorem continuous_uncurry [LocallyCompactSpace X] [LocallyCompactSpace Y] :
     Continuous (uncurry : C(X, C(Y, Z)) → C(X × Y, Z)) := by
   apply continuous_of_continuous_uncurry
   rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
-  apply continuous_eval.comp (continuous_eval.prodMap continuous_id)
+  dsimp [Function.comp_def]
+  exact (continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd
 
 /-- The family of constant maps: `Y → C(X, Y)` as a continuous map. -/
 def const' : C(Y, C(X, Y)) :=

Mathlib/Topology/Connected/PathConnected.lean

@@ -198,14 +198,14 @@ compact-open topology on the space `C(I,X)` of continuous maps from `I` to `X`.
 instance topologicalSpace : TopologicalSpace (Path x y) :=
   TopologicalSpace.induced ((↑) : _ → C(I, X)) ContinuousMap.compactOpen
 
-theorem continuous_eval : Continuous fun p : Path x y × I => p.1 p.2 :=
-  ContinuousMap.continuous_eval.comp <|
-    (continuous_induced_dom (α := Path x y)).prodMap continuous_id
+instance : ContinuousEval (Path x y) I X := .of_continuous_forget continuous_induced_dom
 
-@[continuity]
+@[deprecated (since := "2024-10-04")] protected alias continuous_eval := continuous_eval
+
+@[deprecated Continuous.eval (since := "2024-10-04")]
 theorem _root_.Continuous.path_eval {Y} [TopologicalSpace Y] {f : Y → Path x y} {g : Y → I}
-    (hf : Continuous f) (hg : Continuous g) : Continuous fun y => f y (g y) :=
-  Continuous.comp continuous_eval (hf.prod_mk hg)
+    (hf : Continuous f) (hg : Continuous g) : Continuous fun y => f y (g y) := by
+  continuity
 
 theorem continuous_uncurry_iff {Y} [TopologicalSpace Y] {g : Y → Path x y} :
     Continuous ↿g ↔ Continuous g :=
@@ -427,7 +427,7 @@ theorem symm_continuous_family {ι : Type*} [TopologicalSpace ι]
 
 @[continuity]
 theorem continuous_symm : Continuous (symm : Path x y → Path y x) :=
-  continuous_uncurry_iff.mp <| symm_continuous_family _ (continuous_fst.path_eval continuous_snd)
+  continuous_uncurry_iff.mp <| symm_continuous_family _ (continuous_fst.eval continuous_snd)
 
 @[continuity]
 theorem continuous_uncurry_extend_of_continuous_family {ι : Type*} [TopologicalSpace ι]