remove sorry in add

RemyDegenne · Oct 29, 2024 · 604222b · 604222b
1 parent 3236c88
commit 604222b
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/TestingLowerBounds/FDiv/ERealStieltjes.lean b/TestingLowerBounds/FDiv/ERealStieltjes.lean
@@ -305,7 +305,9 @@ protected def add (f g : ERealStieltjes) : ERealStieltjes where
     have h_tendsto : ContinuousAt (fun (p : EReal × EReal) ↦ p.1 + p.2) (-f x, -g x) :=
       EReal.continuousAt_add (Or.inr hg_bot) (Or.inl hf_bot)
     rw [ContinuousAt] at h_tendsto
-    sorry
+    change Tendsto ((fun p : EReal × EReal ↦ p.1 + p.2) ∘ (fun x ↦ (-f x, -g x)))
+      (𝓝[≥] x) (𝓝 (-f x + -g x))
+    exact h_tendsto.comp <| Tendsto.prod_mk_nhds hf hg
 
 instance : Add ERealStieltjes where
   add := ERealStieltjes.add