From 5d5d7557c0a3dd29615ac8dffc2b71ad3b454899 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 10 Jun 2024 16:00:49 +0200 Subject: [PATCH] Update laplace.lean --- Nevanlinna/laplace.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index 42f6025..35c1128 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -18,7 +18,6 @@ theorem laplace_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nh rw [partialDeriv_eventuallyEq ℝ (partialDeriv_eventuallyEq' ℝ h Complex.I) Complex.I] - theorem laplace_eventuallyEq' {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : Δ f₁ =ᶠ[nhds x] Δ f₂ := by unfold Complex.laplace apply Filter.EventuallyEq.add