exists_eq_const_of_compactSpace — Mathlib

English

There exists a constant value v such that f is identically equal to v on the manifold.

Русский

Существует константное значение v, такое что f тождественно равно v на многообразии.

LaTeX

$$$\exists v \in F,\ f = \text{const}_{M}(v)$$$

Lean4

/-- A holomorphic function on a compact connected complex manifold is the constant function `f ≡ v`,
for some value `v`. -/
theorem exists_eq_const_of_compactSpace [PreconnectedSpace M] {f : M → F} (hf : MDifferentiable I 𝓘(ℂ, F) f) :
    ∃ v : F, f = Function.const M v :=
  hf.isLocallyConstant.exists_eq_const

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