English
If f is holomorphic on a compact complex manifold, then around every point there exists a neighborhood on which f is constant.
Русский
Если f голоморфна на компактном комплексном многообразии, то вокруг каждой точки существует окрестность, на которой f константна.
LaTeX
$$$\text{IsLocallyConstant}(f)$$$
Lean4
/-- A holomorphic function on a compact complex manifold is locally constant. -/
protected theorem isLocallyConstant {f : M → F} (hf : MDifferentiable I 𝓘(ℂ, F) f) : IsLocallyConstant f :=
haveI : LocallyConnectedSpace H := I.toHomeomorph.locallyConnectedSpace
haveI : LocallyConnectedSpace M := ChartedSpace.locallyConnectedSpace H M
IsLocallyConstant.of_constant_on_preconnected_clopens fun _ hpc hclo _a ha _b hb ↦
hf.mdifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen hpc hclo.isClosed.isCompact hclo.isOpen hb ha
