liouville_const_of_tendsto_cocompact
ProvedLiouville (limit-at-infinity form). An entire function that tends to a finite limit along the cocompact filter is constant equal to .
Preamble
import Mathlib.Analysis.Complex.Liouville open Filter Topology
Formal statement
theorem liouville_const_of_tendsto_cocompact {g : ℂ → ℂ} (hg : Differentiable ℂ g) {c : ℂ} (hgc : Tendsto g (cocompact ℂ) (𝓝 c)) (z : ℂ) : g z = c := by sorrySource