bump to nightly-2023-02-21-22

mathlib commit leanprover-community/mathlib@bd9851c

Mathbin/Analysis/Convolution.lean

@@ -148,7 +148,7 @@ theorem HasCompactSupport.convolution_integrand_bound_right (hcg : HasCompactSup
   hcg.convolution_integrand_bound_right_of_subset L hg hx Subset.rfl
 #align has_compact_support.convolution_integrand_bound_right HasCompactSupport.convolution_integrand_bound_right
 
-theorem Continuous.convolution_integrand_fst [HasContinuousSub G] (hg : Continuous g) (t : G) :
+theorem Continuous.convolution_integrand_fst [ContinuousSub G] (hg : Continuous g) (t : G) :
     Continuous fun x => L (f t) (g (x - t)) :=
   L.continuous₂.comp₂ continuous_const <| hg.comp <| continuous_id.sub continuous_const
 #align continuous.convolution_integrand_fst Continuous.convolution_integrand_fst
@@ -362,7 +362,7 @@ theorem HasCompactSupport.convolutionExistsAt {x₀ : G}
   ext x
   simp only [Homeomorph.neg, sub_eq_add_neg, coe_toAddUnits, Homeomorph.trans_apply,
     Equiv.neg_apply, Equiv.toFun_as_coe, Homeomorph.homeomorph_mk_coe, Equiv.coe_fn_mk,
-    Homeomorph.coe_add_left]
+    Homeomorph.coe_addLeft]
 #align has_compact_support.convolution_exists_at HasCompactSupport.convolutionExistsAt
 
 theorem HasCompactSupport.convolutionExistsRight (hcg : HasCompactSupport g)

Mathbin/Analysis/LocallyConvex/ContinuousOfBounded.lean

@@ -53,7 +53,7 @@ def LinearMap.clmOfExistsBoundedImage (f : E →ₗ[𝕜] F)
   ⟨f,
     by
     -- It suffices to show that `f` is continuous at `0`.
-    refine' continuous_of_continuous_at_zero f _
+    refine' continuous_of_continuousAt_zero f _
     rw [continuousAt_def, f.map_zero]
     intro U hU
     -- Continuity means that `U ∈ 𝓝 0` implies that `f ⁻¹' U ∈ 𝓝 0`.

Mathbin/Analysis/LocallyConvex/WithSeminorms.lean

@@ -442,7 +442,7 @@ theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_infᵢ (p : Seminor
         ⨅ i, (p i).toAddGroupSeminorm.toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace :=
   by
   rw [p.with_seminorms_iff_nhds_eq_infi,
-    TopologicalAddGroup.ext_iff inferInstance (topological_add_group_infᵢ fun i => inferInstance),
+    TopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_infᵢ fun i => inferInstance),
     nhds_infᵢ]
   trace
     "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `congrm #[[expr «expr = »(_, «expr⨅ , »((i), _))]]"
