apply_eq_of_compactSpace — Mathlib

English

If a holomorphic function is defined on a compact connected complex manifold, it must be constant on the whole manifold.

Русский

Если голоморфная функция определена на компактном связном комплексном многообразии, она должна быть константной на всём многообразии.

LaTeX

$$$\forall a,b \in M,\ f(a)=f(b)$$$

Lean4

/-- A holomorphic function on a compact connected complex manifold is constant. -/
theorem apply_eq_of_compactSpace [PreconnectedSpace M] {f : M → F} (hf : MDifferentiable I 𝓘(ℂ, F) f) (a b : M) :
    f a = f b :=
  hf.isLocallyConstant.apply_eq_of_preconnectedSpace _ _

Похожие утверждения