Source indexedlemma · leanprover/lean4:v4.32.0

verticalPath_not_eventuallyConst

PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:882 to 890

Mathematical statement

Exact Lean statement

lemma verticalPath_not_eventuallyConst (r : ℝ) (x : ℝ) :
    ¬Filter.EventuallyConst (fun y : ℝ ↦ (r : ℂ) + (y : ℂ) * Complex.I) (nhds x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma verticalPath_not_eventuallyConst (r : ℝ) (x : ℝ) :    ¬Filter.EventuallyConst (fun y : ℝ ↦ (r : ℂ) + (y : ℂ) * Complex.I) (nhds x) := by  intro hc  obtain ⟨c, hc⟩ := Filter.eventuallyConst_iff_exists_eventuallyEq.1 hc  have hpath : HasDerivAt (fun y : ℝ ↦ (r : ℂ) + (y : ℂ) * Complex.I) Complex.I x := by    simpa using ((Complex.ofRealCLM.hasDerivAt (x := x)).mul_const Complex.I).const_add (r : ℂ)  have hconst : HasDerivAt (fun y : ℝ ↦ (r : ℂ) + (y : ℂ) * Complex.I) 0 x :=    (hasDerivAt_const x c).congr_of_eventuallyEq hc  exact Complex.I_ne_zero (hpath.unique hconst)