@@ -591,7 +591,7 @@ theorem continuous_of_continuous_comp {q : SeminormFamily 𝕝₂ F ι'} [Topolo
     [TopologicalAddGroup E] [TopologicalSpace F] [TopologicalAddGroup F] (hq : WithSeminorms q)
     (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i, Continuous ((q i).comp f)) : Continuous f :=
   by
-  refine' continuous_of_continuous_at_zero f _
+  refine' continuous_of_continuousAt_zero f _
   simp_rw [ContinuousAt, f.map_zero, q.with_seminorms_iff_nhds_eq_infi.mp hq, Filter.tendsto_infᵢ,
     Filter.tendsto_comap_iff]
   intro i
@@ -718,7 +718,7 @@ theorem LinearMap.withSeminormsInduced [hι : Nonempty ι] {q : SeminormFamily 
     @WithSeminorms 𝕜 E ι _ _ _ _ (q.comp f) (induced f inferInstance) :=
   by
   letI : TopologicalSpace E := induced f inferInstance
-  letI : TopologicalAddGroup E := topological_add_group_induced f
+  letI : TopologicalAddGroup E := topologicalAddGroup_induced f
   rw [(q.comp f).withSeminorms_iff_nhds_eq_infᵢ, nhds_induced, map_zero,
     q.with_seminorms_iff_nhds_eq_infi.mp hq, Filter.comap_infᵢ]
   refine' infᵢ_congr fun i => _

Mathbin/Analysis/Normed/Group/BallSphere.lean

@@ -34,7 +34,7 @@ theorem coe_neg_sphere {r : ℝ} (v : sphere (0 : E) r) : ↑(-v) = (-v : E) :=
   rfl
 #align coe_neg_sphere coe_neg_sphere
 
-instance : HasContinuousNeg (sphere (0 : E) r) :=
+instance : ContinuousNeg (sphere (0 : E) r) :=
   ⟨continuous_neg.subtypeMap _⟩
 
 /-- We equip the ball, in a seminormed group, with a formal operation of negation, namely the
@@ -49,7 +49,7 @@ theorem coe_neg_ball {r : ℝ} (v : ball (0 : E) r) : ↑(-v) = (-v : E) :=
   rfl
 #align coe_neg_ball coe_neg_ball
 
-instance : HasContinuousNeg (ball (0 : E) r) :=
+instance : ContinuousNeg (ball (0 : E) r) :=
   ⟨continuous_neg.subtypeMap _⟩
 
 /-- We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the
@@ -64,6 +64,6 @@ theorem coe_neg_closedBall {r : ℝ} (v : closedBall (0 : E) r) : ↑(-v) = (-v
   rfl
 #align coe_neg_closed_ball coe_neg_closedBall
 
-instance : HasContinuousNeg (closedBall (0 : E) r) :=
+instance : ContinuousNeg (closedBall (0 : E) r) :=
   ⟨continuous_neg.subtypeMap _⟩
 

Mathbin/Analysis/Normed/Order/Lattice.lean

@@ -212,8 +212,7 @@ theorem isClosed_nonneg {E} [NormedLatticeAddCommGroup E] : IsClosed { x : E | 0
 #align is_closed_nonneg isClosed_nonneg
 
 theorem isClosed_le_of_isClosed_nonneg {G} [OrderedAddCommGroup G] [TopologicalSpace G]
-    [HasContinuousSub G] (h : IsClosed { x : G | 0 ≤ x }) :
-    IsClosed { p : G × G | p.fst ≤ p.snd } :=
+    [ContinuousSub G] (h : IsClosed { x : G | 0 ≤ x }) : IsClosed { p : G × G | p.fst ≤ p.snd } :=
   by
   have : { p : G × G | p.fst ≤ p.snd } = (fun p : G × G => p.snd - p.fst) ⁻¹' { x : G | 0 ≤ x } :=
     by

Mathbin/Analysis/NormedSpace/CompactOperator.lean

@@ -225,7 +225,7 @@ theorem IsCompactOperator.add [ContinuousAdd M₂] {f g : M₁ → M₂} (hf : I
     mem_of_superset (inter_mem hAf hBg) fun x ⟨hxA, hxB⟩ => Set.add_mem_add hxA hxB⟩
 #align is_compact_operator.add IsCompactOperator.add
 
-theorem IsCompactOperator.neg [HasContinuousNeg M₄] {f : M₁ → M₄} (hf : IsCompactOperator f) :
+theorem IsCompactOperator.neg [ContinuousNeg M₄] {f : M₁ → M₄} (hf : IsCompactOperator f) :
     IsCompactOperator (-f) :=
   let ⟨K, hK, hKf⟩ := hf
   ⟨-K, hK.neg, mem_of_superset hKf fun x (hx : f x ∈ K) => Set.neg_mem_neg.mpr hx⟩
@@ -349,7 +349,7 @@ theorem IsCompactOperator.continuous {f : M₁ →ₛₗ[σ₁₂] M₂} (hf : I
   haveI : UniformAddGroup M₂ := topological_add_commGroup_is_uniform
   -- Since `f` is linear, we only need to show that it is continuous at zero.
   -- Let `U` be a neighborhood of `0` in `M₂`.
-  refine' continuous_of_continuous_at_zero f fun U hU => _
+  refine' continuous_of_continuousAt_zero f fun U hU => _
   rw [map_zero] at hU
   -- The compactness of `f` gives us a compact set `K : set M₂` such that `f ⁻¹' K` is a
   -- neighborhood of `0` in `M₁`.