[Merged by Bors] - feat: generalize&merge ContinuousMap.continuous_eval_const{,'}

Mathlib/Topology/CompactOpen.lean

@@ -184,30 +184,36 @@ theorem continuous_eval' [LocallyCompactSpace α] : Continuous fun p : C(α, β)
       mem_nhds_iff.mpr ⟨w, by assumption, by assumption, by assumption⟩
 #align continuous_map.continuous_eval' ContinuousMap.continuous_eval'
 
-/-- See also `ContinuousMap.continuous_eval_const` -/
-theorem continuous_eval_const' [LocallyCompactSpace α] (a : α) :
-    Continuous fun f : C(α, β) => f a :=
-  continuous_eval'.comp (continuous_id.prod_mk continuous_const)
-#align continuous_map.continuous_eval_const' ContinuousMap.continuous_eval_const'
-
-/-- See also `ContinuousMap.continuous_coe` -/
-theorem continuous_coe' [LocallyCompactSpace α] : @Continuous C(α, β) (α → β) _ _ (↑) :=
-  continuous_pi continuous_eval_const'
-#align continuous_map.continuous_coe' ContinuousMap.continuous_coe'
+/-- Evaluation of a continuous map `f` at a point `a` is continuous in `f`.
+
+Porting note: merged `continuous_eval_const` with `continuous_eval_const'` removing unneeded
+assumptions. -/
+@[continuity]
+theorem continuous_eval_const (a : α) :
+    Continuous fun f : C(α, β) => f a := by
+  refine continuous_def.2 fun U hU ↦ ?_
+  convert ContinuousMap.isOpen_gen (isCompact_singleton (a := a)) hU using 1
+  ext; simp [CompactOpen.gen]
+#align continuous_map.continuous_eval_const' ContinuousMap.continuous_eval_const
+#align continuous_map.continuous_eval_const ContinuousMap.continuous_eval_const
+
+/-- Coercion from `C(α, β)` with compact-open topology to `α → β` with pointwise convergence
+topology is a continuous map.
+
+Porting note: merged `continuous_coe` with `continuous_coe'` removing unneeded assumptions. -/
+theorem continuous_coe : Continuous ((⇑) : C(α, β) → (α → β)) :=
+  continuous_pi continuous_eval_const
+#align continuous_map.continuous_coe' ContinuousMap.continuous_coe
+#align continuous_map.continuous_coe ContinuousMap.continuous_coe
+
+instance [T0Space β] : T0Space C(α, β) :=
+  t0Space_of_injective_of_continuous FunLike.coe_injective continuous_coe
+
+instance [T1Space β] : T1Space C(α, β) :=
+  t1Space_of_injective_of_continuous FunLike.coe_injective continuous_coe
 
 instance [T2Space β] : T2Space C(α, β) :=
-  ⟨by
-    intro f₁ f₂ h
-    obtain ⟨x, hx⟩ := not_forall.mp (mt (FunLike.ext f₁ f₂) h)
-    obtain ⟨u, v, hu, hv, hxu, hxv, huv⟩ := t2_separation hx
-    refine'
-      ⟨CompactOpen.gen {x} u, CompactOpen.gen {x} v,
-        ContinuousMap.isOpen_gen isCompact_singleton hu,
-        ContinuousMap.isOpen_gen isCompact_singleton hv, _, _, _⟩
-    · rwa [CompactOpen.gen, mem_setOf_eq, image_singleton, singleton_subset_iff]
-    · rwa [CompactOpen.gen, mem_setOf_eq, image_singleton, singleton_subset_iff]
-    · rw [disjoint_iff_inter_eq_empty, ← gen_inter, huv.inter_eq,
-        gen_empty_right (singleton_nonempty _)]⟩
+  .of_injective_continuous FunLike.coe_injective continuous_coe
 
 end Ev
 
@@ -274,7 +280,7 @@ theorem tendsto_compactOpen_iff_forall {ι : Type _} {l : Filter ι} (F : ι →
 
 /-- A family `F` of functions in `C(α, β)` converges in the compact-open topology, if and only if
 it converges in the compact-open topology on each compact subset of `α`. -/
-theorem exists_tendsto_compactOpen_iff_forall [LocallyCompactSpace α] [T2Space α] [T2Space β]
+theorem exists_tendsto_compactOpen_iff_forall [LocallyCompactSpace α] [T2Space β]
     {ι : Type _} {l : Filter ι} [Filter.NeBot l] (F : ι → C(α, β)) :
     (∃ f, Filter.Tendsto F l (𝓝 f)) ↔
     ∀ (s : Set α) (hs : IsCompact s), ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f) := by
@@ -291,8 +297,8 @@ theorem exists_tendsto_compactOpen_iff_forall [LocallyCompactSpace α] [T2Space
       rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
       haveI := isCompact_iff_compactSpace.mp hs₁
       haveI := isCompact_iff_compactSpace.mp hs₂
-      have h₁ := (continuous_eval_const' (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
-      have h₂ := (continuous_eval_const' (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
+      have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
+      have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.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`
@@ -411,7 +417,7 @@ theorem continuous_uncurry [LocallyCompactSpace α] [LocallyCompactSpace β] :
 
 /-- The family of constant maps: `β → C(α, β)` as a continuous map. -/
 def const' : C(β, C(α, β)) :=
-  curry ⟨Prod.fst, continuous_fst⟩
+  curry ContinuousMap.fst
 #align continuous_map.const' ContinuousMap.const'
 
 @[simp]
@@ -444,8 +450,7 @@ def curry [LocallyCompactSpace α] [LocallyCompactSpace β] : C(α × β, γ) 
 #align homeomorph.curry Homeomorph.curry
 
 /-- If `α` has a single element, then `β` is homeomorphic to `C(α, β)`. -/
-def continuousMapOfUnique [Unique α] : β ≃ₜ C(α, β)
-    where
+def continuousMapOfUnique [Unique α] : β ≃ₜ C(α, β) where
   toFun := const α
   invFun f := f default
   left_inv a := rfl
@@ -454,7 +459,7 @@ def continuousMapOfUnique [Unique α] : β ≃ₜ C(α, β)
     rw [Unique.eq_default a]
     rfl
   continuous_toFun := continuous_const'
-  continuous_invFun := continuous_eval'.comp (continuous_id.prod_mk continuous_const)
+  continuous_invFun := continuous_eval_const _
 #align homeomorph.continuous_map_of_unique Homeomorph.continuousMapOfUnique
 
 @[simp]

Mathlib/Topology/ContinuousFunction/Algebra.lean

@@ -424,20 +424,20 @@ instance [CommGroup β] [TopologicalGroup β] : TopologicalGroup C(α, β) where
 /-- If `α` is locally compact, and an infinite sum of functions in `C(α, β)`
 converges to `g` (for the compact-open topology), then the pointwise sum converges to `g x` for
 all `x ∈ α`. -/
-theorem hasSum_apply {γ : Type _} [LocallyCompactSpace α] [AddCommMonoid β] [ContinuousAdd β]
-  {f : γ → C(α, β)} {g : C(α, β)} (hf : HasSum f g) (x : α) :
-  HasSum (fun i : γ => f i x) (g x) := by
-  let evₓ : AddMonoidHom C(α, β) β := (Pi.evalAddMonoidHom _ x).comp coeFnAddMonoidHom
-  exact hf.map evₓ (ContinuousMap.continuous_eval_const' x)
+theorem hasSum_apply {γ : Type _} [AddCommMonoid β] [ContinuousAdd β]
+    {f : γ → C(α, β)} {g : C(α, β)} (hf : HasSum f g) (x : α) :
+    HasSum (fun i : γ => f i x) (g x) := by
+  let ev : C(α, β) →+ β := (Pi.evalAddMonoidHom _ x).comp coeFnAddMonoidHom
+  exact hf.map ev (ContinuousMap.continuous_eval_const x)
 #align continuous_map.has_sum_apply ContinuousMap.hasSum_apply
 
-theorem summable_apply [LocallyCompactSpace α] [AddCommMonoid β] [ContinuousAdd β] {γ : Type _}
-    {f : γ → C(α, β)} (hf : Summable f) (x : α) : Summable fun i : γ => f i x :=
+theorem summable_apply [AddCommMonoid β] [ContinuousAdd β] {γ : Type _} {f : γ → C(α, β)}
+    (hf : Summable f) (x : α) : Summable fun i : γ => f i x :=
   (hasSum_apply hf.hasSum x).summable
 #align continuous_map.summable_apply ContinuousMap.summable_apply
 
-theorem tsum_apply [LocallyCompactSpace α] [T2Space β] [AddCommMonoid β] [ContinuousAdd β]
-    {γ : Type _} {f : γ → C(α, β)} (hf : Summable f) (x : α) :
+theorem tsum_apply [T2Space β] [AddCommMonoid β] [ContinuousAdd β] {γ : Type _} {f : γ → C(α, β)}
+    (hf : Summable f) (x : α) :
     ∑' i : γ, f i x = (∑' i : γ, f i) x :=
   (hasSum_apply hf.hasSum x).tsum_eq
 #align continuous_map.tsum_apply ContinuousMap.tsum_apply
@@ -1047,8 +1047,8 @@ section Periodicity
 /-- Summing the translates of `f` by `ℤ • p` gives a map which is periodic with period `p`.
 (This is true without any convergence conditions, since if the sum doesn't converge it is taken to
 be the zero map, which is periodic.) -/
-theorem periodic_tsum_comp_add_zsmul [LocallyCompactSpace X] [AddCommGroup X]
-    [TopologicalAddGroup X] [AddCommMonoid Y] [ContinuousAdd Y] [T2Space Y] (f : C(X, Y)) (p : X) :
+theorem periodic_tsum_comp_add_zsmul [AddCommGroup X] [TopologicalAddGroup X] [AddCommMonoid Y]
+    [ContinuousAdd Y] [T2Space Y] (f : C(X, Y)) (p : X) :
     Function.Periodic (⇑(∑' n : ℤ, f.comp (ContinuousMap.addRight (n • p)))) p := by
   intro x
   by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))

Mathlib/Topology/ContinuousFunction/Compact.lean

@@ -168,17 +168,6 @@ theorem continuous_eval : Continuous fun p : C(α, β) × α => p.1 p.2 :=
   continuous_eval.comp ((isometryEquivBoundedOfCompact α β).continuous.prod_map continuous_id)
 #align continuous_map.continuous_eval ContinuousMap.continuous_eval
 
-/-- See also `ContinuousMap.continuous_eval_const'`. -/
-@[continuity]
-theorem continuous_eval_const (x : α) : Continuous fun f : C(α, β) => f x :=
-  continuous_eval.comp (continuous_id.prod_mk continuous_const)
-#align continuous_map.continuous_eval_const ContinuousMap.continuous_eval_const
-
-/-- See also `ContinuousMap.continuous_coe'`. -/
-theorem continuous_coe : @Continuous C(α, β) (α → β) _ _ (↑) :=
-  continuous_pi continuous_eval_const
-#align continuous_map.continuous_coe ContinuousMap.continuous_coe
-
 -- 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`.
 instance : Norm C(α, E) where norm x := dist x 0

Mathlib/Topology/ContinuousFunction/Ideals.lean

@@ -96,11 +96,11 @@ def idealOfSet (s : Set X) : Ideal C(X, R) where
   smul_mem' c f hf x hx := MulZeroClass.mul_zero (c x) ▸ congr_arg (fun y => c x * y) (hf x hx)
 #align continuous_map.ideal_of_set ContinuousMap.idealOfSet
 
-theorem idealOfSet_closed [LocallyCompactSpace X] [T2Space R] (s : Set X) :
+theorem idealOfSet_closed [T2Space R] (s : Set X) :
     IsClosed (idealOfSet R s : Set C(X, R)) := by
   simp only [idealOfSet, Submodule.coe_set_mk, Set.setOf_forall]
   exact isClosed_iInter fun x => isClosed_iInter fun _ =>
-    isClosed_eq (continuous_eval_const' x) continuous_const
+    isClosed_eq (continuous_eval_const x) continuous_const
 #align continuous_map.ideal_of_set_closed ContinuousMap.idealOfSet_closed
 
 variable {R}
@@ -422,7 +422,7 @@ def continuousMapEval : C(X, characterSpace 𝕜 C(X, 𝕜)) where
     ⟨{  toFun := fun f => f x
         map_add' := fun f g => rfl
         map_smul' := fun z f => rfl
-        cont := continuous_eval_const' x }, by
+        cont := continuous_eval_const x }, by
         rw [CharacterSpace.eq_set_map_one_map_mul]; exact ⟨rfl, fun f g => rfl⟩⟩
   continuous_toFun := Continuous.subtype_mk (continuous_of_continuous_eval map_continuous) _
 #align weak_dual.character_space.continuous_map_eval WeakDual.CharacterSpace.continuousMapEval

Mathlib/Topology/Homotopy/HomotopyGroup.lean

@@ -429,7 +429,7 @@ def genLoopHomeoOfIsEmpty (N x) [IsEmpty N] : Ω^ N X x ≃ₜ X where
   invFun y := ⟨ContinuousMap.const _ y, fun _ ⟨i, _⟩ => isEmptyElim i⟩
   left_inv f := by ext; exact congr_arg f (Subsingleton.elim _ _)
   right_inv _ := rfl
-  continuous_toFun := (ContinuousMap.continuous_eval_const' (0 : N → I)).comp continuous_induced_dom
+  continuous_toFun := (ContinuousMap.continuous_eval_const (0 : N → I)).comp continuous_induced_dom
   continuous_invFun := ContinuousMap.const'.2.subtype_mk _
 #align gen_loop_homeo_of_is_empty genLoopHomeoOfIsEmpty
 

Mathlib/Topology/Separation.lean

@@ -1147,9 +1147,17 @@ instance Prod.t2Space {α : Type _} {β : Type _} [TopologicalSpace α] [T2Space
     (fun h₁ => separated_by_continuous continuous_fst h₁) fun h₂ =>
     separated_by_continuous continuous_snd h₂⟩
 
+/-- If the codomain of an injective continuous function is a Hausdorff space, then so is its
+domain. -/
+theorem T2Space.of_injective_continuous [TopologicalSpace β] [T2Space β] {f : α → β}
+    (hinj : Injective f) (hc : Continuous f) : T2Space α :=
+  ⟨fun _ _ h => separated_by_continuous hc (hinj.ne h)⟩
+
+/-- If the codomain of a topological embedding is a Hausdorff space, then so is its domain.
+See also `T2Space.of_continuous_injective`. -/
 theorem Embedding.t2Space [TopologicalSpace β] [T2Space β] {f : α → β} (hf : Embedding f) :
     T2Space α :=
-  ⟨fun _ _ h => separated_by_continuous hf.continuous (hf.inj.ne h)⟩
+  .of_injective_continuous hf.inj hf.continuous
 #align embedding.t2_space Embedding.t2Space
 
 instance {α β : Type _} [TopologicalSpace α] [T2Space α] [TopologicalSpace β] [T2Space β] :